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