awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Init
Goal:
n m : ℕ
rw : m * 2 ≤ n ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
rw₁ : LE.le (α := ℤ) (↑(m * 2) : ℤ) (↑n : ℤ) ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
rw₂ : HMul.hMul (α := ℤ) (↑m : ℤ) (↑2 : ℤ) ≤ (↑n : ℤ) ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
rw₃ rw₄ : HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ) ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)
⊢ m ≤ n / 2 ↔ HMul.hMul (α := ℤ) (↑m : ℤ) 2 ≤ (↑n : ℤ)

Tactic:
rw [Nat.le_div_iff_mul_le Nat.zero_lt_two, ← Int.ofNat_le, Int.natCast_mul, Int.ofNat_two]

Premises used: Int.ofNat_two, Int.natCast_mul, Nat.le_div_iff_mul_le, Nat.zero_lt_two, Int.ofNat_le
-- Module: Mathlib.Data.Nat.Init
Goal:
a b : ℕ
⊢ (a + 1) / (b + 2) < a + 1

Tactic:
Nat.div_lt_self (Nat.succ_pos _) (Nat.succ_lt_succ (Nat.succ_pos _))

Premises used: Nat.succ_lt_succ, Nat.div_lt_self, Nat.succ_pos
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
hn : n % 2 = 1
⊢ 2 * (n / 2) = n - 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Init
Goal:
n m : ℕ
⊢ 1 ≤ (m + 1) ^ n

Tactic:
one_le_pow n (m + 1) (succ_pos m)

Premises used: HAdd.hAdd, Nat.one_le_pow, Nat.succ_pos, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Init
Goal:
C : ℕ → Sort u_1
h0 : C 0
h : (n : ℕ) → C n → C (n + 1)
⊢ rec (motive := fun (x : ℕ) ↦ C x) h0 h 0 = h0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Init
Goal:
C : ℕ → Sort u_1
h0 : C 0
h : (n : ℕ) → C n → C (n + 1)
n : ℕ
⊢ rec (motive := C) h0 h (n + 1) = h n (rec (motive := fun (x : ℕ) ↦ C x) h0 h n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Init
Goal:
C : ℕ → Sort u_1
h0 : C 0
h : (n : ℕ) → C n → C (n + 1)
⊢ rec (motive := C) h0 h 1 = h 0 h0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Init
Goal:
⊢ @leRec = @le.rec

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Init
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) ⋯
zero :
  ∀ {motive : (m : ℕ) → 0 ≤ m → Sort u_1} (refl : motive 0 ⋯)
    (le_succ_of_le : ⦃k : ℕ⦄ → (h : 0 ≤ k) → motive k h → motive (k + 1) ⋯),
    leRec (motive := motive) refl le_succ_of_le ⋯ = refl
succ :
  ∀ (n : ℕ) {motive : (m : ℕ) → n + 1 ≤ m → Sort u_1} (refl : motive (n + 1) ⋯)
    (le_succ_of_le : ⦃k : ℕ⦄ → (h : n + 1 ≤ k) → motive k h → motive (k + 1) ⋯),
    leRec (motive := motive) refl le_succ_of_le ⋯ = refl
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ = refl

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Init
Goal:
motive : (m : ℕ) → 0 ≤ m → Sort u_1
refl : motive 0 ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : 0 ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ = refl

Tactic:
simp [leRec, Or.by_cases, dif_neg]

Premises used: dif_neg, Or.by_cases
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
motive : (m : ℕ) → n + 1 ≤ m → Sort u_1
refl : motive (n + 1) ⋯
le_succ_of_le : ⦃k : ℕ⦄ → (h : n + 1 ≤ k) → motive k h → motive (k + 1) ⋯
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ = refl

Tactic:
simp [leRec, Or.by_cases, dif_neg]

Premises used: dif_neg, Or.by_cases
-- Module: Mathlib.Data.Nat.Init
Goal:
m 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) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
lhs : leRec (motive := motive) refl le_succ_of_le h2
| leRec (motive := motive) refl le_succ_of_le h2 = le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)

