[GOAL]
μ ν : YoungDiagram
h : (fun y => ↑y.cells) μ = (fun y => ↑y.cells) ν
⊢ μ = ν
[PROOFSTEP]
rwa [YoungDiagram.ext_iff, ← Finset.coe_inj]
[GOAL]
μ ν : YoungDiagram
⊢ IsLowerSet ↑(μ.cells ∪ ν.cells)
[PROOFSTEP]
rw [Finset.coe_union]
[GOAL]
μ ν : YoungDiagram
⊢ IsLowerSet (↑μ.cells ∪ ↑ν.cells)
[PROOFSTEP]
exact μ.isLowerSet.union ν.isLowerSet
[GOAL]
μ ν : YoungDiagram
⊢ IsLowerSet ↑(μ.cells ∩ ν.cells)
[PROOFSTEP]
rw [Finset.coe_inter]
[GOAL]
μ ν : YoungDiagram
⊢ IsLowerSet (↑μ.cells ∩ ↑ν.cells)
[PROOFSTEP]
exact μ.isLowerSet.inter ν.isLowerSet
[GOAL]
⊢ IsLowerSet ↑∅
[PROOFSTEP]
intros a b _ h
[GOAL]
a b : ℕ × ℕ
a✝ : b ≤ a
h : a ∈ ↑∅
⊢ b ∈ ↑∅
[PROOFSTEP]
simp only [Finset.coe_empty, Set.mem_empty_iff_false]
[GOAL]
a b : ℕ × ℕ
a✝ : b ≤ a
h : a ∈ ↑∅
⊢ False
[PROOFSTEP]
simp only [Finset.coe_empty, Set.mem_empty_iff_false] at h
[GOAL]
x✝¹ : YoungDiagram
x✝ : ℕ × ℕ
⊢ x✝ ∈ ⊥ → x✝ ∈ x✝¹
[PROOFSTEP]
intro y
[GOAL]
x✝¹ : YoungDiagram
x✝ : ℕ × ℕ
y : x✝ ∈ ⊥
⊢ x✝ ∈ x✝¹
[PROOFSTEP]
simp only [mem_mk, Finset.not_mem_empty] at y
[GOAL]
⊢ ↑⊥.cells = ∅
[PROOFSTEP]
refine' Set.eq_of_subset_of_subset _ _
[GOAL]
case refine'_1
⊢ ↑⊥.cells ⊆ ∅
case refine'_2 ⊢ ∅ ⊆ ↑⊥.cells
[PROOFSTEP]
intros x h
[GOAL]
case refine'_1
x : ℕ × ℕ
h : x ∈ ↑⊥.cells
⊢ x ∈ ∅
case refine'_2 ⊢ ∅ ⊆ ↑⊥.cells
[PROOFSTEP]
simp [mem_mk, Finset.coe_empty, Set.mem_empty_iff_false] at h
[GOAL]
case refine'_2
⊢ ∅ ⊆ ↑⊥.cells
[PROOFSTEP]
simp only [cells_bot, Finset.coe_empty, Set.empty_subset]
[GOAL]
μ ν : YoungDiagram
h : μ.cells = ν.cells
⊢ μ = ν
[PROOFSTEP]
rwa [YoungDiagram.ext_iff]
[GOAL]
μ : YoungDiagram
x✝¹ x✝ : ℕ × ℕ
h : x✝ ≤ x✝¹
⊢ x✝¹ ∈ ↑(↑(Equiv.finsetCongr (Equiv.prodComm ℕ ℕ)) μ.cells) → x✝ ∈ ↑(↑(Equiv.finsetCongr (Equiv.prodComm ℕ ℕ)) μ.cells)
[PROOFSTEP]
simp only [Finset.mem_coe, Equiv.finsetCongr_apply, Finset.mem_map_equiv]
[GOAL]
μ : YoungDiagram
x✝¹ x✝ : ℕ × ℕ
h : x✝ ≤ x✝¹
⊢ ↑(Equiv.prodComm ℕ ℕ).symm x✝¹ ∈ μ.cells → ↑(Equiv.prodComm ℕ ℕ).symm x✝ ∈ μ.cells
[PROOFSTEP]
intro hcell
[GOAL]
μ : YoungDiagram
x✝¹ x✝ : ℕ × ℕ
h : x✝ ≤ x✝¹
hcell : ↑(Equiv.prodComm ℕ ℕ).symm x✝¹ ∈ μ.cells
⊢ ↑(Equiv.prodComm ℕ ℕ).symm x✝ ∈ μ.cells
[PROOFSTEP]
apply μ.isLowerSet _ hcell
[GOAL]
μ : YoungDiagram
x✝¹ x✝ : ℕ × ℕ
h : x✝ ≤ x✝¹
hcell : ↑(Equiv.prodComm ℕ ℕ).symm x✝¹ ∈ μ.cells
⊢ ↑(Equiv.prodComm ℕ ℕ).symm x✝ ≤ ↑(Equiv.prodComm ℕ ℕ).symm x✝¹
[PROOFSTEP]
simp [h]
[GOAL]
μ : YoungDiagram
c : ℕ × ℕ
⊢ c ∈ transpose μ ↔ Prod.swap c ∈ μ
[PROOFSTEP]
simp [transpose]
[GOAL]
μ : YoungDiagram
⊢ transpose (transpose μ) = μ
[PROOFSTEP]
ext x
[GOAL]
case cells.a
μ : YoungDiagram
x : ℕ × ℕ
⊢ x ∈ (transpose (transpose μ)).cells ↔ x ∈ μ.cells
[PROOFSTEP]
simp
[GOAL]
μ ν : YoungDiagram
⊢ transpose μ = ν ↔ μ = transpose ν
[PROOFSTEP]
constructor
[GOAL]
case mp
μ ν : YoungDiagram
⊢ transpose μ = ν → μ = transpose ν
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
μ : YoungDiagram
⊢ μ = transpose (transpose μ)
[PROOFSTEP]
simp
[GOAL]
case mpr
μ ν : YoungDiagram
⊢ μ = transpose ν → transpose μ = ν
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
ν : YoungDiagram
⊢ transpose (transpose ν) = ν
[PROOFSTEP]
simp
[GOAL]
μ ν : YoungDiagram
⊢ transpose μ = transpose ν ↔ μ = ν
[PROOFSTEP]
rw [transpose_eq_iff_eq_transpose]
[GOAL]
μ ν : YoungDiagram
⊢ μ = transpose (transpose ν) ↔ μ = ν
[PROOFSTEP]
simp
[GOAL]
μ ν : YoungDiagram
h_le : transpose μ ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ c ∈ (transpose ν).cells
[PROOFSTEP]
simp only [mem_cells, mem_transpose]
[GOAL]
μ ν : YoungDiagram
h_le : transpose μ ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ Prod.swap c ∈ ν
[PROOFSTEP]
apply h_le
[GOAL]
case a
μ ν : YoungDiagram
h_le : transpose μ ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ Prod.swap c ∈ (transpose μ).cells
[PROOFSTEP]
simpa
[GOAL]
μ ν : YoungDiagram
h : transpose μ ≤ transpose ν
⊢ μ ≤ ν
[PROOFSTEP]
convert YoungDiagram.le_of_transpose_le h
[GOAL]
case h.e'_4
μ ν : YoungDiagram
h : transpose μ ≤ transpose ν
⊢ ν = transpose (transpose ν)
[PROOFSTEP]
simp
[GOAL]
μ ν : YoungDiagram
h : μ ≤ ν
⊢ transpose μ ≤ transpose ν
[PROOFSTEP]
rw [← transpose_transpose μ] at h
[GOAL]
μ ν : YoungDiagram
h : transpose (transpose μ) ≤ ν
⊢ transpose μ ≤ transpose ν
[PROOFSTEP]
exact YoungDiagram.le_of_transpose_le h
[GOAL]
x✝ : YoungDiagram
⊢ transpose (transpose x✝) = x✝
[PROOFSTEP]
simp
[GOAL]
x✝ : YoungDiagram
⊢ transpose (transpose x✝) = x✝
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ {a b : YoungDiagram},
    ↑{ toFun := transpose, invFun := transpose, left_inv := (_ : ∀ (x : YoungDiagram), transpose (transpose x) = x),
              right_inv := (_ : ∀ (x : YoungDiagram), transpose (transpose x) = x) }
          a ≤
        ↑{ toFun := transpose, invFun := transpose, left_inv := (_ : ∀ (x : YoungDiagram), transpose (transpose x) = x),
              right_inv := (_ : ∀ (x : YoungDiagram), transpose (transpose x) = x) }
          b ↔
      a ≤ b
