case intro
μ : YoungDiagram
i j : ℕ
hj :
  ¬j ∈
      Finset.preimage μ.cells (Prod.mk i)
        (_ :
          ∀ (x : ℕ),
            x ∈ Prod.mk i ⁻¹' ↑μ.cells → ∀ (x_2 : ℕ), x_2 ∈ Prod.mk i ⁻¹' ↑μ.cells → (i, x) = (i, x_2) → x = x_2)
⊢ ∃ j, ¬(i, j) ∈ μ
μ : YoungDiagram
i : ℕ
⊢ ∃ j, ¬(i, j) ∈ μ
obtain ⟨j, hj⟩ :=
  Infinite.exists_not_mem_finset
    (μ.cells.preimage (Prod.mk i) fun _ _ _ _ h => by
      cases h
      rfl)
case intro
μ : YoungDiagram
i j : ℕ
hj : ¬(i, j) ∈ μ.cells
⊢ ∃ j, ¬(i, j) ∈ μ

μ : YoungDiagram
i x✝³ : ℕ
x✝² : x✝³ ∈ Prod.mk i ⁻¹' ↑μ.cells
x✝¹ : ℕ
x✝ : x✝¹ ∈ Prod.mk i ⁻¹' ↑μ.cells
h : (i, x✝³) = (i, x✝¹)
⊢ x✝³ = x✝¹
case intro
μ : YoungDiagram
i j : ℕ
hj :
  ¬j ∈
      Finset.preimage μ.cells (Prod.mk i)
        (_ :
          ∀ (x : ℕ),
            x ∈ Prod.mk i ⁻¹' ↑μ.cells → ∀ (x_2 : ℕ), x_2 ∈ Prod.mk i ⁻¹' ↑μ.cells → (i, x) = (i, x_2) → x = x_2)
⊢ ∃ j, ¬(i, j) ∈ μ
rw [Finset.mem_preimage] at hj
no goals
case intro
μ : YoungDiagram
i j : ℕ
hj : ¬(i, j) ∈ μ.cells
⊢ ∃ j, ¬(i, j) ∈ μ

μ : YoungDiagram
i x✝³ : ℕ
x✝² : x✝³ ∈ Prod.mk i ⁻¹' ↑μ.cells
x✝¹ : ℕ
x✝ : x✝¹ ∈ Prod.mk i ⁻¹' ↑μ.cells
h : (i, x✝³) = (i, x✝¹)
⊢ x✝³ = x✝¹
exact ⟨j, hj⟩
case refl
μ : YoungDiagram
i x✝² : ℕ
x✝¹ x✝ : x✝² ∈ Prod.mk i ⁻¹' ↑μ.cells
⊢ x✝² = x✝²
μ : YoungDiagram
i x✝³ : ℕ
x✝² : x✝³ ∈ Prod.mk i ⁻¹' ↑μ.cells
x✝¹ : ℕ
x✝ : x✝¹ ∈ Prod.mk i ⁻¹' ↑μ.cells
h : (i, x✝³) = (i, x✝¹)
⊢ x✝³ = x✝¹
cases h
no goals
case refl
μ : YoungDiagram
i x✝² : ℕ
x✝¹ x✝ : x✝² ∈ Prod.mk i ⁻¹' ↑μ.cells
⊢ x✝² = x✝²
rfl