awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n : ℕ
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
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = (↑(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]

Premises used: neg_add_rev, tsub_self, MulZeroClass.mul_zero, Nat.cast_add, Nat.centralBinom_zero, Nat.sub_zero, Nat.cast_zero, _private.0.gosperCatalan, mul_one, Nat.cast_one, one_mul, zero_sub
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n : ℕ
⊢ (↑(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:
field
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n : ℕ
this : (↑(catalan n) : ℚ) = (↑n.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
⊢ n + 1 ∣ n.centralBinom

Tactic:
have h := Nat.succ_dvd_centralBinom n
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n : ℕ
this : (↑(catalan n) : ℚ) = (↑n.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
h : n + 1 ∣ n.centralBinom
⊢ catalan n = n.centralBinom / (n + 1)

Tactic:
mod_cast this

Premises used: Int.cast, Int.cast_natCast, catalan, Int.cast_div_ofNat_charZero._simp_1, congrArg, Nat.cast_add._simp_1, cast, HDiv.hDiv, Nat.centralBinom, Nat.cast, Int.cast_inj._simp_1, HAdd.hAdd, Nat.cast_inj._simp_1, OfNat.ofNat, Eq.symm, Eq, Nat.cast_one, Eq.trans
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n : ℕ
this : (↑(catalan n) : ℚ) = (↑n.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
h : n + 1 ∣ n.centralBinom
⊢ catalan n = n.centralBinom / (n + 1)

Tactic:
exact mod_cast this
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n : ℕ
suffices : (↑(catalan n) : ℚ) = (↑n.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑n : ℚ) 1
⊢ catalan n = n.centralBinom / (n + 1)

Tactic:
suffices (catalan n : ℚ) = Nat.centralBinom n / (n + 1) by
    have h := Nat.succ_dvd_centralBinom n
    exact mod_cast this
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
⊢ (↑(catalan 0) : ℚ) = (↑(Nat.centralBinom 0) : ℚ) / HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
ind :
  ∑ x : Fin d.succ, HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ) =
    (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
⊢ (↑(catalan d.succ) : ℚ) = (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1

Tactic:
simp_rw [catalan_succ, Nat.cast_sum, Nat.cast_mul]

Premises used: Nat.cast_sum, Nat.cast_mul, catalan_succ
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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)))
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
⊢ ∑ x : Fin d.succ, HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ) =
    (↑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)) : ℚ)

Premises used: HMul.hMul, Finset.univ, HSub.hSub, HDiv.hDiv, Nat.centralBinom, Fin.val, Nat.cast, HAdd.hAdd, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
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))
⊢ 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:
congr
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
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))
⊢ 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:
ext1 x
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
x : Fin d.succ
⊢ (↑x : ℕ) ≤ d

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
x : Fin d.succ
⊢ (↑x : ℕ) ≤ d

Tactic:
have m_le_d : x.val ≤ d := by lia
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
x : Fin d.succ
m_le_d : (↑x : ℕ) ≤ d
⊢ d - (↑x : ℕ) ≤ d

Tactic:
have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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
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))
⊢ HMul.hMul (α := ℚ) (↑(catalan (↑x : ℕ)) : ℚ) (↑(catalan (d - (↑x : ℕ))) : ℚ) =
    (↑(↑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]
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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
e_f e_f₁ e_f₂ 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) : ℚ)
⊢ (↑(↑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:
norm_cast
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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 : ℕ)))
trans₁ :
  ∑ i : Fin d.succ, (gosperCatalan (d + 1) ((↑i : ℕ) + 1) - gosperCatalan (d + 1) (↑i : ℕ)) =
    (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 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

Tactic:
trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))

Premises used: Finset.univ, HSub.hSub, Fin.val, HAdd.hAdd, _private.0.gosperCatalan, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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 : ℕ)))

Tactic:
sum_congr rfl fun i _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
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 : ℕ)
⊢ 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:
refine sum_congr rfl fun i _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
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)
rw₁ 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 : ℕ)

Tactic:
rw [gosper_trick i.is_le, mul_div]

Premises used: mul_div, Fin.is_le, _private.0.gosper_trick
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
rw :
  gosperCatalan (d + 1) (d + 1) - gosperCatalan (d + 1) 0 =
    (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(d + 1) : ℚ) 1
