Make `@[trans]`/`calc` work with `homeomorph` etc

[urkud]

Here is a minimal non-working example. See also homeomorph.trans in mathlib. It seems that calc makes very strict assumptions on the meaning of implicit arguments preceding the explicit arguments of the @[trans] lemma, and we can't satisfy these assumptions with homeomorph, local_homeomorph, monoid_hom etc, see Zulip chat.

structure inhabited_hom (α β : Type*) [inhabited α] [inhabited β] :=
(to_fun : α → β)
(map_default : to_fun (default α) = default β)

notation α `→'`:25 β := inhabited_hom α β

@[trans] def inhabited_hom.trans {α β γ : Type*} [inhabited α] [inhabited β] [inhabited γ]
  (f : α →' β) (g : β →' γ) :
  α →' γ :=
{ to_fun := λ x, g.to_fun (f.to_fun x),
  map_default := by rw [f.map_default, g.map_default] }

example {α β γ : Type*} [inhabited α] [inhabited β] [inhabited γ]
  (f : α →' β) (g : β →' γ) : α →' γ :=
calc α →' β : f
... →' γ : g

[urkud]

One more bug in calc:

import data.set.basic

example (α : Type*) (x : α) (s t t' : set α) (hx : x ∈ s) (h : s ⊆ t) (ht : t = t') : x ∈ t' :=
calc x ∈ s : hx
... ⊆ t : h
... = t' : ht

fails with

6:1: type mismatch at application
  trans_rel_left
term
  t
has type
  set α
but is expected to have type
  α