n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
have l₁ : (n : ℚ) + 1 ≠ 0 := by norm_cast; exact n.succ_ne_zero
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
have l₂ : (n : ℚ) + 1 + 1 ≠ 0 := by norm_cast; exact (n + 1).succ_ne_zero
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
have l₃ : (i : ℚ) + 1 ≠ 0 := by norm_cast; exact i.succ_ne_zero
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
have l₄ : (n : ℚ) - i + 1 ≠ 0 := by norm_cast; exact (n - i).succ_ne_zero
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
have h₁ := (mul_div_cancel_left (↑(Nat.centralBinom (i + 1))) l₃).symm
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
have h₂ := (mul_div_cancel_left (↑(Nat.centralBinom (n - i + 1))) l₄).symm
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
have h₃ : ((i : ℚ) + 1) * (i + 1).centralBinom = 2 * (2 * i + 1) * i.centralBinom := by
  exact_mod_cast Nat.succ_mul_centralBinom_succ i
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
have h₄ :
  ((n : ℚ) - i + 1) * (n - i + 1).centralBinom = 2 * (2 * (n - i) + 1) * (n - i).centralBinom :=
  by exact_mod_cast Nat.succ_mul_centralBinom_succ (n - i)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ ↑(Nat.centralBinom (i + 1)) * ↑(Nat.centralBinom (n + 1 - (i + 1))) * (2 * ↑(i + 1) - ↑(n + 1)) /
        (2 * ↑(n + 1) * (↑(n + 1) + 1)) -
      ↑(Nat.centralBinom i) * ↑(Nat.centralBinom (n + 1 - i)) * (2 * ↑i - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ gosperCatalan (n + 1) (i + 1) - gosperCatalan (n + 1) i =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
simp only [gosperCatalan]
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ ↑(Nat.centralBinom (i + 1)) * ↑(Nat.centralBinom (n + 1 - (i + 1))) * (2 * (↑i + 1) - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑(Nat.centralBinom i) * ↑(Nat.centralBinom (n + 1 - i)) * (2 * ↑i - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ ↑(Nat.centralBinom (i + 1)) * ↑(Nat.centralBinom (n + 1 - (i + 1))) * (2 * ↑(i + 1) - ↑(n + 1)) /
        (2 * ↑(n + 1) * (↑(n + 1) + 1)) -
      ↑(Nat.centralBinom i) * ↑(Nat.centralBinom (n + 1 - i)) * (2 * ↑i - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
push_cast
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ ↑(Nat.centralBinom (i + 1)) * ↑(Nat.centralBinom (n + 1 - (i + 1))) * (2 * (↑i + 1) - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑(Nat.centralBinom i) * ↑(Nat.centralBinom (n - i + 1)) * (2 * ↑i - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ ↑(Nat.centralBinom (i + 1)) * ↑(Nat.centralBinom (n + 1 - (i + 1))) * (2 * (↑i + 1) - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑(Nat.centralBinom i) * ↑(Nat.centralBinom (n + 1 - i)) * (2 * ↑i - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
rw [show n + 1 - i = n - i + 1 by rw [Nat.add_comm (n - i) 1, ←(Nat.add_sub_assoc h 1), add_comm]]
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n + 1 - (i + 1))) *
          (2 * (↑i + 1) - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑(Nat.centralBinom i) * (2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)) *
          (2 * ↑i - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ ↑(Nat.centralBinom (i + 1)) * ↑(Nat.centralBinom (n + 1 - (i + 1))) * (2 * (↑i + 1) - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑(Nat.centralBinom i) * ↑(Nat.centralBinom (n - i + 1)) * (2 * ↑i - (↑n + 1)) / (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
rw [h₁, h₂, h₃, h₄]
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ (2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i) * ↑(Nat.centralBinom (n - i)) * (2 * (↑i + 1) - (↑n + 1)) *
          ((↑n - ↑i + 1) * (2 * (↑n + 1) * (↑n + 1 + 1))) -
        (↑i + 1) * (2 * (↑n + 1) * (↑n + 1 + 1)) *
          (↑(Nat.centralBinom i) * (2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))) * (2 * ↑i - (↑n + 1)))) *
      ((↑i + 1) * (↑n - ↑i + 1)) =
    ↑(Nat.centralBinom i) * ↑(Nat.centralBinom (n - i)) *
      ((↑i + 1) * (2 * (↑n + 1) * (↑n + 1 + 1)) * ((↑n - ↑i + 1) * (2 * (↑n + 1) * (↑n + 1 + 1))))
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n + 1 - (i + 1))) *
          (2 * (↑i + 1) - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) -
      ↑(Nat.centralBinom i) * (2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)) *
          (2 * ↑i - (↑n + 1)) /
        (2 * (↑n + 1) * (↑n + 1 + 1)) =
    ↑(Nat.centralBinom i) / (↑i + 1) * ↑(Nat.centralBinom (n - i)) / (↑n - ↑i + 1)
field_simp
no goals
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ (2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i) * ↑(Nat.centralBinom (n - i)) * (2 * (↑i + 1) - (↑n + 1)) *
          ((↑n - ↑i + 1) * (2 * (↑n + 1) * (↑n + 1 + 1))) -
        (↑i + 1) * (2 * (↑n + 1) * (↑n + 1 + 1)) *
          (↑(Nat.centralBinom i) * (2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))) * (2 * ↑i - (↑n + 1)))) *
      ((↑i + 1) * (↑n - ↑i + 1)) =
    ↑(Nat.centralBinom i) * ↑(Nat.centralBinom (n - i)) *
      ((↑i + 1) * (2 * (↑n + 1) * (↑n + 1 + 1)) * ((↑n - ↑i + 1) * (2 * (↑n + 1) * (↑n + 1 + 1))))
