awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 - 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)
have 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)
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]]
-- 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 - 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)
have 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)
Tactic: rw [h₁, h₂, h₃, h₄]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n : ℕ
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = (↑(n + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑n : ℚ) 2
have simp : (↑(n + 1).centralBinom : ℚ) * (2 * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 - HAdd.hAdd (α := ℚ) (↑n : ℚ) 1) /
      (2 * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1)) -
    (↑(n + 1).centralBinom : ℚ) * HAdd.hAdd (α := ℚ) (-1) (-(↑n : ℚ)) /
      (2 * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1)) =
  (↑(n + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑n : ℚ) 2
Tactic: simp only [gosperCatalan, tsub_self, Nat.centralBinom_zero, Nat.cast_one, mul_one, Nat.cast_add,
    Nat.sub_zero, one_mul, Nat.cast_zero, mul_zero, zero_sub, neg_add_rev]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (hypothesis)
Goal:
n : ℕ
this : (↑(catalan n) : ℚ) = (↑n.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
⊢ catalan n = n.centralBinom / (n + 1)
have h : n + 1 ∣ n.centralBinom
Tactic: have h := Nat.succ_dvd_centralBinom n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n : ℕ
⊢ catalan n = n.centralBinom / (n + 1)
have suffices : (↑(catalan n) : ℚ) = (↑n.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
Tactic: suffices (catalan n : ℚ) = Nat.centralBinom n / (n + 1) by
    have h := Nat.succ_dvd_centralBinom n
    exact mod_cast this
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
⊢ (↑(catalan d.succ) : ℚ) = (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
have ind : ∑ x : Fin d.succ, HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ) =
  (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
Tactic: simp_rw [catalan_succ, Nat.cast_sum, Nat.cast_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
⊢ ∑ x : Fin d.succ, HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ) =
    (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
have trans : Eq (α := ℚ) (∑ x : Fin d.succ, HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ))
  (∑ i : Fin d.succ,
    (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
      ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)))
Tactic: trans (∑ i : Fin d.succ, Nat.centralBinom i / (i + 1) *
                            (Nat.centralBinom (d - i) / (d - i + 1)) : ℚ)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
trans :
  Eq (α := ℚ) (∑ x : Fin d.succ, HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ))
    (∑ i : Fin d.succ,
      (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
        ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)))
⊢ ∑ x : Fin d.succ, HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ) =
    (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
have trans₁ : ∑ i : Fin d.succ,
    (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
      ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)) =
  (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
Tactic: trans (∑ i : Fin d.succ, Nat.centralBinom i / (i + 1) *
                            (Nat.centralBinom (d - i) / (d - i + 1)) : ℚ)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
⊢ Eq (α := ℚ) (∑ x : Fin d.succ, HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ))
    (∑ i : Fin d.succ,
      (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
        ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)))
have e_f : Eq (α := Fin d.succ → ℚ)
  (fun (x : Fin d.succ) ↦ HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ))
  fun (i : Fin d.succ) ↦
  (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
    ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1))
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
⊢ Eq (α := Fin d.succ → ℚ)
    (fun (x : Fin d.succ) ↦ HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ))
    fun (i : Fin d.succ) ↦
    (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
      ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1))
have e_f : ∀ (x : Fin d.succ),
  HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ) =
    (↑(↑x : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑x : ℕ) : ℚ) 1 *
      ((↑(d - (↑x : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑x : ℕ) : ℚ) + 1))
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (hypothesis)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
x : Fin d.succ
⊢ HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ) =
    (↑(↑x : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑x : ℕ) : ℚ) 1 *
      ((↑(d - (↑x : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑x : ℕ) : ℚ) + 1))
have m_le_d : (↑x : ℕ) ≤ d
Tactic: have m_le_d : x.val ≤ d := by lia
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (hypothesis)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
x : Fin d.succ
m_le_d : (↑x : ℕ) ≤ d
⊢ HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ) =
    (↑(↑x : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑x : ℕ) : ℚ) 1 *
      ((↑(d - (↑x : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑x : ℕ) : ℚ) + 1))
