Theorem: Tutorial.mul_left_cancel (Solution/Advanced/Algebra/Lecture1.lean)

State before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
⊢ a * x = a * y → x = y
Tactic:
intro h
State after:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ x = y

State before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ x = y
Tactic:
calc
  x = 1 * x := by simp
  _ = (a⁻¹ * a) * x := by simp
  _ = a⁻¹ * (a * x) := by rw [mul_assoc]
  _ = a⁻¹ * (a * y) := by rw [h]
  _ = (a⁻¹ * a) * y := by rw [← mul_assoc]
  _ = 1 * y := by simp
  _ = y := by simp
State after:
no goals

State before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ x = 1 * x
Tactic:
simp
State after:
no goals

State before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ 1 * x = a⁻¹ * a * x
Tactic:
simp
State after:
no goals

State before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ a⁻¹ * a * x = a⁻¹ * (a * x)
Tactic:
rw [mul_assoc]
State after:
no goals

State before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ a⁻¹ * (a * x) = a⁻¹ * (a * y)
Tactic:
rw [h]
State after:
no goals

State before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ a⁻¹ * (a * y) = a⁻¹ * a * y
Tactic:
rw [← mul_assoc]
State after:
no goals

State before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ a⁻¹ * a * y = 1 * y
Tactic:
simp
State after:
no goals

State before:
A : Type ?u.4453
G : Type
inst✝¹ : Ring A
inst✝ : Group G
a x y : G
h : a * x = a * y
⊢ 1 * y = y
Tactic:
simp
State after:
no goals