Theorem: MonoidHom.range_isCommutative (Jordan/Mathlib/GroupTheory/Subgroup/Basic.lean)

State before:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
⊢ Subgroup.IsCommutative (range f)
Tactic:
apply Subgroup.IsCommutative.mk
State after:
case is_comm
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
⊢ Std.Commutative fun x x_1 => x * x_1

State before:
case is_comm
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
constructor
State after:
case is_comm.comm
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
⊢ ∀ (a b : ↥(range f)), a * b = b * a

State before:
case is_comm.comm
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
⊢ ∀ (a b : ↥(range f)), a * b = b * a
Tactic:
rintro ⟨_, a, rfl⟩ ⟨_, b, rfl⟩
State after:
case is_comm.comm.mk.intro.mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
a b : G
⊢ { val := f a, property := ⋯ } * { val := f b, property := ⋯ } =
    { val := f b, property := ⋯ } * { val := f a, property := ⋯ }

State before:
case is_comm.comm.mk.intro.mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
a b : G
⊢ { val := f a, property := ⋯ } * { val := f b, property := ⋯ } =
    { val := f b, property := ⋯ } * { val := f a, property := ⋯ }
Tactic:
rw [← Subtype.coe_inj]
State after:
case is_comm.comm.mk.intro.mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
a b : G
⊢ ↑({ val := f a, property := ⋯ } * { val := f b, property := ⋯ }) =
    ↑({ val := f b, property := ⋯ } * { val := f a, property := ⋯ })

State before:
case is_comm.comm.mk.intro.mk.intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hG : Std.Commutative fun x x_1 => x * x_1
a b : G
⊢ ↑({ val := f a, property := ⋯ } * { val := f b, property := ⋯ }) =
    ↑({ val := f b, property := ⋯ } * { val := f a, property := ⋯ })
Tactic:
simp only [Submonoid.coe_mul, ← map_mul, hG.comm]
State after:
no goals