awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) ⋯
⊢ 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 =
    of_succ n ⋯ self
have rw : (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)
    (motive := fun {m : ℕ} (h : m ≤ n) ↦ motive m sorry) (fun (i : ℕ) (hi : i < n) ↦ of_succ i sorry) (of_succ n sorry self) =
  of_succ n sorry self
Tactic: rw [leRec_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n k : ℕ
hmn : m ≤ 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 ⋯ =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) of_succ self ⋯) hmn
have refl : decreasingInduction (motive := motive) of_succ self sorry =
  decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x sorry) self
    hmn
Tactic: rw [decreasingInduction_self]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n k : ℕ
hmn : m ≤ n
m_1 : ℕ
hnk : n.le m_1
ih :
  ∀ {motive : (m : ℕ) → m ≤ m_1 → Sort u_1} (of_succ : (k : ℕ) → (h : k < m_1) → motive (k + 1) h → motive k ⋯)
    (self : motive m_1 ⋯),
    decreasingInduction (motive := motive) of_succ self ⋯ =
      decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯) of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m_1.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m_1.succ) → motive (k + 1) h → motive k ⋯
self : motive m_1.succ ⋯
⊢ decreasingInduction (motive := motive) of_succ self ⋯ =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn
have step : Eq.{u_1} (α := motive m sorry)
  (decreasingInduction (motive := fun (m : ℕ) (h : m ≤ m_1) ↦ motive m sorry) (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x sorry)
      (of_succ m_1 sorry self) sorry :
    motive m sorry)
  (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x sorry)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x sorry) of_succ self sorry) hmn :
    motive m sorry)
Tactic: rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n k : ℕ
hmn : m ≤ n
m_1 : ℕ
hnk : n.le m_1
ih :
  ∀ {motive : (m : ℕ) → m ≤ m_1 → Sort u_1} (of_succ : (k : ℕ) → (h : k < m_1) → motive (k + 1) h → motive k ⋯)
    (self : motive m_1 ⋯),
    decreasingInduction (motive := motive) of_succ self ⋯ =
      decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯) of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m_1.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m_1.succ) → motive (k + 1) h → motive k ⋯
self : motive m_1.succ ⋯
step :
  Eq.{u_1} (α := motive m ⋯)
    (decreasingInduction (motive := fun (m : ℕ) (h : m ≤ m_1) ↦ motive m ⋯) (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯)
        (of_succ m_1 ⋯ self) ⋯ :
      motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn :
      motive m ⋯)
⊢ decreasingInduction (motive := motive) of_succ self ⋯ =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn
have step₁ : Eq.{u_1} (α := motive m sorry)
  (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x sorry)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x sorry)
        (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x sorry) (of_succ m_1 sorry self) hnk)
      hmn :
    motive m sorry)
  (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x sorry)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x sorry) of_succ self sorry) hmn :
    motive m sorry)
Tactic: rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n k : ℕ
hmn : m ≤ n
m_1 : ℕ
hnk : n.le m_1
ih :
  ∀ {motive : (m : ℕ) → m ≤ m_1 → Sort u_1} (of_succ : (k : ℕ) → (h : k < m_1) → motive (k + 1) h → motive k ⋯)
    (self : motive m_1 ⋯),
    decreasingInduction (motive := motive) of_succ self ⋯ =
      decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯) of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m_1.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m_1.succ) → motive (k + 1) h → motive k ⋯
self : motive m_1.succ ⋯
step :
  Eq.{u_1} (α := motive m ⋯)
    (decreasingInduction (motive := fun (m : ℕ) (h : m ≤ m_1) ↦ motive m ⋯) (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯)
        (of_succ m_1 ⋯ self) ⋯ :
      motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn :
      motive m ⋯)
step₁ :
  Eq.{u_1} (α := motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯)
          (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯) (of_succ m_1 ⋯ self) hnk)
        hmn :
      motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn :
      motive m ⋯)
⊢ decreasingInduction (motive := motive) of_succ self ⋯ =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn
have step₂ : Eq.{u_1} (α := motive m sorry)
  (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x sorry)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x sorry)
        (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x sorry) (of_succ m_1 sorry self) hnk)
      hmn :
    motive m sorry)
  (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x sorry)
      (decreasingInduction (motive := fun (m : ℕ) (h : m ≤ m_1) ↦ motive m sorry)
        (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x sorry) (of_succ m_1 sorry self) hnk)
      hmn :
    motive m sorry)
