-- Mathlib/.lake/packages/lean4/src/lean/Init/Internal/Order/Basic.lean
theorem find_spec : ∀ n m, find P n = some m → n ≤ m ∧ P m

Proof state:
case isTrue
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
h✝ : P n = true
heq : some n = some m
⊢ n ≤ m ∧ P m = true

Tactic:
simp_all

Result:
no goals

Proof state:
case isFalse
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
h✝ : ¬P n = true
heq : f (n + 1) = some m
⊢ n ≤ m ∧ P m = true

Tactic:
obtain ⟨ih1, ih2⟩ := ih _ _ heq

Result:
case isFalse.intro
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
h✝ : ¬P n = true
heq : f (n + 1) = some m
ih1 : n + 1 ≤ m
ih2 : P m = true
⊢ n ≤ m ∧ P m = true

Proof state:
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
heq : findF P f n = some m
⊢ n ≤ m ∧ P m = true

Tactic:
simp only [findF] at heq

Result:
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
heq : (if P n = true then some n else f (n + 1)) = some m
⊢ n ≤ m ∧ P m = true

Proof state:
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
heq : (if P n = true then some n else f (n + 1)) = some m
⊢ n ≤ m ∧ P m = true

Tactic:
split at heq

Result:
case isTrue
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
h✝ : P n = true
heq : some n = some m
⊢ n ≤ m ∧ P m = true

case isFalse
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
h✝ : ¬P n = true
heq : f (n + 1) = some m
⊢ n ≤ m ∧ P m = true

Proof state:
P : Nat → Bool
⊢ ∀ (n m : Nat), find P n = some m → n ≤ m ∧ P m = true

Tactic:
unfold find

Result:
P : Nat → Bool
⊢ ∀ (n m : Nat), fix (findF P) ⋯ n = some m → n ≤ m ∧ P m = true

Proof state:
case isFalse.intro
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
h✝ : ¬P n = true
heq : f (n + 1) = some m
ih1 : n + 1 ≤ m
ih2 : P m = true
⊢ n ≤ m ∧ P m = true

Tactic:
constructor

Result:
case isFalse.intro.left
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
h✝ : ¬P n = true
heq : f (n + 1) = some m
ih1 : n + 1 ≤ m
ih2 : P m = true
⊢ n ≤ m

case isFalse.intro.right
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
h✝ : ¬P n = true
heq : f (n + 1) = some m
ih1 : n + 1 ≤ m
ih2 : P m = true
⊢ P m = true

Proof state:
case hadm
P : Nat → Bool
⊢ admissible fun f => ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true

case hstep
P : Nat → Bool
⊢ ∀ (x : Nat → Option Nat),
    (fun f => ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true) x →
      (fun f => ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true) (findF P x)

Tactic:
case hadm =>
  exact admissible_pi_apply _ (fun n => admissible_pi _ (fun m => Option.admissible_eq_some _ m))

Result:
case hstep
P : Nat → Bool
⊢ ∀ (x : Nat → Option Nat),
    (fun f => ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true) x →
      (fun f => ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true) (findF P x)

Proof state:
P : Nat → Bool
⊢ admissible fun f => ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true

Tactic:
exact admissible_pi_apply _ (fun n => admissible_pi _ (fun m => Option.admissible_eq_some _ m))

Result:
no goals

Proof state:
case isFalse.intro.right
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
h✝ : ¬P n = true
heq : f (n + 1) = some m
ih1 : n + 1 ≤ m
ih2 : P m = true
⊢ P m = true

Tactic:
exact ih2

Result:
no goals

Proof state:
P : Nat → Bool
⊢ ∀ (x : Nat → Option Nat),
    (fun f => ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true) x →
      (fun f => ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true) (findF P x)

Tactic:
intro f ih n m heq

Result:
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
heq : findF P f n = some m
⊢ n ≤ m ∧ P m = true

Proof state:
P : Nat → Bool
⊢ ∀ (n m : Nat), fix (findF P) ⋯ n = some m → n ≤ m ∧ P m = true

Tactic:
refine fix_induct (motive := fun (f : Nat → Option Nat) => ∀ n m, f n = some m → n ≤ m ∧ P m) _ ?hadm ?hstep

Result:
case hadm
P : Nat → Bool
⊢ admissible fun f => ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true

case hstep
P : Nat → Bool
⊢ ∀ (x : Nat → Option Nat),
    (fun f => ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true) x →
      (fun f => ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true) (findF P x)

Proof state:
case isFalse.intro.left
P : Nat → Bool
f : Nat → Option Nat
ih : ∀ (n m : Nat), f n = some m → n ≤ m ∧ P m = true
n m : Nat
h✝ : ¬P n = true
heq : f (n + 1) = some m
ih1 : n + 1 ≤ m
ih2 : P m = true
⊢ n ≤ m

Tactic:
exact Nat.le_trans (Nat.le_add_right _ _ ) ih1

Result:
no goals