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)
n : ℕ
⊢ treesOfNumNodesEq (n + 1) =
    Finset.biUnion (Nat.antidiagonal n) fun ij => pairwiseNode (treesOfNumNodesEq ij.fst) (treesOfNumNodesEq ij.snd)
rw [treesOfNumNodesEq]
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)
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)
ext
no goals
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)
simp