n : ℕ
⊢ ↑(catalan n) = ↑(Nat.centralBinom n) / (↑n + 1)
n : ℕ
⊢ catalan n = Nat.centralBinom n / (n + 1)
suffices (catalan n : ℚ) = Nat.centralBinom n / (n + 1) by
  have h := Nat.succ_dvd_centralBinom n
  exact_mod_cast this
case hz

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

case hi
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ↑(catalan (Nat.succ d)) = ↑(Nat.centralBinom (Nat.succ d)) / (↑(Nat.succ d) + 1)
n : ℕ
⊢ ↑(catalan n) = ↑(Nat.centralBinom n) / (↑n + 1)
induction' n using Nat.case_strong_induction_on with d hd
n : ℕ
this : ↑(catalan n) = ↑(Nat.centralBinom n) / (↑n + 1)
h : n + 1 ∣ Nat.centralBinom n
⊢ catalan n = Nat.centralBinom n / (n + 1)
n : ℕ
this : ↑(catalan n) = ↑(Nat.centralBinom n) / (↑n + 1)
⊢ catalan n = Nat.centralBinom n / (n + 1)
have h := Nat.succ_dvd_centralBinom n
no goals
n : ℕ
this : ↑(catalan n) = ↑(Nat.centralBinom n) / (↑n + 1)
h : n + 1 ∣ Nat.centralBinom n
⊢ catalan n = Nat.centralBinom n / (n + 1)
exact_mod_cast this
no goals
case hz

⊢ ↑(catalan 0) = ↑(Nat.centralBinom 0) / (↑0 + 1)
simp
case hi
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ∑ x : Fin (Nat.succ d), ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑(Nat.centralBinom (Nat.succ d)) / (↑(Nat.succ d) + 1)
case hi
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ↑(catalan (Nat.succ d)) = ↑(Nat.centralBinom (Nat.succ d)) / (↑(Nat.succ d) + 1)
simp_rw [catalan_succ, Nat.cast_sum, Nat.cast_mul]
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ∑ x : Fin (Nat.succ d), ↑(catalan ↑x) * ↑(catalan (d - ↑x)) =
    ∑ i : Fin (Nat.succ d), ↑(Nat.centralBinom ↑i) / (↑↑i + 1) * (↑(Nat.centralBinom (d - ↑i)) / (↑d - ↑↑i + 1))

d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ∑ i : Fin (Nat.succ d), ↑(Nat.centralBinom ↑i) / (↑↑i + 1) * (↑(Nat.centralBinom (d - ↑i)) / (↑d - ↑↑i + 1)) =
    ↑(Nat.centralBinom (Nat.succ d)) / (↑(Nat.succ d) + 1)
case hi
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ∑ x : Fin (Nat.succ d), ↑(catalan ↑x) * ↑(catalan (d - ↑x)) = ↑(Nat.centralBinom (Nat.succ d)) / (↑(Nat.succ d) + 1)
trans (∑ i : Fin d.succ, Nat.centralBinom i / (i + 1) *
                         (Nat.centralBinom (d - i) / (d - i + 1)) : ℚ)
case e_f
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ (fun x => ↑(catalan ↑x) * ↑(catalan (d - ↑x))) = fun i =>
    ↑(Nat.centralBinom ↑i) / (↑↑i + 1) * (↑(Nat.centralBinom (d - ↑i)) / (↑d - ↑↑i + 1))
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ∑ x : Fin (Nat.succ d), ↑(catalan ↑x) * ↑(catalan (d - ↑x)) =
    ∑ i : Fin (Nat.succ d), ↑(Nat.centralBinom ↑i) / (↑↑i + 1) * (↑(Nat.centralBinom (d - ↑i)) / (↑d - ↑↑i + 1))
congr
case e_f.h
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) =
    ↑(Nat.centralBinom ↑x) / (↑↑x + 1) * (↑(Nat.centralBinom (d - ↑x)) / (↑d - ↑↑x + 1))
case e_f
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ (fun x => ↑(catalan ↑x) * ↑(catalan (d - ↑x))) = fun i =>
    ↑(Nat.centralBinom ↑i) / (↑↑i + 1) * (↑(Nat.centralBinom (d - ↑i)) / (↑d - ↑↑i + 1))
ext1 x
case e_f.h
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
m_le_d : ↑x ≤ d
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) =
    ↑(Nat.centralBinom ↑x) / (↑↑x + 1) * (↑(Nat.centralBinom (d - ↑x)) / (↑d - ↑↑x + 1))
case e_f.h
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) =
    ↑(Nat.centralBinom ↑x) / (↑↑x + 1) * (↑(Nat.centralBinom (d - ↑x)) / (↑d - ↑↑x + 1))
have m_le_d : x.val ≤ d := by apply Nat.le_of_lt_succ; apply x.2
case e_f.h
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
m_le_d : ↑x ≤ d
d_minus_x_le_d : d - ↑x ≤ d
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) =
    ↑(Nat.centralBinom ↑x) / (↑↑x + 1) * (↑(Nat.centralBinom (d - ↑x)) / (↑d - ↑↑x + 1))