[PROOFSTEP]
simp
[GOAL]
μ : YoungDiagram
i : ℕ
c : ℕ × ℕ
⊢ c ∈ row μ i ↔ c ∈ μ ∧ c.fst = i
[PROOFSTEP]
simp [row]
[GOAL]
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ row μ i ↔ (i, j) ∈ μ
[PROOFSTEP]
simp [row]
[GOAL]
μ : YoungDiagram
i : ℕ
⊢ ∃ j, ¬(i, j) ∈ μ
[PROOFSTEP]
obtain ⟨j, hj⟩ :=
  Infinite.exists_not_mem_finset
    (μ.cells.preimage (Prod.mk i) fun _ _ _ _ h => by
      cases h
      rfl)
[GOAL]
μ : YoungDiagram
i x✝³ : ℕ
x✝² : x✝³ ∈ Prod.mk i ⁻¹' ↑μ.cells
x✝¹ : ℕ
x✝ : x✝¹ ∈ Prod.mk i ⁻¹' ↑μ.cells
h : (i, x✝³) = (i, x✝¹)
⊢ x✝³ = x✝¹
[PROOFSTEP]
cases h
[GOAL]
case refl
μ : YoungDiagram
i x✝² : ℕ
x✝¹ x✝ : x✝² ∈ Prod.mk i ⁻¹' ↑μ.cells
⊢ x✝² = x✝²
[PROOFSTEP]
rfl
[GOAL]
case intro
μ : YoungDiagram
i j : ℕ
hj :
  ¬j ∈
      Finset.preimage μ.cells (Prod.mk i)
        (_ :
          ∀ (x : ℕ),
            x ∈ Prod.mk i ⁻¹' ↑μ.cells → ∀ (x_2 : ℕ), x_2 ∈ Prod.mk i ⁻¹' ↑μ.cells → (i, x) = (i, x_2) → x = x_2)
