-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem catalan_eq_centralBinom_div (n : ℕ) : catalan n = n.centralBinom / (n + 1)

Proof state:
case zero

⊢ ↑(catalan 0) = ↑(Nat.centralBinom 0) / (↑0 + 1)

Tactic:
simp

Result:
no goals

Proof state:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i : Fin d.succ, (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i) = ↑d.succ.centralBinom / (↑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]

Result:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ gosperCatalan (d + 1) (d + 1) - gosperCatalan (d + 1) 0 = ↑(d + 1).centralBinom / (↑(d + 1) + 1)

Proof state:
case e_f
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ (fun x => ↑(catalan ↑x) * ↑(catalan (d - ↑x))) = fun i =>
    ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1))

Tactic:
ext1 x

Result:
case e_f.h
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 1))

Proof state:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ gosperCatalan (d + 1) (d + 1) - gosperCatalan (d + 1) 0 = ↑(d + 1).centralBinom / (↑(d + 1) + 1)

Tactic:
rw [gosper_catalan_sub_eq_central_binom_div d]

Result:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ↑(d + 1).centralBinom / (↑d + 2) = ↑(d + 1).centralBinom / (↑(d + 1) + 1)

Proof state:
n : ℕ
⊢ 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

Result:
n : ℕ
⊢ ↑(catalan n) = ↑n.centralBinom / (↑n + 1)

Proof state:
case e_f.h
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
m_le_d : ↑x ≤ d
d_minus_x_le_d : d - ↑x ≤ d
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 1))

Tactic:
rw [hd _ m_le_d, hd _ d_minus_x_le_d]

Result:
case e_f.h
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
m_le_d : ↑x ≤ d
d_minus_x_le_d : d - ↑x ≤ d
⊢ ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑(d - ↑x) + 1)) =
    ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 1))

Proof state:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i : Fin d.succ, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) =
    ∑ i : Fin d.succ, (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i)

Tactic:
refine sum_congr rfl fun i _ => ?_

Result:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
i : Fin d.succ
x✝ : i ∈ univ
⊢ ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) =
    gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i

Proof state:
case e_f.h
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
m_le_d : ↑x ≤ d
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 1))

Tactic:
have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self

Result:
case e_f.h
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
m_le_d : ↑x ≤ d
d_minus_x_le_d : d - ↑x ≤ d
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 1))

Proof state:
n : ℕ
this : ↑(catalan n) = ↑n.centralBinom / (↑n + 1)
h : n + 1 ∣ n.centralBinom
⊢ catalan n = n.centralBinom / (n + 1)

Tactic:
exact mod_cast this

Result:
no goals

Proof state:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ x : Fin d.succ, ↑(catalan ↑x) * ↑(catalan (d - ↑x)) =
    ∑ i : Fin d.succ, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1))

Tactic:
congr

Result:
case e_f
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ (fun x => ↑(catalan ↑x) * ↑(catalan (d - ↑x))) = fun i =>
    ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1))

Proof state:
case e_f.h
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
m_le_d : ↑x ≤ d
d_minus_x_le_d : d - ↑x ≤ d
⊢ ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑(d - ↑x) + 1)) =
    ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 1))

Tactic:
norm_cast

Result:
no goals

Proof state:
case ind
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ x : Fin d.succ, ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑d.succ.centralBinom / (↑d.succ + 1)

Tactic:
trans (∑ i : Fin d.succ, Nat.centralBinom i / (i + 1) *
                        (Nat.centralBinom (d - i) / (d - i + 1)) : ℚ)

Result:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ x : Fin d.succ, ↑(catalan ↑x) * ↑(catalan (d - ↑x)) =
    ∑ i : Fin d.succ, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1))

d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i : Fin d.succ, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) =
    ↑d.succ.centralBinom / (↑d.succ + 1)

Proof state:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
i : Fin d.succ
x✝ : i ∈ univ
⊢ ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) =
    gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i

Tactic:
rw [gosper_trick i.is_le, mul_div]

Result:
no goals

Proof state:
case e_f.h
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 1))

Tactic:
have m_le_d : x.val ≤ d := by omega

Result:
case e_f.h
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
m_le_d : ↑x ≤ d
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑(↑x).centralBinom / (↑↑x + 1) * (↑(d - ↑x).centralBinom / (↑d - ↑↑x + 1))

Proof state:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
x : Fin d.succ
⊢ ↑x ≤ d

Tactic:
omega

Result:
no goals

Proof state:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ↑(d + 1).centralBinom / (↑d + 2) = ↑(d + 1).centralBinom / (↑(d + 1) + 1)

Tactic:
norm_cast

Result:
no goals

Proof state:
n : ℕ
this : ↑(catalan n) = ↑n.centralBinom / (↑n + 1)
⊢ catalan n = n.centralBinom / (n + 1)

Tactic:
have h := Nat.succ_dvd_centralBinom n

Result:
n : ℕ
this : ↑(catalan n) = ↑n.centralBinom / (↑n + 1)
h : n + 1 ∣ n.centralBinom
⊢ catalan n = n.centralBinom / (n + 1)

Proof state:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i : Fin d.succ, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) =
    ↑d.succ.centralBinom / (↑d.succ + 1)

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

Result:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i : Fin d.succ, ↑(↑i).centralBinom / (↑↑i + 1) * (↑(d - ↑i).centralBinom / (↑d - ↑↑i + 1)) =
    ∑ i : Fin d.succ, (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i)

d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ i : Fin d.succ, (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i) = ↑d.succ.centralBinom / (↑d.succ + 1)

Proof state:
case ind
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ↑(catalan d.succ) = ↑d.succ.centralBinom / (↑d.succ + 1)

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

Result:
case ind
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ∑ x : Fin d.succ, ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑d.succ.centralBinom / (↑d.succ + 1)