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
μ : YoungDiagram
⊢ ofRowLens (rowLens μ) (_ : List.Sorted (fun x x_1 => x ≥ x_1) (rowLens μ)) = μ
ext ⟨i, j⟩
case cells.a.mk
μ : YoungDiagram
i j : ℕ
⊢ (∃ h, j < rowLen μ i) ↔ (i, j) ∈ μ
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
simp only [mem_cells, mem_ofRowLens, length_rowLens, get_rowLens]
no goals
case cells.a.mk
μ : YoungDiagram
i j : ℕ
⊢ (∃ h, j < rowLen μ i) ↔ (i, j) ∈ μ
simpa [← mem_iff_lt_colLen, mem_iff_lt_rowLen] using j.zero_le.trans_lt