awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
h : n + 2 ≠ 0
k : ℕ
hk : k ∈ Iic (n + 1)
⊢ Even (k.largeSchroder * (n + 1 - k).largeSchroder)
have zero : ∀ (hk : 0 ∈ Iic (n + 1)), Even (largeSchroder 0 * (n + 1 - 0).largeSchroder)
Tactic: obtain _ | k := k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
h : n + 2 ≠ 0
k : ℕ
hk : k ∈ Iic (n + 1)
zero : ∀ (hk : 0 ∈ Iic (n + 1)), Even (largeSchroder 0 * (n + 1 - 0).largeSchroder)
⊢ Even (k.largeSchroder * (n + 1 - k).largeSchroder)
have succ : ∀ (k : ℕ) (hk : k + 1 ∈ Iic (n + 1)), Even ((k + 1).largeSchroder * (n + 1 - (k + 1)).largeSchroder)
Tactic: obtain _ | k := k
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (hypothesis)
Goal:
n : ℕ
h : n + 2 ≠ 0
k : ℕ
hk : k + 1 ∈ Iic (n + 1)
⊢ k < n + 1
have hk₁ : k ≤ n
Tactic: simp at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (hypothesis)
Goal:
n : ℕ
h : n + 2 ≠ 0
k : ℕ
hk : k + 1 ∈ Iic (n + 1)
⊢ Even ((k + 1).largeSchroder * (n + 1 - (k + 1)).largeSchroder)
have this : k < n + 1
Tactic: have : k < n + 1 := by simp at hk; lia
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ 2 * (n + 1).smallSchroder = n.largeSchroder
have rw : 2 * (n.largeSchroder / 2) = n.largeSchroder
Tactic: rw [smallSchroder_succ_eq_largeSchroder_div_two hn,
    Nat.mul_div_cancel_left' (even_largeSchroder hn).two_dvd]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : 2 * (n.largeSchroder / 2) = n.largeSchroder
⊢ 2 * (n + 1).smallSchroder = n.largeSchroder
have rw₁ : n.largeSchroder = n.largeSchroder
Tactic: rw [smallSchroder_succ_eq_largeSchroder_div_two hn,
    Nat.mul_div_cancel_left' (even_largeSchroder hn).two_dvd]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n
⊢ (n + 1).smallSchroder =
    3 * n.smallSchroder + HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n - 1), (i + 1).smallSchroder * (n - i).smallSchroder)
have zero : ∀ (hn : LT.lt (α := ℕ) 1 0),
  (HAdd.hAdd (α := ℕ) 0 1).smallSchroder =
    3 * smallSchroder 0 +
      HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (HSub.hSub (α := ℕ) 0 1), (i + 1).smallSchroder * (0 - i).smallSchroder)
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n
zero :
  ∀ (hn : LT.lt (α := ℕ) 1 0),
    (HAdd.hAdd (α := ℕ) 0 1).smallSchroder =
      3 * smallSchroder 0 +
        HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (HSub.hSub (α := ℕ) 0 1), (i + 1).smallSchroder * (0 - i).smallSchroder)
⊢ (n + 1).smallSchroder =
    3 * n.smallSchroder + HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n - 1), (i + 1).smallSchroder * (n - i).smallSchroder)
have succ : ∀ (hn : 1 < HAdd.hAdd (α := ℕ) 0 1),
  (HAdd.hAdd (α := ℕ) 0 1 + 1).smallSchroder =
    3 * (HAdd.hAdd (α := ℕ) 0 1).smallSchroder +
      HMul.hMul (α := ℕ) 2
        (∑ i ∈ Ioo 0 (HAdd.hAdd (α := ℕ) 0 1 - 1), (i + 1).smallSchroder * (HAdd.hAdd (α := ℕ) 0 1 - i).smallSchroder)
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n
zero :
  ∀ (hn : LT.lt (α := ℕ) 1 0),
    (HAdd.hAdd (α := ℕ) 0 1).smallSchroder =
      3 * smallSchroder 0 +
        HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (HSub.hSub (α := ℕ) 0 1), (i + 1).smallSchroder * (0 - i).smallSchroder)
