Theorem: Equiv.Perm.this1 (Jordan/PermIwasawa.lean)

State before:
α : Type ?u.19573
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : Type u_1
H : Type u_2
inst✝¹ : Group H
inst✝ : Group G
f : H →* G
g : G
⊢ MulAut.conj g • MonoidHom.range f = MonoidHom.range (MonoidHom.comp (MulEquiv.toMonoidHom (MulAut.conj g)) f)
Tactic:
simp only [← MonoidHom.map_range]
State after:
α : Type ?u.19573
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : Type u_1
H : Type u_2
inst✝¹ : Group H
inst✝ : Group G
f : H →* G
g : G
⊢ MulAut.conj g • MonoidHom.range f = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (MonoidHom.range f)

State before:
α : Type ?u.19573
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : Type u_1
H : Type u_2
inst✝¹ : Group H
inst✝ : Group G
f : H →* G
g : G
⊢ MulAut.conj g • MonoidHom.range f = Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (MonoidHom.range f)
Tactic:
rfl
State after:
no goals