awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
h : n + 2 ≠ 0
k : ℕ
hk : k + 1 ∈ Iic (n + 1)
this : k < n + 1
⊢ Even ((k + 1).largeSchroder * (n + 1 - (k + 1)).largeSchroder)

Tactic:
exact .mul_right (even_largeSchroder k.succ_ne_zero) _
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
⊢ smallSchroder 0 = 1

Tactic:
simp [smallSchroder]

Premises used: Nat.smallSchroder
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
⊢ smallSchroder 1 = 1

Tactic:
simp [smallSchroder]

Premises used: Nat.smallSchroder
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
h : n ≠ 0
⊢ (n + 1).smallSchroder = n.largeSchroder / 2

Tactic:
simp [smallSchroder]

Premises used: Nat.smallSchroder
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : n ≠ 0
rw : 2 * (n.largeSchroder / 2) = n.largeSchroder
rw₁ rw₂ : n.largeSchroder = n.largeSchroder
⊢ 2 * (n + 1).smallSchroder = n.largeSchroder

Tactic:
rw [smallSchroder_succ_eq_largeSchroder_div_two hn,
    Nat.mul_div_cancel_left' (even_largeSchroder hn).two_dvd]

Premises used: Nat.smallSchroder_succ_eq_largeSchroder_div_two, Nat.mul_div_cancel_left', Nat.even_largeSchroder, Even.two_dvd
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
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)
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)
⊢ (n + 1).smallSchroder =
    3 * n.smallSchroder + HMul.hMul (α := ℕ) 2 (∑ i ∈ Ioo 0 (n - 1), (i + 1).smallSchroder * (n - i).smallSchroder)

Tactic:
obtain _ | _ | n := n
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
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:
simp at hn
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
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:
simp at hn
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
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)

Tactic:
Nat.mul_left_cancel zero_lt_two ?_

Premises used: Nat.mul_left_cancel, zero_lt_two
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
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))
⊢ (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:
refine Nat.mul_left_cancel zero_lt_two ?_

Premises used: Nat.mul_left_cancel, zero_lt_two
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
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
rw₃ : n + 2 ≠ 0
⊢ 2 * (n + 3).smallSchroder =
    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]

Premises used: Nat.two_mul_smallSchroder_succ, Nat.largeSchroder_succ, Finset.sum_Ioc_add_eq_sum_Icc, Finset.sum_Ioo_add_eq_sum_Ioc, Finset.Icc_bot
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
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
⊢ (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:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ < n + 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ ≤ n + 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ (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:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
h :
  ∀ (i : ℕ) (hi : i ∈ Ioo 0 (n + 1)),
    i.largeSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).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), 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

Tactic:
congr! 2 with i hi
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : i ∈ Ioo 0 (n + 1)
⊢ 0 < i ∧ i ≤ n

Tactic:
simp at hi
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
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
h₂ : i ≠ 0
⊢ i.largeSchroder * (n + 1 - i).largeSchroder = 2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

Tactic:
rw [← two_mul_smallSchroder_succ, ← two_mul_smallSchroder_succ]

Premises used: Nat.two_mul_smallSchroder_succ
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ 2 * (i + 1).smallSchroder * (2 * (n + 1 - i + 1).smallSchroder) =
    2 * (i + 1).smallSchroder * (2 * (n + 2 - i).smallSchroder)

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ n + 1 - i ≠ 0

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
i : ℕ
hi : 0 < i ∧ i ≤ n
⊢ i ≠ 0

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 1 ≠ 0

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
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)
⊢ 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:
rw [← two_mul_smallSchroder_succ (by lia)]

Premises used: Nat.two_mul_smallSchroder_succ
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
simp : 3 * (2 * (n + 1 + 1).smallSchroder) = 6 * (n + 2).smallSchroder
⊢ 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:
simp [mul_mul_mul_comm _ _ 2, ← Finset.mul_sum]

Premises used: Finset.mul_sum, mul_mul_mul_comm, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ 3 * (2 * (n + 1 + 1).smallSchroder) = 6 * (n + 2).smallSchroder

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
hn : 1 < n + 1 + 1
⊢ 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:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
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)
_₃ :
  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))
⊢ 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:
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

Premises used: Nat.largeSchroder, HAdd.hAdd, OfNat.ofNat, Finset.Ioo, Nat.smallSchroder
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
⊢ stirlingFirst 0 0 = 1

Tactic:
rfl

