awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ 0 < HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)
have hn : LT.lt (α := ℕ) 0 (prod (map (fun (j : ℕ) ↦ j !) m))
Tactic: apply Nat.mul_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
hn : LT.lt (α := ℕ) 0 (prod (map (fun (j : ℕ) ↦ j !) m))
⊢ 0 < HMul.hMul (α := ℕ) (prod (map (fun (j : ℕ) ↦ j !) m)) (∏ j ∈ m.toFinset.erase 0, (count j m)!)
have hm : LT.lt (α := ℕ) 0 (∏ j ∈ m.toFinset.erase 0, (count j m)!)
Tactic: apply Nat.mul_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ LT.lt (α := ℕ) 0 (prod (map (fun (j : ℕ) ↦ j !) m))
have hn : ∀ a ∈ m, 0 < a !
Tactic: simp only [CanonicallyOrderedAdd.multiset_prod_pos, mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m : Multiset ℕ
⊢ LT.lt (α := ℕ) 0 (∏ j ∈ m.toFinset.erase 0, (count j m)!)
have hm : ∀ i ∈ m.toFinset.erase 0, 0 < (count i m)!
Tactic: apply Finset.prod_pos
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
⊢ (multinomial (replicate m n).toFinset fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ k ∈ (replicate m n).toFinset.erase 0,
        ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
have rw : (multinomial (if m = 0 then ∅ else {n}) fun (k : ℕ) ↦ k * count k (replicate m n)) *
    ∏ k ∈ Finset.erase (if m = 0 then ∅ else {n}) 0,
      ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
  ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Tactic: rw [toFinset_replicate]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
⊢ (multinomial (if m = 0 then ∅ else {n}) fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ k ∈ Finset.erase (if m = 0 then ∅ else {n}) 0,
        ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
have pos : ∀ (hm : m = 0),
  (multinomial ∅ fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ x ∈ Finset.erase ∅ 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
pos :
  ∀ (hm : m = 0),
    (multinomial ∅ fun (k : ℕ) ↦ k * count k (replicate m n)) *
        ∏ x ∈ Finset.erase ∅ 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
      ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
⊢ (multinomial (if m = 0 then ∅ else {n}) fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ k ∈ Finset.erase (if m = 0 then ∅ else {n}) 0,
        ∏ j ∈ Finset.range (count k (replicate m n)), (j * k + k - 1).choose (k - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
have neg : ∀ (hm : ¬m = 0),
  (multinomial {n} fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ x ∈ Finset.erase {n} 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hm : ¬m = 0
⊢ (multinomial {n} fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ x ∈ Finset.erase {n} 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
have pos : ∀ (hn : n = 0),
  (multinomial {n} fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ x ∈ Finset.erase {n} 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hm : ¬m = 0
pos :
  ∀ (hn : n = 0),
    (multinomial {n} fun (k : ℕ) ↦ k * count k (replicate m n)) *
        ∏ x ∈ Finset.erase {n} 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
      ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
⊢ (multinomial {n} fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ x ∈ Finset.erase {n} 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
have neg : ∀ (hn : ¬n = 0),
  (multinomial {n} fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ x ∈ Finset.erase {n} 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun (k : ℕ) ↦ k * count k (replicate m n)) *
      ∏ x ∈ Finset.erase {n} 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
have neg : (multinomial {n} fun (k : ℕ) ↦ k * count k (replicate m n)) *
    ∏ x ∈ {n}, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
  ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Tactic: rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
⊢ m.uniformBell n * n ! ^ m * m ! = (m * n)!
have h : n ! ^ m = prod (map (fun (j : ℕ) ↦ j !) (replicate m n))
Tactic: convert! bell_mul_eq (replicate m n)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
h : n ! ^ m = prod (map (fun (j : ℕ) ↦ j !) (replicate m n))
⊢ m.uniformBell n * n ! ^ m * m ! = (m * n)!
have h₁ : m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!
Tactic: convert! bell_mul_eq (replicate m n)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
h : n ! ^ m = prod (map (fun (j : ℕ) ↦ j !) (replicate m n))
h₁ : m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!
⊢ m.uniformBell n * n ! ^ m * m ! = (m * n)!
have h₂ : m * n = (replicate m n).sum
Tactic: convert! bell_mul_eq (replicate m n)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!
have h : m ! = ∏ x ∈ Finset.erase (if m = 0 then ∅ else {n}) 0, (count x (replicate m n))!
Tactic: simp only [toFinset_replicate]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
⊢ m ! = ∏ x ∈ Finset.erase (if m = 0 then ∅ else {n}) 0, (count x (replicate m n))!
have pos : ∀ (hm : m = 0), m ! = ∏ x ∈ Finset.erase ∅ 0, (count x (replicate m n))!
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
pos : ∀ (hm : m = 0), m ! = ∏ x ∈ Finset.erase ∅ 0, (count x (replicate m n))!
⊢ m ! = ∏ x ∈ Finset.erase (if m = 0 then ∅ else {n}) 0, (count x (replicate m n))!
have neg : ∀ (hm : ¬m = 0), m ! = ∏ x ∈ Finset.erase {n} 0, (count x (replicate m n))!
Tactic: split_ifs with hm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ m ! = ∏ x ∈ Finset.erase ∅ 0, (count x (replicate m n))!
have pos : Eq (α := ℕ) (∏ x ∈ Finset.erase ∅ 0, (count x (replicate 0 n))!) 1
Tactic: rw [hm, factorial_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hm : m = 0
⊢ Eq (α := ℕ) (∏ x ∈ Finset.erase ∅ 0, (count x (replicate 0 n))!) 1
have pos : Eq (α := ℕ) (∏ x ∈ ∅, (count x (replicate 0 n))!) 1
Tactic: rw [show (∅ : Finset ℕ).erase 0 = ∅ from rfl, Finset.prod_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hm : m = 0
pos : Eq (α := ℕ) (∏ x ∈ ∅, (count x (replicate 0 n))!) 1
⊢ Eq (α := ℕ) (∏ x ∈ Finset.erase ∅ 0, (count x (replicate 0 n))!) 1
have pos₁ : Eq (α := ℕ) 1 1
Tactic: rw [show (∅ : Finset ℕ).erase 0 = ∅ from rfl, Finset.prod_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ m ! = ∏ x ∈ Finset.erase {n} 0, (count x (replicate m n))!
have neg : m ! = ∏ x ∈ {n}, (count x (replicate m n))!
Tactic: rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
⊢ m.uniformBell n = (m * n)! / (n ! ^ m * m !)
have rw : (m * n)! / (n ! ^ m * m !) = m.uniformBell n
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! / (n ! ^ m * m !) = m.uniformBell n
have H1 : 0 < n ! ^ m * m !
Tactic: apply Nat.div_eq_of_eq_mul_left
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
H1 : 0 < n ! ^ m * m !
⊢ (m * n)! / (n ! ^ m * m !) = m.uniformBell n
have H2 : (m * n)! = m.uniformBell n * (n ! ^ m * m !)
Tactic: apply Nat.div_eq_of_eq_mul_left
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
⊢ (m * n)! = m.uniformBell n * (n ! ^ m * m !)
have H2 : (m * n)! = m.uniformBell n * n ! ^ m * m !
Tactic: rw [← mul_assoc, ← uniformBell_mul_eq _ hn]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
m n : ℕ
hn : n ≠ 0
H2 : (m * n)! = m.uniformBell n * n ! ^ m * m !
⊢ (m * n)! = m.uniformBell n * (n ! ^ m * m !)
have H2₁ : m.uniformBell n * n ! ^ m * m ! = m.uniformBell n * n ! ^ m * m !
Tactic: rw [← mul_assoc, ← uniformBell_mul_eq _ hn]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
n : ℕ
⊢ (n + 1).bell = ∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell
have rw : Eq (α := ℕ) (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
  (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
Tactic: rw [Nat.bell]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
n : ℕ
⊢ (n + 1).bell = ∑ ij ∈ @Finset.antidiagonal _ instAddMonoid _ n, n.choose ij.1 * ij.2.bell
have rw : Eq (α := ℕ) (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
  (∑ ij ∈ @Finset.antidiagonal _ instAddMonoid _ n, n.choose ij.1 * ij.2.bell)
Tactic: rw [Nat.bell_succ,
    Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => Nat.choose n x * Nat.bell y) n,
    Finset.sum_range]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
n : ℕ
rw :
  Eq (α := ℕ) (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
    (∑ ij ∈ @Finset.antidiagonal _ instAddMonoid _ n, n.choose ij.1 * ij.2.bell)
⊢ (n + 1).bell = ∑ ij ∈ @Finset.antidiagonal _ instAddMonoid _ n, n.choose ij.1 * ij.2.bell
have rw₁ : Eq (α := ℕ) (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
  (∑ k ∈ Finset.range n.succ, n.choose k * (n - k).bell)
Tactic: rw [Nat.bell_succ,
    Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => Nat.choose n x * Nat.bell y) n,
    Finset.sum_range]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Bell (goal)
Goal:
n : ℕ
rw :
  Eq (α := ℕ) (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
    (∑ ij ∈ @Finset.antidiagonal _ instAddMonoid _ n, n.choose ij.1 * ij.2.bell)
rw₁ :
  Eq (α := ℕ) (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
    (∑ k ∈ Finset.range n.succ, n.choose k * (n - k).bell)
⊢ (n + 1).bell = ∑ ij ∈ @Finset.antidiagonal _ instAddMonoid _ n, n.choose ij.1 * ij.2.bell
have rw₂ : Eq (α := ℕ) (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
  (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
Tactic: rw [Nat.bell_succ,
    Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => Nat.choose n x * Nat.bell y) n,
    Finset.sum_range]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
⊢ catalan 0 = 1
have rw : Eq (α := ℕ) 1 1
Tactic: rw [catalan]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n : ℕ
⊢ catalan (n + 1) = ∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ))
have rw : Eq (α := ℕ) (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
  (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
Tactic: rw [catalan]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n : ℕ
⊢ catalan (n + 1) = ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan ij.1 * catalan ij.2
have rw : Eq (α := ℕ) (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
  (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan ij.1 * catalan ij.2)
Tactic: rw [catalan_succ, Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => catalan x * catalan y) n,
    sum_range]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n : ℕ
rw :
  Eq (α := ℕ) (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan ij.1 * catalan ij.2)
⊢ catalan (n + 1) = ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan ij.1 * catalan ij.2
have rw₁ : Eq (α := ℕ) (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
  (∑ k ∈ range n.succ, catalan k * catalan (n - k))
Tactic: rw [catalan_succ, Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => catalan x * catalan y) n,
    sum_range]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n : ℕ
rw :
  Eq (α := ℕ) (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan ij.1 * catalan ij.2)
rw₁ :
  Eq (α := ℕ) (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
    (∑ k ∈ range n.succ, catalan k * catalan (n - k))
⊢ catalan (n + 1) = ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan ij.1 * catalan ij.2
have rw₂ : Eq (α := ℕ) (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
  (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
Tactic: rw [catalan_succ, Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => catalan x * catalan y) n,
    sum_range]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n i : ℕ
h : i ≤ n
⊢ HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
have norm_cast : ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (hypothesis)
Goal:
n i : ℕ
h : i ≤ n
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    (↑i.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(n - i).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
have l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
Tactic: have l₁ : (i : ℚ) + 1 ≠ 0 := by norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
⊢ HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0
have norm_cast : ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (hypothesis)
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    (↑i.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(n - i).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
have l₂ : HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0
Tactic: have l₂ : (n : ℚ) - i + 1 ≠ 0 := by norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (hypothesis)
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
l₂ : HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    (↑i.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(n - i).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
have h₁ : (↑(i + 1).centralBinom : ℚ) =
  HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1
Tactic: have h₁ := (mul_div_cancel_left₀ (↑(Nat.centralBinom (i + 1))) l₁).symm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (hypothesis)
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
l₂ : HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0
h₁ :
  (↑(i + 1).centralBinom : ℚ) =
    HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    (↑i.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(n - i).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
have h₂ : (↑(n - i + 1).centralBinom : ℚ) =
  (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) /
    (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
Tactic: have h₂ := (mul_div_cancel_left₀ (↑(Nat.centralBinom (n - i + 1))) l₂).symm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (hypothesis)
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
l₂ : HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0
h₁ :
  (↑(i + 1).centralBinom : ℚ) =
    HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1
h₂ :
  (↑(n - i + 1).centralBinom : ℚ) =
    (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    (↑i.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(n - i).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
have h₃ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) =
  2 * (HMul.hMul (α := ℚ) 2 (↑i : ℚ) + 1) * (↑i.centralBinom : ℚ)
Tactic: have h₃ : ((i : ℚ) + 1) * (i + 1).centralBinom = 2 * (2 * i + 1) * i.centralBinom :=
    mod_cast Nat.succ_mul_centralBinom_succ i
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (hypothesis)
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
l₂ : HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0
h₁ :
  (↑(i + 1).centralBinom : ℚ) =
    HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1
h₂ :
  (↑(n - i + 1).centralBinom : ℚ) =
    (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
h₃ :
  HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) =
    2 * (HMul.hMul (α := ℚ) 2 (↑i : ℚ) + 1) * (↑i.centralBinom : ℚ)
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    (↑i.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(n - i).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
have h₄ : (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) =
  2 * (2 * HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i).centralBinom : ℚ)
Tactic: have h₄ :
    ((n : ℚ) - i + 1) * (n - i + 1).centralBinom = 2 * (2 * (n - i) + 1) * (n - i).centralBinom :=
      mod_cast Nat.succ_mul_centralBinom_succ (n - i)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
l₂ : HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0
h₁ :
  (↑(i + 1).centralBinom : ℚ) =
    HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1
h₂ :
  (↑(n - i + 1).centralBinom : ℚ) =
    (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
h₃ :
  HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) =
    2 * (HMul.hMul (α := ℚ) 2 (↑i : ℚ) + 1) * (↑i.centralBinom : ℚ)
h₄ :
  (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) =
    2 * (2 * HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i).centralBinom : ℚ)
⊢ HMul.hMul (α := ℚ) (↑(i + 1).centralBinom : ℚ) (↑(n + 1 - (i + 1)).centralBinom : ℚ) *
          (HMul.hMul (α := ℚ) 2 (↑(i + 1) : ℚ) - (↑(n + 1) : ℚ)) /
        (HMul.hMul (α := ℚ) 2 (↑(n + 1) : ℚ) * HAdd.hAdd (α := ℚ) (↑(n + 1) : ℚ) 1) -
      HMul.hMul (α := ℚ) (↑i.centralBinom : ℚ) (↑(n + 1 - i).centralBinom : ℚ) *
          (HMul.hMul (α := ℚ) 2 (↑i : ℚ) - (↑(n + 1) : ℚ)) /
        (HMul.hMul (α := ℚ) 2 (↑(n + 1) : ℚ) * HAdd.hAdd (α := ℚ) (↑(n + 1) : ℚ) 1) =
    (↑i.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(n - i).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
have push_cast : HMul.hMul (α := ℚ) (↑(i + 1).centralBinom : ℚ) (↑(n - i).centralBinom : ℚ) *
        (2 * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 - HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) /
      (2 * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1)) -
    HMul.hMul (α := ℚ) (↑i.centralBinom : ℚ) (↑(n + 1 - i).centralBinom : ℚ) *
        (HMul.hMul (α := ℚ) 2 (↑i : ℚ) - HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) /
      (2 * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1)) =
  (↑i.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(n - i).centralBinom : ℚ) /
    (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
l₂ : HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0
h₁ :
  (↑(i + 1).centralBinom : ℚ) =
    HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1
h₂ :
  (↑(n - i + 1).centralBinom : ℚ) =
    (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
h₃ :
  HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) =
    2 * (HMul.hMul (α := ℚ) 2 (↑i : ℚ) + 1) * (↑i.centralBinom : ℚ)
h₄ :
  (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) =
    2 * (2 * HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i).centralBinom : ℚ)
⊢ n + 1 - i = n - i + 1
have rw : n + 1 - i = 1 + (n - i)
Tactic: rw [Nat.add_comm (n - i) 1, ← (Nat.add_sub_assoc h 1),
    add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
l₂ : HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0
h₁ :
  (↑(i + 1).centralBinom : ℚ) =
    HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1
h₂ :
  (↑(n - i + 1).centralBinom : ℚ) =
    (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
h₃ :
  HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) =
    2 * (HMul.hMul (α := ℚ) 2 (↑i : ℚ) + 1) * (↑i.centralBinom : ℚ)
h₄ :
  (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) =
    2 * (2 * HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i).centralBinom : ℚ)
rw : n + 1 - i = 1 + (n - i)
⊢ n + 1 - i = n - i + 1
have rw₁ : n + 1 - i = 1 + n - i
Tactic: rw [Nat.add_comm (n - i) 1, ← (Nat.add_sub_assoc h 1),
    add_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
l₂ : HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0
h₁ :
  (↑(i + 1).centralBinom : ℚ) =
    HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1
h₂ :
  (↑(n - i + 1).centralBinom : ℚ) =
    (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)
h₃ :
  HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 * (↑(i + 1).centralBinom : ℚ) =
    2 * (HMul.hMul (α := ℚ) 2 (↑i : ℚ) + 1) * (↑i.centralBinom : ℚ)
h₄ :
  (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i + 1).centralBinom : ℚ) =
    2 * (2 * HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i).centralBinom : ℚ)
rw : n + 1 - i = 1 + (n - i)
rw₁ : n + 1 - i = 1 + n - i
⊢ n + 1 - i = n - i + 1
have rw₂ : 1 + n - i = 1 + n - i
Tactic: rw [Nat.add_comm (n - i) 1, ← (Nat.add_sub_assoc h 1),
    add_comm]