⊢ ∃ j, ¬(i, j) ∈ μ
[PROOFSTEP]
rw [Finset.mem_preimage] at hj
[GOAL]
case intro
μ : YoungDiagram
i j : ℕ
hj : ¬(i, j) ∈ μ.cells
⊢ ∃ j, ¬(i, j) ∈ μ
[PROOFSTEP]
exact ⟨j, hj⟩
[GOAL]
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ j < rowLen μ i
[PROOFSTEP]
rw [rowLen, Nat.lt_find_iff]
[GOAL]
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ (m : ℕ), m ≤ j → ¬¬(i, m) ∈ μ
[PROOFSTEP]
push_neg
[GOAL]
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ (m : ℕ), m ≤ j → (i, m) ∈ μ
[PROOFSTEP]
exact ⟨fun h _ hmj => μ.up_left_mem (by rfl) hmj h, fun h => h _ (by rfl)⟩
[GOAL]
μ : YoungDiagram
i j : ℕ
h : (i, j) ∈ μ
x✝ : ℕ
hmj : x✝ ≤ j
⊢ i ≤ i
[PROOFSTEP]
rfl
[GOAL]
μ : YoungDiagram
i j : ℕ
h : ∀ (m : ℕ), m ≤ j → (i, m) ∈ μ
⊢ j ≤ j
[PROOFSTEP]
rfl
[GOAL]
μ : YoungDiagram
i : ℕ
⊢ row μ i = {i} ×ˢ Finset.range (rowLen μ i)
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case a.mk
μ : YoungDiagram
i a b : ℕ
⊢ (a, b) ∈ row μ i ↔ (a, b) ∈ {i} ×ˢ Finset.range (rowLen μ i)
[PROOFSTEP]
simp only [Finset.mem_product, Finset.mem_singleton, Finset.mem_range, mem_row_iff, mem_iff_lt_rowLen, and_comm,
  and_congr_right_iff]