ring
n i : ℕ
h : i ≤ n
⊢ ¬n + 1 = 0
n i : ℕ
h : i ≤ n
⊢ ↑n + 1 ≠ 0
norm_cast
no goals
n i : ℕ
h : i ≤ n
⊢ ¬n + 1 = 0
exact n.succ_ne_zero
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
⊢ ¬n + 1 + 1 = 0
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
⊢ ↑n + 1 + 1 ≠ 0
norm_cast
no goals
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
⊢ ¬n + 1 + 1 = 0
exact (n + 1).succ_ne_zero
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
⊢ ¬i + 1 = 0
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
⊢ ↑i + 1 ≠ 0
norm_cast
no goals
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
⊢ ¬i + 1 = 0
exact i.succ_ne_zero
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
⊢ ¬n - i + 1 = 0
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
⊢ ↑n - ↑i + 1 ≠ 0
norm_cast
no goals
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
⊢ ¬n - i + 1 = 0
exact (n - i).succ_ne_zero
no goals
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
⊢ (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
exact_mod_cast Nat.succ_mul_centralBinom_succ i
no goals
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
⊢ (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
exact_mod_cast Nat.succ_mul_centralBinom_succ (n - i)
no goals
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
l₄ : ↑n - ↑i + 1 ≠ 0
h₁ : ↑(Nat.centralBinom (i + 1)) = (↑i + 1) * ↑(Nat.centralBinom (i + 1)) / (↑i + 1)
h₂ : ↑(Nat.centralBinom (n - i + 1)) = (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) / (↑n - ↑i + 1)
h₃ : (↑i + 1) * ↑(Nat.centralBinom (i + 1)) = 2 * (2 * ↑i + 1) * ↑(Nat.centralBinom i)
h₄ : (↑n - ↑i + 1) * ↑(Nat.centralBinom (n - i + 1)) = 2 * (2 * (↑n - ↑i) + 1) * ↑(Nat.centralBinom (n - i))
⊢ n + 1 - i = n - i + 1
rw [Nat.add_comm (n - i) 1, ←(Nat.add_sub_assoc h 1), add_comm]