Theorem: map_inv_of_inv (LeanCourse/MIL/C07_Hierarchies/S02_Morphisms.lean)

State before:
M N F : Type
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass₂ F M N
f : F
m m' : M
h : m * m' = 1
⊢ ↑f m * ↑f m' = 1
Tactic:
rw [← MonoidHomClass₂.map_mul, h, MonoidHomClass₂.map_one]
State after:
no goals