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

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

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

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

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

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

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

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

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

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

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

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