case h.e'_4
μ ν : YoungDiagram
h : transpose μ ≤ transpose ν
⊢ ν = transpose (transpose ν)
μ ν : YoungDiagram
h : transpose μ ≤ transpose ν
⊢ μ ≤ ν
convert YoungDiagram.le_of_transpose_le h
no goals
case h.e'_4
μ ν : YoungDiagram
h : transpose μ ≤ transpose ν
⊢ ν = transpose (transpose ν)
simp
μ ν : YoungDiagram
h : transpose (transpose μ) ≤ ν
⊢ transpose μ ≤ transpose ν
μ ν : YoungDiagram
h : μ ≤ ν
⊢ transpose μ ≤ transpose ν
rw [←transpose_transpose μ] at h
no goals
μ ν : YoungDiagram
h : transpose (transpose μ) ≤ ν
⊢ transpose μ ≤ transpose ν
exact YoungDiagram.le_of_transpose_le h