succ :
  ∀ (hn : 1 < HAdd.hAdd (α := ℕ) 0 1),
    (HAdd.hAdd (α := ℕ) 0 1 + 1).smallSchroder =
      3 * (HAdd.hAdd (α := ℕ) 0 1).smallSchroder +
        HMul.hMul (α := ℕ) 2
          (∑ i ∈ Ioo 0 (HAdd.hAdd (α := ℕ) 0 1 - 1), (i + 1).smallSchroder * (HAdd.hAdd (α := ℕ) 0 1 - i).smallSchroder)
⊢ (n + 1).smallSchroder =
    3 * n.smallSchroder + HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n - 1), (i + 1).smallSchroder * (n - i).smallSchroder)
have succ₁ : ∀ (n : ℕ) (hn : 1 < n + 1 + 1),
  (n + 1 + 1 + 1).smallSchroder =
    3 * (n + 1 + 1).smallSchroder +
      HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n + 1 + 1 - 1), (i + 1).smallSchroder * (n + 1 + 1 - i).smallSchroder)
Tactic: obtain _ | _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ (n + 1 + 1 + 1).smallSchroder =
    3 * (n + 1 + 1).smallSchroder +
      HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n + 1 + 1 - 1), (i + 1).smallSchroder * (n + 1 + 1 - i).smallSchroder)
have succ : 2 * (n + 1 + 1 + 1).smallSchroder =
  2 *
    (3 * (n + 1 + 1).smallSchroder +
      HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n + 1 + 1 - 1), (i + 1).smallSchroder * (n + 1 + 1 - i).smallSchroder))
