[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ a * 1 = a
[PROOFSTEP]
have mul_right_inv : ∀ a, a * a⁻¹ = 1 := fun a =>
  calc
    a * a⁻¹ = 1 * (a * a⁻¹) := (one_mul _).symm
    _ = ((a * a⁻¹)⁻¹ * (a * a⁻¹)) * (a * a⁻¹) := by rw [mul_left_inv]
    _ = (a * a⁻¹)⁻¹ * (a * ((a⁻¹ * a) * a⁻¹)) := by simp only [assoc]
    _ = 1 := by rw [mul_left_inv, one_mul, mul_left_inv]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a✝ a : G
⊢ 1 * (a * a⁻¹) = (a * a⁻¹)⁻¹ * (a * a⁻¹) * (a * a⁻¹)
[PROOFSTEP]
rw [mul_left_inv]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a✝ a : G
⊢ (a * a⁻¹)⁻¹ * (a * a⁻¹) * (a * a⁻¹) = (a * a⁻¹)⁻¹ * (a * (a⁻¹ * a * a⁻¹))
[PROOFSTEP]
simp only [assoc]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a✝ a : G
⊢ (a * a⁻¹)⁻¹ * (a * (a⁻¹ * a * a⁻¹)) = 1
[PROOFSTEP]
rw [mul_left_inv, one_mul, mul_left_inv]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
one_mul : ∀ (a : G), 1 * a = a
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a : G
mul_right_inv : ∀ (a : G), a * a⁻¹ = 1
⊢ a * 1 = a
[PROOFSTEP]
rw [← mul_left_inv a, ← assoc, mul_right_inv a, one_mul]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_right_inv : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a * 1 = a⁻¹ * a * (a⁻¹ * a * (a⁻¹ * a)⁻¹)
[PROOFSTEP]
rw [mul_right_inv]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_right_inv : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a * (a⁻¹ * a * (a⁻¹ * a)⁻¹) = a⁻¹ * (a * a⁻¹) * a * (a⁻¹ * a)⁻¹
[PROOFSTEP]
simp only [assoc]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_right_inv : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * (a * a⁻¹) * a * (a⁻¹ * a)⁻¹ = 1
[PROOFSTEP]
rw [mul_right_inv, mul_one, mul_right_inv]
[GOAL]
G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_right_inv : ∀ (a : G), a * a⁻¹ = 1
mul_left_inv : ∀ (a : G), a⁻¹ * a = 1
a : G
⊢ 1 * a = a
[PROOFSTEP]
rw [← mul_right_inv a, assoc, mul_left_inv, mul_one]