⊢ ∑ i : Fin d.succ, (gosperCatalan (d + 1) ((↑i : ℕ) + 1) - gosperCatalan (d + 1) (↑i : ℕ)) =
    (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1

Tactic:
rw [← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i,
            sum_range_sub, Nat.succ_eq_add_one]

Premises used: Nat.succ_eq_add_one, HSub.hSub, Finset.sum_range, HAdd.hAdd, _private.0.gosperCatalan, OfNat.ofNat, Finset.sum_range_sub
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
rw :
  (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d : ℚ) 2 =
    (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(d + 1) : ℚ) 1
⊢ gosperCatalan (d + 1) (d + 1) - gosperCatalan (d + 1) 0 =
    (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(d + 1) : ℚ) 1

Tactic:
rw [gosper_catalan_sub_eq_central_binom_div d]

Premises used: _private.0.gosper_catalan_sub_eq_central_binom_div
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
d : ℕ
hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  HDiv.hDiv (α := ℚ) (↑(d + 1).centralBinom : ℚ) (↑(d + 2) : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(d + 1).centralBinom : ℚ) (↑(d + 1 + 1) : ℚ)
⊢ (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d : ℚ) 2 =
    (↑(d + 1).centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑(d + 1) : ℚ) 1

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n : ℕ
zero : (↑(catalan 0) : ℚ) = (↑(Nat.centralBinom 0) : ℚ) / HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1
ind :
  ∀ (d : ℕ) (hd : ∀ m ≤ d, (↑(catalan m) : ℚ) = (↑m.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑m : ℚ) 1),
    (↑(catalan d.succ) : ℚ) = (↑d.succ.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑d.succ : ℚ) 1
⊢ (↑(catalan n) : ℚ) = (↑n.centralBinom : ℚ) / HAdd.hAdd (α := ℚ) (↑n : ℚ) 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

Premises used: mul_div, Nat.succ_eq_add_one, Nat.cast_sum, Nat.cast_mul, catalan_succ, Finset.sum_congr, rfl, Finset.sum_range_sub
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
n : ℕ
⊢ (n + 1) * catalan n = n.centralBinom

Tactic:
(Nat.eq_mul_of_div_eq_right n.succ_dvd_centralBinom (catalan_eq_centralBinom_div n).symm).symm

Premises used: Nat.succ_dvd_centralBinom, Nat.eq_mul_of_div_eq_right, Eq.symm, catalan_eq_centralBinom_div
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
⊢ catalan 2 = 2

Tactic:
norm_num [catalan_eq_centralBinom_div, Nat.centralBinom, Nat.choose]

Premises used: Nat.choose, Nat.centralBinom, catalan_eq_centralBinom_div
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic
Goal:
⊢ catalan 3 = 5

Tactic:
norm_num [catalan_eq_centralBinom_div, Nat.centralBinom, Nat.choose]

Premises used: Nat.choose, Nat.centralBinom, catalan_eq_centralBinom_div
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
a b : Finset (Tree Unit)
x x_1 : Tree Unit × Tree Unit
x₁ x₂ y₁ y₂ : Tree Unit
h :
  Eq (α := Tree Unit) ((fun (x : Tree Unit × Tree Unit) ↦ node () x.1 x.2) (x₁, x₂))
    ((fun (x : Tree Unit × Tree Unit) ↦ node () x.1 x.2) (y₁, y₂))
⊢ (x₁, x₂) = (y₁, y₂)

Tactic:
simpa using h
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
ijh : ↥(@antidiagonal _ Nat.instAddMonoid _ n)
⊢ (↑ijh : ℕ × ℕ).1 ≤ n

Tactic:
have := fst_le ijh.2
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
ijh : ↥(@antidiagonal _ Nat.instAddMonoid _ n)
this : (↑ijh : ℕ × ℕ).1 ≤ n
⊢ (↑ijh : ℕ × ℕ).1 < n + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
ijh : ↥(@antidiagonal _ Nat.instAddMonoid _ n)
⊢ (↑ijh : ℕ × ℕ).2 ≤ n

Tactic:
have := snd_le ijh.2
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
ijh : ↥(@antidiagonal _ Nat.instAddMonoid _ n)
this : (↑ijh : ℕ × ℕ).2 ≤ n
⊢ (↑ijh : ℕ × ℕ).2 < n + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
rw rw₁ : Eq (α := Finset (Tree Unit)) {nil} {nil}
⊢ treesOfNumNodesEq 0 = {nil}

Tactic:
rw [treesOfNumNodesEq]

Premises used: Tree.treesOfNumNodesEq
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
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))
⊢ treesOfNumNodesEq (n + 1) =
    (@antidiagonal _ Nat.instAddMonoid _ n).biUnion fun (ij : ℕ × ℕ) ↦
      pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)

Tactic:
rw [treesOfNumNodesEq]

Premises used: Tree.treesOfNumNodesEq
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
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
⊢ 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:
ext
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
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:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
x : Tree Unit
n : ℕ
base : ∀ {n : ℕ}, nil ∈ treesOfNumNodesEq n ↔ numNodes (α := Unit) nil = n
ind :
  ∀ (x y : Tree Unit),
    (∀ {n : ℕ}, x ∈ treesOfNumNodesEq n ↔ x.numNodes = n) →
      (∀ {n : ℕ}, y ∈ treesOfNumNodesEq n ↔ y.numNodes = n) →
        ∀ {n : ℕ}, node () x y ∈ treesOfNumNodesEq n ↔ (node () x y).numNodes = n
