[GOAL]
⊢ catalan 0 = 1
[PROOFSTEP]
rw [catalan]
[GOAL]
n : ℕ
⊢ catalan (n + 1) = ∑ i : Fin (Nat.succ n), catalan ↑i * catalan (n - ↑i)
[PROOFSTEP]
rw [catalan]
[GOAL]
n : ℕ
⊢ catalan (n + 1) = ∑ ij in Nat.antidiagonal n, catalan ij.fst * catalan ij.snd
[PROOFSTEP]
rw [catalan_succ, Nat.sum_antidiagonal_eq_sum_range_succ (fun x y => catalan x * catalan y) n, sum_range]
[GOAL]
⊢ catalan 1 = 1
[PROOFSTEP]
simp [catalan_succ]
[GOAL]
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)
[PROOFSTEP]
have l₁ : (n : ℚ) + 1 ≠ 0 := by norm_cast; exact n.succ_ne_zero
[GOAL]
n i : ℕ
h : i ≤ n
⊢ ↑n + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n i : ℕ
h : i ≤ n
⊢ ¬n + 1 = 0
[PROOFSTEP]
exact n.succ_ne_zero
[GOAL]
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)
[PROOFSTEP]
have l₂ : (n : ℚ) + 1 + 1 ≠ 0 := by norm_cast; exact (n + 1).succ_ne_zero
[GOAL]
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
⊢ ↑n + 1 + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
⊢ ¬n + 1 + 1 = 0
[PROOFSTEP]
exact (n + 1).succ_ne_zero
[GOAL]
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)
[PROOFSTEP]
have l₃ : (i : ℚ) + 1 ≠ 0 := by norm_cast; exact i.succ_ne_zero
[GOAL]
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
⊢ ↑i + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
⊢ ¬i + 1 = 0
[PROOFSTEP]
exact i.succ_ne_zero
[GOAL]
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)
[PROOFSTEP]
have l₄ : (n : ℚ) - i + 1 ≠ 0 := by norm_cast; exact (n - i).succ_ne_zero
[GOAL]
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
⊢ ↑n - ↑i + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n i : ℕ
h : i ≤ n
l₁ : ↑n + 1 ≠ 0
l₂ : ↑n + 1 + 1 ≠ 0
l₃ : ↑i + 1 ≠ 0
⊢ ¬n - i + 1 = 0
[PROOFSTEP]
exact (n - i).succ_ne_zero
[GOAL]
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)
[PROOFSTEP]
have h₁ := (mul_div_cancel_left (↑(Nat.centralBinom (i + 1))) l₃).symm
[GOAL]
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)
[PROOFSTEP]
have h₂ := (mul_div_cancel_left (↑(Nat.centralBinom (n - i + 1))) l₄).symm
[GOAL]
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)
[PROOFSTEP]
have h₃ : ((i : ℚ) + 1) * (i + 1).centralBinom = 2 * (2 * i + 1) * i.centralBinom := by
  exact_mod_cast Nat.succ_mul_centralBinom_succ i
[GOAL]
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)
[PROOFSTEP]
exact_mod_cast Nat.succ_mul_centralBinom_succ i
[GOAL]
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)
[PROOFSTEP]
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)
[GOAL]
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))
[PROOFSTEP]
exact_mod_cast Nat.succ_mul_centralBinom_succ (n - i)
[GOAL]
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)
[PROOFSTEP]
simp only [gosperCatalan]
[GOAL]
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)
[PROOFSTEP]
push_cast
[GOAL]
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)
[PROOFSTEP]
rw [show n + 1 - i = n - i + 1 by rw [Nat.add_comm (n - i) 1, ← (Nat.add_sub_assoc h 1), add_comm]]
[GOAL]
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
[PROOFSTEP]
rw [Nat.add_comm (n - i) 1, ← (Nat.add_sub_assoc h 1), add_comm]
[GOAL]
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)
[PROOFSTEP]
rw [h₁, h₂, h₃, h₄]
[GOAL]
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)
[PROOFSTEP]
field_simp
[GOAL]
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))))
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
[PROOFSTEP]
have : (n : ℚ) + 1 ≠ 0 := by norm_cast; exact n.succ_ne_zero
[GOAL]
n : ℕ
⊢ ↑n + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
⊢ ¬n + 1 = 0
[PROOFSTEP]
exact n.succ_ne_zero
[GOAL]
n : ℕ
this : ↑n + 1 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
[PROOFSTEP]
have : (n : ℚ) + 1 + 1 ≠ 0 := by norm_cast; exact (n + 1).succ_ne_zero
[GOAL]
n : ℕ
this : ↑n + 1 ≠ 0
⊢ ↑n + 1 + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
this : ↑n + 1 ≠ 0
⊢ ¬n + 1 + 1 = 0
[PROOFSTEP]
exact (n + 1).succ_ne_zero
[GOAL]
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
[PROOFSTEP]
have h : (n : ℚ) + 2 ≠ 0 := by norm_cast; exact (n + 1).succ_ne_zero
[GOAL]
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
⊢ ↑n + 2 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
⊢ ¬n + 2 = 0
[PROOFSTEP]
exact (n + 1).succ_ne_zero
[GOAL]
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
[PROOFSTEP]
simp only [gosperCatalan, Nat.sub_zero, Nat.centralBinom_zero, Nat.sub_self]
[GOAL]
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ ↑(Nat.centralBinom (n + 1)) * ↑1 * (2 * ↑(n + 1) - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) -
      ↑1 * ↑(Nat.centralBinom (n + 1)) * (2 * ↑0 - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) =
    ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
