awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m_1 : ℕ
hmk : m.le m_1
ih :
  leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) hmk
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) ⋯
have step : le_succ_of_le sorry (leRec (motive := motive) refl le_succ_of_le sorry) =
  leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x sorry)
    (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x sorry) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
    (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le sorry) sorry
Tactic: rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m_1 : ℕ
hmk : m.le m_1
ih :
  leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) hmk
step :
  le_succ_of_le ⋯ (leRec (motive := motive) refl le_succ_of_le ⋯) =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) ⋯
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) ⋯
have step₁ : le_succ_of_le sorry
    (leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x sorry)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x sorry) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le sorry) hmk) =
  leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x sorry)
    (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x sorry) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
    (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le sorry) sorry
Tactic: rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m_1 : ℕ
hmk : m.le m_1
ih :
  leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) hmk
step :
  le_succ_of_le ⋯ (leRec (motive := motive) refl le_succ_of_le ⋯) =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) ⋯
step₁ :
  le_succ_of_le ⋯
      (leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
        (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
        (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) hmk) =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) ⋯
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) ⋯
have step₂ : le_succ_of_le sorry
    (leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x sorry)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x sorry) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le sorry) hmk) =
  le_succ_of_le sorry
    (leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x sorry)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x sorry) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le sorry) hmk)
Tactic: rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
m_1 : ℕ
hmk : m.le m_1
ih :
  leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) hmk
step :
  le_succ_of_le ⋯ (leRec (motive := motive) refl le_succ_of_le ⋯) =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) ⋯
step₁ :
  le_succ_of_le ⋯
      (leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
        (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
        (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) hmk) =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) ⋯
step₂ :
  le_succ_of_le ⋯
      (leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
        (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
        (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) hmk) =
    le_succ_of_le ⋯
      (leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
        (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
        (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) hmk)
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) ⋯
have step₃ : m ≤ m_1
Tactic: rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
hmk : m ≤ k
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) hmk
have refl₁ : leRec (motive := motive) refl le_succ_of_le sorry =
  leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x sorry)
    (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x sorry) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
    (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le sorry) sorry
Tactic: induction hmk with
  | refl => rw [leRec_self]
  | step hmk ih => rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]
Cleared hypotheses: hmk
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n m k : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
hnm : n ≤ m
hmk : m ≤ k
refl₁ :
  leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) ⋯
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x ⋯)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le ⋯) hmk
have step : ∀ {m_1 : ℕ} (hmk : m.le m_1)
  (ih :
    leRec (motive := motive) refl le_succ_of_le sorry =
      leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x sorry)
        (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x sorry) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
        (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le sorry) hmk),
  leRec (motive := motive) refl le_succ_of_le sorry =
    leRec (motive := fun (x : ℕ) (x_1 : m ≤ x) ↦ motive x sorry)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x sorry) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm)
      (fun (x : ℕ) (h : m ≤ x) ↦ le_succ_of_le sorry) sorry
Tactic: induction hmk with
  | refl => rw [leRec_self]
  | step hmk ih => rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]
Cleared hypotheses: hmk
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
m : ℕ
h1 : n ≤ m
h2 : n + 1 ≤ m
⊢ leRec (motive := fun (x : ℕ) (h : n + 1 ≤ x) ↦ motive x ⋯) (le_succ_of_le ⋯ refl)
      (fun (x : ℕ) (h : n + 1 ≤ x) (ih : motive x ⋯) ↦ le_succ_of_le ⋯ ih) h2 =
    leRec (motive := motive) refl le_succ_of_le h1
have rw : Eq.{u_1} (α := motive m sorry)
  (leRec (motive := fun (x : ℕ) (h : n + 1 ≤ x) ↦ motive x sorry) (le_succ_of_le sorry refl)
      (fun (x : ℕ) (h : n + 1 ≤ x) (ih : motive x sorry) ↦ le_succ_of_le sorry ih) h2 :
    motive m sorry)
  (leRec (motive := fun (x : ℕ) (x_1 : n.succ ≤ x) ↦ motive x sorry)
      (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x sorry) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) sorry)
      (fun (x : ℕ) (h : n.succ ≤ x) ↦ le_succ_of_le sorry) h2 :
    motive m sorry)