Premises used: Nat.stirlingFirst, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
k : ℕ
⊢ stirlingFirst 0 k.succ = 0

Tactic:
rfl

Premises used: Nat.stirlingFirst, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
⊢ n.succ.stirlingFirst 0 = 0

Tactic:
rfl

Premises used: Nat.stirlingFirst, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n k : ℕ
hk : k ≠ 0
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)
⊢ (n + 1).stirlingFirst k = n * n.stirlingFirst k + n.stirlingFirst (k - 1)

Tactic:
obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.pos_of_ne_zero hk)

Premises used: Nat.pos_of_ne_zero, Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n 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:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n k : ℕ
hn : n ≠ 0
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
⊢ n.stirlingFirst (k + 1) = (n - 1) * (n - 1).stirlingFirst (k + 1) + (n - 1).stirlingFirst k

Tactic:
obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.pos_of_ne_zero hn)

Premises used: Nat.pos_of_ne_zero, Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
k 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:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n k : ℕ
⊢ (n + 1).stirlingFirst (k + 1) = n * n.stirlingFirst (k + 1) + n.stirlingFirst k

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
h : 0 < n + 1
rw rw₁ : Eq (α := ℕ) 0 0
⊢ stirlingFirst 0 (n + 1) = 0

Tactic:
rw [stirlingFirst]

Premises used: Nat.stirlingFirst
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
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
rw₃ rw₄ : HAdd.hAdd (α := ℕ) 0 0 = 0
⊢ (n + 1).stirlingFirst (k + 1) = 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]

Premises used: MulZeroClass.mul_zero, Nat.stirlingFirst_succ_succ, Nat.lt_of_succ_lt, Nat.lt_of_succ_lt_succ
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
zero : stirlingFirst 0 0 = 1
succ : ∀ (n : ℕ), n.stirlingFirst n = 1 → (n + 1).stirlingFirst (n + 1) = 1
⊢ n.stirlingFirst n = 1

Tactic:
induction n
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
⊢ stirlingFirst 0 0 = 1

Tactic:
simp only [*, stirlingFirst, stirlingFirst_eq_zero_of_lt (Nat.lt_succ_self _),
    mul_zero]

Premises used: Nat.stirlingFirst_eq_zero_of_lt, Nat.lt_succ_self, Nat.stirlingFirst, MulZeroClass.mul_zero
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
h : n.stirlingFirst n = 1
⊢ (n + 1).stirlingFirst (n + 1) = 1

Tactic:
simp only [*, stirlingFirst, stirlingFirst_eq_zero_of_lt (Nat.lt_succ_self _),
    mul_zero]

Premises used: Nat.stirlingFirst_eq_zero_of_lt, Nat.lt_succ_self, Nat.stirlingFirst, MulZeroClass.mul_zero
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
⊢ (HAdd.hAdd (α := ℕ) 0 1).stirlingFirst 0 = (HAdd.hAdd (α := ℕ) 0 1).choose 2

Tactic:
simp only [zero_add, stirlingFirst_succ_zero, choose_succ_self]

Premises used: zero_add, Nat.stirlingFirst_succ_zero, Nat.choose_succ_self
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
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
succ₄ : n + 1 + (n + 1).choose 2 = (n + 1).choose 1 + (n + 1).choose (Nat.succ 1)
succ₅ succ₆ : n + 1 + (n + 1).choose 2 = n + 1 + (n + 1).choose (Nat.succ 1)
⊢ (n + 1 + 1).stirlingFirst (n + 1) = (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]

Premises used: Nat.choose_succ_succ, Nat.choose_one_right, HAdd.hAdd, Nat.stirlingFirst_succ_succ, mul_one, OfNat.ofNat, Nat.stirlingFirst_self
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingFirst 0 = (HAdd.hAdd (α := ℕ) 0 1).choose 2
succ :
  ∀ (n : ℕ) (ih : (n + 1).stirlingFirst n = (n + 1).choose 2), (n + 1 + 1).stirlingFirst (n + 1) = (n + 1 + 1).choose 2
⊢ (n + 1).stirlingFirst n = (n + 1).choose 2

Tactic:
induction n with
  | zero => simp only [zero_add, stirlingFirst_succ_zero, choose_succ_self]
  | succ n ih =>
    rw [stirlingFirst_succ_succ, ih, stirlingFirst_self, mul_one, Nat.choose_succ_succ (n + 1),
      Nat.choose_one_right]

