[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
