Theorem: commutative_of_squares_id (Lectures/GroupSquaresId.lean)

State before:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x * x = 1) → ∀ (x y : G), x * y = y * x
Tactic:
intro h
State after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
⊢ ∀ (x y : G), x * y = y * x

State before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
⊢ ∀ (x y : G), x * y = y * x
Tactic:
intro x y
State after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
⊢ x * y = y * x

State before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
⊢ x * y = y * x
Tactic:
have rel_xy := self_inv_of_squares_id h (y * x)
State after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : (y * x)⁻¹ = y * x
⊢ x * y = y * x

State before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : (y * x)⁻¹ = y * x
⊢ x * y = y * x
Tactic:
simp only [mul_inv_rev] at rel_xy
State after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : x⁻¹ * y⁻¹ = y * x
⊢ x * y = y * x

State before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : x⁻¹ * y⁻¹ = y * x
⊢ x * y = y * x
Tactic:
simp only [self_inv_of_squares_id h] at rel_xy
State after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : x * y = y * x
⊢ x * y = y * x

State before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x y : G
rel_xy : x * y = y * x
⊢ x * y = y * x
Tactic:
assumption
State after:
no goals