Theorem: Pos.lt.dest (Extra/Pos/Lemmas.lean)

State before:
x y : Pos
⊢ x < y → ∃ z, x + z = y
Tactic:
intro h
State after:
x y : Pos
h : x < y
⊢ ∃ z, x + z = y

State before:
x y : Pos
h : x < y
⊢ ∃ z, x + z = y
Tactic:
induction x, y with
| one_one =>
  absurd h
  exact Pos.not_lt_one 1
| one_succ y =>
  exists y
  exact Pos.one_add_eq_add_one y
| succ_one x =>
  absurd h
  exact Pos.not_lt_one (x+1)
| succ_succ x y ih =>
  match ih (Pos.lt_of_succ_lt_succ h) with
  | ⟨z, hz⟩ =>
    exists z
    rw [Pos.succ_add, hz]
State after:
no goals

State before:
case one_one
h : 1 < 1
⊢ ∃ z, 1 + z = 1
Tactic:
absurd h
State after:
case one_one
h : 1 < 1
⊢ ¬1 < 1

State before:
case one_one
h : 1 < 1
⊢ ¬1 < 1
Tactic:
exact Pos.not_lt_one 1
State after:
no goals

State before:
case one_succ
y : Pos
a✝ : 1 < y → ∃ z, 1 + z = y
h : 1 < y + 1
⊢ ∃ z, 1 + z = y + 1
Tactic:
exists y
State after:
case one_succ
y : Pos
a✝ : 1 < y → ∃ z, 1 + z = y
h : 1 < y + 1
⊢ 1 + y = y + 1

State before:
case one_succ
y : Pos
a✝ : 1 < y → ∃ z, 1 + z = y
h : 1 < y + 1
⊢ 1 + y = y + 1
Tactic:
exact Pos.one_add_eq_add_one y
State after:
no goals

State before:
case succ_one
x : Pos
a✝ : x < 1 → ∃ z, x + z = 1
h : x + 1 < 1
⊢ ∃ z, x + 1 + z = 1
Tactic:
absurd h
State after:
case succ_one
x : Pos
a✝ : x < 1 → ∃ z, x + z = 1
h : x + 1 < 1
⊢ ¬x + 1 < 1

State before:
case succ_one
x : Pos
a✝ : x < 1 → ∃ z, x + z = 1
h : x + 1 < 1
⊢ ¬x + 1 < 1
Tactic:
exact Pos.not_lt_one (x+1)
State after:
no goals

State before:
case succ_succ
x y : Pos
ih : x < y → ∃ z, x + z = y
h : x + 1 < y + 1
⊢ ∃ z, x + 1 + z = y + 1
Tactic:
match ih (Pos.lt_of_succ_lt_succ h) with
| ⟨z, hz⟩ =>
  exists z
  rw [Pos.succ_add, hz]
State after:
no goals

State before:
x y : Pos
ih : x < y → ∃ z, x + z = y
h : x + 1 < y + 1
z : Pos
hz : x + z = y
⊢ ∃ z, x + 1 + z = y + 1
Tactic:
exists z
State after:
x y : Pos
ih : x < y → ∃ z, x + z = y
h : x + 1 < y + 1
z : Pos
hz : x + z = y
⊢ x + 1 + z = y + 1

State before:
x y : Pos
ih : x < y → ∃ z, x + z = y
h : x + 1 < y + 1
z : Pos
hz : x + z = y
⊢ x + 1 + z = y + 1
Tactic:
rw [Pos.succ_add, hz]
State after:
no goals