[GOAL]
case a.mk
μ : YoungDiagram
i a b : ℕ
⊢ a = i → (b < rowLen μ a ↔ b < rowLen μ i)
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk
μ : YoungDiagram
a b : ℕ
⊢ b < rowLen μ a ↔ b < rowLen μ a
[PROOFSTEP]
rfl
[GOAL]
μ : YoungDiagram
i : ℕ
⊢ rowLen μ i = Finset.card (row μ i)
[PROOFSTEP]
simp [row_eq_prod]
[GOAL]
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
⊢ rowLen μ i2 ≤ rowLen μ i1
[PROOFSTEP]
by_contra' h_lt
[GOAL]
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : rowLen μ i1 < rowLen μ i2
⊢ False
[PROOFSTEP]
rw [← lt_self_iff_false (μ.rowLen i1)]
[GOAL]
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : rowLen μ i1 < rowLen μ i2
⊢ rowLen μ i1 < rowLen μ i1
[PROOFSTEP]
rw [← mem_iff_lt_rowLen] at h_lt ⊢
[GOAL]
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, rowLen μ i1) ∈ μ
⊢ (i1, rowLen μ i1) ∈ μ
[PROOFSTEP]
exact μ.up_left_mem hi (by rfl) h_lt
[GOAL]
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, rowLen μ i1) ∈ μ
⊢ rowLen μ i1 ≤ rowLen μ i1
[PROOFSTEP]
rfl
[GOAL]
μ : YoungDiagram
j : ℕ
c : ℕ × ℕ
⊢ c ∈ col μ j ↔ c ∈ μ ∧ c.snd = j
[PROOFSTEP]
simp [col]
[GOAL]
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ col μ j ↔ (i, j) ∈ μ
[PROOFSTEP]
simp [col]
[GOAL]
μ : YoungDiagram
j : ℕ
⊢ ∃ i, ¬(i, j) ∈ μ.cells
[PROOFSTEP]
convert μ.transpose.exists_not_mem_row j using 1
[GOAL]
case h.e'_2
μ : YoungDiagram
j : ℕ
⊢ (fun i => ¬(i, j) ∈ μ.cells) = fun j_1 => ¬(j, j_1) ∈ transpose μ
[PROOFSTEP]
simp
[GOAL]
μ : YoungDiagram
j : ℕ
⊢ colLen (transpose μ) j = rowLen μ j
[PROOFSTEP]
simp [rowLen, colLen]
[GOAL]
μ : YoungDiagram
i : ℕ
⊢ rowLen (transpose μ) i = colLen μ i
[PROOFSTEP]
simp [rowLen, colLen]
[GOAL]
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ i < colLen μ j
[PROOFSTEP]
rw [← rowLen_transpose, ← mem_iff_lt_rowLen]
[GOAL]
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ (j, i) ∈ transpose μ
[PROOFSTEP]
simp
[GOAL]
μ : YoungDiagram
j : ℕ
⊢ col μ j = Finset.range (colLen μ j) ×ˢ {j}
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case a.mk
μ : YoungDiagram
j a b : ℕ
⊢ (a, b) ∈ col μ j ↔ (a, b) ∈ Finset.range (colLen μ j) ×ˢ {j}
[PROOFSTEP]
simp only [Finset.mem_product, Finset.mem_singleton, Finset.mem_range, mem_col_iff, mem_iff_lt_colLen, and_comm,
  and_congr_right_iff]