Tactic:
lhs
-- Module: Mathlib.Data.Nat.Init
Goal:
m 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) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
rw : le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
| leRec (motive := motive) refl le_succ_of_le h2

Tactic:
rw [leRec, Or.by_cases, dif_pos h1]

Premises used: dif_pos, Or.by_cases
-- Module: Mathlib.Data.Nat.Init
Goal:
m 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) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
rw : le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
| leRec (motive := motive) refl le_succ_of_le h2 = le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)

Tactic:
lhs
    rw [leRec, Or.by_cases, dif_pos h1]

Premises used: dif_pos, Or.by_cases
-- Module: Mathlib.Data.Nat.Init
Goal:
m 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) ⋯
h1 : n ≤ m
h2 : n ≤ m + 1
conv :
  leRec (motive := motive) refl le_succ_of_le h2 = le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
conv₁ :
  le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1) =
    le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)
⊢ leRec (motive := motive) refl le_succ_of_le h2 = le_succ_of_le h1 (leRec (motive := motive) refl le_succ_of_le h1)

Tactic:
conv =>
    lhs
    rw [leRec, Or.by_cases, dif_pos h1]

Premises used: dif_pos, Or.by_cases
-- Module: Mathlib.Data.Nat.Init
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) ⋯
rw : le_succ_of_le ⋯ (leRec (motive := motive) refl le_succ_of_le ⋯) = le_succ_of_le ⋯ refl
h1 : n ≤ n
rw₁ : le_succ_of_le ⋯ refl = le_succ_of_le ⋯ refl
h1₁ : n ≤ n
rw₂ : le_succ_of_le ⋯ refl = le_succ_of_le ⋯ refl
h1₂ : n ≤ n
⊢ leRec (motive := motive) refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl

Tactic:
rw [leRec_succ, leRec_self]

Premises used: Nat.leRec_succ, Nat.leRec_self
-- Module: Mathlib.Data.Nat.Init
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
refl₁ refl₂ :
  leRec (motive := motive) refl le_succ_of_le ⋯ =
    leRec (motive := fun (x : ℕ) (x_1 : n ≤ x) ↦ motive x ⋯) refl (fun (x : ℕ) (h : n ≤ x) ↦ le_succ_of_le h) hnm
⊢ 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 ⋯) ⋯

Tactic:
rw [leRec_self]

Premises used: Nat.leRec_self
-- Module: Mathlib.Data.Nat.Init
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)
step₃ : m ≤ m_1
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)
step₅ : m ≤ m_1
⊢ 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 ⋯) ⋯

Tactic:
rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]

Premises used: Nat.le_trans, Nat.leRec_succ
-- Module: Mathlib.Data.Nat.Init
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 ⋯) ⋯
step :
  ∀ {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 ⋯) ⋯
⊢ 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

Tactic:
induction hmk with
  | refl => rw [leRec_self]
  | step hmk ih => rw [leRec_succ _ _ (Nat.le_trans hnm hmk), ih, leRec_succ]