Tactic: rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n k : ℕ
hmn : m ≤ n
m_1 : ℕ
hnk : n.le m_1
ih :
  ∀ {motive : (m : ℕ) → m ≤ m_1 → Sort u_1} (of_succ : (k : ℕ) → (h : k < m_1) → motive (k + 1) h → motive k ⋯)
    (self : motive m_1 ⋯),
    decreasingInduction (motive := motive) of_succ self ⋯ =
      decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯) of_succ self hnk) hmn
motive : (m : ℕ) → m ≤ m_1.succ → Sort u_1
of_succ : (k : ℕ) → (h : k < m_1.succ) → motive (k + 1) h → motive k ⋯
self : motive m_1.succ ⋯
step :
  Eq.{u_1} (α := motive m ⋯)
    (decreasingInduction (motive := fun (m : ℕ) (h : m ≤ m_1) ↦ motive m ⋯) (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯)
        (of_succ m_1 ⋯ self) ⋯ :
      motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn :
      motive m ⋯)
step₁ :
  Eq.{u_1} (α := motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯)
          (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯) (of_succ m_1 ⋯ self) hnk)
        hmn :
      motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn :
      motive m ⋯)
step₂ :
  Eq.{u_1} (α := motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x ⋯)
          (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯) (of_succ m_1 ⋯ self) hnk)
        hmn :
      motive m ⋯)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (m : ℕ) (h : m ≤ m_1) ↦ motive m ⋯)
          (fun (x : ℕ) (x_1 : x < m_1) ↦ of_succ x ⋯) (of_succ m_1 ⋯ self) hnk)
        hmn :
      motive m ⋯)
⊢ decreasingInduction (motive := motive) of_succ self ⋯ =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x ⋯) of_succ self ⋯) hmn
have step₃ : n ≤ m_1
Tactic: rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n k : ℕ
motive : (m : ℕ) → m ≤ k → Sort u_1
hmn : m ≤ n
hnk : n ≤ k
of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯
self : motive k ⋯
⊢ decreasingInduction (motive := motive) of_succ self ⋯ =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ k) ↦ motive x ⋯) of_succ self hnk) hmn
have refl : ∀ {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k sorry)
  (self : motive n sorry),
  decreasingInduction (motive := motive) of_succ self sorry =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x sorry)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) of_succ self sorry) hmn
Tactic: induction hnk with
  | refl => rw [decreasingInduction_self]
  | step hnk ih =>
      rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]
Cleared hypotheses: motive, hnk, of_succ, self
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n k : ℕ
motive : (m : ℕ) → m ≤ k → Sort u_1
hmn : m ≤ n
hnk : n ≤ k
of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive k_1 ⋯
self : motive k ⋯
refl :
  ∀ {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 ⋯ =
      decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
        (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) of_succ self ⋯) hmn
⊢ decreasingInduction (motive := motive) of_succ self ⋯ =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ k) ↦ motive x ⋯) of_succ self hnk) hmn
have step : ∀ {m_1 : ℕ} (hnk : n.le m_1)
  (ih :
    ∀ {motive : (m : ℕ) → m ≤ m_1 → Sort u_1} (of_succ : (k : ℕ) → (h : k < m_1) → motive (k + 1) h → motive k sorry)
      (self : motive m_1 sorry),
      decreasingInduction (motive := motive) of_succ self sorry =
        decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x sorry)
          (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1) ↦ motive x sorry) of_succ self hnk) hmn)
  {motive : (m : ℕ) → m ≤ m_1.succ → Sort u_1} (of_succ : (k : ℕ) → (h : k < m_1.succ) → motive (k + 1) h → motive k sorry)
  (self : motive m_1.succ sorry),
  decreasingInduction (motive := motive) of_succ self sorry =
    decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) (fun (x : ℕ) (x_1 : x < n) ↦ of_succ x sorry)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m_1.succ) ↦ motive x sorry) of_succ self sorry) hmn