have d_minus_x_le_d : d - (↑x : ℕ) ≤ d
Tactic: have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
x : Fin d.succ
m_le_d : (↑x : ℕ) ≤ d
d_minus_x_le_d : d - (↑x : ℕ) ≤ d
⊢ HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ) =
    (↑(↑x : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑x : ℕ) : ℚ) 1 *
      ((↑(d - (↑x : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑x : ℕ) : ℚ) + 1))
have e_f : (↑(↑x : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑x : ℕ) : ℚ) 1 *
    ((↑(d - (↑x : ℕ)).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(d - (↑x : ℕ)) : ℚ) 1) =
  (↑(↑x : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑x : ℕ) : ℚ) 1 *
    ((↑(d - (↑x : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑x : ℕ) : ℚ) + 1))
Tactic: rw [hd _ m_le_d, hd _ d_minus_x_le_d]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
x : Fin d.succ
m_le_d : (↑x : ℕ) ≤ d
d_minus_x_le_d : d - (↑x : ℕ) ≤ d
⊢ (↑(↑x : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑x : ℕ) : ℚ) 1 *
      ((↑(d - (↑x : ℕ)).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(d - (↑x : ℕ)) : ℚ) 1) =
    (↑(↑x : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑x : ℕ) : ℚ) 1 *
      ((↑(d - (↑x : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑x : ℕ) : ℚ) + 1))
have e_f : HDiv.hDiv (α := ℚ) (↑(↑x : ℕ).centralBinom : ℚ) (↑((↑x : ℕ) + 1) : ℚ) *
    HDiv.hDiv (α := ℚ) (↑(d - (↑x : ℕ)).centralBinom : ℚ) (↑(d - (↑x : ℕ) + 1) : ℚ) =
  HDiv.hDiv (α := ℚ) (↑(↑x : ℕ).centralBinom : ℚ) (↑((↑x : ℕ) + 1) : ℚ) *
    HDiv.hDiv (α := ℚ) (↑(d - (↑x : ℕ)).centralBinom : ℚ) (↑(d - (↑x : ℕ) + 1) : ℚ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
⊢ ∑ i : Fin d.succ,
      (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
        ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)) =
    (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
have trans : Eq (α := ℚ)
  (∑ i : Fin d.succ,
    (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
      ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)))
  (∑ i : Fin d.succ, (gosperCatalan (d + 1) ((↑i : ℕ) + 1) - gosperCatalan (d + 1) (↑i : ℕ)))
Tactic: trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
trans :
  Eq (α := ℚ)
    (∑ i : Fin d.succ,
      (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
        ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)))
    (∑ i : Fin d.succ, (gosperCatalan (d + 1) ((↑i : ℕ) + 1) - gosperCatalan (d + 1) (↑i : ℕ)))
⊢ ∑ i : Fin d.succ,
      (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
        ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)) =
    (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
have trans₁ : ∑ i : Fin d.succ, (gosperCatalan (d + 1) ((↑i : ℕ) + 1) - gosperCatalan (d + 1) (↑i : ℕ)) =
  (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
Tactic: trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
⊢ Eq (α := ℚ)
    (∑ i : Fin d.succ,
      (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
        ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)))
    (∑ i : Fin d.succ, (gosperCatalan (d + 1) ((↑i : ℕ) + 1) - gosperCatalan (d + 1) (↑i : ℕ)))
have refine : ∀ (i : Fin d.succ),
  Membership.mem (γ := Finset (Fin d.succ)) univ i →
    (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
        ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)) =
      gosperCatalan (d + 1) ((↑i : ℕ) + 1) - gosperCatalan (d + 1) (↑i : ℕ)
Tactic: refine sum_congr rfl fun i _ => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
i : Fin d.succ
h : Membership.mem (γ := Finset (Fin d.succ)) univ i
⊢ (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
      ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)) =
    gosperCatalan (d + 1) ((↑i : ℕ) + 1) - gosperCatalan (d + 1) (↑i : ℕ)