[GOAL]
case a.mk
μ : YoungDiagram
j a b : ℕ
⊢ b = j → (a < colLen μ b ↔ a < colLen μ j)
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk
μ : YoungDiagram
a b : ℕ
⊢ a < colLen μ b ↔ a < colLen μ b
[PROOFSTEP]
rfl
[GOAL]
μ : YoungDiagram
j : ℕ
⊢ colLen μ j = Finset.card (col μ j)
[PROOFSTEP]
simp [col_eq_prod]
[GOAL]
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ colLen μ j2 ≤ colLen μ j1
[PROOFSTEP]
convert μ.transpose.rowLen_anti j1 j2 hj using 1
[GOAL]
case h.e'_3
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ colLen μ j2 = rowLen (transpose μ) j2
[PROOFSTEP]
simp
[GOAL]
case h.e'_4
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ colLen μ j1 = rowLen (transpose μ) j1
[PROOFSTEP]
simp
[GOAL]
μ : YoungDiagram
i : Fin (List.length (rowLens μ))
⊢ List.get (rowLens μ) i = rowLen μ ↑i
[PROOFSTEP]
simp only [rowLens, List.get_range, List.get_map]
[GOAL]
μ : YoungDiagram
⊢ List.length (rowLens μ) = colLen μ 0
[PROOFSTEP]
simp only [rowLens, List.length_map, List.length_range]
[GOAL]
μ : YoungDiagram
x : ℕ
hx : x ∈ rowLens μ
⊢ 0 < x
[PROOFSTEP]
rw [rowLens, List.mem_map] at hx
[GOAL]
μ : YoungDiagram
x : ℕ
hx : ∃ a, a ∈ List.range (colLen μ 0) ∧ rowLen μ a = x
⊢ 0 < x
[PROOFSTEP]
obtain ⟨i, hi, rfl : μ.rowLen i = x⟩ := hx
[GOAL]
case intro.intro
μ : YoungDiagram
i : ℕ
hi : i ∈ List.range (colLen μ 0)
⊢ 0 < rowLen μ i
[PROOFSTEP]
rwa [List.mem_range, ← mem_iff_lt_colLen, mem_iff_lt_rowLen] at hi
[GOAL]
w : List ℕ
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens w ↔ ∃ h, c.snd < List.get w { val := c.fst, isLt := h }
[PROOFSTEP]
induction' w with w_hd w_tl w_ih generalizing c
[GOAL]
case nil
c✝ c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens [] ↔ ∃ h, c.snd < List.get [] { val := c.fst, isLt := h }
[PROOFSTEP]
rw [YoungDiagram.cellsOfRowLens]
[GOAL]
case cons
c✝ : ℕ × ℕ
w_hd : ℕ
w_tl : List ℕ
w_ih : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens w_tl ↔ ∃ h, c.snd < List.get w_tl { val := c.fst, isLt := h }
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens (w_hd :: w_tl) ↔ ∃ h, c.snd < List.get (w_hd :: w_tl) { val := c.fst, isLt := h }
[PROOFSTEP]
rw [YoungDiagram.cellsOfRowLens]
[GOAL]
case nil
c✝ c : ℕ × ℕ
⊢ c ∈ ∅ ↔ ∃ h, c.snd < List.get [] { val := c.fst, isLt := h }
[PROOFSTEP]
simp [YoungDiagram.cellsOfRowLens]
[GOAL]
case cons
c✝ : ℕ × ℕ
w_hd : ℕ
w_tl : List ℕ
w_ih : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens w_tl ↔ ∃ h, c.snd < List.get w_tl { val := c.fst, isLt := h }
c : ℕ × ℕ
⊢ c ∈
      {0} ×ˢ Finset.range w_hd ∪
        Finset.map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens w_tl) ↔
    ∃ h, c.snd < List.get (w_hd :: w_tl) { val := c.fst, isLt := h }
[PROOFSTEP]
rcases c with ⟨⟨_, _⟩, _⟩
[GOAL]
case cons.mk.zero
c : ℕ × ℕ
w_hd : ℕ
w_tl : List ℕ
w_ih : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens w_tl ↔ ∃ h, c.snd < List.get w_tl { val := c.fst, isLt := h }
snd✝ : ℕ
⊢ (Nat.zero, snd✝) ∈
      {0} ×ˢ Finset.range w_hd ∪
        Finset.map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens w_tl) ↔
    ∃ h, (Nat.zero, snd✝).snd < List.get (w_hd :: w_tl) { val := (Nat.zero, snd✝).fst, isLt := h }
[PROOFSTEP]
simp
  -- Porting note: was `simpa`
[GOAL]
case cons.mk.succ
c : ℕ × ℕ
w_hd : ℕ
w_tl : List ℕ
w_ih : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens w_tl ↔ ∃ h, c.snd < List.get w_tl { val := c.fst, isLt := h }
snd✝ n✝ : ℕ
⊢ (Nat.succ n✝, snd✝) ∈
      {0} ×ˢ Finset.range w_hd ∪
        Finset.map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens w_tl) ↔
    ∃ h, (Nat.succ n✝, snd✝).snd < List.get (w_hd :: w_tl) { val := (Nat.succ n✝, snd✝).fst, isLt := h }
