Theorem: alternatingGroup.isCommutative_of_exponent_two (Jordan/V4.lean)

State before:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
suffices ∀ g : G, g⁻¹ = g by
  constructor
  intro a b
  rw [← mul_inv_eq_iff_eq_mul, ← mul_inv_eq_one, this, this, ← hG2 (a * b), pow_two,
    mul_assoc (a * b) a b]
State after:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
⊢ ∀ (g : G), g⁻¹ = g

State before:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
⊢ ∀ (g : G), g⁻¹ = g
Tactic:
intro g
State after:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
g : G
⊢ g⁻¹ = g

State before:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
g : G
⊢ g⁻¹ = g
Tactic:
rw [← mul_eq_one_iff_inv_eq, ← hG2 g, pow_two]
State after:
no goals

State before:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
this : ∀ (g : G), g⁻¹ = g
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
constructor
State after:
case comm
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
this : ∀ (g : G), g⁻¹ = g
⊢ ∀ (a b : G), a * b = b * a

State before:
case comm
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
this : ∀ (g : G), g⁻¹ = g
⊢ ∀ (a b : G), a * b = b * a
Tactic:
intro a b
State after:
case comm
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
this : ∀ (g : G), g⁻¹ = g
a b : G
⊢ a * b = b * a

State before:
case comm
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
this : ∀ (g : G), g⁻¹ = g
a b : G
⊢ a * b = b * a
Tactic:
rw [← mul_inv_eq_iff_eq_mul, ← mul_inv_eq_one, this, this, ← hG2 (a * b), pow_two,
  mul_assoc (a * b) a b]
State after:
no goals