case hz

⊢ card (treesOfNumNodesEq 0) = catalan 0

case hi
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
⊢ card (treesOfNumNodesEq (Nat.succ n)) = catalan (Nat.succ n)
n : ℕ
⊢ card (treesOfNumNodesEq n) = catalan n
induction' n using Nat.case_strong_induction_on with n ih
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

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))
case hi
n : ℕ
ih : ∀ (m : ℕ), m ≤ n → card (treesOfNumNodesEq m) = catalan m
⊢ card (treesOfNumNodesEq (Nat.succ n)) = catalan (Nat.succ n)
rw [treesOfNumNodesEq_succ, card_biUnion, catalan_succ']
no goals
case hz

⊢ card (treesOfNumNodesEq 0) = catalan 0
simp
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
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
apply sum_congr rfl
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
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
rintro ⟨i, j⟩ H
no goals
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
rw [card_map, card_product, ih _ (fst_le H), ih _ (snd_le H)]
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)
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))
simp_rw [disjoint_left]
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)
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)
rintro ⟨i, j⟩ _ ⟨i', j'⟩ _
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)
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)
intros h a
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)

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)
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)
cases' a with a l r
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)
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)
intro h
no goals
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)
simp at h
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
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)
intro h1 h2
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')
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
apply h
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)

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')
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')
trans (numNodes l, numNodes r)
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)
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)
simp at h1
no goals
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)
simp [h1]
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')
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')
simp at h2
no goals
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')
simp [h2]