AlgEquiv_invFun_apply

Stream: Is there code for X?

[Bolton Bailey]

Do we have this lemma?

lemma AlgEquiv_invFun_apply {R α β : Type} [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β]
    (e : α ≃ₐ[R] β) (x : α) : x = (e).toEquiv.invFun ((e) x) := by
  rw [AlgEquiv.toEquiv_eq_coe, Equiv.invFun_as_coe, @Equiv.eq_symm_apply]
  exact rfl

[Bolton Bailey]

(and more importantly, can rw_search prove it?)

[Eric Rodriguez]

this should be defeq to e.symm $ e x = x no?

[Eric Wieser]

invFun should never appear in any lemma statement other than the one that eliminates it