Tactic: induction hnk with
  | refl => rw [decreasingInduction_self]
  | step hnk ih =>
      rw [decreasingInduction_succ _ _ (Nat.le_trans hmn hnk), ih, decreasingInduction_succ]
Cleared hypotheses: motive, hnk, of_succ, self
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
rw :
  decreasingInduction (motive := motive) of_succ self ⋯ =
    of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)
⊢ decreasingInduction (motive := motive) of_succ self mn =
    of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)
have rw₁ : decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m + 1) ↦ motive x sorry) (fun (x : ℕ) (x_1 : x < m + 1) ↦ of_succ x sorry)
    (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) of_succ self smn) sorry =
  of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)
Tactic: rw [Subsingleton.elim mn (Nat.le_trans (le_succ m) smn),
    decreasingInduction_trans (n := m + 1) (Nat.le_succ m),
    decreasingInduction_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
smn : m + 1 ≤ n
mn : m ≤ n
rw :
  decreasingInduction (motive := motive) of_succ self ⋯ =
    of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)
rw₁ :
  decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ m + 1) ↦ motive x ⋯)
      (fun (x : ℕ) (x_1 : x < m + 1) ↦ of_succ x ⋯)
      (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x ⋯) of_succ self smn) ⋯ =
    of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)
hnk : m + 1 ≤ n
⊢ decreasingInduction (motive := motive) of_succ self mn =
    of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)
have rw₂ : of_succ m sorry (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x sorry) of_succ self smn) =
  of_succ m smn (decreasingInduction (motive := fun (x : ℕ) (x_1 : x ≤ n) ↦ motive x x_1) of_succ self smn)
