μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ (j, i) ∈ transpose μ
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ i < colLen μ j
rw [← rowLen_transpose, ← mem_iff_lt_rowLen]
no goals
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ (j, i) ∈ transpose μ
simp