Tactic: rw [leRec_trans _ _ (le_succ n) h2, leRec_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n : ℕ
motive : (m : ℕ) → n ≤ m → Sort u_1
refl : motive n ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯
m : ℕ
h1 : n ≤ m
h2 : n + 1 ≤ m
rw :
  Eq.{u_1} (α := motive m ⋯)
    (leRec (motive := fun (x : ℕ) (h : n + 1 ≤ x) ↦ motive x ⋯) (le_succ_of_le ⋯ refl)
        (fun (x : ℕ) (h : n + 1 ≤ x) (ih : motive x ⋯) ↦ le_succ_of_le ⋯ ih) h2 :
      motive m ⋯)
    (leRec (motive := fun (x : ℕ) (x_1 : n.succ ≤ x) ↦ motive x ⋯)
        (leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) ⋯)
        (fun (x : ℕ) (h : n.succ ≤ x) ↦ le_succ_of_le ⋯) h2 :
      motive m ⋯)
⊢ leRec (motive := fun (x : ℕ) (h : n + 1 ≤ x) ↦ motive x ⋯) (le_succ_of_le ⋯ refl)
      (fun (x : ℕ) (h : n + 1 ≤ x) (ih : motive x ⋯) ↦ le_succ_of_le ⋯ ih) h2 =
    leRec (motive := motive) refl le_succ_of_le h1
have rw₁ : Eq.{u_1} (α := motive m sorry)
  (leRec (motive := fun (x : ℕ) (h : n + 1 ≤ x) ↦ motive x sorry) (le_succ_of_le sorry refl)
      (fun (x : ℕ) (h : n + 1 ≤ x) (ih : motive x sorry) ↦ le_succ_of_le sorry ih) h2 :
    motive m sorry)
  (leRec (motive := fun (x : ℕ) (x_1 : n.succ ≤ x) ↦ motive x sorry) (le_succ_of_le sorry refl)
      (fun (x : ℕ) (h : n.succ ≤ x) ↦ le_succ_of_le sorry) h2 :
    motive m sorry)
Tactic: rw [leRec_trans _ _ (le_succ n) h2, leRec_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
p : ℕ → Sort u_1
H : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n
n_1 n : ℕ
ih :
  ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ) (lt : m_1 < m), strongRecAux (p := p) H m m_1 lt = H m_1 (strongRecAux (p := p) H m_1)
m : ℕ
hmn : m < n
⊢ strongRecAux (p := p) H n m hmn = H m (strongRecAux (p := p) H m)
have zero : ∀
  (ih :
    ∀ (m : ℕ),
      m < 0 → ∀ (m_1 : ℕ) (lt : m_1 < m), strongRecAux (p := p) H m m_1 lt = H m_1 (strongRecAux (p := p) H m_1))
  (hmn : m < 0), strongRecAux (p := p) H 0 m hmn = H m (strongRecAux (p := p) H m)
Tactic: obtain _ | n := n
Cleared hypotheses: n, ih, hmn
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
p : ℕ → Sort u_1
H : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n
n_1 n : ℕ
ih :
  ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ) (lt : m_1 < m), strongRecAux (p := p) H m m_1 lt = H m_1 (strongRecAux (p := p) H m_1)
m : ℕ
hmn : m < n
zero :
  ∀
    (ih :
      ∀ (m : ℕ),
        m < 0 → ∀ (m_1 : ℕ) (lt : m_1 < m), strongRecAux (p := p) H m m_1 lt = H m_1 (strongRecAux (p := p) H m_1))
    (hmn : m < 0), strongRecAux (p := p) H 0 m hmn = H m (strongRecAux (p := p) H m)
⊢ strongRecAux (p := p) H n m hmn = H m (strongRecAux (p := p) H m)
have succ : ∀ (n : ℕ)
  (ih :
    ∀ (m : ℕ),
      m < n + 1 → ∀ (m_1 : ℕ) (lt : m_1 < m), strongRecAux (p := p) H m m_1 lt = H m_1 (strongRecAux (p := p) H m_1))
  (hmn : m < n + 1), strongRecAux (p := p) H (n + 1) m hmn = H m (strongRecAux (p := p) H m)
Tactic: obtain _ | n := n
Cleared hypotheses: n, ih, hmn
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
p : ℕ → Sort u_1
H : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n
n_1 m n : ℕ
ih :
  ∀ (m : ℕ),
    m < n + 1 → ∀ (m_1 : ℕ) (lt : m_1 < m), strongRecAux (p := p) H m m_1 lt = H m_1 (strongRecAux (p := p) H m_1)
