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

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

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

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

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

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

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

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

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

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