case cells.a
μ : YoungDiagram
x : ℕ × ℕ
⊢ x ∈ (transpose (transpose μ)).cells ↔ x ∈ μ.cells
μ : YoungDiagram
⊢ transpose (transpose μ) = μ
ext x
no goals
case cells.a
μ : YoungDiagram
x : ℕ × ℕ
⊢ x ∈ (transpose (transpose μ)).cells ↔ x ∈ μ.cells
simp