Tactic: refine Nat.mul_left_cancel zero_lt_two ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ 2 * (n + 3).smallSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
have rw : (n + 1).largeSchroder +
    (∑ x ∈ Ioo ⊥ (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder +
        (n + 1).largeSchroder * (n + 1 - (n + 1)).largeSchroder +
      largeSchroder ⊥ * (n + 1 - ⊥).largeSchroder) =
  3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
Tactic: rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
rw :
  (n + 1).largeSchroder +
      (∑ x ∈ Ioo ⊥ (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder +
          (n + 1).largeSchroder * (n + 1 - (n + 1)).largeSchroder +
        largeSchroder ⊥ * (n + 1 - ⊥).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
⊢ 2 * (n + 3).smallSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
have rw₁ : ⊥ < n + 1
Tactic: rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
rw :
  (n + 1).largeSchroder +
      (∑ x ∈ Ioo ⊥ (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder +
          (n + 1).largeSchroder * (n + 1 - (n + 1)).largeSchroder +
        largeSchroder ⊥ * (n + 1 - ⊥).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
rw₁ : ⊥ < n + 1
⊢ 2 * (n + 3).smallSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
have rw₂ : ⊥ ≤ n + 1
Tactic: rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
rw :
  (n + 1).largeSchroder +
      (∑ x ∈ Ioo ⊥ (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder +
          (n + 1).largeSchroder * (n + 1 - (n + 1)).largeSchroder +
        largeSchroder ⊥ * (n + 1 - ⊥).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
rw₁ : ⊥ < n + 1
rw₂ : ⊥ ≤ n + 1
⊢ 2 * (n + 3).smallSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
have rw₃ : n + 2 ≠ 0
Tactic: rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ (n + 1).largeSchroder +
      (∑ x ∈ Ioo ⊥ (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder +
          (n + 1).largeSchroder * (n + 1 - (n + 1)).largeSchroder +
        largeSchroder ⊥ * (n + 1 - ⊥).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
have simp : (n + 1).largeSchroder +
    (∑ x ∈ Ioo 0 (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder + (n + 1).largeSchroder + (n + 1).largeSchroder) =
  3 * (n + 1).largeSchroder + ∑ x ∈ Ioo 0 (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder
Tactic: simp
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ 3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
have h : ∀ (i : ℕ) (hi : i ∈ Ioo 0 (n + 1)),
  i.largeSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
Tactic: congr! 2 with i hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (hypothesis)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : i ∈ Ioo 0 (n + 1)
⊢ i.largeSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
have hi₁ : 0 < i ∧ i ≤ n
Tactic: simp at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i.largeSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
have h : 2 * (i + 1).smallSchroder * (2 * (n + 1 - i + 1).smallSchroder) =
  2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
Tactic: rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
h :
  2 * (i + 1).smallSchroder * (2 * (n + 1 - i + 1).smallSchroder) =
    2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
⊢ i.largeSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
have h₁ : n + 1 - i ≠ 0
Tactic: rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
h :
  2 * (i + 1).smallSchroder * (2 * (n + 1 - i + 1).smallSchroder) =
    2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
h₁ : n + 1 - i ≠ 0
⊢ i.largeSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
have h₂ : i ≠ 0
Tactic: rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ 3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder) =
    6 * (n + 2).smallSchroder +
      HMul.hMul (α := ℕ) 4 (∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder)
have rw : 3 * (2 * (n + 1 + 1).smallSchroder) + ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder) =
  6 * (n + 2).smallSchroder +
    HMul.hMul (α := ℕ) 4 (∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder)
Tactic: rw [← two_mul_smallSchroder_succ (by lia)]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ 3 * (2 * (n + 1 + 1).smallSchroder) +
      ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder) =
    6 * (n + 2).smallSchroder +
      HMul.hMul (α := ℕ) 4 (∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder)
have simp : 3 * (2 * (n + 1 + 1).smallSchroder) = 6 * (n + 2).smallSchroder
Tactic: simp [mul_mul_mul_comm _ _ 2, ← Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ 2 * (n + 1 + 1 + 1).smallSchroder =
    2 *
      (3 * (n + 1 + 1).smallSchroder +
        HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n + 1 + 1 - 1), (i + 1).smallSchroder * (n + 1 + 1 - i).smallSchroder))
have _ : 2 * (n + 3).smallSchroder = 3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
Tactic: calc
        2 * (n + 3).smallSchroder
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder := by
      rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc] <;> simp; lia
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), (2 * (i + 1).smallSchroder) * (2 * (n + 2 - i).smallSchroder) := by
      congr! 2 with i hi
      simp at hi
      rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ] <;> lia
    _ = 6 * (n + 2).smallSchroder +
          4 * ∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder := by
      rw [← two_mul_smallSchroder_succ (by lia)]
      simp [mul_mul_mul_comm _ _ 2, ← Finset.mul_sum]
      lia
    _ = _ := by lia
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
_ :
  2 * (n + 3).smallSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
⊢ 2 * (n + 1 + 1 + 1).smallSchroder =
    2 *
      (3 * (n + 1 + 1).smallSchroder +
        HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n + 1 + 1 - 1), (i + 1).smallSchroder * (n + 1 + 1 - i).smallSchroder))
have _₁ : 3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder =
  3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
Tactic: calc
        2 * (n + 3).smallSchroder
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder := by
      rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc] <;> simp; lia
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), (2 * (i + 1).smallSchroder) * (2 * (n + 2 - i).smallSchroder) := by
      congr! 2 with i hi
      simp at hi
      rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ] <;> lia
    _ = 6 * (n + 2).smallSchroder +
          4 * ∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder := by
      rw [← two_mul_smallSchroder_succ (by lia)]
      simp [mul_mul_mul_comm _ _ 2, ← Finset.mul_sum]
      lia
    _ = _ := by lia
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
_ :
  2 * (n + 3).smallSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
_₁ :
  3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
⊢ 2 * (n + 1 + 1 + 1).smallSchroder =
    2 *
      (3 * (n + 1 + 1).smallSchroder +
        HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n + 1 + 1 - 1), (i + 1).smallSchroder * (n + 1 + 1 - i).smallSchroder))
have _₂ : 3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder) =
  6 * (n + 2).smallSchroder +
    HMul.hMul (α := ℕ) 4 (∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder)