[PROOFSTEP]
simp [w_ih, -Finset.singleton_product, Nat.succ_lt_succ_iff]
[GOAL]
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
⊢ IsLowerSet ↑(YoungDiagram.cellsOfRowLens w)
[PROOFSTEP]
rintro ⟨i2, j2⟩ ⟨i1, j1⟩ ⟨hi : i1 ≤ i2, hj : j1 ≤ j2⟩ hcell
[GOAL]
case mk.mk.intro
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
hcell : (i2, j2) ∈ ↑(YoungDiagram.cellsOfRowLens w)
⊢ (i1, j1) ∈ ↑(YoungDiagram.cellsOfRowLens w)
[PROOFSTEP]
rw [Finset.mem_coe, YoungDiagram.mem_cellsOfRowLens] at hcell ⊢
[GOAL]
case mk.mk.intro
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
hcell : ∃ h, (i2, j2).snd < List.get w { val := (i2, j2).fst, isLt := h }
⊢ ∃ h, (i1, j1).snd < List.get w { val := (i1, j1).fst, isLt := h }
[PROOFSTEP]
obtain ⟨h1, h2⟩ := hcell
[GOAL]
case mk.mk.intro.intro
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).fst < List.length w
h2 : (i2, j2).snd < List.get w { val := (i2, j2).fst, isLt := h1 }
⊢ ∃ h, (i1, j1).snd < List.get w { val := (i1, j1).fst, isLt := h }
[PROOFSTEP]
refine' ⟨hi.trans_lt h1, _⟩
[GOAL]
case mk.mk.intro.intro
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).fst < List.length w
h2 : (i2, j2).snd < List.get w { val := (i2, j2).fst, isLt := h1 }
⊢ (i1, j1).snd < List.get w { val := (i1, j1).fst, isLt := (_ : i1 < List.length w) }
[PROOFSTEP]
calc
  j1 ≤ j2 := hj
  _ < w.get ⟨i2, _⟩ := h2
  _ ≤ w.get ⟨i1, _⟩ := by
    obtain rfl | h := eq_or_lt_of_le hi
    · convert le_refl (w.get ⟨i1, h1⟩)
    · exact List.pairwise_iff_get.mp hw _ _ h
[GOAL]
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).fst < List.length w
h2 : (i2, j2).snd < List.get w { val := (i2, j2).fst, isLt := h1 }
⊢ List.get w { val := i2, isLt := h1 } ≤ List.get w { val := i1, isLt := (_ : i1 < List.length w) }
[PROOFSTEP]
obtain rfl | h := eq_or_lt_of_le hi
[GOAL]
case inl
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
j2 i1 j1 : ℕ
hj : j1 ≤ j2
hi : i1 ≤ i1
h1 : (i1, j2).fst < List.length w
h2 : (i1, j2).snd < List.get w { val := (i1, j2).fst, isLt := h1 }
⊢ List.get w { val := i1, isLt := h1 } ≤ List.get w { val := i1, isLt := (_ : i1 < List.length w) }
[PROOFSTEP]
convert le_refl (w.get ⟨i1, h1⟩)
[GOAL]
case inr
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).fst < List.length w
h2 : (i2, j2).snd < List.get w { val := (i2, j2).fst, isLt := h1 }
h : i1 < i2
⊢ List.get w { val := i2, isLt := h1 } ≤ List.get w { val := i1, isLt := (_ : i1 < List.length w) }
[PROOFSTEP]
exact List.pairwise_iff_get.mp hw _ _ h
[GOAL]
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
hpos : ∀ (x : ℕ), x ∈ w → 0 < x
⊢ List.length (rowLens (ofRowLens w hw)) = List.length w
[PROOFSTEP]
simp only [length_rowLens, colLen, Nat.find_eq_iff, mem_cells, mem_ofRowLens, lt_self_iff_false, IsEmpty.exists_iff,
  Classical.not_not]
[GOAL]
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
hpos : ∀ (x : ℕ), x ∈ w → 0 < x
⊢ True ∧ ∀ (n : ℕ), n < List.length w → ∃ h, 0 < List.get w { val := n, isLt := (_ : (n, 0).fst < List.length w) }
[PROOFSTEP]
refine' ⟨True.intro, fun n hn => ⟨hn, hpos _ (List.get_mem _ _ hn)⟩⟩
[GOAL]
w : List ℕ
hw : List.Sorted (fun x x_1 => x ≥ x_1) w
i : Fin (List.length w)
⊢ rowLen (ofRowLens w hw) ↑i = List.get w i
[PROOFSTEP]
simp [rowLen, Nat.find_eq_iff, mem_ofRowLens]
[GOAL]
μ : YoungDiagram
⊢ ofRowLens (rowLens μ) (_ : List.Sorted (fun x x_1 => x ≥ x_1) (rowLens μ)) = μ
[PROOFSTEP]
ext ⟨i, j⟩
[GOAL]
case cells.a.mk
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ (ofRowLens (rowLens μ) (_ : List.Sorted (fun x x_1 => x ≥ x_1) (rowLens μ))).cells ↔ (i, j) ∈ μ.cells
[PROOFSTEP]
simp only [mem_cells, mem_ofRowLens, length_rowLens, get_rowLens]
[GOAL]
case cells.a.mk
μ : YoungDiagram
i j : ℕ
⊢ (∃ h, j < rowLen μ i) ↔ (i, j) ∈ μ
[PROOFSTEP]
simpa [← mem_iff_lt_colLen, mem_iff_lt_rowLen] using j.zero_le.trans_lt


