Theorem: Poland1998P4.strengthen (Compfiles/Poland1998P4.lean)

State before:
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
he : ∃ N, P N
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ P M
Tactic:
obtain ⟨N0, hn0⟩ := he
State after:
case intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ P M

State before:
case intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
⊢ ∀ (N : ℕ), ∃ M, N < M ∧ P M
Tactic:
intro N
State after:
case intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
N : ℕ
⊢ ∃ M, N < M ∧ P M

State before:
case intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
N : ℕ
⊢ ∃ M, N < M ∧ P M
Tactic:
induction' N with pn hpn
State after:
case intro.zero
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
⊢ ∃ M, 0 < M ∧ P M

case intro.succ
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn : ℕ
hpn : ∃ M, pn < M ∧ P M
⊢ ∃ M, pn + 1 < M ∧ P M

State before:
case intro.zero
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
⊢ ∃ M, 0 < M ∧ P M
Tactic:
obtain (hlt : 0 < N0) | (hlte : N0 ≤ 0) := lt_or_ge 0 N0
State after:
case intro.zero.inl
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlt : 0 < N0
⊢ ∃ M, 0 < M ∧ P M

case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlte : N0 ≤ 0
⊢ ∃ M, 0 < M ∧ P M

State before:
case intro.zero.inl
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlt : 0 < N0
⊢ ∃ M, 0 < M ∧ P M
Tactic:
exact ⟨N0, hlt, hn0⟩
State after:
no goals

State before:
case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlte : N0 ≤ 0
⊢ ∃ M, 0 < M ∧ P M
Tactic:
have heq : N0 = 0 := eq_bot_iff.mpr hlte
State after:
case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlte : N0 ≤ 0
heq : N0 = 0
⊢ ∃ M, 0 < M ∧ P M

State before:
case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
hlte : N0 ≤ 0
heq : N0 = 0
⊢ ∃ M, 0 < M ∧ P M
Tactic:
rw [heq] at hn0
State after:
case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P 0
hlte : N0 ≤ 0
heq : N0 = 0
⊢ ∃ M, 0 < M ∧ P M

State before:
case intro.zero.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P 0
hlte : N0 ≤ 0
heq : N0 = 0
⊢ ∃ M, 0 < M ∧ P M
Tactic:
exact h 0 hn0
State after:
no goals

State before:
case intro.succ
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn : ℕ
hpn : ∃ M, pn < M ∧ P M
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
obtain ⟨m, hm, hmp⟩ := hpn
State after:
case intro.succ.intro.intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
⊢ ∃ M, pn + 1 < M ∧ P M

State before:
case intro.succ.intro.intro
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
obtain (hlt : pn + 1 < m) |  (hlte : m ≤ pn + 1) := lt_or_ge (pn + 1) m
State after:
case intro.succ.intro.intro.inl
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlt : pn + 1 < m
⊢ ∃ M, pn + 1 < M ∧ P M

case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlte : m ≤ pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M

State before:
case intro.succ.intro.intro.inl
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlt : pn + 1 < m
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
exact ⟨m, hlt, hmp⟩
State after:
no goals

State before:
case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlte : m ≤ pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
have heq : m = pn + 1 := le_antisymm hlte hm
State after:
case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlte : m ≤ pn + 1
heq : m = pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M

State before:
case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P m
hlte : m ≤ pn + 1
heq : m = pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
rw [heq] at hmp
State after:
case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P (pn + 1)
hlte : m ≤ pn + 1
heq : m = pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M

State before:
case intro.succ.intro.intro.inr
P : ℕ → Prop
h : ∀ (N : ℕ), P N → ∃ M, N < M ∧ P M
N0 : ℕ
hn0 : P N0
pn m : ℕ
hm : pn < m
hmp : P (pn + 1)
hlte : m ≤ pn + 1
heq : m = pn + 1
⊢ ∃ M, pn + 1 < M ∧ P M
Tactic:
exact h (pn.succ) hmp
State after:
no goals