Tactic: rw [Subsingleton.elim mn (Nat.le_trans (le_succ m) smn),
    decreasingInduction_trans (n := m + 1) (Nat.le_succ m),
    decreasingInduction_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
a b c d e m n k : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
h : (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k
mn : m ≤ n
hP : P n
⊢ P m
have self : (h : (k : ℕ) → k < n → n ≤ k → P (k + 1) → P k) → P n
Tactic: induction mn using decreasingInduction with
  | self => exact hP
  | of_succ k hk ih =>
    exact h _ (lt_of_succ_le hk) (Nat.le_refl _)
      (ih fun k' hk' h'' => h k' hk' <| le_of_succ_le h'')
Cleared hypotheses: h, mn
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
a b c d e m n k : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
h : (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k
mn : m ≤ n
hP : P n
self : (h : (k : ℕ) → k < n → n ≤ k → P (k + 1) → P k) → P n
⊢ P m
have of_succ : (k : ℕ) →
  (hk : k < n) →
    (ih : (h : (k_1 : ℕ) → k_1 < n → k + 1 ≤ k_1 → P (k_1 + 1) → P k_1) → P (k + 1)) →
      (h : (k_1 : ℕ) → k_1 < n → k ≤ k_1 → P (k_1 + 1) → P k_1) → P k
Tactic: induction mn using decreasingInduction with
  | self => exact hP
  | of_succ k hk ih =>
    exact h _ (lt_of_succ_le hk) (Nat.le_refl _)
      (ih fun k' hk' h'' => h k' hk' <| le_of_succ_le h'')
Cleared hypotheses: h, mn
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P (a + 1) (b + 1)
have a₁ : P (a + 1) b
Tactic: apply hd _ _ (Nat.add_lt_add_iff_right.1 h)
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
a₁ : P (a + 1) b
⊢ P (a + 1) (b + 1)
have a₂ : P a (b + 1)
Tactic: apply hd _ _ (Nat.add_lt_add_iff_right.1 h)
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P (a + 1) b
have a₁ : ∀ (this : a + 1 = b ∨ a + 1 < b), P (a + 1) b
Tactic: have this : a + 1 = b ∨ a + 1 < b := by lia
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
this : a + 1 = b ∨ a + 1 < b
⊢ P (a + 1) b
have a₁ : ∀ (h : a + 1 < a + 1 + 1), P (a + 1) (a + 1)
Tactic: rcases this with (rfl | h)
Cleared hypotheses: b, h, this
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
this : a + 1 = b ∨ a + 1 < b
a₁ : ∀ (h : a + 1 < a + 1 + 1), P (a + 1) (a + 1)
⊢ P (a + 1) b
have a₂ : ∀ (h : a + 1 < b), P (a + 1) b
Tactic: rcases this with (rfl | h)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P a (b + 1)
have a₁ : a < b + 1
Tactic: apply diag_induction P ha hb hd a (b + 1)
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n_1 : ℕ
h : m = n_1
n : ℕ
⊢ m ∣ n ↔ n_1 ∣ n
have rw : n_1 ∣ n ↔ n_1 ∣ n
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
m n_1 : ℕ
h : m = n_1
n : ℕ
⊢ n ∣ m ↔ n ∣ n_1
have rw : n ∣ n_1 ↔ n ∣ n_1
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst : DecidablePred P
⊢ (∀ (x : ℕ), x < hi - lo → P (lo + x)) ↔ ∀ (x : ℕ), lo ≤ x → x < hi → P x
have refine : ∀ (al : ∀ (x : ℕ), x < hi - lo → P (lo + x)) (x : ℕ) (hl : lo ≤ x) (hh : x < hi), P x
Tactic: refine ⟨fun al x hl hh ↦ ?_,
      fun al x h ↦ al _ (Nat.le_add_right _ _) (Nat.lt_sub_iff_add_lt'.1 h)⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
⊢ P x
have have : ∀ (this : P (lo + (x - lo))), P x
Tactic: have := al (x - lo) ((Nat.sub_lt_sub_iff_right hl).2 hh)
-- Lean 4 proof step from Mathlib.Data.Nat.Init (goal)
Goal:
a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
this : P (lo + (x - lo))
⊢ P x
have rwa : ∀ (this : P x), P x
Tactic: rwa [Nat.add_sub_cancel' hl] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Nat.Init (hypothesis)
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ n - 1 ≠ 0
have this : 2 ≤ n
Tactic: have := prop (n := n)
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
h : s = ∅
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
have inl : Eq (α := ℕ) (sInf ∅) 0 ↔ Membership.mem (γ := Set ℕ) ∅ 0 ∨ Eq (α := Set ℕ) ∅ ∅
Tactic: subst h
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (hypothesis)
Goal:
s : Set ℕ
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅
have x : s = ∅ ∨ s.Nonempty
Tactic: cases eq_empty_or_nonempty s with
  | inl h => subst h
             simp only [or_true, InfSet.sInf,
                        mem_empty_iff_false, exists_false, dif_neg, not_false_iff]
  | inr h => simp only [h.ne_empty, or_false, Nat.sInf_def, h, Nat.find_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
⊢ Eq (α := ℕ) (sInf ∅) 0
have rw : Membership.mem (γ := Set ℕ) ∅ 0 ∨ Eq (α := Set ℕ) ∅ ∅
Tactic: rw [sInf_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
⊢ Membership.mem (γ := Set ℕ) ∅ 0 ∨ Eq (α := Set ℕ) ∅ ∅
have h : Eq (α := Set ℕ) ∅ ∅
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℕ
⊢ iInf f = 0
have rw : Eq (α := ℕ) (sInf ∅) 0
Tactic: rw [iInf_of_isEmpty, sInf_empty]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℕ
rw : Eq (α := ℕ) (sInf ∅) 0
⊢ iInf f = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [iInf_of_isEmpty, sInf_empty]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
h : s.Nonempty
⊢ sInf s ∈ s
have rw : Nat.find (p := fun (n : ℕ) ↦ n ∈ s) h ∈ s
Tactic: rw [Nat.sInf_def h]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
h : s.Nonempty
⊢ sInf s ∈ s
have rw : Nat.find (p := fun (n : ℕ) ↦ n ∈ s) h ∈ s
Tactic: classical
  rw [Nat.sInf_def h]
  exact Nat.find_spec h
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s = ∅
⊢ m ∉ s
have inl : ∀ (hm : m < sInf ∅), m ∉ ∅
Tactic: subst h
Cleared hypotheses: s, hm, h
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (hypothesis)
Goal:
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s.Nonempty
⊢ m ∉ s
have hm₁ : m < Nat.find (p := fun (n : ℕ) ↦ n ∈ s) h
Tactic: rw [Nat.sInf_def h] at hm
Cleared hypotheses: hm