Theorem: Ex112.one_mul (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
this✝ : a * (a⁻¹ * a) * a⁻¹ = a * (a * a⁻¹) * a⁻¹
this : a * (a⁻¹ * a) = a * (a * a⁻¹)
⊢ 1 * a = a
Tactic:
rw [h2, h1] at this
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
this✝ : a * (a⁻¹ * a) * a⁻¹ = a * (a * a⁻¹) * a⁻¹
this : a * (a⁻¹ * a) = a
⊢ 1 * 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⁻¹ = a * (a * a⁻¹) * a⁻¹
Tactic:
calc
  a * (a⁻¹ * a) * a⁻¹ = a * a⁻¹ * (a * a⁻¹) := ?_
  _ = a * a⁻¹ * 1 := ?_
  _ = a * 1 * a⁻¹ := ?_
  _ = a * (a * a⁻¹) * a⁻¹ := ?_
State after:
case calc_1
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⁻¹ = a * a⁻¹ * (a * a⁻¹)

case calc_2
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⁻¹) = a * a⁻¹ * 1

case calc_3
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 = a * 1 * a⁻¹

case calc_4
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 * a⁻¹) * a⁻¹

State before:
case calc_2
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⁻¹) = a * a⁻¹ * 1
Tactic:
rw [h2]
State after:
no goals

State before:
case calc_3
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 = a * 1 * a⁻¹
Tactic:
rw [h1, h1]
State after:
no goals

State before:
case calc_4
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 * 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
this✝ : a * (a⁻¹ * a) * a⁻¹ = a * (a * a⁻¹) * a⁻¹
this : (fun x => x * a⁻¹⁻¹) (a * (a⁻¹ * a) * a⁻¹) = (fun x => x * a⁻¹⁻¹) (a * (a * a⁻¹) * a⁻¹)
⊢ a * (a⁻¹ * a) = a * (a * a⁻¹)
Tactic:
simp only at this
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
this✝ : a * (a⁻¹ * a) * a⁻¹ = a * (a * a⁻¹) * a⁻¹
this : a * (a⁻¹ * a) * a⁻¹ * a⁻¹⁻¹ = a * (a * a⁻¹) * a⁻¹ * a⁻¹⁻¹
⊢ a * (a⁻¹ * 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
this✝ : a * (a⁻¹ * a) * a⁻¹ = a * (a * a⁻¹) * a⁻¹
this : a * (a⁻¹ * a) = a * (a * a⁻¹)
⊢ a * (a⁻¹ * a) = a * (a * a⁻¹)
Tactic:
exact this
State after:
no goals