Premises used: Nat.choose_succ_succ, zero_add, Nat.choose_one_right, HAdd.hAdd, Nat.stirlingFirst_succ_succ, Nat.zero, Nat.stirlingFirst_succ_zero, mul_one, OfNat.ofNat, Nat.choose_succ_self, Nat.succ, Nat.stirlingFirst_self
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
⊢ (HAdd.hAdd (α := ℕ) 0 1).stirlingFirst 1 = 0!

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
hn : (n + 1).stirlingFirst 1 = n !
succ : (n + 1) * n ! + 0 = (n + 1)!
⊢ (n + 1 + 1).stirlingFirst 1 = (n + 1)!

Tactic:
rw [stirlingFirst_succ_succ, zero_add, hn, stirlingFirst_succ_zero]

Premises used: zero_add, Nat.stirlingFirst_succ_succ, Nat.stirlingFirst_succ_zero
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
hn : (n + 1).stirlingFirst 1 = n !
⊢ (n + 1) * n ! + 0 = (n + 1)!

Tactic:
simp [Nat.factorial_succ]

Premises used: Nat.factorial_succ
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingFirst 1 = 0!
succ : ∀ (n : ℕ) (hn : (n + 1).stirlingFirst 1 = n !), (n + 1 + 1).stirlingFirst 1 = (n + 1)!
⊢ (n + 1).stirlingFirst 1 = n !

Tactic:
induction n with
  | zero => rfl
  | succ n hn =>
    rw [stirlingFirst_succ_succ, zero_add, hn, stirlingFirst_succ_zero]
    simp [Nat.factorial_succ]

Premises used: Nat.factorial_succ, zero_add, Nat.stirlingFirst_succ_succ, Nat.zero, Nat.stirlingFirst_succ_zero, Nat.succ
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
⊢ stirlingSecond 0 0 = 1

Tactic:
rfl

Premises used: Nat.stirlingSecond, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
k : ℕ
⊢ stirlingSecond 0 k.succ = 0

Tactic:
rfl

Premises used: Nat.stirlingSecond, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
⊢ n.succ.stirlingSecond 0 = 0

Tactic:
rfl

Premises used: Nat.stirlingSecond, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n k : ℕ
hk : k ≠ 0
obtain :
  ∀ (l : ℕ) (hk : l + succ 0 ≠ 0),
    (n + 1).stirlingSecond (l + succ 0) =
      (l + succ 0) * n.stirlingSecond (l + succ 0) + n.stirlingSecond (l + succ 0 - 1)
⊢ (n + 1).stirlingSecond k = k * n.stirlingSecond k + n.stirlingSecond (k - 1)

Tactic:
obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.pos_of_ne_zero hk)

Premises used: Nat.pos_of_ne_zero, Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n l : ℕ
hk : l + succ 0 ≠ 0
⊢ (n + 1).stirlingSecond (l + succ 0) = (l + succ 0) * n.stirlingSecond (l + succ 0) + n.stirlingSecond (l + succ 0 - 1)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n k : ℕ
hn : n ≠ 0
obtain :
  ∀ (l : ℕ) (hn : l + succ 0 ≠ 0),
    (l + succ 0).stirlingSecond (k + 1) =
      (k + 1) * (l + succ 0 - 1).stirlingSecond (k + 1) + (l + succ 0 - 1).stirlingSecond k
⊢ n.stirlingSecond (k + 1) = (k + 1) * (n - 1).stirlingSecond (k + 1) + (n - 1).stirlingSecond k

Tactic:
obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.pos_of_ne_zero hn)

Premises used: Nat.pos_of_ne_zero, Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
k l : ℕ
hn : l + succ 0 ≠ 0
⊢ (l + succ 0).stirlingSecond (k + 1) =
    (k + 1) * (l + succ 0 - 1).stirlingSecond (k + 1) + (l + succ 0 - 1).stirlingSecond k

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n k : ℕ
⊢ (n + 1).stirlingSecond (k + 1) = (k + 1) * n.stirlingSecond (k + 1) + n.stirlingSecond k

Tactic:
rfl

Premises used: Nat.stirlingSecond, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
h : 0 < n + 1
rw rw₁ : Eq (α := ℕ) 0 0
⊢ stirlingSecond 0 (n + 1) = 0

Tactic:
rw [stirlingSecond]

Premises used: Nat.stirlingSecond
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n k : ℕ
hk : n + 1 < k + 1
⊢ (n + 1).stirlingSecond (k + 1) = 0