Tactic: calc
        2 * (n + 3).smallSchroder
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder := by
      rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc] <;> simp; lia
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), (2 * (i + 1).smallSchroder) * (2 * (n + 2 - i).smallSchroder) := by
      congr! 2 with i hi
      simp at hi
      rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ] <;> lia
    _ = 6 * (n + 2).smallSchroder +
          4 * ∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder := by
      rw [← two_mul_smallSchroder_succ (by lia)]
      simp [mul_mul_mul_comm _ _ 2, ← Finset.mul_sum]
      lia
    _ = _ := by lia
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
hn : 1 < n + 1 + 1
_ :
  2 * (n + 3).smallSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder
_₁ :
  3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)
_₂ :
  3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder) =
    6 * (n + 2).smallSchroder +
      HMul.hMul (α := ℕ) 4 (∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder)
⊢ 2 * (n + 1 + 1 + 1).smallSchroder =
    2 *
      (3 * (n + 1 + 1).smallSchroder +
        HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n + 1 + 1 - 1), (i + 1).smallSchroder * (n + 1 + 1 - i).smallSchroder))
have _₃ : 6 * (n + 2).smallSchroder +
    HMul.hMul (α := ℕ) 4 (∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder) =
  2 *
    (3 * (n + 1 + 1).smallSchroder +
      HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n + 1 + 1 - 1), (i + 1).smallSchroder * (n + 1 + 1 - i).smallSchroder))
Tactic: calc
        2 * (n + 3).smallSchroder
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder := by
      rw [two_mul_smallSchroder_succ, largeSchroder_succ, ← Icc_bot, ← sum_Ioc_add_eq_sum_Icc,
        ← sum_Ioo_add_eq_sum_Ioc] <;> simp; lia
    _ = 3 * (n + 1).largeSchroder +
          ∑ i ∈ Ioo 0 (n + 1), (2 * (i + 1).smallSchroder) * (2 * (n + 2 - i).smallSchroder) := by
      congr! 2 with i hi
      simp at hi
      rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ] <;> lia
    _ = 6 * (n + 2).smallSchroder +
          4 * ∑ i ∈ Ioo 0 (n + 1), (i + 1).smallSchroder * (n + 2 - i).smallSchroder := by
      rw [← two_mul_smallSchroder_succ (by lia)]
      simp [mul_mul_mul_comm _ _ 2, ← Finset.mul_sum]
      lia
    _ = _ := by lia
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n k : ℕ
hk : k ≠ 0
⊢ (n + 1).stirlingFirst k = n * n.stirlingFirst k + n.stirlingFirst (k - 1)
have obtain : ∀ (l : ℕ) (hk : l + succ 0 ≠ 0),
  (n + 1).stirlingFirst (l + succ 0) = n * n.stirlingFirst (l + succ 0) + n.stirlingFirst (l + succ 0 - 1)
Tactic: obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.pos_of_ne_zero hk)
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n k : ℕ
hn : n ≠ 0
⊢ n.stirlingFirst (k + 1) = (n - 1) * (n - 1).stirlingFirst (k + 1) + (n - 1).stirlingFirst k
have obtain : ∀ (l : ℕ) (hn : l + succ 0 ≠ 0),
  (l + succ 0).stirlingFirst (k + 1) =
    (l + succ 0 - 1) * (l + succ 0 - 1).stirlingFirst (k + 1) + (l + succ 0 - 1).stirlingFirst k
Tactic: obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.pos_of_ne_zero hn)
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
h : 0 < n + 1
⊢ stirlingFirst 0 (n + 1) = 0
have rw : Eq (α := ℕ) 0 0
Tactic: rw [stirlingFirst]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n k : ℕ
hk : n + 1 < k + 1
⊢ (n + 1).stirlingFirst (k + 1) = 0
have rw : n * n.stirlingFirst (k + 1) + n.stirlingFirst k = 0
Tactic: rw [stirlingFirst_succ_succ, stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt_succ hk),
      stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt hk), mul_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n k : ℕ
