Apply a coercion to both sides of an equation

Stream: new members

[Michael Rothgang]

(I'm not new to Lean any more, but this feels like a basic question - which need not mean easy.)

My question comes up in #8738. In essence, I have

• a structure with a coercion to functions (in my case, ContinuousLinearMap),
• this type has an identity and a composition (which match the identity and composition on the level of functions),
• I want to prove "f.comp g = id" implies "g ∘ f = id".

On a high level, this proof is just "coerce both sides, and then let simp prove this". What's the idiomatic way to do this in Lean? MWE:

import Mathlib
variable {R E F : Type*} [Semiring R]
  [TopologicalSpace E] [AddCommMonoid E] [Module R E]
  [TopologicalSpace F] [AddCommMonoid F] [Module R F]

lemma RightInverse.of_composition {f : E →L[R] F} {g : F →L[R] E}
    (hinv : f.comp g = ContinuousLinearMap.id R F) : Function.RightInverse g f :=
  sorry

[Aaron Liu]

I discovered simpa [Function.rightInverse_iff_comp] using congr(⇑$hinv) should do it

[Aaron Liu]

It's shorter than apply_fun

[Michael Rothgang]

And I found a fun bug in core (?):

/-- error: internal exception: postpone -/
#guard_msgs in
lemma _root_.LeftInverse.of_composition {f : E →L[R] F} {g : F →L[R] E}
    (hinv : g.comp f = ContinuousLinearMap.id R E) : Function.LeftInverse g f := by
  apply_fun (⇑) at hinv
  sorry

[Weiyi Wang]

My guess is it tries to infer the type of ⇑ and got trapped somewhere :thinking: