[GOAL]
μ : YoungDiagram
T T' : Ssyt μ
h : T.entry = T'.entry
⊢ T = T'
[PROOFSTEP]
cases T
[GOAL]
case mk
μ : YoungDiagram
T' : Ssyt μ
entry✝ : ℕ → ℕ → ℕ
row_weak'✝ : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry✝ i j1 ≤ entry✝ i j2
col_strict'✝ : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry✝ i1 j < entry✝ i2 j
zeros'✝ : ∀ {i j : ℕ}, ¬(i, j) ∈ μ → entry✝ i j = 0
h : { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ }.entry = T'.entry
⊢ { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ } = T'
[PROOFSTEP]
cases T'
[GOAL]
case mk.mk
μ : YoungDiagram
entry✝¹ : ℕ → ℕ → ℕ
row_weak'✝¹ : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry✝¹ i j1 ≤ entry✝¹ i j2
col_strict'✝¹ : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry✝¹ i1 j < entry✝¹ i2 j
zeros'✝¹ : ∀ {i j : ℕ}, ¬(i, j) ∈ μ → entry✝¹ i j = 0
entry✝ : ℕ → ℕ → ℕ
row_weak'✝ : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry✝ i j1 ≤ entry✝ i j2
col_strict'✝ : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry✝ i1 j < entry✝ i2 j
zeros'✝ : ∀ {i j : ℕ}, ¬(i, j) ∈ μ → entry✝ i j = 0
h :
  { entry := entry✝¹, row_weak' := row_weak'✝¹, col_strict' := col_strict'✝¹, zeros' := zeros'✝¹ }.entry =
    { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ }.entry
⊢ { entry := entry✝¹, row_weak' := row_weak'✝¹, col_strict' := col_strict'✝¹, zeros' := zeros'✝¹ } =
    { entry := entry✝, row_weak' := row_weak'✝, col_strict' := col_strict'✝, zeros' := zeros'✝ }
[PROOFSTEP]
congr
[GOAL]
μ : YoungDiagram
T T' : Ssyt μ
h : ∀ (i j : ℕ), ↑T i j = ↑T' i j
x✝ : ℕ
⊢ ↑T x✝ = ↑T' x✝
[PROOFSTEP]
funext
[GOAL]
case h
μ : YoungDiagram
T T' : Ssyt μ
h : ∀ (i j : ℕ), ↑T i j = ↑T' i j
x✝¹ x✝ : ℕ
⊢ ↑T x✝¹ x✝ = ↑T' x✝¹ x✝
[PROOFSTEP]
apply h
[GOAL]
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
⊢ ↑T i j1 ≤ ↑T i j2
[PROOFSTEP]
cases' eq_or_lt_of_le hj with h h
[GOAL]
case inl
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 = j2
⊢ ↑T i j1 ≤ ↑T i j2
[PROOFSTEP]
rw [h]
[GOAL]
case inr
μ : YoungDiagram
T : Ssyt μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ ↑T i j1 ≤ ↑T i j2
[PROOFSTEP]
exact T.row_weak h cell
[GOAL]
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
⊢ ↑T i1 j ≤ ↑T i2 j
[PROOFSTEP]
cases' eq_or_lt_of_le hi with h h
[GOAL]
case inl
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 = i2
⊢ ↑T i1 j ≤ ↑T i2 j
[PROOFSTEP]
rw [h]
[GOAL]
case inr
μ : YoungDiagram
T : Ssyt μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ ↑T i1 j ≤ ↑T i2 j
[PROOFSTEP]
exact le_of_lt (T.col_strict h cell)
[GOAL]
μ : YoungDiagram
i✝ j1✝ j2✝ : ℕ
hj : j1✝ < j2✝
hcell : (i✝, j2✝) ∈ μ
⊢ (fun i j => if (i, j) ∈ μ then i else 0) i✝ j1✝ ≤ (fun i j => if (i, j) ∈ μ then i else 0) i✝ j2✝
[PROOFSTEP]
simp only
[GOAL]
μ : YoungDiagram
i✝ j1✝ j2✝ : ℕ
hj : j1✝ < j2✝
hcell : (i✝, j2✝) ∈ μ
⊢ (if (i✝, j1✝) ∈ μ then i✝ else 0) ≤ if (i✝, j2✝) ∈ μ then i✝ else 0
[PROOFSTEP]
rw [if_pos hcell, if_pos (μ.up_left_mem (by rfl) (le_of_lt hj) hcell)]
[GOAL]
μ : YoungDiagram
i✝ j1✝ j2✝ : ℕ
hj : j1✝ < j2✝
hcell : (i✝, j2✝) ∈ μ
⊢ i✝ ≤ i✝
[PROOFSTEP]
rfl
[GOAL]
μ : YoungDiagram
i1✝ i2✝ j✝ : ℕ
hi : i1✝ < i2✝
hcell : (i2✝, j✝) ∈ μ
⊢ (fun i j => if (i, j) ∈ μ then i else 0) i1✝ j✝ < (fun i j => if (i, j) ∈ μ then i else 0) i2✝ j✝
[PROOFSTEP]
simp only
[GOAL]
μ : YoungDiagram
i1✝ i2✝ j✝ : ℕ
hi : i1✝ < i2✝
hcell : (i2✝, j✝) ∈ μ
⊢ (if (i1✝, j✝) ∈ μ then i1✝ else 0) < if (i2✝, j✝) ∈ μ then i2✝ else 0
[PROOFSTEP]
rwa [if_pos hcell, if_pos (μ.up_left_mem (le_of_lt hi) (by rfl) hcell)]
[GOAL]
μ : YoungDiagram
i1✝ i2✝ j✝ : ℕ
hi : i1✝ < i2✝
hcell : (i2✝, j✝) ∈ μ
⊢ j✝ ≤ j✝
[PROOFSTEP]
rfl
