case h.e'_2
μ : YoungDiagram
j : ℕ
⊢ (fun i => ¬(i, j) ∈ μ.cells) = fun j_1 => ¬(j, j_1) ∈ transpose μ
μ : YoungDiagram
j : ℕ
⊢ ∃ i, ¬(i, j) ∈ μ.cells
convert μ.transpose.exists_not_mem_row j using 1
no goals
case h.e'_2
μ : YoungDiagram
j : ℕ
⊢ (fun i => ¬(i, j) ∈ μ.cells) = fun j_1 => ¬(j, j_1) ∈ transpose μ
simp