[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]


[GOAL]
α : Type u_1
n : ℕ
p q : Partition n
⊢ Decidable (p = q)
[PROOFSTEP]
simp [Partition.ext_iff]
[GOAL]
α : Type u_1
n : ℕ
p q : Partition n
⊢ Decidable (p.parts = q.parts)
[PROOFSTEP]
exact decidableEq p.parts q.parts
[GOAL]
α : Type u_1
n : ℕ
c : Composition n
⊢ sum ↑c.blocks = n
[PROOFSTEP]
rw [Multiset.coe_sum, c.blocks_sum]
[GOAL]
α : Type u_1
n : ℕ
⊢ Function.Surjective (ofComposition n)
[PROOFSTEP]
rintro ⟨b, hb₁, hb₂⟩
[GOAL]
case mk
α : Type u_1
n : ℕ
b : Multiset ℕ
hb₁ : ∀ {i : ℕ}, i ∈ b → 0 < i
hb₂ : sum b = n
⊢ ∃ a, ofComposition n a = { parts := b, parts_pos := hb₁, parts_sum := hb₂ }
[PROOFSTEP]
rcases Quotient.exists_rep b with ⟨b, rfl⟩
[GOAL]
case mk.intro
α : Type u_1
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ Quotient.mk (List.isSetoid ℕ) b → 0 < i
hb₂ : sum (Quotient.mk (List.isSetoid ℕ) b) = n
⊢ ∃ a, ofComposition n a = { parts := Quotient.mk (List.isSetoid ℕ) b, parts_pos := hb₁, parts_sum := hb₂ }
[PROOFSTEP]
refine' ⟨⟨b, fun {i} hi => hb₁ hi, _⟩, Partition.ext _ _ rfl⟩
[GOAL]
case mk.intro
α : Type u_1
n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ Quotient.mk (List.isSetoid ℕ) b → 0 < i
hb₂ : sum (Quotient.mk (List.isSetoid ℕ) b) = n
⊢ List.sum b = n
[PROOFSTEP]
simpa using hb₂
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
i : ℕ
hi : i ∈ filter (fun x => x ≠ 0) l
⊢ i ≠ 0
[PROOFSTEP]
apply of_mem_filter hi
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
⊢ sum (filter (fun x => x ≠ 0) l) = n
[PROOFSTEP]
have lt : l.filter (· = 0) + l.filter (· ≠ 0) = l := filter_add_not _ l
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
lt : filter (fun x => x = 0) l + filter (fun x => x ≠ 0) l = l
⊢ sum (filter (fun x => x ≠ 0) l) = n
[PROOFSTEP]
apply_fun Multiset.sum at lt
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
lt : sum (filter (fun x => x = 0) l + filter (fun x => x ≠ 0) l) = sum l
⊢ sum (filter (fun x => x ≠ 0) l) = n
[PROOFSTEP]
have lz : (l.filter (· = 0)).sum = 0 := by
  rw [Multiset.sum_eq_zero_iff]
  simp
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
lt : sum (filter (fun x => x = 0) l + filter (fun x => x ≠ 0) l) = sum l
⊢ sum (filter (fun x => x = 0) l) = 0
[PROOFSTEP]
rw [Multiset.sum_eq_zero_iff]
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
lt : sum (filter (fun x => x = 0) l + filter (fun x => x ≠ 0) l) = sum l
⊢ ∀ (x : ℕ), x ∈ filter (fun x => x = 0) l → x = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
n : ℕ
l : Multiset ℕ
hl : sum l = n
lt : sum (filter (fun x => x = 0) l + filter (fun x => x ≠ 0) l) = sum l
lz : sum (filter (fun x => x = 0) l) = 0
⊢ sum (filter (fun x => x ≠ 0) l) = n
[PROOFSTEP]
rwa [sum_add (filter (fun x => x = 0) l) (filter (fun x => ¬x = 0) l), lz, hl, zero_add] at lt