Theorem: Pos.mul_right_cancel (Extra/Pos/Lemmas.lean)

State before:
x y z : Pos
⊢ x * y = z * y → x = z
Tactic:
intro h
State after:
x y z : Pos
h : x * y = z * y
⊢ x = z

State before:
x y z : Pos
h : x * y = z * y
⊢ x = z
Tactic:
induction x, z with
| one_one => rfl
| one_succ x _ =>
  rw [Pos.one_mul, Pos.succ_mul] at h
  absurd h
  apply Pos.ne_add_self_left
| succ_one z _ =>
  rw [Pos.one_mul, Pos.succ_mul] at h
  absurd h.symm
  apply Pos.ne_add_self_left
| succ_succ x z H =>
  rw [Pos.succ_mul, Pos.succ_mul] at h
  rw [H (Pos.add_right_cancel h)]
State after:
no goals

State before:
case one_one
y : Pos
h : 1 * y = 1 * y
⊢ 1 = 1
Tactic:
rfl
State after:
no goals

State before:
case one_succ
y x : Pos
a✝ : 1 * y = x * y → 1 = x
h : 1 * y = (x + 1) * y
⊢ 1 = x + 1
Tactic:
rw [Pos.one_mul, Pos.succ_mul] at h
State after:
case one_succ
y x : Pos
a✝ : 1 * y = x * y → 1 = x
h : y = x * y + y
⊢ 1 = x + 1

State before:
case one_succ
y x : Pos
a✝ : 1 * y = x * y → 1 = x
h : y = x * y + y
⊢ 1 = x + 1
Tactic:
absurd h
State after:
case one_succ
y x : Pos
a✝ : 1 * y = x * y → 1 = x
h : y = x * y + y
⊢ ¬y = x * y + y

State before:
case one_succ
y x : Pos
a✝ : 1 * y = x * y → 1 = x
h : y = x * y + y
⊢ ¬y = x * y + y
Tactic:
apply Pos.ne_add_self_left
State after:
no goals

State before:
case succ_one
y z : Pos
a✝ : z * y = 1 * y → z = 1
h : (z + 1) * y = 1 * y
⊢ z + 1 = 1
Tactic:
rw [Pos.one_mul, Pos.succ_mul] at h
State after:
case succ_one
y z : Pos
a✝ : z * y = 1 * y → z = 1
h : z * y + y = y
⊢ z + 1 = 1

State before:
case succ_one
y z : Pos
a✝ : z * y = 1 * y → z = 1
h : z * y + y = y
⊢ z + 1 = 1
Tactic:
absurd h.symm
State after:
case succ_one
y z : Pos
a✝ : z * y = 1 * y → z = 1
h : z * y + y = y
⊢ ¬y = z * y + y

State before:
case succ_one
y z : Pos
a✝ : z * y = 1 * y → z = 1
h : z * y + y = y
⊢ ¬y = z * y + y
Tactic:
apply Pos.ne_add_self_left
State after:
no goals

State before:
case succ_succ
y x z : Pos
H : x * y = z * y → x = z
h : (x + 1) * y = (z + 1) * y
⊢ x + 1 = z + 1
Tactic:
rw [Pos.succ_mul, Pos.succ_mul] at h
State after:
case succ_succ
y x z : Pos
H : x * y = z * y → x = z
h : x * y + y = z * y + y
⊢ x + 1 = z + 1

State before:
case succ_succ
y x z : Pos
H : x * y = z * y → x = z
h : x * y + y = z * y + y
⊢ x + 1 = z + 1
Tactic:
rw [H (Pos.add_right_cancel h)]
State after:
no goals