Tactic:
simp only [stirlingSecond_succ_succ, stirlingSecond_eq_zero_of_lt (Nat.lt_of_succ_lt_succ hk),
      stirlingSecond_eq_zero_of_lt (Nat.lt_of_succ_lt hk), mul_zero]

Premises used: MulZeroClass.mul_zero, Nat.lt_of_succ_lt, Nat.stirlingSecond_succ_succ, Nat.lt_of_succ_lt_succ
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
zero : stirlingSecond 0 0 = 1
succ : ∀ (n : ℕ), n.stirlingSecond n = 1 → (n + 1).stirlingSecond (n + 1) = 1
⊢ n.stirlingSecond n = 1

Tactic:
induction n
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
⊢ stirlingSecond 0 0 = 1

Tactic:
simp only [*, stirlingSecond, stirlingSecond_eq_zero_of_lt (lt_succ_self _),
    mul_zero]

Premises used: Nat.lt_succ_self, MulZeroClass.mul_zero, Nat.stirlingSecond_eq_zero_of_lt, Nat.stirlingSecond
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
h : n.stirlingSecond n = 1
⊢ (n + 1).stirlingSecond (n + 1) = 1

Tactic:
simp only [*, stirlingSecond, stirlingSecond_eq_zero_of_lt (lt_succ_self _),
    mul_zero]

Premises used: Nat.lt_succ_self, MulZeroClass.mul_zero, Nat.stirlingSecond_eq_zero_of_lt, Nat.stirlingSecond
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
⊢ (HAdd.hAdd (α := ℕ) 0 1).stirlingSecond 1 = 1

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
ih : (n + 1).stirlingSecond 1 = 1
succ : HAdd.hAdd (α := ℕ) 0 1 * (n + 1).stirlingSecond (HAdd.hAdd (α := ℕ) 0 1) + (n + 1).stirlingSecond 0 = 1
succ₁ : HAdd.hAdd (α := ℕ) 0 1 * (n + 1).stirlingSecond (HAdd.hAdd (α := ℕ) 0 1) + 0 = 1
succ₂ succ₃ : HAdd.hAdd (α := ℕ) 0 1 * 1 + 0 = 1
⊢ (n + 1 + 1).stirlingSecond 1 = 1

Tactic:
rw [stirlingSecond, stirlingSecond_succ_zero, ih]

Premises used: Nat.stirlingSecond_succ_zero, Nat.stirlingSecond
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
zero : (HAdd.hAdd (α := ℕ) 0 1).stirlingSecond 1 = 1
succ : ∀ (n : ℕ) (ih : (n + 1).stirlingSecond 1 = 1), (n + 1 + 1).stirlingSecond 1 = 1
⊢ (n + 1).stirlingSecond 1 = 1

Tactic:
induction n with
  | zero => rfl
  | succ n ih => rw [stirlingSecond, stirlingSecond_succ_zero, ih]

Premises used: Nat.stirlingSecond_succ_zero, Nat.zero, Nat.succ, Nat.stirlingSecond
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
⊢ (HAdd.hAdd (α := ℕ) 0 1).stirlingSecond 0 = (HAdd.hAdd (α := ℕ) 0 1).choose 2

Tactic:
simp only [zero_add, stirlingSecond_succ_zero, choose_succ_self]

Premises used: zero_add, Nat.stirlingSecond_succ_zero, Nat.choose_succ_self
-- Module: Mathlib.Combinatorics.Enumerative.Stirling
Goal:
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
succ : (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).stirlingSecond n = (n + 1 + 1).choose 2
succ₁ : (n + 1) * (n + 1).stirlingSecond (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
succ₄ : n + 1 + (n + 1).choose 2 = (n + 1).choose 1 + (n + 1).choose (Nat.succ 1)
succ₅ succ₆ : n + 1 + (n + 1).choose 2 = n + 1 + (n + 1).choose (Nat.succ 1)
⊢ (n + 1 + 1).stirlingSecond (n + 1) = (n + 1 + 1).choose 2

Tactic:
rw [stirlingSecond_succ_succ, ih, stirlingSecond_self, mul_one,
      Nat.choose_succ_succ (n + 1), Nat.choose_one_right]

Premises used: Nat.choose_succ_succ, Nat.choose_one_right, HAdd.hAdd, mul_one, Nat.stirlingSecond_self, OfNat.ofNat, Nat.stirlingSecond_succ_succ