μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : rowLen μ i1 < rowLen μ i2
⊢ False
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
⊢ rowLen μ i2 ≤ rowLen μ i1
by_contra' h_lt
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : rowLen μ i1 < rowLen μ i2
⊢ rowLen μ i1 < rowLen μ i1
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : rowLen μ i1 < rowLen μ i2
⊢ False
rw [← lt_self_iff_false (μ.rowLen i1)]
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, rowLen μ i1) ∈ μ
⊢ (i1, rowLen μ i1) ∈ μ
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : rowLen μ i1 < rowLen μ i2
⊢ rowLen μ i1 < rowLen μ i1
rw [← mem_iff_lt_rowLen] at h_lt⊢
no goals
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, rowLen μ i1) ∈ μ
⊢ (i1, rowLen μ i1) ∈ μ
exact μ.up_left_mem hi (by rfl) h_lt
no goals
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, rowLen μ i1) ∈ μ
⊢ rowLen μ i1 ≤ rowLen μ i1
rfl