Premises used: Nat.le_trans, Nat.leRec_succ, Nat.leRec_self
-- Module: Mathlib.Data.Nat.Init
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 ⋯)
rw₁ 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 ⋯) (le_succ_of_le ⋯ refl)
        (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

Tactic:
rw [leRec_trans _ _ (le_succ n) h2, leRec_succ']

Premises used: Nat.leRec_trans, Nat.leRec_succ', Nat.le_succ
-- Module: Mathlib.Data.Nat.Init
Goal:
C : ℕ → Sort u_1
n : ℕ
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn (C := fun (x : ℕ) ↦ C x) ⋯ (fun {k : ℕ} ↦ next) x = x

Tactic:
leRec_self _ _

Premises used: Nat.leRecOn, Nat.leRec_self
-- Module: Mathlib.Data.Nat.Init
Goal:
C : ℕ → Sort u_1
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn (C := fun (x : ℕ) ↦ C x) h2 (@next) x = next (leRecOn (C := fun (x : ℕ) ↦ C x) h1 (fun {k : ℕ} ↦ next) x)

Tactic:
leRec_succ _ _ _

Premises used: Nat.leRecOn, Nat.leRec_succ
-- Module: Mathlib.Data.Nat.Init
Goal:
C : ℕ → Sort u_1
n : ℕ
h : n ≤ n + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn (C := fun (x : ℕ) ↦ C x) h (fun {k : ℕ} ↦ next) x = next x

Tactic:
leRec_succ' _ _

Premises used: Nat.leRec_succ', Nat.leRecOn
-- Module: Mathlib.Data.Nat.Init
Goal:
C : ℕ → Sort u_1
n m k : ℕ
hnm : n ≤ m
hmk : m ≤ k
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn (C := fun (x : ℕ) ↦ C x) ⋯ (@next) x =
    leRecOn (C := fun (x : ℕ) ↦ C x) hmk (@next) (leRecOn (C := fun (x : ℕ) ↦ C x) hnm (@next) x)

Tactic:
leRec_trans _ _ _ _

Premises used: Nat.leRec_trans, Nat.leRecOn
-- Module: Mathlib.Data.Nat.Init
Goal:
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
x : C n
h1 : n ≤ m
h2 : n + 1 ≤ m
⊢ leRecOn (C := fun (x : ℕ) ↦ C x) h2 (fun {k : ℕ} ↦ next) (next x) =
    leRecOn (C := fun (x : ℕ) ↦ C x) h1 (fun {k : ℕ} ↦ next) x

Tactic:
leRec_succ_left (motive := fun n _ => C n) _ (fun _ _ => @next _) _ _

Premises used: Nat.leRecOn, Nat.leRec_succ_left
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m n k : ℕ
p_1 : ℕ → Prop
p : ℕ → Sort u_1
H : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n
x : ℕ
h : x < 0
⊢ p x

Tactic:
simp at h
-- Module: Mathlib.Data.Nat.Init
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)
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)
⊢ strongRecAux (p := p) H n m hmn = H m (strongRecAux (p := p) H m)

Tactic:
obtain _ | n := n
-- Module: Mathlib.Data.Nat.Init
Goal:
p : ℕ → Sort u_1
H : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n
n m : ℕ
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:
cases hmn
-- Module: Mathlib.Data.Nat.Init
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)

Tactic:
congrArg (H _) ?_

Premises used: congrArg
-- Module: Mathlib.Data.Nat.Init
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
succ : (fun (l : ℕ) (hlm : l < m) ↦ strongRecAux (p := p) H n l ⋯) = strongRecAux (p := p) H m
⊢ strongRecAux (p := p) H (n + 1) m hmn = H m (strongRecAux (p := p) H m)

Tactic:
refine congrArg (H _) ?_

Premises used: congrArg
-- Module: Mathlib.Data.Nat.Init
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
succ : ∀ (l : ℕ) (hlm : l < m), strongRecAux (p := p) H n l ⋯ = strongRecAux (p := p) H m l hlm
⊢ (fun (l : ℕ) (hlm : l < m) ↦ strongRecAux (p := p) H n l ⋯) = strongRecAux (p := p) H m

Tactic:
ext l hlm
-- Module: Mathlib.Data.Nat.Init
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
l : ℕ
hlm : l < m
⊢ strongRecAux (p := p) H n l ⋯ = strongRecAux (p := p) H m l hlm

Tactic:
(ih _ n.lt_succ_self _ _).trans (ih _ hmn _ _).symm

Premises used: Nat.lt_succ_self, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Nat.Init
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
l : ℕ
hlm : l < m
⊢ strongRecAux (p := p) H n l ⋯ = strongRecAux (p := p) H m l hlm

Tactic:
exact (ih _ n.lt_succ_self _ _).trans (ih _ hmn _ _).symm

Premises used: Nat.lt_succ_self, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
p : ℕ → Sort u_1
H : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n
h : ∀ (m : ℕ) (lt : m < n), strongRecAux (p := fun (x : ℕ) ↦ p x) H n m lt = Nat.strongRec' (p := fun (x : ℕ) ↦ p x) H m
⊢ strongRecAux (p := fun (x : ℕ) ↦ p x) H n = fun (m : ℕ) (x : m < n) ↦ Nat.strongRec' (p := fun (x : ℕ) ↦ p x) H m