hk : n + 1 < k + 1
rw : n * n.stirlingFirst (k + 1) + n.stirlingFirst k = 0
⊢ (n + 1).stirlingFirst (k + 1) = 0
have rw₁ : n * n.stirlingFirst (k + 1) + 0 = 0
Tactic: rw [stirlingFirst_succ_succ, stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt_succ hk),
      stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt hk), mul_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n k : ℕ
hk : n + 1 < k + 1
rw : n * n.stirlingFirst (k + 1) + n.stirlingFirst k = 0
rw₁ : n * n.stirlingFirst (k + 1) + 0 = 0
⊢ (n + 1).stirlingFirst (k + 1) = 0
have rw₂ : n * 0 + 0 = 0
Tactic: rw [stirlingFirst_succ_succ, stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt_succ hk),
      stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt hk), mul_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n k : ℕ
hk : n + 1 < k + 1
rw : n * n.stirlingFirst (k + 1) + n.stirlingFirst k = 0
rw₁ : n * n.stirlingFirst (k + 1) + 0 = 0
rw₂ : n * 0 + 0 = 0
⊢ (n + 1).stirlingFirst (k + 1) = 0
have rw₃ : HAdd.hAdd (α := ℕ) 0 0 = 0
Tactic: rw [stirlingFirst_succ_succ, stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt_succ hk),
      stirlingFirst_eq_zero_of_lt (Nat.lt_of_succ_lt hk), mul_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
⊢ n.stirlingFirst n = 1
have zero : stirlingFirst 0 0 = 1
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
zero : stirlingFirst 0 0 = 1
⊢ n.stirlingFirst n = 1
have succ : ∀ (n : ℕ), n.stirlingFirst n = 1 → (n + 1).stirlingFirst (n + 1) = 1
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
⊢ (n + 1 + 1).stirlingFirst (n + 1) = (n + 1 + 1).choose 2
have succ : (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).stirlingFirst n = (n + 1 + 1).choose 2
Tactic: rw [stirlingFirst_succ_succ, ih, stirlingFirst_self, mul_one, Nat.choose_succ_succ (n + 1),
      Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
succ : (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).stirlingFirst n = (n + 1 + 1).choose 2
⊢ (n + 1 + 1).stirlingFirst (n + 1) = (n + 1 + 1).choose 2
have succ₁ : (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
Tactic: rw [stirlingFirst_succ_succ, ih, stirlingFirst_self, mul_one, Nat.choose_succ_succ (n + 1),
      Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
succ : (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).stirlingFirst n = (n + 1 + 1).choose 2
succ₁ : (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
⊢ (n + 1 + 1).stirlingFirst (n + 1) = (n + 1 + 1).choose 2
have succ₂ : (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
Tactic: rw [stirlingFirst_succ_succ, ih, stirlingFirst_self, mul_one, Nat.choose_succ_succ (n + 1),
      Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
succ : (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).stirlingFirst n = (n + 1 + 1).choose 2
succ₁ : (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₂ : (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
⊢ (n + 1 + 1).stirlingFirst (n + 1) = (n + 1 + 1).choose 2
have succ₃ : n + 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
Tactic: rw [stirlingFirst_succ_succ, ih, stirlingFirst_self, mul_one, Nat.choose_succ_succ (n + 1),
      Nat.choose_one_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Stirling (goal)
Goal:
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
succ : (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).stirlingFirst n = (n + 1 + 1).choose 2
succ₁ : (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₂ : (n + 1) * 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
succ₃ : n + 1 + (n + 1).choose 2 = (n + 1 + 1).choose 2
⊢ (n + 1 + 1).stirlingFirst (n + 1) = (n + 1 + 1).choose 2
have succ₄ : n + 1 + (n + 1).choose 2 = (n + 1).choose 1 + (n + 1).choose (Nat.succ 1)
Tactic: rw [stirlingFirst_succ_succ, ih, stirlingFirst_self, mul_one, Nat.choose_succ_succ (n + 1),
      Nat.choose_one_right]