[PROOFSTEP]
field_simp
[GOAL]
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ (↑(Nat.centralBinom (n + 1)) * (2 * (↑n + 1) - (↑n + 1)) - ↑(Nat.centralBinom (n + 1)) * (-1 + -↑n)) * (↑n + 2) =
    ↑(Nat.centralBinom (n + 1)) * (2 * (↑n + 1) * (↑n + 1 + 1))
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ catalan n = Nat.centralBinom n / (n + 1)
[PROOFSTEP]
suffices (catalan n : ℚ) = Nat.centralBinom n / (n + 1)
  by
  have h := Nat.succ_dvd_centralBinom n
  exact_mod_cast this
[GOAL]
n : ℕ
this : ↑(catalan n) = ↑(Nat.centralBinom n) / (↑n + 1)
⊢ catalan n = Nat.centralBinom n / (n + 1)
[PROOFSTEP]
have h := Nat.succ_dvd_centralBinom n
[GOAL]
n : ℕ
this : ↑(catalan n) = ↑(Nat.centralBinom n) / (↑n + 1)
h : n + 1 ∣ Nat.centralBinom n
⊢ catalan n = Nat.centralBinom n / (n + 1)
[PROOFSTEP]
exact_mod_cast this
[GOAL]
n : ℕ
⊢ ↑(catalan n) = ↑(Nat.centralBinom n) / (↑n + 1)
[PROOFSTEP]
induction' n using Nat.case_strong_induction_on with d hd
[GOAL]
case hz
⊢ ↑(catalan 0) = ↑(Nat.centralBinom 0) / (↑0 + 1)
[PROOFSTEP]
simp
[GOAL]
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)
[PROOFSTEP]
simp_rw [catalan_succ, Nat.cast_sum, Nat.cast_mul]
[GOAL]
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)
[PROOFSTEP]
trans (∑ i : Fin d.succ, Nat.centralBinom i / (i + 1) * (Nat.centralBinom (d - i) / (d - i + 1)) : ℚ)
[GOAL]
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))
[PROOFSTEP]
congr
[GOAL]
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))
[PROOFSTEP]
ext1 x
[GOAL]
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))
[PROOFSTEP]
have m_le_d : x.val ≤ d := by apply Nat.le_of_lt_succ; apply x.2
[GOAL]
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
⊢ ↑x ≤ d
[PROOFSTEP]
apply Nat.le_of_lt_succ
[GOAL]
case a
d : ℕ
hd : ∀ (m : ℕ), m ≤ d → ↑(catalan m) = ↑(Nat.centralBinom m) / (↑m + 1)
x : Fin (Nat.succ d)
⊢ ↑x < Nat.succ d
[PROOFSTEP]
apply x.2
[GOAL]
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))
[PROOFSTEP]
have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self
[GOAL]
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))
[PROOFSTEP]
rw [hd _ m_le_d, hd _ d_minus_x_le_d]
[GOAL]
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))
[PROOFSTEP]
norm_cast
[GOAL]
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)
[PROOFSTEP]
trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))
[GOAL]
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)
[PROOFSTEP]
refine' sum_congr rfl fun i _ => _
[GOAL]
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
[PROOFSTEP]
rw [gosper_trick i.is_le, mul_div]
[GOAL]
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)
[PROOFSTEP]
rw [← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i, sum_range_sub, Nat.succ_eq_add_one]
[GOAL]
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)
[PROOFSTEP]
rw [gosper_catalan_sub_eq_central_binom_div d]
[GOAL]
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)
[PROOFSTEP]
norm_cast
[GOAL]
⊢ catalan 2 = 2
[PROOFSTEP]
unfold catalan
[GOAL]
⊢ ∑ i : Fin (Nat.succ 1), catalan ↑i * catalan (1 - ↑i) = 2
[PROOFSTEP]
rfl
[GOAL]
⊢ catalan 3 = 5
[PROOFSTEP]
unfold catalan
[GOAL]
⊢ ∑ i : Fin (Nat.succ 2), catalan ↑i * catalan (2 - ↑i) = 5
[PROOFSTEP]
rfl
[GOAL]
a b : Finset (Tree Unit)
x✝¹ x✝ : Tree Unit × Tree Unit
x₁ x₂ y₁ y₂ : Tree Unit
h : (fun x => node () x.fst x.snd) (x₁, x₂) = (fun x => node () x.fst x.snd) (y₁, y₂)
⊢ (x₁, x₂) = (y₁, y₂)
[PROOFSTEP]
simpa using h
[GOAL]
n : ℕ
ijh : { x // x ∈ Nat.antidiagonal n }
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑ijh).fst (Nat.succ n)
[PROOFSTEP]
simp_wf
[GOAL]
n : ℕ
ijh : { x // x ∈ Nat.antidiagonal n }
⊢ (↑ijh).fst < Nat.succ n
[PROOFSTEP]
try exact Nat.lt_succ_of_le (fst_le ijh.2)
[GOAL]
n : ℕ
ijh : { x // x ∈ Nat.antidiagonal n }
⊢ (↑ijh).fst < Nat.succ n
[PROOFSTEP]
exact Nat.lt_succ_of_le (fst_le ijh.2)
[GOAL]

[PROOFSTEP]
try exact Nat.lt_succ_of_le (snd_le ijh.2)
[GOAL]

[PROOFSTEP]
exact Nat.lt_succ_of_le (snd_le ijh.2)
[GOAL]
n : ℕ
ijh : { x // x ∈ Nat.antidiagonal n }
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (↑ijh).snd (Nat.succ n)
[PROOFSTEP]
simp_wf
[GOAL]
n : ℕ
ijh : { x // x ∈ Nat.antidiagonal n }
⊢ (↑ijh).snd < Nat.succ n
[PROOFSTEP]
try exact Nat.lt_succ_of_le (fst_le ijh.2)
[GOAL]
n : ℕ
ijh : { x // x ∈ Nat.antidiagonal n }
⊢ (↑ijh).snd < Nat.succ n
[PROOFSTEP]
exact Nat.lt_succ_of_le (fst_le ijh.2)
[GOAL]
n : ℕ
ijh : { x // x ∈ Nat.antidiagonal n }
⊢ (↑ijh).snd < Nat.succ n
[PROOFSTEP]
try exact Nat.lt_succ_of_le (snd_le ijh.2)
[GOAL]
n : ℕ
ijh : { x // x ∈ Nat.antidiagonal n }
⊢ (↑ijh).snd < Nat.succ n
[PROOFSTEP]
exact Nat.lt_succ_of_le (snd_le ijh.2)
[GOAL]
⊢ treesOfNumNodesEq 0 = {nil}
[PROOFSTEP]
rw [treesOfNumNodesEq]
[GOAL]
n : ℕ
⊢ treesOfNumNodesEq (n + 1) =
    Finset.biUnion (Nat.antidiagonal n) fun ij => pairwiseNode (treesOfNumNodesEq ij.fst) (treesOfNumNodesEq ij.snd)
[PROOFSTEP]
rw [treesOfNumNodesEq]
[GOAL]
n : ℕ
⊢ (Finset.biUnion (attach (Nat.antidiagonal n)) fun ijh =>
      pairwiseNode (treesOfNumNodesEq (↑ijh).fst) (treesOfNumNodesEq (↑ijh).snd)) =
    Finset.biUnion (Nat.antidiagonal n) fun ij => pairwiseNode (treesOfNumNodesEq ij.fst) (treesOfNumNodesEq ij.snd)
[PROOFSTEP]
ext
[GOAL]
case a
n : ℕ
a✝ : Tree Unit
⊢ (a✝ ∈
      Finset.biUnion (attach (Nat.antidiagonal n)) fun ijh =>
        pairwiseNode (treesOfNumNodesEq (↑ijh).fst) (treesOfNumNodesEq (↑ijh).snd)) ↔
    a✝ ∈
      Finset.biUnion (Nat.antidiagonal n) fun ij => pairwiseNode (treesOfNumNodesEq ij.fst) (treesOfNumNodesEq ij.snd)
[PROOFSTEP]
simp
[GOAL]
x : Tree Unit
n : ℕ
⊢ x ∈ treesOfNumNodesEq n ↔ numNodes x = n
[PROOFSTEP]
induction x using Tree.unitRecOn generalizing n
[GOAL]
case base
n : ℕ
⊢ nil ∈ treesOfNumNodesEq n ↔ numNodes nil = n
[PROOFSTEP]
cases n
[GOAL]
case ind
x✝ y✝ : Tree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ numNodes x✝ = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ numNodes y✝ = n
n : ℕ
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq n ↔ numNodes (node () x✝ y✝) = n
[PROOFSTEP]
cases n
[GOAL]
case base.zero
⊢ nil ∈ treesOfNumNodesEq Nat.zero ↔ numNodes nil = Nat.zero
[PROOFSTEP]
simp [treesOfNumNodesEq_succ, Nat.succ_eq_add_one, *]
[GOAL]
case base.succ
n✝ : ℕ
⊢ nil ∈ treesOfNumNodesEq (Nat.succ n✝) ↔ numNodes nil = Nat.succ n✝
[PROOFSTEP]
simp [treesOfNumNodesEq_succ, Nat.succ_eq_add_one, *]
[GOAL]
case ind.zero
x✝ y✝ : Tree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ numNodes x✝ = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ numNodes y✝ = n
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq Nat.zero ↔ numNodes (node () x✝ y✝) = Nat.zero
[PROOFSTEP]
simp [treesOfNumNodesEq_succ, Nat.succ_eq_add_one, *]
[GOAL]
case ind.succ
x✝ y✝ : Tree Unit
a✝¹ : ∀ {n : ℕ}, x✝ ∈ treesOfNumNodesEq n ↔ numNodes x✝ = n
a✝ : ∀ {n : ℕ}, y✝ ∈ treesOfNumNodesEq n ↔ numNodes y✝ = n
n✝ : ℕ
⊢ node () x✝ y✝ ∈ treesOfNumNodesEq (Nat.succ n✝) ↔ numNodes (node () x✝ y✝) = Nat.succ n✝
[PROOFSTEP]
simp [treesOfNumNodesEq_succ, Nat.succ_eq_add_one, *]
[GOAL]
case base.succ
n✝ : ℕ
⊢ ¬0 = n✝ + 1
[PROOFSTEP]
exact (Nat.succ_ne_zero _).symm
[GOAL]
n : ℕ
⊢ ∀ (x : Tree Unit), x ∈ ↑(treesOfNumNodesEq n) ↔ x ∈ {x | numNodes x = n}
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ card (treesOfNumNodesEq n) = catalan n
[PROOFSTEP]
induction' n using Nat.case_strong_induction_on with n ih
[GOAL]
case hz
⊢ card (treesOfNumNodesEq 0) = catalan 0
[PROOFSTEP]
simp
[GOAL]
case hi
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
⊢ card (treesOfNumNodesEq (Nat.succ n)) = catalan (Nat.succ n)
[PROOFSTEP]
rw [treesOfNumNodesEq_succ, card_biUnion, catalan_succ']
[GOAL]
case hi
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
⊢ ∑ u in Nat.antidiagonal n, card (pairwiseNode (treesOfNumNodesEq u.fst) (treesOfNumNodesEq u.snd)) =
    ∑ ij in Nat.antidiagonal n, catalan ij.fst * catalan ij.snd
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case hi
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
⊢ ∀ (x : ℕ × ℕ),
    x ∈ Nat.antidiagonal n →
      card (pairwiseNode (treesOfNumNodesEq x.fst) (treesOfNumNodesEq x.snd)) = catalan x.fst * catalan x.snd
[PROOFSTEP]
rintro ⟨i, j⟩ H
[GOAL]
case hi.mk
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
H : (i, j) ∈ Nat.antidiagonal n
⊢ card (pairwiseNode (treesOfNumNodesEq (i, j).fst) (treesOfNumNodesEq (i, j).snd)) =
    catalan (i, j).fst * catalan (i, j).snd
[PROOFSTEP]
rw [card_map, card_product, ih _ (fst_le H), ih _ (snd_le H)]
[GOAL]
case hi
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
⊢ ∀ (x : ℕ × ℕ),
    x ∈ Nat.antidiagonal n →
      ∀ (y : ℕ × ℕ),
        y ∈ Nat.antidiagonal n →
          x ≠ y →
            Disjoint (pairwiseNode (treesOfNumNodesEq x.fst) (treesOfNumNodesEq x.snd))
              (pairwiseNode (treesOfNumNodesEq y.fst) (treesOfNumNodesEq y.snd))
[PROOFSTEP]
simp_rw [disjoint_left]
[GOAL]
case hi
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
⊢ ∀ (x : ℕ × ℕ),
    x ∈ Nat.antidiagonal n →
      ∀ (y : ℕ × ℕ),
        y ∈ Nat.antidiagonal n →
          x ≠ y →
            ∀ ⦃a : Tree Unit⦄,
              a ∈ pairwiseNode (treesOfNumNodesEq x.fst) (treesOfNumNodesEq x.snd) →
                ¬a ∈ pairwiseNode (treesOfNumNodesEq y.fst) (treesOfNumNodesEq y.snd)
[PROOFSTEP]
rintro ⟨i, j⟩ _ ⟨i', j'⟩
  _
      -- Porting note: was clear * -; tidy
[GOAL]
case hi.mk.mk
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
a✝¹ : (i, j) ∈ Nat.antidiagonal n
i' j' : ℕ
a✝ : (i', j') ∈ Nat.antidiagonal n
⊢ (i, j) ≠ (i', j') →
    ∀ ⦃a : Tree Unit⦄,
      a ∈ pairwiseNode (treesOfNumNodesEq (i, j).fst) (treesOfNumNodesEq (i, j).snd) →
        ¬a ∈ pairwiseNode (treesOfNumNodesEq (i', j').fst) (treesOfNumNodesEq (i', j').snd)
[PROOFSTEP]
intros h a
[GOAL]
case hi.mk.mk
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
a✝¹ : (i, j) ∈ Nat.antidiagonal n
i' j' : ℕ
a✝ : (i', j') ∈ Nat.antidiagonal n
h : (i, j) ≠ (i', j')
a : Tree Unit
⊢ a ∈ pairwiseNode (treesOfNumNodesEq (i, j).fst) (treesOfNumNodesEq (i, j).snd) →
    ¬a ∈ pairwiseNode (treesOfNumNodesEq (i', j').fst) (treesOfNumNodesEq (i', j').snd)
[PROOFSTEP]
cases' a with a l r
[GOAL]
case hi.mk.mk.nil
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
a✝¹ : (i, j) ∈ Nat.antidiagonal n
i' j' : ℕ
a✝ : (i', j') ∈ Nat.antidiagonal n
h : (i, j) ≠ (i', j')
⊢ nil ∈ pairwiseNode (treesOfNumNodesEq (i, j).fst) (treesOfNumNodesEq (i, j).snd) →
    ¬nil ∈ pairwiseNode (treesOfNumNodesEq (i', j').fst) (treesOfNumNodesEq (i', j').snd)
[PROOFSTEP]
intro h
[GOAL]
case hi.mk.mk.nil
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
a✝¹ : (i, j) ∈ Nat.antidiagonal n
i' j' : ℕ
a✝ : (i', j') ∈ Nat.antidiagonal n
h✝ : (i, j) ≠ (i', j')
h : nil ∈ pairwiseNode (treesOfNumNodesEq (i, j).fst) (treesOfNumNodesEq (i, j).snd)
⊢ ¬nil ∈ pairwiseNode (treesOfNumNodesEq (i', j').fst) (treesOfNumNodesEq (i', j').snd)
[PROOFSTEP]
simp at h 
[GOAL]
case hi.mk.mk.node
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
a✝¹ : (i, j) ∈ Nat.antidiagonal n
i' j' : ℕ
a✝ : (i', j') ∈ Nat.antidiagonal n
h : (i, j) ≠ (i', j')
a : Unit
l r : Tree Unit
⊢ node a l r ∈ pairwiseNode (treesOfNumNodesEq (i, j).fst) (treesOfNumNodesEq (i, j).snd) →
    ¬node a l r ∈ pairwiseNode (treesOfNumNodesEq (i', j').fst) (treesOfNumNodesEq (i', j').snd)
[PROOFSTEP]
intro h1 h2
[GOAL]
case hi.mk.mk.node
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
a✝¹ : (i, j) ∈ Nat.antidiagonal n
i' j' : ℕ
a✝ : (i', j') ∈ Nat.antidiagonal n
h : (i, j) ≠ (i', j')
a : Unit
l r : Tree Unit
h1 : node a l r ∈ pairwiseNode (treesOfNumNodesEq (i, j).fst) (treesOfNumNodesEq (i, j).snd)
h2 : node a l r ∈ pairwiseNode (treesOfNumNodesEq (i', j').fst) (treesOfNumNodesEq (i', j').snd)
⊢ False
[PROOFSTEP]
apply h
[GOAL]
case hi.mk.mk.node
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
a✝¹ : (i, j) ∈ Nat.antidiagonal n
i' j' : ℕ
a✝ : (i', j') ∈ Nat.antidiagonal n
h : (i, j) ≠ (i', j')
a : Unit
l r : Tree Unit
h1 : node a l r ∈ pairwiseNode (treesOfNumNodesEq (i, j).fst) (treesOfNumNodesEq (i, j).snd)
h2 : node a l r ∈ pairwiseNode (treesOfNumNodesEq (i', j').fst) (treesOfNumNodesEq (i', j').snd)
⊢ (i, j) = (i', j')
[PROOFSTEP]
trans (numNodes l, numNodes r)
[GOAL]
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
a✝¹ : (i, j) ∈ Nat.antidiagonal n
i' j' : ℕ
a✝ : (i', j') ∈ Nat.antidiagonal n
h : (i, j) ≠ (i', j')
a : Unit
l r : Tree Unit
h1 : node a l r ∈ pairwiseNode (treesOfNumNodesEq (i, j).fst) (treesOfNumNodesEq (i, j).snd)
h2 : node a l r ∈ pairwiseNode (treesOfNumNodesEq (i', j').fst) (treesOfNumNodesEq (i', j').snd)
⊢ (i, j) = (numNodes l, numNodes r)
[PROOFSTEP]
simp at h1 
[GOAL]
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
a✝¹ : (i, j) ∈ Nat.antidiagonal n
i' j' : ℕ
a✝ : (i', j') ∈ Nat.antidiagonal n
h : (i, j) ≠ (i', j')
a : Unit
l r : Tree Unit
h2 : node a l r ∈ pairwiseNode (treesOfNumNodesEq (i', j').fst) (treesOfNumNodesEq (i', j').snd)
h1 : numNodes l = i ∧ numNodes r = j
⊢ (i, j) = (numNodes l, numNodes r)
[PROOFSTEP]
simp [h1]
[GOAL]
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
a✝¹ : (i, j) ∈ Nat.antidiagonal n
i' j' : ℕ
a✝ : (i', j') ∈ Nat.antidiagonal n
h : (i, j) ≠ (i', j')
a : Unit
l r : Tree Unit
h1 : node a l r ∈ pairwiseNode (treesOfNumNodesEq (i, j).fst) (treesOfNumNodesEq (i, j).snd)
h2 : node a l r ∈ pairwiseNode (treesOfNumNodesEq (i', j').fst) (treesOfNumNodesEq (i', j').snd)
⊢ (numNodes l, numNodes r) = (i', j')
[PROOFSTEP]
simp at h2 
[GOAL]
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
i j : ℕ
a✝¹ : (i, j) ∈ Nat.antidiagonal n
i' j' : ℕ
a✝ : (i', j') ∈ Nat.antidiagonal n
h : (i, j) ≠ (i', j')
a : Unit
l r : Tree Unit
h1 : node a l r ∈ pairwiseNode (treesOfNumNodesEq (i, j).fst) (treesOfNumNodesEq (i, j).snd)
h2 : numNodes l = i' ∧ numNodes r = j'
⊢ (numNodes l, numNodes r) = (i', j')
[PROOFSTEP]
simp [h2]