hmn : m < n + 1
⊢ strongRecAux (p := p) H (n + 1) m hmn = H m (strongRecAux (p := p) H m)
have succ : (fun (l : ℕ) (hlm : l < m) ↦ strongRecAux (p := p) H n l sorry) = strongRecAux (p := p) H m
Tactic: refine congrArg (H _) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
p : ℕ → Sort u_1
H : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n
n_1 m n : ℕ
ih :
  ∀ (m : ℕ),
    m < n + 1 → ∀ (m_1 : ℕ) (lt : m_1 < m), strongRecAux (p := p) H m m_1 lt = H m_1 (strongRecAux (p := p) H m_1)
hmn : m < n + 1
⊢ (fun (l : ℕ) (hlm : l < m) ↦ strongRecAux (p := p) H n l ⋯) = strongRecAux (p := p) H m
have succ : ∀ (l : ℕ) (hlm : l < m), strongRecAux (p := p) H n l sorry = strongRecAux (p := p) H m l hlm
Tactic: ext l hlm
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n : ℕ
p : ℕ → Sort u_1
H : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n
⊢ strongRecAux (p := fun (x : ℕ) ↦ p x) H n = fun (m : ℕ) (x : m < n) ↦ Nat.strongRec' (p := fun (x : ℕ) ↦ p x) H m
have h : ∀ (m : ℕ) (lt : m < n), strongRecAux (p := fun (x : ℕ) ↦ p x) H n m lt = Nat.strongRec' (p := fun (x : ℕ) ↦ p x) H m
Tactic: ext m lt
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
a b c d e m_1 n_1 k : ℕ
p : ℕ → Prop
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
m : ℕ
mn : m ≤ n
⊢ motive m mn
have refl : {motive : (m_2 : ℕ) → m_2 ≤ m → Sort u_1} →
  (of_succ : (k : ℕ) → (h : k < m) → motive (k + 1) h → motive k sorry) → (self : motive m sorry) → motive m sorry
Tactic: induction mn using leRec with
  | refl => exact self
  | @le_succ_of_le k _ ih =>
    apply ih (fun i hi => of_succ i (le_succ_of_le hi)) (of_succ k (lt_succ_self _) self)
Cleared hypotheses: motive, of_succ, self, mn
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
a b c d e m_1 n_1 k : ℕ
p : ℕ → Prop
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
m : ℕ
mn : m ≤ n
refl :
  {motive : (m_2 : ℕ) → m_2 ≤ m → Sort u_1} →
    (of_succ : (k : ℕ) → (h : k < m) → motive (k + 1) h → motive k ⋯) → (self : motive m ⋯) → motive m ⋯
⊢ motive m mn
have le_succ_of_le : ⦃k : ℕ⦄ →
  (h : m ≤ k) →
    (ih :
        {motive : (m : ℕ) → m ≤ k → Sort u_1} →
          (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 sorry) →
            (self : motive k sorry) → motive m h) →
      {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1} →
        (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 sorry) →
          (self : motive (k + 1) sorry) → motive m sorry
Tactic: induction mn using leRec with
  | refl => exact self
  | @le_succ_of_le k _ ih =>
    apply ih (fun i hi => of_succ i (le_succ_of_le hi)) (of_succ k (lt_succ_self _) self)
