μ ν : YoungDiagram
h_le : transpose μ ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ Prod.swap c ∈ ν
μ ν : YoungDiagram
h_le : transpose μ ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ c ∈ (transpose ν).cells
simp only [mem_cells, mem_transpose]
case a
μ ν : YoungDiagram
h_le : transpose μ ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ Prod.swap c ∈ (transpose μ).cells
μ ν : YoungDiagram
h_le : transpose μ ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ Prod.swap c ∈ ν
apply h_le
no goals
case a
μ ν : YoungDiagram
h_le : transpose μ ≤ ν
c : ℕ × ℕ
hc : c ∈ μ.cells
⊢ Prod.swap c ∈ (transpose μ).cells
simpa