μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ (m : ℕ), m ≤ j → ¬¬(i, m) ∈ μ
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ j < rowLen μ i
rw [rowLen, Nat.lt_find_iff]
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ (m : ℕ), m ≤ j → (i, m) ∈ μ
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ (m : ℕ), m ≤ j → ¬¬(i, m) ∈ μ
push_neg
no goals
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ (m : ℕ), m ≤ j → (i, m) ∈ μ
exact ⟨fun h _ hmj => μ.up_left_mem (by rfl) hmj h, fun h => h _ (by rfl)⟩
no goals
μ : YoungDiagram
i j : ℕ
h : (i, j) ∈ μ
x✝ : ℕ
hmj : x✝ ≤ j
⊢ i ≤ i
rfl
no goals
μ : YoungDiagram
i j : ℕ
h : ∀ (m : ℕ), m ≤ j → (i, m) ∈ μ
⊢ j ≤ j
rfl