case inl
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 = j2
⊢ ↑T i j1 ≤ ↑T i j2

case inr
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ ↑T i j1 ≤ ↑T i j2
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
⊢ ↑T i j1 ≤ ↑T i j2
cases' eq_or_lt_of_le hj with h h
case inr
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ ↑T i j1 ≤ ↑T i j2
case inl
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 = j2
⊢ ↑T i j1 ≤ ↑T i j2

case inr
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ ↑T i j1 ≤ ↑T i j2
. rw [h]
no goals
case inr
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ ↑T i j1 ≤ ↑T i j2
. exact T.row_weak h cell
no goals
case inl
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 = j2
⊢ ↑T i j1 ≤ ↑T i j2
rw [h]
no goals
case inr
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ ↑T i j1 ≤ ↑T i j2
exact T.row_weak h cell