case a.mk
μ : YoungDiagram
i a b : ℕ
⊢ (a, b) ∈ row μ i ↔ (a, b) ∈ {i} ×ˢ Finset.range (rowLen μ i)
μ : YoungDiagram
i : ℕ
⊢ row μ i = {i} ×ˢ Finset.range (rowLen μ i)
ext ⟨a, b⟩
case a.mk
μ : YoungDiagram
i a b : ℕ
⊢ a = i → (b < rowLen μ a ↔ b < rowLen μ i)
case a.mk
μ : YoungDiagram
i a b : ℕ
⊢ (a, b) ∈ row μ i ↔ (a, b) ∈ {i} ×ˢ Finset.range (rowLen μ i)
simp only [Finset.mem_product, Finset.mem_singleton, Finset.mem_range, mem_row_iff,
  mem_iff_lt_rowLen, and_comm, and_congr_right_iff]
case a.mk
μ : YoungDiagram
a b : ℕ
⊢ b < rowLen μ a ↔ b < rowLen μ a
case a.mk
μ : YoungDiagram
i a b : ℕ
⊢ a = i → (b < rowLen μ a ↔ b < rowLen μ i)
rintro rfl
no goals
case a.mk
μ : YoungDiagram
a b : ℕ
⊢ b < rowLen μ a ↔ b < rowLen μ a
rfl