⊢ x ∈ treesOfNumNodesEq n ↔ x.numNodes = n

Tactic:
induction x using Tree.unitRecOn generalizing n
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
base : nil ∈ treesOfNumNodesEq 0 ↔ numNodes (α := Unit) nil = 0
base₁ : ∀ (n : ℕ), nil ∈ treesOfNumNodesEq (n + 1) ↔ numNodes (α := Unit) nil = n + 1
⊢ nil ∈ treesOfNumNodesEq n ↔ numNodes (α := Unit) nil = n

Tactic:
cases n
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
x y : Tree Unit
h : ∀ {n : ℕ}, x ∈ treesOfNumNodesEq n ↔ x.numNodes = n
h_1 : ∀ {n : ℕ}, y ∈ treesOfNumNodesEq n ↔ y.numNodes = n
n : ℕ
ind : node () x y ∈ treesOfNumNodesEq 0 ↔ (node () x y).numNodes = 0
ind₁ : ∀ (n : ℕ), node () x y ∈ treesOfNumNodesEq (n + 1) ↔ (node () x y).numNodes = n + 1
⊢ node () x y ∈ treesOfNumNodesEq n ↔ (node () x y).numNodes = n

Tactic:
cases n
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
⊢ nil ∈ treesOfNumNodesEq 0 ↔ numNodes (α := Unit) nil = 0

Tactic:
simp [treesOfNumNodesEq_succ, *]

Premises used: Tree.treesOfNumNodesEq_succ
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
⊢ nil ∈ treesOfNumNodesEq (n + 1) ↔ numNodes (α := Unit) nil = n + 1

Tactic:
simp [treesOfNumNodesEq_succ, *]

Premises used: Tree.treesOfNumNodesEq_succ
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
x y : Tree Unit
h : ∀ {n : ℕ}, x ∈ treesOfNumNodesEq n ↔ x.numNodes = n
h_1 : ∀ {n : ℕ}, y ∈ treesOfNumNodesEq n ↔ y.numNodes = n
⊢ node () x y ∈ treesOfNumNodesEq 0 ↔ (node () x y).numNodes = 0

Tactic:
simp [treesOfNumNodesEq_succ, *]

Premises used: Tree.treesOfNumNodesEq_succ
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
x y : Tree Unit
h : ∀ {n : ℕ}, x ∈ treesOfNumNodesEq n ↔ x.numNodes = n
h_1 : ∀ {n : ℕ}, y ∈ treesOfNumNodesEq n ↔ y.numNodes = n
n : ℕ
⊢ node () x y ∈ treesOfNumNodesEq (n + 1) ↔ (node () x y).numNodes = n + 1

Tactic:
simp [treesOfNumNodesEq_succ, *]

Premises used: Tree.treesOfNumNodesEq_succ
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
x : Tree Unit
⊢ x ∈ treesOfNumNodesEq x.numNodes

Tactic:
mem_treesOfNumNodesEq.mpr rfl

Premises used: Iff.mpr, Tree.mem_treesOfNumNodesEq, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
⊢ ∀ (x : Tree Unit),
    x ∈ (↑(treesOfNumNodesEq n) : Set (Tree Unit)) ↔
      Membership.mem (γ := Set (Tree Unit)) {x : Tree Unit | x.numNodes = n} x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
⊢ #(treesOfNumNodesEq 0) = catalan 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
hi :
  Eq (α := ℕ)
    (∑ u ∈ @antidiagonal _ Nat.instAddMonoid _ n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)))
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan ij.1 * catalan ij.2)
hi₁ :
  (↑(@antidiagonal _ Nat.instAddMonoid _ n) : Set (ℕ × ℕ)).PairwiseDisjoint (α := Finset (Tree Unit)) fun (ij : ℕ × ℕ) ↦
    pairwiseNode (treesOfNumNodesEq ij.1) (treesOfNumNodesEq ij.2)
⊢ #(treesOfNumNodesEq (n + 1)) = catalan (n + 1)

Tactic:
rw [treesOfNumNodesEq_succ, card_biUnion, catalan_succ']

Premises used: Tree.treesOfNumNodesEq_succ, Finset.card_biUnion, catalan_succ'
-- Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree
Goal:
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
hi :
  ∀ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    #(pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2)) = catalan x.1 * catalan x.2
⊢ Eq (α := ℕ)
    (∑ u ∈ @antidiagonal _ Nat.instAddMonoid _ n, #(pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)))
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, catalan ij.1 * catalan ij.2)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl