awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
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:
simp [hm]
-- Module: Mathlib.Combinatorics.Enumerative.Bell
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)
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)
⊢ (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
-- Module: Mathlib.Combinatorics.Enumerative.Bell
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)

Tactic:
simp [hn]
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ Eq (α := Finset ℕ) (Finset.erase {n} 0) {n}

Tactic:
simp [Ne.symm hn]

Premises used: Ne.symm
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
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)
⊢ (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:
rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (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:
simp [count_replicate]

Premises used: Multiset.count_replicate
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
n : ℕ
⊢ uniformBell 0 n = 1

Tactic:
simp [uniformBell_eq]

Premises used: Nat.uniformBell_eq
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : ℕ
⊢ m.uniformBell 0 = 1

Tactic:
simp [uniformBell_eq]

Premises used: Nat.uniformBell_eq
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
⊢ (m + 1).uniformBell n = (m * n + n - 1).choose (n - 1) * m.uniformBell n

Tactic:
simp only [uniformBell_eq, Finset.prod_range_succ, mul_comm]

Premises used: Nat.uniformBell_eq, mul_comm, Finset.prod_range_succ
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
n : ℕ
⊢ uniformBell 1 n = 1

Tactic:
simp only [uniformBell_eq, Finset.range_one, Finset.prod_singleton, zero_mul,
    zero_add, choose_self]

Premises used: Finset.prod_singleton, MulZeroClass.zero_mul, zero_add, Nat.uniformBell_eq, Finset.range_one, Nat.choose_self
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m : ℕ
⊢ m.uniformBell 1 = 1

Tactic:
simp only [uniformBell_eq, mul_one, add_tsub_cancel_right, le_refl,
    tsub_eq_zero_of_le, choose_zero_right, Finset.prod_const_one]

Premises used: le_refl, tsub_eq_zero_of_le, Nat.uniformBell_eq, Finset.prod_const_one, add_tsub_cancel_right, mul_one, Nat.choose_zero_right
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
⊢ (replicate m n).bell * prod (map (fun (j : ℕ) ↦ j !) (replicate m n)) *
      ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))! =
    (replicate m n).sum !

Tactic:
bell_mul_eq (replicate m n)

Premises used: Multiset.bell_mul_eq, Multiset.replicate
-- Module: Mathlib.Combinatorics.Enumerative.Bell
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))!
h₂ : m * n = (replicate m n).sum
⊢ m.uniformBell n * n ! ^ m * m ! = (m * n)!

Tactic:
convert! bell_mul_eq (replicate m n)

Premises used: Multiset.bell_mul_eq, Multiset.replicate
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
⊢ n ! ^ m = prod (map (fun (j : ℕ) ↦ j !) (replicate m n))

Tactic:
simp only [map_replicate, prod_replicate]

Premises used: Multiset.prod_replicate, Multiset.map_replicate
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
h : m ! = ∏ x ∈ Finset.erase (if m = 0 then ∅ else {n}) 0, (count x (replicate m n))!
⊢ m ! = ∏ j ∈ (replicate m n).toFinset.erase 0, (count j (replicate m n))!

Tactic:
simp only [toFinset_replicate]

Premises used: Multiset.toFinset_replicate
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
pos : ∀ (hm : m = 0), m ! = ∏ x ∈ Finset.erase ∅ 0, (count x (replicate m n))!
neg : ∀ (hm : ¬m = 0), m ! = ∏ x ∈ Finset.erase {n} 0, (count x (replicate m n))!
⊢ m ! = ∏ x ∈ Finset.erase (if m = 0 then ∅ else {n}) 0, (count x (replicate m n))!

Tactic:
split_ifs with hm
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
hm : m = 0
pos : Eq (α := ℕ) (∏ x ∈ Finset.erase ∅ 0, (count x (replicate 0 n))!) 1
⊢ m ! = ∏ x ∈ Finset.erase ∅ 0, (count x (replicate m n))!

Tactic:
rw [hm, factorial_zero, eq_comm]

Premises used: eq_comm, Nat.factorial_zero
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
hm : m = 0
pos : Eq (α := ℕ) (∏ x ∈ ∅, (count x (replicate 0 n))!) 1
pos₁ pos₂ : Eq (α := ℕ) 1 1
⊢ Eq (α := ℕ) (∏ x ∈ Finset.erase ∅ 0, (count x (replicate 0 n))!) 1

Tactic:
rw [show (∅ : Finset ℕ).erase 0 = ∅ from rfl, Finset.prod_empty]

Premises used: Finset.prod_empty, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ Eq (α := Finset ℕ) (Finset.erase {n} 0) {n}

Tactic:
simp [Ne.symm hn]

Premises used: Ne.symm
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
neg : m ! = ∏ x ∈ {n}, (count x (replicate m n))!
⊢ m ! = ∏ x ∈ Finset.erase {n} 0, (count x (replicate m n))!

Tactic:
rw [show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]]
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ m ! = ∏ x ∈ {n}, (count x (replicate m n))!

Tactic:
simp only [Finset.prod_singleton, count_replicate_self]

Premises used: Finset.prod_singleton, Multiset.count_replicate_self
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
⊢ m * n = (replicate m n).sum

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
rw : (m * n)! / (n ! ^ m * m !) = m.uniformBell n
⊢ m.uniformBell n = (m * n)! / (n ! ^ m * m !)

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
H1 : 0 < n ! ^ m * m !
H2 : (m * n)! = m.uniformBell n * (n ! ^ m * m !)
⊢ (m * n)! / (n ! ^ m * m !) = m.uniformBell n

Tactic:
apply Nat.div_eq_of_eq_mul_left

Premises used: Nat.div_eq_of_eq_mul_left
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
⊢ 0 < n ! ^ m * m !

Tactic:
Nat.mul_pos (Nat.pow_pos (Nat.factorial_pos n)) m.factorial_pos

Premises used: Nat.mul_pos, Nat.pow_pos, Nat.factorial_pos
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
⊢ 0 < n ! ^ m * m !

Tactic:
exact Nat.mul_pos (Nat.pow_pos (Nat.factorial_pos n)) m.factorial_pos

Premises used: Nat.mul_pos, Nat.pow_pos, Nat.factorial_pos
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
m n : ℕ
hn : n ≠ 0
H2 : (m * n)! = m.uniformBell n * n ! ^ m * m !
H2₁ H2₂ : m.uniformBell n * n ! ^ m * m ! = m.uniformBell n * n ! ^ m * m !
⊢ (m * n)! = m.uniformBell n * (n ! ^ m * m !)

Tactic:
rw [← mul_assoc, ← uniformBell_mul_eq _ hn]

Premises used: Nat.uniformBell_mul_eq, mul_assoc
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
n : ℕ
rw rw₁ :
  Eq (α := ℕ) (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
    (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
⊢ (n + 1).bell = ∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell

Tactic:
rw [Nat.bell]

Premises used: Nat.bell
-- Module: Mathlib.Combinatorics.Enumerative.Bell
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)
rw₂ rw₃ :
  Eq (α := ℕ) (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
    (∑ i : Fin n.succ, n.choose (↑i : ℕ) * (n - (↑i : ℕ)).bell)
⊢ (n + 1).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]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, Nat.choose, HMul.hMul, Nat.bell_succ, Finset.sum_range, Nat.bell
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
⊢ Nat.bell 0 = 1

Tactic:
simp [Nat.bell]

Premises used: Nat.bell
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
⊢ Nat.bell 1 = 1

Tactic:
simp [Nat.bell]

Premises used: Nat.bell
-- Module: Mathlib.Combinatorics.Enumerative.Bell
Goal:
⊢ Nat.bell 2 = 2

Tactic:
simp [Nat.bell]

Premises used: Nat.bell
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
rw rw₁ : Eq (α := ℕ) 1 1
⊢ catalan 0 = 1

Tactic:
rw [catalan]

Premises used: catalan
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n : ℕ
rw rw₁ :
  Eq (α := ℕ) (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
    (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
⊢ catalan (n + 1) = ∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ))

Tactic:
rw [catalan]

Premises used: catalan
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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))
rw₂ rw₃ :
  Eq (α := ℕ) (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
    (∑ i : Fin n.succ, catalan (↑i : ℕ) * catalan (n - (↑i : ℕ)))
⊢ catalan (n + 1) = ∑ 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]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, catalan, HMul.hMul, Finset.sum_range, catalan_succ
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
⊢ catalan 1 = 1

Tactic:
simp [catalan_succ]

Premises used: catalan_succ
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n i : ℕ
h : i ≤ n
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬False
⊢ HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n i : ℕ
h : i ≤ n
⊢ HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0

Tactic:
have l₁ : (i : ℚ) + 1 ≠ 0 := by norm_cast
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬False
⊢ HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
⊢ HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0

Tactic:
have l₂ : (n : ℚ) - i + 1 ≠ 0 := by norm_cast
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n i : ℕ
h : i ≤ n
l₁ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
l₂ : HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1 ≠ 0
⊢ (↑(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
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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
⊢ (↑(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
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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)
⊢ 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
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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 : ℚ)
⊢ (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)
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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 : ℚ)
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)
⊢ 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)

Tactic:
push_cast
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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
rw₂ rw₃ : 1 + n - i = 1 + n - i
⊢ n + 1 - i = n - i + 1

Tactic:
rw [Nat.add_comm (n - i) 1, ← (Nat.add_sub_assoc h 1),
    add_comm]

Premises used: Nat.add_sub_assoc, HSub.hSub, add_comm, OfNat.ofNat, Nat.add_comm
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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 :
  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 - i + 1).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)
⊢ 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:
rw [show n + 1 - i = n - i + 1 by rw [Nat.add_comm (n - i) 1, ← (Nat.add_sub_assoc h 1),
    add_comm]]
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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 :
  2 * (HMul.hMul (α := ℚ) 2 (↑i : ℚ) + 1) * (↑i.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 *
            (↑(n - i).centralBinom : ℚ) *
          (2 * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 - HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) /
        (2 * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1)) -
      (↑i.centralBinom : ℚ) *
            (2 * (2 * HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i).centralBinom : ℚ) /
              (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)) *
          (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)
⊢ 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 - i + 1).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:
rw [h₁, h₂, h₃, h₄]
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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 : ℚ)
⊢ 2 * (HMul.hMul (α := ℚ) 2 (↑i : ℚ) + 1) * (↑i.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 *
            (↑(n - i).centralBinom : ℚ) *
          (2 * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 - HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) /
        (2 * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1)) -
      (↑i.centralBinom : ℚ) *
            (2 * (2 * HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1) * (↑(n - i).centralBinom : ℚ) /
              (HSub.hSub (α := ℚ) (↑n : ℚ) (↑i : ℚ) + 1)) *
          (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:
field