have rw : (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
    ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)) =
  (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 * (↑(d - (↑i : ℕ)).centralBinom : ℚ) /
    (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)
Tactic: rw [gosper_trick i.is_le, mul_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
i : Fin d.succ
h : Membership.mem (γ := Finset (Fin d.succ)) univ i
rw :
  (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
      ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)) =
    (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 * (↑(d - (↑i : ℕ)).centralBinom : ℚ) /
      (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)
⊢ (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 *
      ((↑(d - (↑i : ℕ)).centralBinom : ℚ) / (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)) =
    gosperCatalan (d + 1) ((↑i : ℕ) + 1) - gosperCatalan (d + 1) (↑i : ℕ)
have rw₁ : (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 * (↑(d - (↑i : ℕ)).centralBinom : ℚ) /
    (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1) =
  (↑(↑i : ℕ).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(↑i : ℕ) : ℚ) 1 * (↑(d - (↑i : ℕ)).centralBinom : ℚ) /
    (HSub.hSub (α := ℚ) (↑d : ℚ) (↑(↑i : ℕ) : ℚ) + 1)
Tactic: rw [gosper_trick i.is_le, mul_div]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
⊢ ∑ i : Fin d.succ, (gosperCatalan (d + 1) ((↑i : ℕ) + 1) - gosperCatalan (d + 1) (↑i : ℕ)) =
    (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
have rw : gosperCatalan (d + 1) (d + 1) - gosperCatalan (d + 1) 0 =
  (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(d + 1) : ℚ) 1
Tactic: rw [← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i,
            sum_range_sub, Nat.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
⊢ gosperCatalan (d + 1) (d + 1) - gosperCatalan (d + 1) 0 =
    (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(d + 1) : ℚ) 1
have rw : (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d : ℚ) 2 =
  (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(d + 1) : ℚ) 1
Tactic: rw [gosper_catalan_sub_eq_central_binom_div d]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
⊢ (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d : ℚ) 2 =
    (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(d + 1) : ℚ) 1
have norm_cast : HDiv.hDiv (α := ℚ) (↑(d + 1).centralBinom : ℚ) (↑(d + 2) : ℚ) =
  HDiv.hDiv (α := ℚ) (↑(d + 1).centralBinom : ℚ) (↑(d + 1 + 1) : ℚ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n : ℕ
⊢ (↑(catalan n) : ℚ) = (↑n.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
have zero : (↑(catalan 0) : ℚ) = (↑(Nat.centralBinom 0) : ℚ) / HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1
Tactic: induction n using Nat.caseStrongRecOn with
  | zero => simp
  | ind d hd =>
    simp_rw [catalan_succ, Nat.cast_sum, Nat.cast_mul]
    trans (∑ i : Fin d.succ, Nat.centralBinom i / (i + 1) *
                            (Nat.centralBinom (d - i) / (d - i + 1)) : ℚ)
    · congr
      ext1 x
      have m_le_d : x.val ≤ d := by lia
      have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self
      rw [hd _ m_le_d, hd _ d_minus_x_le_d]
      norm_cast
    · trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))
      · refine sum_congr rfl fun i _ => ?_
        rw [gosper_trick i.is_le, mul_div]
      · rw [← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i,
            sum_range_sub, Nat.succ_eq_add_one]
        rw [gosper_catalan_sub_eq_central_binom_div d]
        norm_cast
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Basic (goal)
Goal:
n : ℕ
zero : (↑(catalan 0) : ℚ) = (↑(Nat.centralBinom 0) : ℚ) / HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1
⊢ (↑(catalan n) : ℚ) = (↑n.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
have ind : ∀ (d : ℕ) (hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1),
  (↑(catalan d.succ) : ℚ) = (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
Tactic: induction n using Nat.caseStrongRecOn with
  | zero => simp
  | ind d hd =>
    simp_rw [catalan_succ, Nat.cast_sum, Nat.cast_mul]
    trans (∑ i : Fin d.succ, Nat.centralBinom i / (i + 1) *
                            (Nat.centralBinom (d - i) / (d - i + 1)) : ℚ)
    · congr
      ext1 x
      have m_le_d : x.val ≤ d := by lia
      have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self
      rw [hd _ m_le_d, hd _ d_minus_x_le_d]
      norm_cast
    · trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))
      · refine sum_congr rfl fun i _ => ?_
        rw [gosper_trick i.is_le, mul_div]
      · rw [← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i,
            sum_range_sub, Nat.succ_eq_add_one]
        rw [gosper_catalan_sub_eq_central_binom_div d]
        norm_cast
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (hypothesis)
Goal:
n : ℕ
ijh : ↥(@antidiagonal _ Nat.instAddMonoid _ n)
⊢ (↑ijh : ℕ × ℕ).1 < n + 1
have this : (↑ijh : ℕ × ℕ).1 ≤ n
Tactic: have := fst_le ijh.2
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (hypothesis)
Goal:
n : ℕ
ijh : ↥(@antidiagonal _ Nat.instAddMonoid _ n)
⊢ (↑ijh : ℕ × ℕ).2 < n + 1
have this : (↑ijh : ℕ × ℕ).2 ≤ n
Tactic: have := snd_le ijh.2
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
⊢ treesOfNumNodesEq 0 = {nil}
have rw : Eq (α := Finset (Tree Unit)) {nil} {nil}
Tactic: rw [treesOfNumNodesEq]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
n : ℕ
⊢ treesOfNumNodesEq (n + 1) =
    (@antidiagonal _ Nat.instAddMonoid _ n).biUnion fun (ij : ℕ × ℕ) ↦
      pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
have rw : Eq (α := Finset (Tree Unit))
  ((@antidiagonal _ Nat.instAddMonoid _ n).attach.biUnion fun (ijh : ↥(@antidiagonal _ Nat.instAddMonoid _ n)) ↦
    pairwiseNode (treesOfNumNodesEq (↑ijh : ℕ × ℕ).1) (treesOfNumNodesEq (↑ijh : ℕ × ℕ).2))
  ((@antidiagonal _ Nat.instAddMonoid _ n).biUnion fun (ij : ℕ × ℕ) ↦
    pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2))
Tactic: rw [treesOfNumNodesEq]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
n : ℕ
⊢ Eq (α := Finset (Tree Unit))
    ((@antidiagonal _ Nat.instAddMonoid _ n).attach.biUnion fun (ijh : ↥(@antidiagonal _ Nat.instAddMonoid _ n)) ↦
      pairwiseNode (treesOfNumNodesEq (↑ijh : ℕ × ℕ).1) (treesOfNumNodesEq (↑ijh : ℕ × ℕ).2))
    ((@antidiagonal _ Nat.instAddMonoid _ n).biUnion fun (ij : ℕ × ℕ) ↦
      pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2))
have h : ∀ (a : Tree Unit),
  Membership.mem (γ := Finset (Tree Unit))
      ((@antidiagonal _ Nat.instAddMonoid _ n).attach.biUnion fun (ijh : ↥(@antidiagonal _ Nat.instAddMonoid _ n)) ↦
        pairwiseNode (treesOfNumNodesEq (↑ijh : ℕ × ℕ).1) (treesOfNumNodesEq (↑ijh : ℕ × ℕ).2))
      a ↔
    Membership.mem (γ := Finset (Tree Unit))
      ((@antidiagonal _ Nat.instAddMonoid _ n).biUnion fun (ij : ℕ × ℕ) ↦
        pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2))
      a
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Catalan.Tree (goal)
Goal:
x : Tree Unit
n : ℕ
⊢ x ∈ treesOfNumNodesEq n ↔ x.numNodes = n
have base : ∀ {n : ℕ}, nil ∈ treesOfNumNodesEq n ↔ numNodes (α := Unit) nil = n
Tactic: induction x using Tree.unitRecOn generalizing n
Cleared hypotheses: x, n