Cleared hypotheses: motive, of_succ, self, mn
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ decreasingInduction (motive := motive) of_succ self ⋯ = self
have dsimp : leRec (motive := fun {n_1 : ℕ} (mn : n ≤ n_1) ↦
    {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
      (of_succ : (k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k sorry) → (self : motive n_1 sorry) → motive n mn)
    (fun {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k sorry)
        (self : motive n sorry) ↦
      self)
    (fun ⦃k : ℕ⦄ (h : n ≤ k)
        (ih :
          {motive : (m : ℕ) → m ≤ k → Sort u_1} →
            (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 sorry) →
              (self : motive k sorry) → motive n h)
        {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
        (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 sorry) (self : motive (k + 1) sorry) ↦
      ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m sorry) (fun (i : ℕ) (hi : i < k) ↦ of_succ i sorry) (of_succ k sorry self))
    sorry (motive := motive) of_succ self =
  self
Tactic: dsimp only [decreasingInduction]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
⊢ leRec (motive := fun {n_1 : ℕ} (mn : n ≤ n_1) ↦
      {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
        (of_succ : (k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → (self : motive n_1 ⋯) → motive n mn)
      (fun {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯)
          (self : motive n ⋯) ↦
        self)
      (fun ⦃k : ℕ⦄ (h : n ≤ k)
          (ih :
            {motive : (m : ℕ) → m ≤ k → Sort u_1} →
              (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯) →
                (self : motive k ⋯) → motive n h)
          {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
          (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 ⋯) (self : motive (k + 1) ⋯) ↦
        ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m ⋯) (fun (i : ℕ) (hi : i < k) ↦ of_succ i ⋯) (of_succ k ⋯ self))
      ⋯ (motive := motive) of_succ self =
    self
have rw : self = self
Tactic: rw [leRec_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
mn : m ≤ n
msn : m ≤ n + 1
⊢ decreasingInduction (motive := motive) of_succ self msn =
    decreasingInduction (motive := fun (m : ℕ) (h : m ≤ n) ↦ motive m ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (of_succ n ⋯ self) mn
have dsimp : Eq.{u_1} (α := motive m msn)
  (leRec (motive := fun {n : ℕ} (mn : m ≤ n) ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k sorry) → (self : motive n sorry) → motive m mn)
      (fun {motive : (m_1 : ℕ) → m_1 ≤ m → Sort u_1} (of_succ : (k : ℕ) → (h : k < m) → motive (k + 1) h → motive k sorry)
          (self : motive m sorry) ↦
        self)
      (fun ⦃k : ℕ⦄ (h : m ≤ k)
          (ih :
            {motive : (m : ℕ) → m ≤ k → Sort u_1} →
              (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 sorry) →
                (self : motive k sorry) → motive m h)
          {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
          (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 sorry) (self : motive (k + 1) sorry) ↦
        ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m sorry) (fun (i : ℕ) (hi : i < k) ↦ of_succ i sorry) (of_succ k sorry self))
      msn (motive := motive) of_succ self :
    motive m msn)
  (leRec (motive := fun {n : ℕ} (mn : m ≤ n) ↦
      {motive : (m : ℕ) → m ≤ n → Sort u_1} →
        (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k sorry) → (self : motive n sorry) → motive m mn)
      (fun {motive : (m_1 : ℕ) → m_1 ≤ m → Sort u_1} (of_succ : (k : ℕ) → (h : k < m) → motive (k + 1) h → motive k sorry)
          (self : motive m sorry) ↦
        self)
      (fun ⦃k : ℕ⦄ (h : m ≤ k)
          (ih :
            {motive : (m : ℕ) → m ≤ k → Sort u_1} →
              (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 sorry) →
                (self : motive k sorry) → motive m h)
          {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
          (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 sorry) (self : motive (k + 1) sorry) ↦
        ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m sorry) (fun (i : ℕ) (hi : i < k) ↦ of_succ i sorry) (of_succ k sorry self))
      mn (motive := fun (m : ℕ) (h : m ≤ n) ↦ motive m sorry) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x sorry) (of_succ n sorry self) :
    motive m sorry)
Tactic: dsimp only [decreasingInduction]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
⊢ decreasingInduction (motive := motive) of_succ self ⋯ = of_succ n ⋯ self
have dsimp : leRec (motive := fun {n_1 : ℕ} (mn : n ≤ n_1) ↦
    {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
      (of_succ : (k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k sorry) → (self : motive n_1 sorry) → motive n mn)
    (fun {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k sorry)
        (self : motive n sorry) ↦
      self)
    (fun ⦃k : ℕ⦄ (h : n ≤ k)
        (ih :
          {motive : (m : ℕ) → m ≤ k → Sort u_1} →
            (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 sorry) →
              (self : motive k sorry) → motive n h)
        {motive : (m : ℕ) → m ≤ k + 1 → Sort u_1}
        (of_succ : (k_1 : ℕ) → (h : k_1 < k + 1) → motive (k_1 + 1) h → motive k_1 sorry) (self : motive (k + 1) sorry) ↦
      ih (motive := fun {m : ℕ} (h : m ≤ k) ↦ motive m sorry) (fun (i : ℕ) (hi : i < k) ↦ of_succ i sorry) (of_succ k sorry self))
    sorry (motive := motive) of_succ self =
  of_succ n sorry self
Tactic: dsimp only [decreasingInduction]