Tactic:
ext m lt
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
p : ℕ → Sort u_1
H : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n
m : ℕ
lt : m < n
⊢ strongRecAux (p := fun (x : ℕ) ↦ p x) H n m lt = Nat.strongRec' (p := fun (x : ℕ) ↦ p x) H m

Tactic:
apply strongRecAux_spec

Premises used: _private.0.Nat.strongRecAux_spec
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n
⊢ n.strongRecOn' (P := fun (x : ℕ) ↦ P x) h = h n fun (m : ℕ) (x : m < n) ↦ m.strongRecOn' (P := fun (x : ℕ) ↦ P x) h

Tactic:
strongRec'_spec _

Premises used: Nat.strongRecOn', Nat.strongRec'_spec
-- Module: Mathlib.Data.Nat.Init
Goal:
m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m ⋯
succ : ∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (n + 1) ⋯
⊢ ∀ (n : ℕ) (hmn : m ≤ n), P n hmn

Tactic:
@Nat.leRec (motive := P) _ base succ

Premises used: Nat.leRec
-- Module: Mathlib.Data.Nat.Init
Goal:
a_1 b c d e m n k_1 : ℕ
p : ℕ → Prop
motive : ℕ → Sort u_1
k : ℕ
base : (i : ℕ) → i < k → motive i
step : (n : ℕ) → ((i : ℕ) → i < k → motive (n + i)) → motive (n + k)
a : ℕ
h : ¬a < k
⊢ a - k + k = a

Tactic:
lia
-- Module: Mathlib.Data.Nat.Init
Goal:
p : ℕ → Prop
n : ℕ
h : ∀ (n : ℕ), (∀ (m : ℕ), m < n → p m) → p n
⊢ p n

Tactic:
Nat.strongRecOn n h

Premises used: Nat.strongRecOn
-- Module: Mathlib.Data.Nat.Init
Goal:
p : ℕ → Prop
a : ℕ
hz : p 0
hi : ∀ (n : ℕ), (∀ (m : ℕ), m ≤ n → p m) → p (n + 1)
⊢ p a

Tactic:
Nat.caseStrongRecOn a hz hi

Premises used: Nat.caseStrongRecOn
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m_1 n_1 k : ℕ
p : ℕ → Prop
n m : ℕ
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 ⋯

Tactic:
exact self
-- Module: Mathlib.Data.Nat.Init
Goal:
a b c d e m_1 n_1 k_1 : ℕ
p : ℕ → Prop
n m k : ℕ
h : m ≤ k
ih :
  {motive : (m : ℕ) → m ≤ k → Sort u_1} →
    (of_succ : (k_2 : ℕ) → (h : k_2 < k) → motive (k_2 + 1) h → motive k_2 ⋯) → (self : motive k ⋯) → motive m h
motive : (m : ℕ) → m ≤ k + 1 → Sort u_1
of_succ : (k_2 : ℕ) → (h : k_2 < k + 1) → motive (k_2 + 1) h → motive k_2 ⋯
self : motive (k + 1) ⋯
⊢ motive m ⋯

Tactic:
apply ih (fun i hi => of_succ i (le_succ_of_le hi)) (of_succ k (lt_succ_self _) self)
-- Module: Mathlib.Data.Nat.Init
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 ⋯
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 ⋯) →
              (self : motive k ⋯) → 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 ⋯) →
            (self : motive (k + 1) ⋯) → motive m ⋯
⊢ motive m mn

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)

Premises used: Nat.le_succ_of_le
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
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 ⋯) → (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
⊢ decreasingInduction (motive := motive) of_succ self ⋯ = self

Tactic:
dsimp only [decreasingInduction]
-- Module: Mathlib.Data.Nat.Init
Goal:
n : ℕ
motive : (m : ℕ) → m ≤ n → Sort u_1
of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯
self : motive n ⋯
rw rw₁ : self = self
⊢ 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

Tactic:
rw [leRec_self]

Premises used: Nat.leRec_self