problems with coercion to function

Stream: general

[Johan Commelin]

Can someone explain to me how I should convince Lean that f and g can be coerced to a function in the assumption h on this line: https://github.com/leanprover-community/mathlib/pull/1064/files#diff-694e7969af05a14241540bb2e6204a01R1132

@[extensionality] lemma ext {f g : β ≃ₗ[α] γ} (h : f.to_fun = g.to_fun) : f = g :=
to_equiv_injective (equiv.eq_of_to_fun_eq h)

[Johan Commelin]

I can't write (h : (f : β → γ) = g). I also can't write (h : ∀ x:β, f x = g x).

[Chris Hughes]

Put it later in the file, so it's after the has_coe instance.

[Johan Commelin]

Oooh, that was silly.