-- Mathlib/Order/Interval/Finset/Nat.lean
@[elab_as_elim]
lemma Nat.strong_decreasing_induction (base : ∃ n, ∀ m > n, P m) (step : ∀ n, (∀ m > n, P m) → P n)
    (n : ℕ) : P n

Proof state:
case intro.intro
P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b : ℕ
hb : b ∈ upperBounds {x | (fun n => ∀ m ≥ n, P m) x}
n : ℕ
hn : ∀ m > n, P m
m : ℕ
hm : m ≥ n + b + 1
⊢ m > n

case intro.intro
P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b n : ℕ
hn : ∀ m > n, P m
hb : n + b + 1 ≤ b
⊢ False

Tactic:
all_goals omega

Result:
no goals

Proof state:
case inr
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm✝ : m ≥ n
hm : n < m
⊢ P m

Tactic:
exact ih m hm

Result:
no goals

Proof state:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ¬BddAbove {x | (fun n => ∀ m ≥ n, P m) x}

Tactic:
rintro ⟨b, hb⟩

Result:
case intro
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n b : ℕ
hb : b ∈ upperBounds {x | (fun n => ∀ m ≥ n, P m) x}
⊢ False

Proof state:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm : m ≥ n
⊢ P m

Tactic:
rcases hm.eq_or_lt with rfl | hm

Result:
case inl
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
hm : n ≥ n
⊢ P n

case inr
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm✝ : m ≥ n
hm : n < m
⊢ P m

Proof state:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ P n

Tactic:
apply Nat.decreasing_induction_of_not_bddAbove (P := fun n ↦ ∀ m ≥ n, P m) _ _ n n le_rfl

Result:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ∀ (n : ℕ), (fun n => ∀ m ≥ n, P m) (n + 1) → (fun n => ∀ m ≥ n, P m) n

P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ¬BddAbove {x | (fun n => ∀ m ≥ n, P m) x}

Proof state:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ∀ (n : ℕ), (fun n => ∀ m ≥ n, P m) (n + 1) → (fun n => ∀ m ≥ n, P m) n

Tactic:
intro n ih m hm

Result:
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
m : ℕ
hm : m ≥ n
⊢ P m

Proof state:
case inl
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ n : ℕ
ih : ∀ m ≥ n + 1, P m
hm : n ≥ n
⊢ P n

Tactic:
exact step n ih

Result:
no goals

Proof state:
case intro.intro
P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b : ℕ
hb : b ∈ upperBounds {x | (fun n => ∀ m ≥ n, P m) x}
n : ℕ
hn : ∀ m > n, P m
⊢ False

Tactic:
specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)

Result:
case intro.intro
P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b : ℕ
hb : b ∈ upperBounds {x | (fun n => ∀ m ≥ n, P m) x}
n : ℕ
hn : ∀ m > n, P m
m : ℕ
hm : m ≥ n + b + 1
⊢ m > n

case intro.intro
P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b n : ℕ
hn : ∀ m > n, P m
hb : n + b + 1 ≤ b
⊢ False

Proof state:
case intro.intro
P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b n : ℕ
hn : ∀ m > n, P m
hb : n + b + 1 ≤ b
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case intro
P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n b : ℕ
hb : b ∈ upperBounds {x | (fun n => ∀ m ≥ n, P m) x}
⊢ False

Tactic:
rcases base with ⟨n, hn⟩

Result:
case intro.intro
P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b : ℕ
hb : b ∈ upperBounds {x | (fun n => ∀ m ≥ n, P m) x}
n : ℕ
hn : ∀ m > n, P m
⊢ False