case e_f.h
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
m_le_d : ↑x ≤ d
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) =
    ↑(Nat.centralBinom ↑x) / (↑↑x + 1) * (↑(Nat.centralBinom (d - ↑x)) / (↑d - ↑↑x + 1))
have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self
case e_f.h
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
m_le_d : ↑x ≤ d
d_minus_x_le_d : d - ↑x ≤ d
⊢ ↑(Nat.centralBinom ↑x) / (↑↑x + 1) * (↑(Nat.centralBinom (d - ↑x)) / (↑(d - ↑x) + 1)) =
    ↑(Nat.centralBinom ↑x) / (↑↑x + 1) * (↑(Nat.centralBinom (d - ↑x)) / (↑d - ↑↑x + 1))
case e_f.h
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
m_le_d : ↑x ≤ d
d_minus_x_le_d : d - ↑x ≤ d
⊢ ↑(catalan ↑x) * ↑(catalan (d - ↑x)) =
    ↑(Nat.centralBinom ↑x) / (↑↑x + 1) * (↑(Nat.centralBinom (d - ↑x)) / (↑d - ↑↑x + 1))
rw [hd _ m_le_d, hd _ d_minus_x_le_d]
no goals
case e_f.h
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
m_le_d : ↑x ≤ d
d_minus_x_le_d : d - ↑x ≤ d
⊢ ↑(Nat.centralBinom ↑x) / (↑↑x + 1) * (↑(Nat.centralBinom (d - ↑x)) / (↑(d - ↑x) + 1)) =
    ↑(Nat.centralBinom ↑x) / (↑↑x + 1) * (↑(Nat.centralBinom (d - ↑x)) / (↑d - ↑↑x + 1))
norm_cast
case a
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
⊢ ↑x < Nat.succ d
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
⊢ ↑x ≤ d
apply Nat.le_of_lt_succ
no goals
case a
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
⊢ ↑x < Nat.succ d
apply x.2
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ∑ i : Fin (Nat.succ d), ↑(Nat.centralBinom ↑i) / (↑↑i + 1) * (↑(Nat.centralBinom (d - ↑i)) / (↑d - ↑↑i + 1)) =
    ∑ i : Fin (Nat.succ d), (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i)

d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ∑ i : Fin (Nat.succ d), (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i) =
    ↑(Nat.centralBinom (Nat.succ d)) / (↑(Nat.succ d) + 1)
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ∑ i : Fin (Nat.succ d), ↑(Nat.centralBinom ↑i) / (↑↑i + 1) * (↑(Nat.centralBinom (d - ↑i)) / (↑d - ↑↑i + 1)) =
    ↑(Nat.centralBinom (Nat.succ d)) / (↑(Nat.succ d) + 1)
trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
i : Fin (Nat.succ d)
x✝ : i ∈ univ
⊢ ↑(Nat.centralBinom ↑i) / (↑↑i + 1) * (↑(Nat.centralBinom (d - ↑i)) / (↑d - ↑↑i + 1)) =
    gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ∑ i : Fin (Nat.succ d), ↑(Nat.centralBinom ↑i) / (↑↑i + 1) * (↑(Nat.centralBinom (d - ↑i)) / (↑d - ↑↑i + 1)) =
    ∑ i : Fin (Nat.succ d), (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i)
refine' sum_congr rfl fun i _ => _
no goals
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
i : Fin (Nat.succ d)
x✝ : i ∈ univ
⊢ ↑(Nat.centralBinom ↑i) / (↑↑i + 1) * (↑(Nat.centralBinom (d - ↑i)) / (↑d - ↑↑i + 1)) =
    gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i
rw [gosper_trick i.is_le, mul_div]
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ gosperCatalan (d + 1) (d + 1) - gosperCatalan (d + 1) 0 = ↑(Nat.centralBinom (d + 1)) / (↑(d + 1) + 1)
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ∑ i : Fin (Nat.succ d), (gosperCatalan (d + 1) (↑i + 1) - gosperCatalan (d + 1) ↑i) =
    ↑(Nat.centralBinom (Nat.succ d)) / (↑(Nat.succ d) + 1)
rw [← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i,
    sum_range_sub, Nat.succ_eq_add_one]
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ↑(Nat.centralBinom (d + 1)) / (↑d + 2) = ↑(Nat.centralBinom (d + 1)) / (↑(d + 1) + 1)
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ gosperCatalan (d + 1) (d + 1) - gosperCatalan (d + 1) 0 = ↑(Nat.centralBinom (d + 1)) / (↑(d + 1) + 1)
rw [gosper_catalan_sub_eq_central_binom_div d]
no goals
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
⊢ ↑(Nat.centralBinom (d + 1)) / (↑d + 2) = ↑(Nat.centralBinom (d + 1)) / (↑(d + 1) + 1)
norm_cast