Theorem: surj_to_comm (Jordan/Mathlib/Commutators.lean)

State before:
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
⊢ a * b = b * a
Tactic:
obtain ⟨a', ha'⟩ := is_surj a
State after:
case intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
⊢ a * b = b * a

State before:
case intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
⊢ a * b = b * a
Tactic:
obtain ⟨b', hb'⟩ := is_surj b
State after:
case intro.intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
b' : G
hb' : φ b' = b
⊢ a * b = b * a

State before:
case intro.intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
b' : G
hb' : φ b' = b
⊢ a * b = b * a
Tactic:
simp only [← ha', ← hb', ← map_mul]
State after:
case intro.intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
b' : G
hb' : φ b' = b
⊢ φ (a' * b') = φ (b' * a')

State before:
case intro.intro
G✝ : Type ?u.3685
inst✝² : Group G✝
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
φ : G →ₙ* H
is_surj : Function.Surjective ⇑φ
is_comm : Std.Commutative fun x x_1 => x * x_1
a b : H
a' : G
ha' : φ a' = a
b' : G
hb' : φ b' = b
⊢ φ (a' * b') = φ (b' * a')
Tactic:
rw [is_comm.comm]
State after:
no goals