α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : MulOneClass R
inst✝² : Monoid S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ ↑f ⅟r = ⅟(↑f r)
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : MulOneClass R
inst✝² : Monoid S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
ifr : Invertible (↑f r)
h : ifr = Invertible.map f r
⊢ ↑f ⅟r = ⅟(↑f r)
subst h
no goals
α : Type u
R : Type u_1
S : Type u_2
F : Type u_3
inst✝³ : MulOneClass R
inst✝² : Monoid S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ ↑f ⅟r = ⅟(↑f r)
rfl