case inl
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 = i2
⊢ ↑T i1 j ≤ ↑T i2 j

case inr
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ ↑T i1 j ≤ ↑T i2 j
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
⊢ ↑T i1 j ≤ ↑T i2 j
cases' eq_or_lt_of_le hi with h h
case inr
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ ↑T i1 j ≤ ↑T i2 j
case inl
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 = i2
⊢ ↑T i1 j ≤ ↑T i2 j

case inr
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ ↑T i1 j ≤ ↑T i2 j
. rw [h]
no goals
case inr
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ ↑T i1 j ≤ ↑T i2 j
. exact le_of_lt (T.col_strict h cell)
no goals
case inl
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 = i2
⊢ ↑T i1 j ≤ ↑T i2 j
rw [h]
no goals
case inr
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ ↑T i1 j ≤ ↑T i2 j
exact le_of_lt (T.col_strict h cell)