Theorem: Ex112.mul_left_inv (AlgebraI/Groups.lean)

State before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a = 1
Tactic:
calc
  a⁻¹ * a = a⁻¹ * a⁻¹⁻¹ := ?_
  _ = 1 := h2 a⁻¹
State after:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a = a⁻¹ * a⁻¹⁻¹

State before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a = a⁻¹ * a⁻¹⁻¹
Tactic:
apply congr_arg
State after:
case h
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a = a⁻¹⁻¹

State before:
case h
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a = a⁻¹⁻¹
Tactic:
calc
  a = a * 1 := (h1 a).symm
  _ = a * (a⁻¹ * a⁻¹⁻¹) := by rw [h2]
  _ = a * a⁻¹ * a⁻¹⁻¹ := (Std.Associative.assoc a a⁻¹ a⁻¹⁻¹).symm
  _ = 1 * a⁻¹⁻¹ := by rw [h2]
  _ = a⁻¹⁻¹ := one_mul h1 h2 a⁻¹⁻¹
State after:
no goals

State before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * 1 = a * (a⁻¹ * a⁻¹⁻¹)
Tactic:
rw [h2]
State after:
no goals

State before:
G : Type u_1
inst✝³ : One G
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : Std.Associative fun x x_1 => x * x_1
h1 : ∀ (a : G), a * 1 = a
h2 : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a * a⁻¹ * a⁻¹⁻¹ = 1 * a⁻¹⁻¹
Tactic:
rw [h2]
State after:
no goals