/-
SPDX-FileCopyrightText: 2026 Advameg, Inc.
SPDX-License-Identifier: Apache-2.0
-/

import Mathlib.Combinatorics.Hall.Finite
import Mathlib.Data.Fintype.EquivFin
import Mathlib.Data.Finset.Basic
import Mathlib.Order.Antichain
import Mathlib.Order.Basic
import Mathlib.Order.Preorder.Finite
import Mathlib.Tactic

/-!
# Dilworth Theorem Seed

This file prepares a finite-poset version of Dilworth's theorem:
width at most `k` implies a cover by `k` chains.
-/

namespace AtlasKnownTheorems.DilworthTheorem

variable {α : Type} [PartialOrder α] [DecidableEq α]

/-- A finite subset is a chain when every two members are comparable. -/
def IsChain (s : Finset α) : Prop :=
  ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ≤ b ∨ b ≤ a

/-- A finite subset is an antichain when distinct members are incomparable. -/
def IsAntichain (s : Finset α) : Prop :=
  ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬ a ≤ b ∧ ¬ b ≤ a

/-- Every antichain inside `U` has cardinality at most `k`. -/
def WidthAtMost (U : Finset α) (k : ℕ) : Prop :=
  ∀ s : Finset α, (∀ x, x ∈ s → x ∈ U) → IsAntichain s → s.card ≤ k

/-- A family of chains covers `U`. -/
def CoversByChains (U : Finset α) {k : ℕ} (chains : Fin k → Finset α) : Prop :=
  (∀ i, IsChain (chains i)) ∧ ∀ x, x ∈ U → ∃ i, x ∈ chains i

/-- A family of chains covers `U`, and each listed chain is contained in `U`. -/
def StrongCoversByChains (U : Finset α) {k : ℕ} (chains : Fin k → Finset α) : Prop :=
  (∀ i, IsChain (chains i)) ∧ (∀ i, chains i ⊆ U) ∧
    ∀ x, x ∈ U → ∃ i, x ∈ chains i

omit [DecidableEq α] in
/-- Minimal elements of a finite set in the inherited order. -/
noncomputable def minimalElements (U : Finset α) : Finset α := by
  classical
  exact U.filter fun x => ∀ ⦃y⦄, y ∈ U → y ≤ x → x ≤ y

/-- Antichains contained in a finite set. -/
noncomputable def antichainsIn (U : Finset α) : Finset (Finset α) := by
  classical
  exact U.powerset.filter IsAntichain

/-- Elements of `U` lying below some member of `A`. -/
noncomputable def lowerClosure (U A : Finset α) : Finset α := by
  classical
  exact U.filter fun x => ∃ a, a ∈ A ∧ x ≤ a

/-- Elements of `U` lying above some member of `A`. -/
noncomputable def upperClosure (U A : Finset α) : Finset α := by
  classical
  exact U.filter fun x => ∃ a, a ∈ A ∧ a ≤ x

/-- Minimum finite-poset Dilworth target. -/
def DilworthTheoremStatement : Prop :=
  ∀ (α : Type) [Fintype α] [DecidableEq α] [PartialOrder α] (k : ℕ),
    WidthAtMost (Finset.univ : Finset α) k →
      ∃ chains : Fin k → Finset α, CoversByChains (Finset.univ : Finset α) chains

omit [DecidableEq α] in
theorem isChain_empty :
    IsChain (∅ : Finset α) := by
  intro a ha
  simp at ha

omit [DecidableEq α] in
theorem isChain_singleton (a : α) :
    IsChain ({a} : Finset α) := by
  intro x hx y hy
  simp only [Finset.mem_singleton] at hx hy
  subst x
  subst y
  exact Or.inl le_rfl

omit [DecidableEq α] in
theorem isAntichain_empty :
    IsAntichain (∅ : Finset α) := by
  intro a ha
  simp at ha

omit [DecidableEq α] in
theorem isAntichain_singleton (a : α) :
    IsAntichain ({a} : Finset α) := by
  intro x hx y hy hxy
  simp only [Finset.mem_singleton] at hx hy
  subst x
  subst y
  exact (hxy rfl).elim

omit [DecidableEq α] in
theorem isChain_iff_set_isChain (s : Finset α) :
    IsChain s ↔ _root_.IsChain (· ≤ ·) (s : Set α) := by
  constructor
  · intro hs a ha b hb _hne
    exact hs ha hb
  · intro hs a ha b hb
    by_cases h : a = b
    · subst b
      exact Or.inl le_rfl
    · exact hs ha hb h

omit [DecidableEq α] in
theorem isAntichain_iff_set_isAntichain (s : Finset α) :
    IsAntichain s ↔ _root_.IsAntichain (· ≤ ·) (s : Set α) := by
  constructor
  · intro hs a ha b hb hne hle
    exact (hs ha hb hne).1 hle
  · intro hs a ha b hb hne
    exact ⟨fun hle => hs ha hb hne hle, fun hle => hs hb ha hne.symm hle⟩

omit [DecidableEq α] in
theorem IsChain.mono {s t : Finset α} (ht : IsChain t) (hst : s ⊆ t) :
    IsChain s := by
  intro a ha b hb
  exact ht (hst ha) (hst hb)

omit [DecidableEq α] in
theorem IsAntichain.mono {s t : Finset α} (ht : IsAntichain t) (hst : s ⊆ t) :
    IsAntichain s := by
  intro a ha b hb hne
  exact ht (hst ha) (hst hb) hne

theorem IsAntichain.insert {a : α} {s : Finset α} (hs : IsAntichain s)
    (ha : ∀ b, b ∈ s → ¬ a ≤ b ∧ ¬ b ≤ a) :
    IsAntichain (insert a s) := by
  intro x hx y hy hxy
  simp only [Finset.mem_insert] at hx hy
  rcases hx with rfl | hx <;> rcases hy with rfl | hy
  · exact (hxy rfl).elim
  · exact ha y hy
  · exact ⟨(ha x hx).2, (ha x hx).1⟩
  · exact hs hx hy hxy

theorem IsChain.insert_le {a : α} {s : Finset α} (hs : IsChain s)
    (ha : ∀ b, b ∈ s → a ≤ b) :
    IsChain (insert a s) := by
  intro x hx y hy
  simp only [Finset.mem_insert] at hx hy
  rcases hx with rfl | hx <;> rcases hy with rfl | hy
  · exact Or.inl le_rfl
  · exact Or.inl (ha y hy)
  · exact Or.inr (ha x hx)
  · exact hs hx hy

theorem IsChain.insert_ge {a : α} {s : Finset α} (hs : IsChain s)
    (ha : ∀ b, b ∈ s → b ≤ a) :
    IsChain (insert a s) := by
  intro x hx y hy
  simp only [Finset.mem_insert] at hx hy
  rcases hx with rfl | hx <;> rcases hy with rfl | hy
  · exact Or.inl le_rfl
  · exact Or.inr (ha y hy)
  · exact Or.inl (ha x hx)
  · exact hs hx hy

theorem isChain_pair_of_le {x y : α} (hxy : x ≤ y) :
    IsChain ({x, y} : Finset α) := by
  intro a ha b hb
  simp only [Finset.mem_insert, Finset.mem_singleton] at ha hb
  rcases ha with rfl | rfl <;> rcases hb with rfl | rfl
  · exact Or.inl le_rfl
  · exact Or.inl hxy
  · exact Or.inr hxy
  · exact Or.inl le_rfl

omit [DecidableEq α] in
theorem WidthAtMost.mono {U V : Finset α} {k : ℕ} (hV : WidthAtMost V k)
    (hUV : U ⊆ V) :
    WidthAtMost U k := by
  intro s hs hsAnti
  exact hV s (fun x hx => hUV (hs x hx)) hsAnti

omit [DecidableEq α] in
theorem CoversByChains.mono_set {U V : Finset α} {k : ℕ} {chains : Fin k → Finset α}
    (hV : CoversByChains V chains) (hUV : U ⊆ V) :
    CoversByChains U chains :=
  ⟨hV.1, fun x hx => hV.2 x (hUV hx)⟩

omit [DecidableEq α] in
theorem StrongCoversByChains.toCovers {U : Finset α} {k : ℕ}
    {chains : Fin k → Finset α} (h : StrongCoversByChains U chains) :
    CoversByChains U chains :=
  ⟨h.1, h.2.2⟩

theorem CoversByChains.toStrong {U : Finset α} {k : ℕ}
    {chains : Fin k → Finset α} (h : CoversByChains U chains) :
    StrongCoversByChains U fun i => chains i ∩ U := by
  refine ⟨?_, ?_, ?_⟩
  · intro i
    exact (h.1 i).mono (Finset.inter_subset_left)
  · intro i
    exact Finset.inter_subset_right
  · intro x hx
    obtain ⟨i, hxi⟩ := h.2 x hx
    exact ⟨i, Finset.mem_inter.mpr ⟨hxi, hx⟩⟩

omit [DecidableEq α] in
theorem StrongCoversByChains.mono_set {U V : Finset α} {k : ℕ}
    {chains : Fin k → Finset α} (hV : StrongCoversByChains V chains)
    (hUV : U ⊆ V) (hchains : ∀ i, chains i ⊆ U) :
    StrongCoversByChains U chains :=
  ⟨hV.1, hchains, fun x hx => hV.2.2 x (hUV hx)⟩

omit [DecidableEq α] in
theorem CoversByChains.extend {U : Finset α} {k l : ℕ} {chains : Fin k → Finset α}
    (h : CoversByChains U chains) (hkl : k ≤ l) :
    ∃ chains' : Fin l → Finset α, CoversByChains U chains' := by
  let chains' : Fin l → Finset α := fun j =>
    if hj : j.val < k then chains ⟨j.val, hj⟩ else ∅
  refine ⟨chains', ?_, ?_⟩
  · intro j
    by_cases hj : j.val < k
    · simpa [chains', hj] using h.1 ⟨j.val, hj⟩
    · simpa [chains', hj] using (isChain_empty (α := α))
  · intro x hx
    obtain ⟨i, hi⟩ := h.2 x hx
    refine ⟨⟨i.val, lt_of_lt_of_le i.isLt hkl⟩, ?_⟩
    have hiLt : (⟨i.val, lt_of_lt_of_le i.isLt hkl⟩ : Fin l).val < k := i.isLt
    simpa [chains', hiLt] using hi

omit [DecidableEq α] in
theorem StrongCoversByChains.extend {U : Finset α} {k l : ℕ} {chains : Fin k → Finset α}
    (h : StrongCoversByChains U chains) (hkl : k ≤ l) :
    ∃ chains' : Fin l → Finset α, StrongCoversByChains U chains' := by
  let chains' : Fin l → Finset α := fun j =>
    if hj : j.val < k then chains ⟨j.val, hj⟩ else ∅
  refine ⟨chains', ?_, ?_, ?_⟩
  · intro j
    by_cases hj : j.val < k
    · simpa [chains', hj] using h.1 ⟨j.val, hj⟩
    · simpa [chains', hj] using (isChain_empty (α := α))
  · intro j x hx
    by_cases hj : j.val < k
    · exact h.2.1 ⟨j.val, hj⟩ (by simpa [chains', hj] using hx)
    · simp [chains', hj] at hx
  · intro x hx
    obtain ⟨i, hi⟩ := h.2.2 x hx
    refine ⟨⟨i.val, lt_of_lt_of_le i.isLt hkl⟩, ?_⟩
    have hiLt : (⟨i.val, lt_of_lt_of_le i.isLt hkl⟩ : Fin l).val < k := i.isLt
    simpa [chains', hiLt] using hi

omit [DecidableEq α] in
theorem StrongCoversByChains.snoc {W U C : Finset α} {k : ℕ}
    {chains : Fin k → Finset α} (h : StrongCoversByChains W chains)
    (hWU : W ⊆ U) (hC_chain : IsChain C) (hCU : C ⊆ U)
    (hcoverU : ∀ x, x ∈ U → x ∈ W ∨ x ∈ C) :
    ∃ chains' : Fin (k + 1) → Finset α, StrongCoversByChains U chains' := by
  let chains' : Fin (k + 1) → Finset α := fun j =>
    if hj : j.val < k then chains ⟨j.val, hj⟩ else C
  refine ⟨chains', ?_, ?_, ?_⟩
  · intro j
    by_cases hj : j.val < k
    · simpa [chains', hj] using h.1 ⟨j.val, hj⟩
    · simpa [chains', hj] using hC_chain
  · intro j x hx
    by_cases hj : j.val < k
    · exact hWU (h.2.1 ⟨j.val, hj⟩ (by simpa [chains', hj] using hx))
    · exact hCU (by simpa [chains', hj] using hx)
  · intro x hx
    rcases hcoverU x hx with hxW | hxC
    · obtain ⟨i, hxi⟩ := h.2.2 x hxW
      refine ⟨⟨i.val, lt_trans i.isLt (Nat.lt_succ_self k)⟩, ?_⟩
      have hiLt : (⟨i.val, lt_trans i.isLt (Nat.lt_succ_self k)⟩ : Fin (k + 1)).val < k :=
        i.isLt
      simpa [chains', hiLt] using hxi
    · refine ⟨⟨k, Nat.lt_succ_self k⟩, ?_⟩
      have hnot : ¬ (⟨k, Nat.lt_succ_self k⟩ : Fin (k + 1)).val < k := by
        exact Nat.lt_irrefl k
      simpa [chains', hnot] using hxC

theorem StrongCoversByChains.snoc_erase_pair {U : Finset α} {x y : α} {k : ℕ}
    {chains : Fin k → Finset α}
    (h : StrongCoversByChains ((U.erase x).erase y) chains)
    (hxU : x ∈ U) (hyU : y ∈ U) (hxy : x ≤ y) :
    ∃ chains' : Fin (k + 1) → Finset α, StrongCoversByChains U chains' := by
  refine h.snoc (U := U) (C := ({x, y} : Finset α)) ?_ ?_ ?_ ?_
  · intro z hz
    exact Finset.erase_subset x U (Finset.erase_subset y (U.erase x) hz)
  · exact isChain_pair_of_le hxy
  · intro z hz
    simp only [Finset.mem_insert, Finset.mem_singleton] at hz
    rcases hz with rfl | rfl
    · exact hxU
    · exact hyU
  · intro z hzU
    by_cases hzx : z = x
    · exact Or.inr (by simp [hzx])
    by_cases hzy : z = y
    · exact Or.inr (by simp [hzy])
    · exact Or.inl (by simp [Finset.mem_erase, hzU, hzx, hzy])

omit [DecidableEq α] in
theorem mem_minimalElements {U : Finset α} {x : α} :
    x ∈ minimalElements U ↔ x ∈ U ∧ ∀ ⦃y⦄, y ∈ U → y ≤ x → x ≤ y := by
  classical
  simp [minimalElements]

omit [DecidableEq α] in
theorem minimalElements_subset (U : Finset α) :
    minimalElements U ⊆ U := by
  intro x hx
  exact (mem_minimalElements.mp hx).1

omit [DecidableEq α] in
theorem minimalElements_isAntichain (U : Finset α) :
    IsAntichain (minimalElements U) := by
  intro a ha b hb hne
  rw [mem_minimalElements] at ha hb
  refine ⟨?_, ?_⟩
  · intro hab
    have hba : b ≤ a := hb.2 ha.1 hab
    exact hne (le_antisymm hab hba)
  · intro hba
    have hab : a ≤ b := ha.2 hb.1 hba
    exact hne (le_antisymm hab hba)

omit [DecidableEq α] in
theorem minimalElements_nonempty {U : Finset α} (hU : U.Nonempty) :
    (minimalElements U).Nonempty := by
  obtain ⟨x, hx⟩ := U.exists_minimal hU
  refine ⟨x, ?_⟩
  rw [mem_minimalElements]
  exact ⟨hx.1, fun _ hy hyx => hx.2 hy hyx⟩

omit [DecidableEq α] in
theorem exists_minimal_le_maximal {U : Finset α} (hU : U.Nonempty) :
    ∃ x, x ∈ U ∧ (∀ z, z ∈ U → z ≤ x → x ≤ z) ∧
      ∃ y, y ∈ U ∧ (∀ z, z ∈ U → y ≤ z → z ≤ y) ∧ x ≤ y := by
  classical
  obtain ⟨x, hxMin⟩ := minimalElements_nonempty (α := α) hU
  have hxData := mem_minimalElements.mp hxMin
  let V : Finset α := U.filter fun z => x ≤ z
  have hV_nonempty : V.Nonempty := by
    refine ⟨x, ?_⟩
    simp [V, hxData.1]
  obtain ⟨y, hyMax⟩ := V.exists_maximal hV_nonempty
  have hyData : y ∈ U ∧ x ≤ y := by
    simpa [V] using hyMax.1
  refine ⟨x, hxData.1, (fun z hzU hzx => hxData.2 hzU hzx), y, hyData.1, ?_, hyData.2⟩
  intro z hzU hyz
  have hzV : z ∈ V := by
    simp [V, hzU, hyData.2.trans hyz]
  exact hyMax.2 hzV hyz

omit [DecidableEq α] in
theorem minimalElements_card_le_of_widthAtMost {U : Finset α} {k : ℕ}
    (hU : WidthAtMost U k) :
    (minimalElements U).card ≤ k :=
  hU (minimalElements U) (fun _ hx => minimalElements_subset U hx)
    (minimalElements_isAntichain U)

omit [DecidableEq α] in
theorem mem_antichainsIn {U s : Finset α} :
    s ∈ antichainsIn U ↔ s ⊆ U ∧ IsAntichain s := by
  classical
  simp [antichainsIn]

omit [DecidableEq α] in
theorem antichainsIn_nonempty (U : Finset α) :
    (antichainsIn U).Nonempty := by
  refine ⟨∅, ?_⟩
  rw [mem_antichainsIn]
  exact ⟨by intro x hx; simp at hx, isAntichain_empty⟩

omit [DecidableEq α] in
theorem exists_max_card_antichain (U : Finset α) :
    ∃ A : Finset α, A ⊆ U ∧ IsAntichain A ∧
      ∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ A.card := by
  obtain ⟨A, hAmax⟩ :=
    (antichainsIn U).exists_maximalFor (fun s : Finset α => s.card) (antichainsIn_nonempty U)
  have hAmem : A ∈ antichainsIn U := hAmax.1
  rw [mem_antichainsIn] at hAmem
  refine ⟨A, hAmem.1, hAmem.2, ?_⟩
  intro s hsU hsAnti
  have hs : s ∈ antichainsIn U := by
    rw [mem_antichainsIn]
    exact ⟨hsU, hsAnti⟩
  cases le_total s.card A.card with
  | inl hle => exact hle
  | inr hle => exact hAmax.2 hs hle

omit [DecidableEq α] in
theorem mem_lowerClosure {U A : Finset α} {x : α} :
    x ∈ lowerClosure U A ↔ x ∈ U ∧ ∃ a, a ∈ A ∧ x ≤ a := by
  classical
  simp [lowerClosure]

omit [DecidableEq α] in
theorem mem_upperClosure {U A : Finset α} {x : α} :
    x ∈ upperClosure U A ↔ x ∈ U ∧ ∃ a, a ∈ A ∧ a ≤ x := by
  classical
  simp [upperClosure]

omit [DecidableEq α] in
theorem lowerClosure_subset (U A : Finset α) :
    lowerClosure U A ⊆ U := by
  intro x hx
  exact (mem_lowerClosure.mp hx).1

omit [DecidableEq α] in
theorem upperClosure_subset (U A : Finset α) :
    upperClosure U A ⊆ U := by
  intro x hx
  exact (mem_upperClosure.mp hx).1

omit [DecidableEq α] in
theorem subset_lowerClosure {U A : Finset α} (hA : A ⊆ U) :
    A ⊆ lowerClosure U A := by
  intro x hx
  rw [mem_lowerClosure]
  exact ⟨hA hx, x, hx, le_rfl⟩

omit [DecidableEq α] in
theorem subset_upperClosure {U A : Finset α} (hA : A ⊆ U) :
    A ⊆ upperClosure U A := by
  intro x hx
  rw [mem_upperClosure]
  exact ⟨hA hx, x, hx, le_rfl⟩

theorem upperClosure_eq_of_lowerClosure_eq {U A : Finset α}
    (hA_sub : A ⊆ U) (hA_anti : IsAntichain A)
    (hlower : lowerClosure U A = U) :
    upperClosure U A = A := by
  apply Finset.Subset.antisymm
  · intro x hx
    obtain ⟨hxU, a, haA, hax⟩ := mem_upperClosure.mp hx
    have hxLower : x ∈ lowerClosure U A := by
      simpa [hlower] using hxU
    obtain ⟨_hxU, b, hbA, hxb⟩ := mem_lowerClosure.mp hxLower
    by_cases hab : a = b
    · subst b
      have hxa : x = a := le_antisymm hxb hax
      simpa [hxa] using haA
    · exact ((hA_anti haA hbA hab).1 (hax.trans hxb)).elim
  · exact subset_upperClosure hA_sub

theorem lowerClosure_eq_of_upperClosure_eq {U A : Finset α}
    (hA_sub : A ⊆ U) (hA_anti : IsAntichain A)
    (hupper : upperClosure U A = U) :
    lowerClosure U A = A := by
  apply Finset.Subset.antisymm
  · intro x hx
    obtain ⟨hxU, a, haA, hxa⟩ := mem_lowerClosure.mp hx
    have hxUpper : x ∈ upperClosure U A := by
      simpa [hupper] using hxU
    obtain ⟨_hxU, b, hbA, hbx⟩ := mem_upperClosure.mp hxUpper
    by_cases hba : b = a
    · subst b
      have hxa_eq : x = a := le_antisymm hxa hbx
      simpa [hxa_eq] using haA
    · exact ((hA_anti hbA haA hba).1 (hbx.trans hxa)).elim
  · exact subset_lowerClosure hA_sub

theorem exists_above_of_mem_sdiff_of_lowerClosure_eq {U A : Finset α}
    (hlower : lowerClosure U A = U) {x : α} (hx : x ∈ U \ A) :
    ∃ a, a ∈ A ∧ x ≤ a := by
  have hxLower : x ∈ lowerClosure U A := by
    rw [hlower]
    exact (Finset.mem_sdiff.mp hx).1
  exact (mem_lowerClosure.mp hxLower).2

theorem exists_below_of_mem_sdiff_of_upperClosure_eq {U A : Finset α}
    (hupper : upperClosure U A = U) {x : α} (hx : x ∈ U \ A) :
    ∃ a, a ∈ A ∧ a ≤ x := by
  have hxUpper : x ∈ upperClosure U A := by
    rw [hupper]
    exact (Finset.mem_sdiff.mp hx).1
  exact (mem_upperClosure.mp hxUpper).2

theorem widthAtMost_erase_pair_of_no_proper_max_antichain
    {U A : Finset α}
    (hA_max : ∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ A.card)
    (hA_pos : 0 < A.card)
    (hNoSplit :
      ∀ B : Finset α, B ⊆ U → IsAntichain B →
        (∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ B.card) →
        lowerClosure U B = U ∨ upperClosure U B = U)
    {x y : α} (hxU : x ∈ U) (hyU : y ∈ U)
    (hx_min : ∀ z, z ∈ U → z ≤ x → x ≤ z)
    (hy_max : ∀ z, z ∈ U → y ≤ z → z ≤ y) :
    WidthAtMost ((U.erase x).erase y) (A.card - 1) := by
  intro s hsW hsAnti
  by_contra hnot
  have hsU : s ⊆ U := by
    intro z hz
    exact Finset.erase_subset x U (Finset.erase_subset y (U.erase x) (hsW z hz))
  have hs_le_A : s.card ≤ A.card := hA_max s hsU hsAnti
  have hA_le_s : A.card ≤ s.card := by omega
  have hs_card_eq : s.card = A.card := le_antisymm hs_le_A hA_le_s
  have hs_max : ∀ t : Finset α, t ⊆ U → IsAntichain t → t.card ≤ s.card := by
    intro t htU htAnti
    simpa [hs_card_eq] using hA_max t htU htAnti
  rcases hNoSplit s hsU hsAnti hs_max with hlower | hupper
  · have hyLower : y ∈ lowerClosure U s := by
      rw [hlower]
      exact hyU
    obtain ⟨_hyU, b, hbS, hyb⟩ := mem_lowerClosure.mp hyLower
    have hby : b ≤ y := hy_max b (hsU hbS) hyb
    have hb_eq_y : b = y := le_antisymm hby hyb
    have hbW : b ∈ (U.erase x).erase y := hsW b hbS
    exact (Finset.mem_erase.mp hbW).1 hb_eq_y
  · have hxUpper : x ∈ upperClosure U s := by
      rw [hupper]
      exact hxU
    obtain ⟨_hxU, b, hbS, hbx⟩ := mem_upperClosure.mp hxUpper
    have hxb : x ≤ b := hx_min b (hsU hbS) hbx
    have hb_eq_x : b = x := le_antisymm hbx hxb
    have hbW : b ∈ (U.erase x).erase y := hsW b hbS
    exact (Finset.mem_erase.mp (Finset.mem_erase.mp hbW).2).1 hb_eq_x

theorem mem_lowerClosure_or_mem_upperClosure_of_max_card_antichain
    {U A : Finset α} (hA_sub : A ⊆ U) (hA_anti : IsAntichain A)
    (hA_max : ∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ A.card)
    {x : α} (hxU : x ∈ U) :
    x ∈ lowerClosure U A ∨ x ∈ upperClosure U A := by
  by_cases hxA : x ∈ A
  · exact Or.inl ((subset_lowerClosure hA_sub) hxA)
  by_cases hLower : ∃ a, a ∈ A ∧ x ≤ a
  · exact Or.inl (mem_lowerClosure.mpr ⟨hxU, hLower⟩)
  by_cases hUpper : ∃ a, a ∈ A ∧ a ≤ x
  · exact Or.inr (mem_upperClosure.mpr ⟨hxU, hUpper⟩)
  have hInsertAnti : IsAntichain (insert x A) := by
    exact hA_anti.insert fun a ha =>
      ⟨fun hxa => hLower ⟨a, ha, hxa⟩, fun hax => hUpper ⟨a, ha, hax⟩⟩
  have hInsertSub : insert x A ⊆ U := by
    intro y hy
    simp only [Finset.mem_insert] at hy
    rcases hy with rfl | hy
    · exact hxU
    · exact hA_sub hy
  have hcard_le : (insert x A).card ≤ A.card := hA_max (insert x A) hInsertSub hInsertAnti
  have hcard_eq : (insert x A).card = A.card + 1 := Finset.card_insert_of_notMem hxA
  omega

theorem lowerClosure_union_upperClosure_of_max_card_antichain
    {U A : Finset α} (hA_sub : A ⊆ U) (hA_anti : IsAntichain A)
    (hA_max : ∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ A.card) :
    U ⊆ lowerClosure U A ∪ upperClosure U A := by
  intro x hx
  exact Finset.mem_union.mpr
    (mem_lowerClosure_or_mem_upperClosure_of_max_card_antichain hA_sub hA_anti hA_max hx)

omit [DecidableEq α] in
theorem widthAtMost_max_card_antichain {U A : Finset α}
    (hA_max : ∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ A.card) :
    WidthAtMost U A.card := by
  intro s hsU hsAnti
  exact hA_max s hsU hsAnti

omit [DecidableEq α] in
theorem exists_max_card_antichain_of_widthAtMost {U : Finset α} {k : ℕ}
    (hU : WidthAtMost U k) :
    ∃ A : Finset α, A ⊆ U ∧ IsAntichain A ∧ A.card ≤ k ∧ WidthAtMost U A.card := by
  obtain ⟨A, hA_sub, hA_anti, hA_max⟩ := exists_max_card_antichain U
  exact ⟨A, hA_sub, hA_anti, hU A hA_sub hA_anti, widthAtMost_max_card_antichain hA_max⟩

omit [DecidableEq α] in
theorem widthAtMost_lowerClosure_of_max_card_antichain {U A : Finset α}
    (hA_max : ∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ A.card) :
    WidthAtMost (lowerClosure U A) A.card :=
  (widthAtMost_max_card_antichain hA_max).mono (lowerClosure_subset U A)

omit [DecidableEq α] in
theorem widthAtMost_upperClosure_of_max_card_antichain {U A : Finset α}
    (hA_max : ∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ A.card) :
    WidthAtMost (upperClosure U A) A.card :=
  (widthAtMost_max_card_antichain hA_max).mono (upperClosure_subset U A)

theorem exists_injective_above_of_max_card_antichain {U A B : Finset α}
    (hA_sub : A ⊆ U) (hA_anti : IsAntichain A)
    (hA_max : ∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ A.card)
    (hB_sub : B ⊆ U) (hB_anti : IsAntichain B)
    (hB_above : ∀ b, b ∈ B → ∃ a, a ∈ A ∧ b ≤ a) :
    ∃ f : B → A, Function.Injective f ∧ ∀ b : B, (b : α) ≤ (f b : α) := by
  classical
  let neigh : B → Finset A := fun b =>
    Finset.univ.filter fun a : A => (b : α) ≤ (a : α)
  have hhall : ∀ S : Finset B, S.card ≤ (S.biUnion neigh).card := by
    intro S
    by_contra hnot
    have hlt : (S.biUnion neigh).card < S.card := Nat.lt_of_not_ge hnot
    let Sα : Finset α := S.image fun b : B => (b : α)
    let Nα : Finset α := (S.biUnion neigh).image fun a : A => (a : α)
    let C : Finset α := (A \ Nα) ∪ Sα
    have hN_sub_A : Nα ⊆ A := by
      intro x hx
      rw [Finset.mem_image] at hx
      obtain ⟨a, _ha, rfl⟩ := hx
      exact a.property
    have hS_card : Sα.card = S.card := by
      exact Finset.card_image_of_injective S (fun x y hxy => Subtype.ext hxy)
    have hN_card : Nα.card = (S.biUnion neigh).card := by
      exact Finset.card_image_of_injective (S.biUnion neigh) (fun x y hxy => Subtype.ext hxy)
    have hC_sub : C ⊆ U := by
      intro x hx
      rw [Finset.mem_union] at hx
      rcases hx with hxA | hxS
      · exact hA_sub (Finset.mem_sdiff.mp hxA).1
      · rw [Finset.mem_image] at hxS
        obtain ⟨b, _hbS, rfl⟩ := hxS
        exact hB_sub b.property
    have hdisj : Disjoint (A \ Nα) Sα := by
      rw [Finset.disjoint_left]
      intro x hxAN hxS
      have hxA : x ∈ A := (Finset.mem_sdiff.mp hxAN).1
      have hxNotN : x ∉ Nα := (Finset.mem_sdiff.mp hxAN).2
      rw [Finset.mem_image] at hxS
      obtain ⟨b, hbS, rfl⟩ := hxS
      apply hxNotN
      rw [Finset.mem_image]
      refine ⟨⟨(b : α), hxA⟩, ?_, rfl⟩
      rw [Finset.mem_biUnion]
      refine ⟨b, hbS, ?_⟩
      simp [neigh]
    have hcross :
        ∀ {a b : α}, a ∈ A \ Nα → b ∈ Sα → a ≠ b → ¬ a ≤ b ∧ ¬ b ≤ a := by
      intro a b haAN hbS hne
      have haA : a ∈ A := (Finset.mem_sdiff.mp haAN).1
      have haNotN : a ∉ Nα := (Finset.mem_sdiff.mp haAN).2
      rw [Finset.mem_image] at hbS
      obtain ⟨bB, hbBS, rfl⟩ := hbS
      refine ⟨?_, ?_⟩
      · intro hab
        obtain ⟨a', haA', hba'⟩ := hB_above bB bB.property
        have haa' : a ≤ a' := hab.trans hba'
        by_cases hEq : a = a'
        · subst a'
          exact hne (le_antisymm hab hba')
        · exact (hA_anti haA haA' hEq).1 haa'
      · intro hba
        apply haNotN
        rw [Finset.mem_image]
        refine ⟨⟨a, haA⟩, ?_, rfl⟩
        rw [Finset.mem_biUnion]
        refine ⟨bB, hbBS, ?_⟩
        simp [neigh, hba]
    have hC_anti : IsAntichain C := by
      intro x hx y hy hxy
      rw [Finset.mem_union] at hx hy
      rcases hx with hxA | hxS <;> rcases hy with hyA | hyS
      · exact hA_anti (Finset.mem_sdiff.mp hxA).1 (Finset.mem_sdiff.mp hyA).1 hxy
      · exact hcross hxA hyS hxy
      · have h := hcross hyA hxS hxy.symm
        exact ⟨h.2, h.1⟩
      · rw [Finset.mem_image] at hxS hyS
        obtain ⟨xB, _hxBS, rfl⟩ := hxS
        obtain ⟨yB, _hyBS, rfl⟩ := hyS
        exact hB_anti xB.property yB.property hxy
    have hC_card : C.card = A.card - Nα.card + Sα.card := by
      change ((A \ Nα) ∪ Sα).card = A.card - Nα.card + Sα.card
      rw [Finset.card_union_of_disjoint hdisj, Finset.card_sdiff_of_subset hN_sub_A]
    have hNle : Nα.card ≤ A.card := Finset.card_mono hN_sub_A
    have hC_gt : A.card < C.card := by
      rw [hC_card, hS_card, hN_card]
      omega
    have hC_le : C.card ≤ A.card := hA_max C hC_sub hC_anti
    omega
  obtain ⟨f, hf_inj, hf_mem⟩ :=
    (Finset.all_card_le_biUnion_card_iff_existsInjective' neigh).mp hhall
  refine ⟨f, hf_inj, ?_⟩
  intro b
  have hb := hf_mem b
  simpa [neigh] using hb

theorem exists_injective_below_of_max_card_antichain {U A B : Finset α}
    (hA_sub : A ⊆ U) (hA_anti : IsAntichain A)
    (hA_max : ∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ A.card)
    (hB_sub : B ⊆ U) (hB_anti : IsAntichain B)
    (hB_below : ∀ b, b ∈ B → ∃ a, a ∈ A ∧ a ≤ b) :
    ∃ f : B → A, Function.Injective f ∧ ∀ b : B, (f b : α) ≤ (b : α) := by
  classical
  let neigh : B → Finset A := fun b =>
    Finset.univ.filter fun a : A => (a : α) ≤ (b : α)
  have hhall : ∀ S : Finset B, S.card ≤ (S.biUnion neigh).card := by
    intro S
    by_contra hnot
    have hlt : (S.biUnion neigh).card < S.card := Nat.lt_of_not_ge hnot
    let Sα : Finset α := S.image fun b : B => (b : α)
    let Nα : Finset α := (S.biUnion neigh).image fun a : A => (a : α)
    let C : Finset α := (A \ Nα) ∪ Sα
    have hN_sub_A : Nα ⊆ A := by
      intro x hx
      rw [Finset.mem_image] at hx
      obtain ⟨a, _ha, rfl⟩ := hx
      exact a.property
    have hS_card : Sα.card = S.card := by
      exact Finset.card_image_of_injective S (fun x y hxy => Subtype.ext hxy)
    have hN_card : Nα.card = (S.biUnion neigh).card := by
      exact Finset.card_image_of_injective (S.biUnion neigh) (fun x y hxy => Subtype.ext hxy)
    have hC_sub : C ⊆ U := by
      intro x hx
      rw [Finset.mem_union] at hx
      rcases hx with hxA | hxS
      · exact hA_sub (Finset.mem_sdiff.mp hxA).1
      · rw [Finset.mem_image] at hxS
        obtain ⟨b, _hbS, rfl⟩ := hxS
        exact hB_sub b.property
    have hdisj : Disjoint (A \ Nα) Sα := by
      rw [Finset.disjoint_left]
      intro x hxAN hxS
      have hxA : x ∈ A := (Finset.mem_sdiff.mp hxAN).1
      have hxNotN : x ∉ Nα := (Finset.mem_sdiff.mp hxAN).2
      rw [Finset.mem_image] at hxS
      obtain ⟨b, hbS, rfl⟩ := hxS
      apply hxNotN
      rw [Finset.mem_image]
      refine ⟨⟨(b : α), hxA⟩, ?_, rfl⟩
      rw [Finset.mem_biUnion]
      refine ⟨b, hbS, ?_⟩
      simp [neigh]
    have hcross :
        ∀ {a b : α}, a ∈ A \ Nα → b ∈ Sα → a ≠ b → ¬ a ≤ b ∧ ¬ b ≤ a := by
      intro a b haAN hbS hne
      have haA : a ∈ A := (Finset.mem_sdiff.mp haAN).1
      have haNotN : a ∉ Nα := (Finset.mem_sdiff.mp haAN).2
      rw [Finset.mem_image] at hbS
      obtain ⟨bB, hbBS, rfl⟩ := hbS
      refine ⟨?_, ?_⟩
      · intro hab
        apply haNotN
        rw [Finset.mem_image]
        refine ⟨⟨a, haA⟩, ?_, rfl⟩
        rw [Finset.mem_biUnion]
        refine ⟨bB, hbBS, ?_⟩
        simp [neigh, hab]
      · intro hba
        obtain ⟨a', haA', ha'b⟩ := hB_below bB bB.property
        have ha'a : a' ≤ a := ha'b.trans hba
        by_cases hEq : a' = a
        · subst a'
          exact hne (le_antisymm ha'b hba)
        · exact (hA_anti haA' haA hEq).1 ha'a
    have hC_anti : IsAntichain C := by
      intro x hx y hy hxy
      rw [Finset.mem_union] at hx hy
      rcases hx with hxA | hxS <;> rcases hy with hyA | hyS
      · exact hA_anti (Finset.mem_sdiff.mp hxA).1 (Finset.mem_sdiff.mp hyA).1 hxy
      · exact hcross hxA hyS hxy
      · have h := hcross hyA hxS hxy.symm
        exact ⟨h.2, h.1⟩
      · rw [Finset.mem_image] at hxS hyS
        obtain ⟨xB, _hxBS, rfl⟩ := hxS
        obtain ⟨yB, _hyBS, rfl⟩ := hyS
        exact hB_anti xB.property yB.property hxy
    have hC_card : C.card = A.card - Nα.card + Sα.card := by
      change ((A \ Nα) ∪ Sα).card = A.card - Nα.card + Sα.card
      rw [Finset.card_union_of_disjoint hdisj, Finset.card_sdiff_of_subset hN_sub_A]
    have hNle : Nα.card ≤ A.card := Finset.card_mono hN_sub_A
    have hC_gt : A.card < C.card := by
      rw [hC_card, hS_card, hN_card]
      omega
    have hC_le : C.card ≤ A.card := hA_max C hC_sub hC_anti
    omega
  obtain ⟨f, hf_inj, hf_mem⟩ :=
    (Finset.all_card_le_biUnion_card_iff_existsInjective' neigh).mp hhall
  refine ⟨f, hf_inj, ?_⟩
  intro b
  have hb := hf_mem b
  simpa [neigh] using hb

theorem le_anchor_of_mem_chain_subset_lowerClosure {U A C : Finset α}
    (hA_anti : IsAntichain A) (hC_chain : IsChain C) (hC_sub : C ⊆ lowerClosure U A)
    {a x : α} (haA : a ∈ A) (haC : a ∈ C) (hxC : x ∈ C) :
    x ≤ a := by
  obtain ⟨_hxU, b, hbA, hxb⟩ := mem_lowerClosure.mp (hC_sub hxC)
  rcases hC_chain hxC haC with hxa | hax
  · exact hxa
  · have hab : a ≤ b := le_trans hax hxb
    by_cases hEq : a = b
    · simpa [hEq] using hxb
    · exact (hA_anti haA hbA hEq).1 hab |>.elim

theorem anchor_le_of_mem_chain_subset_upperClosure {U A C : Finset α}
    (hA_anti : IsAntichain A) (hC_chain : IsChain C) (hC_sub : C ⊆ upperClosure U A)
    {a x : α} (haA : a ∈ A) (haC : a ∈ C) (hxC : x ∈ C) :
    a ≤ x := by
  obtain ⟨_hxU, b, hbA, hbx⟩ := mem_upperClosure.mp (hC_sub hxC)
  rcases hC_chain hxC haC with hxa | hax
  · have hba : b ≤ a := le_trans hbx hxa
    by_cases hEq : b = a
    · simpa [hEq] using hbx
    · exact (hA_anti hbA haA hEq).1 hba |>.elim
  · exact hax

theorem IsChain.union_of_le_anchor {L R : Finset α} {a : α}
    (hL : IsChain L) (hR : IsChain R)
    (hLa : ∀ x, x ∈ L → x ≤ a) (haR : ∀ x, x ∈ R → a ≤ x) :
    IsChain (L ∪ R) := by
  intro x hx y hy
  rw [Finset.mem_union] at hx hy
  rcases hx with hxL | hxR <;> rcases hy with hyL | hyR
  · exact hL hxL hyL
  · exact Or.inl ((hLa x hxL).trans (haR y hyR))
  · exact Or.inr ((hLa y hyL).trans (haR x hxR))
  · exact hR hxR hyR

theorem IsChain.union_of_lower_upper_anchor {U A L R : Finset α} {a : α}
    (hA_anti : IsAntichain A) (hL_chain : IsChain L) (hR_chain : IsChain R)
    (hL_sub : L ⊆ lowerClosure U A) (hR_sub : R ⊆ upperClosure U A)
    (haA : a ∈ A) (haL : a ∈ L) (haR : a ∈ R) :
    IsChain (L ∪ R) :=
  hL_chain.union_of_le_anchor hR_chain
    (fun x hx =>
      le_anchor_of_mem_chain_subset_lowerClosure hA_anti hL_chain hL_sub (x := x) haA haL hx)
    (fun x hx =>
      anchor_le_of_mem_chain_subset_upperClosure hA_anti hR_chain hR_sub (x := x) haA haR hx)

theorem IsChain.eq_of_mem_isAntichain {A C : Finset α} (hC : IsChain C)
    (hA : IsAntichain A) {a b : α} (haA : a ∈ A) (hbA : b ∈ A)
    (haC : a ∈ C) (hbC : b ∈ C) :
    a = b := by
  by_contra hne
  rcases hC haC hbC with hab | hba
  · exact (hA haA hbA hne).1 hab
  · exact (hA haA hbA hne).2 hba

theorem StrongCoversByChains.existsUnique_anchor {U A : Finset α}
    (hA_sub : A ⊆ U) (hA_anti : IsAntichain A)
    {chains : Fin A.card → Finset α} (hcover : StrongCoversByChains U chains)
    (i : Fin A.card) :
    ∃! a : A, (a : α) ∈ chains i := by
  classical
  have hAcovered : ∀ a : A, ∃ i : Fin A.card, (a : α) ∈ chains i := by
    intro a
    exact hcover.2.2 a (hA_sub a.property)
  let idx : A → Fin A.card := fun a => Classical.choose (hAcovered a)
  have hidx_mem : ∀ a : A, (a : α) ∈ chains (idx a) := by
    intro a
    exact Classical.choose_spec (hAcovered a)
  have hidx_inj : Function.Injective idx := by
    intro a b hab
    apply Subtype.ext
    by_contra hne
    have hb_chain : (b : α) ∈ chains (idx a) := by
      simpa [hab] using hidx_mem b
    exact hne <|
      IsChain.eq_of_mem_isAntichain (hcover.1 (idx a)) hA_anti
        a.property b.property (hidx_mem a) hb_chain
  have hcard_idx : Fintype.card A = Fintype.card (Fin A.card) := by
    simp [Fintype.card_coe]
  have hidx_bij : Function.Bijective idx :=
    (Fintype.bijective_iff_injective_and_card idx).2 ⟨hidx_inj, hcard_idx⟩
  obtain ⟨a, ha⟩ := hidx_bij.2 i
  refine ⟨a, by simpa [idx, ha] using hidx_mem a, ?_⟩
  intro b hb
  apply Subtype.ext
  exact (IsChain.eq_of_mem_isAntichain (a := (a : α)) (b := (b : α)) (hcover.1 i) hA_anti
    a.property b.property (by simpa [idx, ha] using hidx_mem a) hb
    ).symm

theorem StrongCoversByChains.exists_anchorIndexed {U A : Finset α}
    (hA_sub : A ⊆ U) (hA_anti : IsAntichain A)
    {chains : Fin A.card → Finset α} (hcover : StrongCoversByChains U chains) :
    ∃ anchorChains : A → Finset α,
      (∀ a : A, IsChain (anchorChains a) ∧ anchorChains a ⊆ U ∧
        (a : α) ∈ anchorChains a) ∧
      ∀ x, x ∈ U → ∃ a : A, x ∈ anchorChains a := by
  classical
  have hAcovered : ∀ a : A, ∃ i : Fin A.card, (a : α) ∈ chains i := by
    intro a
    exact hcover.2.2 a (hA_sub a.property)
  let idx : A → Fin A.card := fun a => Classical.choose (hAcovered a)
  have hidx_mem : ∀ a : A, (a : α) ∈ chains (idx a) := by
    intro a
    exact Classical.choose_spec (hAcovered a)
  have hidx_inj : Function.Injective idx := by
    intro a b hab
    apply Subtype.ext
    by_contra hne
    have hb_chain : (b : α) ∈ chains (idx a) := by
      simpa [hab] using hidx_mem b
    exact hne <|
      IsChain.eq_of_mem_isAntichain (hcover.1 (idx a)) hA_anti
        a.property b.property (hidx_mem a) hb_chain
  have hcard_idx : Fintype.card A = Fintype.card (Fin A.card) := by
    simp [Fintype.card_coe]
  have hidx_bij : Function.Bijective idx :=
    (Fintype.bijective_iff_injective_and_card idx).2 ⟨hidx_inj, hcard_idx⟩
  let anchorChains : A → Finset α := fun a => chains (idx a)
  refine ⟨anchorChains, ?_, ?_⟩
  · intro a
    exact ⟨hcover.1 (idx a), hcover.2.1 (idx a), hidx_mem a⟩
  · intro x hx
    obtain ⟨i, hxi⟩ := hcover.2.2 x hx
    obtain ⟨a, ha⟩ := hidx_bij.2 i
    exact ⟨a, by simpa [anchorChains, ha] using hxi⟩

theorem exists_anchorIndexed_split_cover {U A : Finset α}
    (hA_anti : IsAntichain A)
    (hU_split : U ⊆ lowerClosure U A ∪ upperClosure U A)
    {lower upper : A → Finset α}
    (hlower :
      (∀ a : A, IsChain (lower a) ∧ lower a ⊆ lowerClosure U A ∧
        (a : α) ∈ lower a) ∧
      ∀ x, x ∈ lowerClosure U A → ∃ a : A, x ∈ lower a)
    (hupper :
      (∀ a : A, IsChain (upper a) ∧ upper a ⊆ upperClosure U A ∧
        (a : α) ∈ upper a) ∧
      ∀ x, x ∈ upperClosure U A → ∃ a : A, x ∈ upper a) :
    ∃ chains : A → Finset α,
      (∀ a : A, IsChain (chains a) ∧ chains a ⊆ U ∧ (a : α) ∈ chains a) ∧
      ∀ x, x ∈ U → ∃ a : A, x ∈ chains a := by
  let chains : A → Finset α := fun a => lower a ∪ upper a
  refine ⟨chains, ?_, ?_⟩
  · intro a
    have hl := hlower.1 a
    have hu := hupper.1 a
    refine ⟨?_, ?_, ?_⟩
    · exact IsChain.union_of_lower_upper_anchor hA_anti
        hl.1 hu.1 hl.2.1 hu.2.1 a.property hl.2.2 hu.2.2
    · intro x hx
      rw [Finset.mem_union] at hx
      rcases hx with hx | hx
      · exact lowerClosure_subset U A (hl.2.1 hx)
      · exact upperClosure_subset U A (hu.2.1 hx)
    · exact Finset.mem_union.mpr (Or.inl hl.2.2)
  · intro x hx
    have hxsplit := hU_split hx
    rw [Finset.mem_union] at hxsplit
    rcases hxsplit with hxlower | hxupper
    · obtain ⟨a, hxa⟩ := hlower.2 x hxlower
      exact ⟨a, Finset.mem_union.mpr (Or.inl hxa)⟩
    · obtain ⟨a, hxa⟩ := hupper.2 x hxupper
      exact ⟨a, Finset.mem_union.mpr (Or.inr hxa)⟩

omit [DecidableEq α] in
theorem exists_strongCoversByChains_card_of_anchorIndexed {U A : Finset α}
    {chains : A → Finset α}
    (hfamily :
      (∀ a : A, IsChain (chains a) ∧ chains a ⊆ U ∧ (a : α) ∈ chains a) ∧
      ∀ x, x ∈ U → ∃ a : A, x ∈ chains a) :
    ∃ chains' : Fin A.card → Finset α, StrongCoversByChains U chains' := by
  classical
  have hcard : Fintype.card A = A.card := by
    simp [Fintype.card_coe]
  let e : Fin A.card ≃ A := (finCongr hcard.symm).trans (Fintype.equivFin A).symm
  let chains' : Fin A.card → Finset α := fun i => chains (e i)
  refine ⟨chains', ?_, ?_, ?_⟩
  · intro i
    exact (hfamily.1 (e i)).1
  · intro i
    exact (hfamily.1 (e i)).2.1
  · intro x hx
    obtain ⟨a, hxa⟩ := hfamily.2 x hx
    exact ⟨e.symm a, by simpa [chains'] using hxa⟩

omit [DecidableEq α] in
theorem exists_strongCoversByChains_of_anchorIndexed {U A : Finset α} {k : ℕ}
    (hAk : A.card ≤ k) {chains : A → Finset α}
    (hfamily :
      (∀ a : A, IsChain (chains a) ∧ chains a ⊆ U ∧ (a : α) ∈ chains a) ∧
      ∀ x, x ∈ U → ∃ a : A, x ∈ chains a) :
    ∃ chains' : Fin k → Finset α, StrongCoversByChains U chains' := by
  obtain ⟨chainsCard, hchainsCard⟩ :=
    exists_strongCoversByChains_card_of_anchorIndexed hfamily
  exact hchainsCard.extend hAk

theorem exists_strongCoversByChains_card_of_split {U A : Finset α}
    (hA_sub : A ⊆ U) (hA_anti : IsAntichain A)
    (hU_split : U ⊆ lowerClosure U A ∪ upperClosure U A)
    {lower upper : Fin A.card → Finset α}
    (hlower : StrongCoversByChains (lowerClosure U A) lower)
    (hupper : StrongCoversByChains (upperClosure U A) upper) :
    ∃ chains : Fin A.card → Finset α, StrongCoversByChains U chains := by
  obtain ⟨lowerByAnchor, hlowerByAnchor⟩ :=
    hlower.exists_anchorIndexed (subset_lowerClosure hA_sub) hA_anti
  obtain ⟨upperByAnchor, hupperByAnchor⟩ :=
    hupper.exists_anchorIndexed (subset_upperClosure hA_sub) hA_anti
  obtain ⟨chainsByAnchor, hchainsByAnchor⟩ :=
    exists_anchorIndexed_split_cover hA_anti hU_split
      (lower := lowerByAnchor) (upper := upperByAnchor)
      hlowerByAnchor hupperByAnchor
  exact exists_strongCoversByChains_card_of_anchorIndexed hchainsByAnchor

theorem exists_anchorIndexed_cover_union_of_matched_extension {V A B : Finset α}
    (hB_anti : IsAntichain B) (hV_lower : lowerClosure V B = V)
    {chainsB : B → Finset α}
    (hchainsB :
      (∀ b : B, IsChain (chainsB b) ∧ chainsB b ⊆ V ∧
        (b : α) ∈ chainsB b) ∧
      ∀ x, x ∈ V → ∃ b : B, x ∈ chainsB b)
    {f : B → A} (hf_inj : Function.Injective f)
    (hf_le : ∀ b : B, (b : α) ≤ (f b : α)) :
    ∃ chainsA : A → Finset α,
      (∀ a : A, IsChain (chainsA a) ∧ chainsA a ⊆ V ∪ A ∧
        (a : α) ∈ chainsA a) ∧
      ∀ x, x ∈ V ∪ A → ∃ a : A, x ∈ chainsA a := by
  classical
  let chainsA : A → Finset α := fun a =>
    if h : ∃ b : B, f b = a then insert (a : α) (chainsB (Classical.choose h))
    else {(a : α)}
  refine ⟨chainsA, ?_, ?_⟩
  · intro a
    by_cases h : ∃ b : B, f b = a
    · let b : B := Classical.choose h
      have hb_eq : f b = a := Classical.choose_spec h
      have hb_le_a : (b : α) ≤ (a : α) := by
        simpa [b, hb_eq] using hf_le b
      have hb_data := hchainsB.1 b
      refine ⟨?_, ?_, ?_⟩
      · simp only [chainsA, dif_pos h]
        apply IsChain.insert_ge hb_data.1
        intro x hx
        have hx_le_b : x ≤ (b : α) :=
          le_anchor_of_mem_chain_subset_lowerClosure (U := V) hB_anti hb_data.1
            (fun y hy => by
              rw [hV_lower]
              exact hb_data.2.1 hy)
            b.property hb_data.2.2 hx
        exact hx_le_b.trans hb_le_a
      · intro x hx
        simp only [chainsA, dif_pos h] at hx
        rw [Finset.mem_insert] at hx
        rcases hx with rfl | hx
        · exact Finset.mem_union.mpr (Or.inr a.property)
        · exact Finset.mem_union.mpr (Or.inl (hb_data.2.1 hx))
      · simp only [chainsA, dif_pos h]
        exact Finset.mem_insert_self (a : α) (chainsB b)
    · refine ⟨?_, ?_, ?_⟩
      · simp only [chainsA, dif_neg h]
        exact isChain_singleton (a : α)
      · intro x hx
        simp only [chainsA, dif_neg h] at hx
        rw [Finset.mem_singleton] at hx
        subst x
        exact Finset.mem_union.mpr (Or.inr a.property)
      · simp only [chainsA, dif_neg h]
        exact Finset.mem_singleton.mpr rfl
  · intro x hx
    rw [Finset.mem_union] at hx
    rcases hx with hxV | hxA
    · obtain ⟨b, hxb⟩ := hchainsB.2 x hxV
      let a : A := f b
      have h : ∃ b' : B, f b' = a := ⟨b, rfl⟩
      have hchoose : Classical.choose h = b := hf_inj (Classical.choose_spec h)
      refine ⟨a, ?_⟩
      simp only [chainsA, dif_pos h]
      exact Finset.mem_insert.mpr (Or.inr (by simpa [hchoose] using hxb))
    · let a : A := ⟨x, hxA⟩
      refine ⟨a, ?_⟩
      by_cases h : ∃ b : B, f b = a
      · simp only [chainsA, dif_pos h]
        exact Finset.mem_insert.mpr (Or.inl rfl)
      · simp only [chainsA, dif_neg h]
        exact Finset.mem_singleton.mpr rfl

theorem exists_anchorIndexed_cover_union_of_max_antichain_extension {V A B : Finset α}
    (hA_anti : IsAntichain A)
    (hA_max :
      ∀ s : Finset α, s ⊆ V ∪ A → IsAntichain s → s.card ≤ A.card)
    (hB_sub : B ⊆ V) (hB_anti : IsAntichain B)
    (hB_above : ∀ b, b ∈ B → ∃ a, a ∈ A ∧ b ≤ a)
    (hV_lower : lowerClosure V B = V)
    {chainsB : B → Finset α}
    (hchainsB :
      (∀ b : B, IsChain (chainsB b) ∧ chainsB b ⊆ V ∧
        (b : α) ∈ chainsB b) ∧
      ∀ x, x ∈ V → ∃ b : B, x ∈ chainsB b) :
    ∃ chainsA : A → Finset α,
      (∀ a : A, IsChain (chainsA a) ∧ chainsA a ⊆ V ∪ A ∧
        (a : α) ∈ chainsA a) ∧
      ∀ x, x ∈ V ∪ A → ∃ a : A, x ∈ chainsA a := by
  have hA_sub_union : A ⊆ V ∪ A := by
    intro a ha
    exact Finset.mem_union.mpr (Or.inr ha)
  have hB_sub_union : B ⊆ V ∪ A := by
    intro b hb
    exact Finset.mem_union.mpr (Or.inl (hB_sub hb))
  obtain ⟨f, hf_inj, hf_le⟩ :=
    exists_injective_above_of_max_card_antichain
      (U := V ∪ A) (A := A) (B := B)
      hA_sub_union hA_anti hA_max hB_sub_union hB_anti hB_above
  exact exists_anchorIndexed_cover_union_of_matched_extension
    hB_anti hV_lower hchainsB hf_inj hf_le

theorem exists_anchorIndexed_cover_union_of_matched_lower_extension {V A B : Finset α}
    (hB_anti : IsAntichain B) (hV_upper : upperClosure V B = V)
    {chainsB : B → Finset α}
    (hchainsB :
      (∀ b : B, IsChain (chainsB b) ∧ chainsB b ⊆ V ∧
        (b : α) ∈ chainsB b) ∧
      ∀ x, x ∈ V → ∃ b : B, x ∈ chainsB b)
    {f : B → A} (hf_inj : Function.Injective f)
    (hf_le : ∀ b : B, (f b : α) ≤ (b : α)) :
    ∃ chainsA : A → Finset α,
      (∀ a : A, IsChain (chainsA a) ∧ chainsA a ⊆ V ∪ A ∧
        (a : α) ∈ chainsA a) ∧
      ∀ x, x ∈ V ∪ A → ∃ a : A, x ∈ chainsA a := by
  classical
  let chainsA : A → Finset α := fun a =>
    if h : ∃ b : B, f b = a then insert (a : α) (chainsB (Classical.choose h))
    else {(a : α)}
  refine ⟨chainsA, ?_, ?_⟩
  · intro a
    by_cases h : ∃ b : B, f b = a
    · let b : B := Classical.choose h
      have hb_eq : f b = a := Classical.choose_spec h
      have ha_le_b : (a : α) ≤ (b : α) := by
        simpa [b, hb_eq] using hf_le b
      have hb_data := hchainsB.1 b
      refine ⟨?_, ?_, ?_⟩
      · simp only [chainsA, dif_pos h]
        apply IsChain.insert_le hb_data.1
        intro x hx
        have hb_le_x : (b : α) ≤ x :=
          anchor_le_of_mem_chain_subset_upperClosure (U := V) hB_anti hb_data.1
            (fun y hy => by
              rw [hV_upper]
              exact hb_data.2.1 hy)
            b.property hb_data.2.2 hx
        exact ha_le_b.trans hb_le_x
      · intro x hx
        simp only [chainsA, dif_pos h] at hx
        rw [Finset.mem_insert] at hx
        rcases hx with rfl | hx
        · exact Finset.mem_union.mpr (Or.inr a.property)
        · exact Finset.mem_union.mpr (Or.inl (hb_data.2.1 hx))
      · simp only [chainsA, dif_pos h]
        exact Finset.mem_insert_self (a : α) (chainsB b)
    · refine ⟨?_, ?_, ?_⟩
      · simp only [chainsA, dif_neg h]
        exact isChain_singleton (a : α)
      · intro x hx
        simp only [chainsA, dif_neg h] at hx
        rw [Finset.mem_singleton] at hx
        subst x
        exact Finset.mem_union.mpr (Or.inr a.property)
      · simp only [chainsA, dif_neg h]
        exact Finset.mem_singleton.mpr rfl
  · intro x hx
    rw [Finset.mem_union] at hx
    rcases hx with hxV | hxA
    · obtain ⟨b, hxb⟩ := hchainsB.2 x hxV
      let a : A := f b
      have h : ∃ b' : B, f b' = a := ⟨b, rfl⟩
      have hchoose : Classical.choose h = b := hf_inj (Classical.choose_spec h)
      refine ⟨a, ?_⟩
      simp only [chainsA, dif_pos h]
      exact Finset.mem_insert.mpr (Or.inr (by simpa [hchoose] using hxb))
    · let a : A := ⟨x, hxA⟩
      refine ⟨a, ?_⟩
      by_cases h : ∃ b : B, f b = a
      · simp only [chainsA, dif_pos h]
        exact Finset.mem_insert.mpr (Or.inl rfl)
      · simp only [chainsA, dif_neg h]
        exact Finset.mem_singleton.mpr rfl

theorem exists_anchorIndexed_cover_union_of_max_antichain_lower_extension {V A B : Finset α}
    (hA_anti : IsAntichain A)
    (hA_max :
      ∀ s : Finset α, s ⊆ V ∪ A → IsAntichain s → s.card ≤ A.card)
    (hB_sub : B ⊆ V) (hB_anti : IsAntichain B)
    (hB_below : ∀ b, b ∈ B → ∃ a, a ∈ A ∧ a ≤ b)
    (hV_upper : upperClosure V B = V)
    {chainsB : B → Finset α}
    (hchainsB :
      (∀ b : B, IsChain (chainsB b) ∧ chainsB b ⊆ V ∧
        (b : α) ∈ chainsB b) ∧
      ∀ x, x ∈ V → ∃ b : B, x ∈ chainsB b) :
    ∃ chainsA : A → Finset α,
      (∀ a : A, IsChain (chainsA a) ∧ chainsA a ⊆ V ∪ A ∧
        (a : α) ∈ chainsA a) ∧
      ∀ x, x ∈ V ∪ A → ∃ a : A, x ∈ chainsA a := by
  have hA_sub_union : A ⊆ V ∪ A := by
    intro a ha
    exact Finset.mem_union.mpr (Or.inr ha)
  have hB_sub_union : B ⊆ V ∪ A := by
    intro b hb
    exact Finset.mem_union.mpr (Or.inl (hB_sub hb))
  obtain ⟨f, hf_inj, hf_le⟩ :=
    exists_injective_below_of_max_card_antichain
      (U := V ∪ A) (A := A) (B := B)
      hA_sub_union hA_anti hA_max hB_sub_union hB_anti hB_below
  exact exists_anchorIndexed_cover_union_of_matched_lower_extension
    hB_anti hV_upper hchainsB hf_inj hf_le

omit [DecidableEq α] in
theorem one_le_of_mem_of_widthAtMost {U : Finset α} {k : ℕ} {x : α}
    (hx : x ∈ U) (hU : WidthAtMost U k) :
    1 ≤ k := by
  simpa using
    hU ({x} : Finset α)
      (by
        intro y hy
        simp only [Finset.mem_singleton] at hy
        subst y
        exact hx)
      (isAntichain_singleton x)

omit [DecidableEq α] in
theorem one_le_of_nonempty_widthAtMost {U : Finset α} {k : ℕ}
    (hNonempty : U.Nonempty) (hU : WidthAtMost U k) :
    1 ≤ k := by
  obtain ⟨x, hx⟩ := hNonempty
  exact one_le_of_mem_of_widthAtMost hx hU

omit [DecidableEq α] in
theorem eq_empty_of_widthAtMost_zero {U : Finset α}
    (hU : WidthAtMost U 0) :
    U = ∅ := by
  apply Finset.eq_empty_iff_forall_notMem.mpr
  intro x hx
  have hle : 1 ≤ 0 := one_le_of_mem_of_widthAtMost hx hU
  omega

theorem isChain_of_widthAtMost_one {U : Finset α}
    (hU : WidthAtMost U 1) :
    IsChain U := by
  intro a ha b hb
  by_cases hab : a ≤ b
  · exact Or.inl hab
  · by_cases hba : b ≤ a
    · exact Or.inr hba
    · have hne : a ≠ b := fun h => hab (h ▸ le_rfl)
      have hAnti : IsAntichain ({a, b} : Finset α) := by
        intro x hx y hy hxy
        simp only [Finset.mem_insert, Finset.mem_singleton] at hx hy
        rcases hx with rfl | rfl <;> rcases hy with rfl | rfl
        · exact (hxy rfl).elim
        · exact ⟨hab, hba⟩
        · exact ⟨hba, hab⟩
        · exact (hxy rfl).elim
      have hsubset : ∀ x, x ∈ ({a, b} : Finset α) → x ∈ U := by
        intro x hx
        simp only [Finset.mem_insert, Finset.mem_singleton] at hx
        rcases hx with rfl | rfl
        · exact ha
        · exact hb
      have hcard : ({a, b} : Finset α).card ≤ 1 := hU ({a, b} : Finset α) hsubset hAnti
      have hcard_eq : ({a, b} : Finset α).card = 2 := by
        simp [hne]
      omega

theorem exists_coversByChains_of_widthAtMost_one {U : Finset α}
    (hU : WidthAtMost U 1) :
    ∃ chains : Fin 1 → Finset α, CoversByChains U chains := by
  refine ⟨fun _ => U, ?_⟩
  exact ⟨fun _ => isChain_of_widthAtMost_one hU, fun _ hx => ⟨0, hx⟩⟩

theorem exists_strongCoversByChains_of_widthAtMost_one {U : Finset α}
    (hU : WidthAtMost U 1) :
    ∃ chains : Fin 1 → Finset α, StrongCoversByChains U chains := by
  refine ⟨fun _ => U, ?_, ?_, ?_⟩
  · intro _
    exact isChain_of_widthAtMost_one hU
  · intro _ x hx
    exact hx
  · intro _ hx
    exact ⟨0, hx⟩

omit [DecidableEq α] in
theorem coversByChains_empty (k : ℕ) :
    ∃ chains : Fin k → Finset α, CoversByChains (∅ : Finset α) chains := by
  refine ⟨fun _ => ∅, ?_⟩
  exact ⟨fun _ => isChain_empty, by simp⟩

omit [DecidableEq α] in
theorem strongCoversByChains_empty (k : ℕ) :
    ∃ chains : Fin k → Finset α, StrongCoversByChains (∅ : Finset α) chains := by
  refine ⟨fun _ => ∅, ?_, ?_, ?_⟩
  · intro _
    exact isChain_empty
  · intro _ x hx
    simp at hx
  · simp

theorem exists_coversByChains_of_card_le {U : Finset α} {k : ℕ}
    (hcard : U.card ≤ k) :
    ∃ chains : Fin k → Finset α, CoversByChains U chains := by
  classical
  have hcard' : Fintype.card U ≤ Fintype.card (Fin k) := by
    simpa [Fintype.card_coe] using hcard
  obtain ⟨e⟩ := Function.Embedding.nonempty_of_card_le hcard'
  let chains : Fin k → Finset α := fun i =>
    (Finset.univ.filter fun u : U => e u = i).image Subtype.val
  refine ⟨chains, ?_, ?_⟩
  · intro i a ha b hb
    rw [Finset.mem_image] at ha hb
    obtain ⟨u, hu, hua⟩ := ha
    obtain ⟨v, hv, hvb⟩ := hb
    rw [Finset.mem_filter] at hu hv
    have huv : u = v := e.injective (hu.2.trans hv.2.symm)
    subst v
    subst a
    subst b
    exact Or.inl le_rfl
  · intro x hx
    let u : U := ⟨x, hx⟩
    refine ⟨e u, ?_⟩
    rw [Finset.mem_image]
    refine ⟨u, ?_, rfl⟩
    rw [Finset.mem_filter]
    exact ⟨Finset.mem_univ u, rfl⟩

theorem exists_strongCoversByChains_of_card_le {U : Finset α} {k : ℕ}
    (hcard : U.card ≤ k) :
    ∃ chains : Fin k → Finset α, StrongCoversByChains U chains := by
  classical
  have hcard' : Fintype.card U ≤ Fintype.card (Fin k) := by
    simpa [Fintype.card_coe] using hcard
  obtain ⟨e⟩ := Function.Embedding.nonempty_of_card_le hcard'
  let chains : Fin k → Finset α := fun i =>
    (Finset.univ.filter fun u : U => e u = i).image Subtype.val
  refine ⟨chains, ?_, ?_, ?_⟩
  · intro i a ha b hb
    rw [Finset.mem_image] at ha hb
    obtain ⟨u, hu, hua⟩ := ha
    obtain ⟨v, hv, hvb⟩ := hb
    rw [Finset.mem_filter] at hu hv
    have huv : u = v := e.injective (hu.2.trans hv.2.symm)
    subst v
    subst a
    subst b
    exact Or.inl le_rfl
  · intro i x hx
    rw [Finset.mem_image] at hx
    obtain ⟨u, _hu, hux⟩ := hx
    subst x
    exact u.property
  · intro x hx
    let u : U := ⟨x, hx⟩
    refine ⟨e u, ?_⟩
    rw [Finset.mem_image]
    refine ⟨u, ?_, rfl⟩
    rw [Finset.mem_filter]
    exact ⟨Finset.mem_univ u, rfl⟩

theorem exists_coversByChains_univ_of_card_le [Fintype α] {k : ℕ}
    (hcard : Fintype.card α ≤ k) :
    ∃ chains : Fin k → Finset α, CoversByChains (Finset.univ : Finset α) chains := by
  simpa using
    (exists_coversByChains_of_card_le (α := α) (U := (Finset.univ : Finset α)) hcard)

theorem exists_strongCoversByChains_univ_of_card_le [Fintype α] {k : ℕ}
    (hcard : Fintype.card α ≤ k) :
    ∃ chains : Fin k → Finset α, StrongCoversByChains (Finset.univ : Finset α) chains := by
  simpa using
    (exists_strongCoversByChains_of_card_le (α := α) (U := (Finset.univ : Finset α)) hcard)

omit [DecidableEq α] in
theorem isEmpty_of_widthAtMost_univ_zero [Fintype α]
    (hU : WidthAtMost (Finset.univ : Finset α) 0) :
    IsEmpty α := by
  refine isEmpty_iff.mpr ?_
  intro x
  have hle : 1 ≤ 0 := by
    simpa using
      hU ({x} : Finset α) (by intro y _hy; simp)
        (isAntichain_singleton x)
  omega

omit [DecidableEq α] in
theorem exists_coversByChains_univ_zero [Fintype α]
    (hU : WidthAtMost (Finset.univ : Finset α) 0) :
    ∃ chains : Fin 0 → Finset α, CoversByChains (Finset.univ : Finset α) chains := by
  haveI : IsEmpty α := isEmpty_of_widthAtMost_univ_zero hU
  simpa [Finset.univ_eq_empty] using (coversByChains_empty (α := α) 0)

omit [DecidableEq α] in
theorem exists_strongCoversByChains_univ_zero [Fintype α]
    (hU : WidthAtMost (Finset.univ : Finset α) 0) :
    ∃ chains : Fin 0 → Finset α, StrongCoversByChains (Finset.univ : Finset α) chains := by
  haveI : IsEmpty α := isEmpty_of_widthAtMost_univ_zero hU
  simpa [Finset.univ_eq_empty] using (strongCoversByChains_empty (α := α) 0)

theorem exists_strongCoversByChains_of_widthAtMost {U : Finset α} {k : ℕ}
    (hU : WidthAtMost U k) :
    ∃ chains : Fin k → Finset α, StrongCoversByChains U chains := by
  classical
  refine
    Nat.strong_induction_on
      (p := fun n =>
        ∀ U : Finset α, U.card = n → ∀ k : ℕ, WidthAtMost U k →
          ∃ chains : Fin k → Finset α, StrongCoversByChains U chains)
      U.card ?_ U rfl k hU
  intro n ih U hUn k hU
  by_cases hcard : U.card ≤ k
  · exact exists_strongCoversByChains_of_card_le hcard
  have hU_nonempty : U.Nonempty := by
    have hpos : 0 < U.card := by omega
    exact Finset.card_pos.mp hpos
  obtain ⟨A, hA_sub, hA_anti, hA_max⟩ := exists_max_card_antichain U
  have hAk : A.card ≤ k := hU A hA_sub hA_anti
  have hA_width : WidthAtMost U A.card := widthAtMost_max_card_antichain hA_max
  have hA_pos : 0 < A.card := by
    by_contra hnot
    have hA_zero : A.card = 0 := Nat.eq_zero_of_not_pos hnot
    have hU_empty : U = ∅ := by
      exact eq_empty_of_widthAtMost_zero (by simpa [hA_zero] using hA_width)
    have : U.card ≤ k := by simp [hU_empty]
    exact hcard this
  by_cases hA_one : A.card = 1
  · obtain ⟨chainsOne, hchainsOne⟩ :=
      exists_strongCoversByChains_of_widthAtMost_one (by simpa [hA_one] using hA_width)
    exact hchainsOne.extend (by simpa [hA_one] using hAk)
  by_cases hsplit :
      ∃ B : Finset α, B ⊆ U ∧ IsAntichain B ∧ B.card ≤ k ∧
        (∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ B.card) ∧
        lowerClosure U B ≠ U ∧ upperClosure U B ≠ U
  · obtain ⟨B, hB_sub, hB_anti, hBk, hB_max, hB_lower_ne, hB_upper_ne⟩ := hsplit
    have hLower_lt : (lowerClosure U B).card < n := by
      rw [← hUn]
      apply Finset.card_lt_card
      refine ⟨lowerClosure_subset U B, ?_⟩
      intro hUsub
      exact hB_lower_ne (Finset.Subset.antisymm (lowerClosure_subset U B) hUsub)
    have hUpper_lt : (upperClosure U B).card < n := by
      rw [← hUn]
      apply Finset.card_lt_card
      refine ⟨upperClosure_subset U B, ?_⟩
      intro hUsub
      exact hB_upper_ne (Finset.Subset.antisymm (upperClosure_subset U B) hUsub)
    obtain ⟨lowerChains, hlowerChains⟩ :=
      ih (lowerClosure U B).card hLower_lt (lowerClosure U B) rfl B.card
        (widthAtMost_lowerClosure_of_max_card_antichain hB_max)
    obtain ⟨upperChains, hupperChains⟩ :=
      ih (upperClosure U B).card hUpper_lt (upperClosure U B) rfl B.card
        (widthAtMost_upperClosure_of_max_card_antichain hB_max)
    obtain ⟨chainsB, hchainsB⟩ :=
      exists_strongCoversByChains_card_of_split hB_sub hB_anti
        (lowerClosure_union_upperClosure_of_max_card_antichain hB_sub hB_anti hB_max)
        hlowerChains hupperChains
    exact hchainsB.extend hBk
  · have hNoSplit :
        ∀ B : Finset α, B ⊆ U → IsAntichain B →
          (∀ s : Finset α, s ⊆ U → IsAntichain s → s.card ≤ B.card) →
          lowerClosure U B = U ∨ upperClosure U B = U := by
      intro B hB_sub hB_anti hB_max
      by_cases hLower : lowerClosure U B = U
      · exact Or.inl hLower
      by_cases hUpper : upperClosure U B = U
      · exact Or.inr hUpper
      exfalso
      exact hsplit ⟨B, hB_sub, hB_anti, hU B hB_sub hB_anti, hB_max, hLower, hUpper⟩
    obtain ⟨x, hxU, hx_min, y, hyU, hy_max, hxy⟩ := exists_minimal_le_maximal hU_nonempty
    let W : Finset α := (U.erase x).erase y
    have hW_width : WidthAtMost W (A.card - 1) := by
      exact widthAtMost_erase_pair_of_no_proper_max_antichain
        hA_max hA_pos hNoSplit hxU hyU hx_min hy_max
    have hW_lt : W.card < n := by
      rw [← hUn]
      have hW_le : W.card ≤ (U.erase x).card := by
        exact Finset.card_mono (Finset.erase_subset y (U.erase x))
      have hErase_lt : (U.erase x).card < U.card := Finset.card_erase_lt_of_mem hxU
      omega
    obtain ⟨chainsW, hchainsW⟩ :=
      ih W.card hW_lt W rfl (A.card - 1) hW_width
    have hsnocExact :
        ∃ chainsA : Fin A.card → Finset α, StrongCoversByChains U chainsA := by
      have hsnoc := hchainsW.snoc_erase_pair (U := U) (x := x) (y := y) hxU hyU hxy
      have hcard_succ : A.card - 1 + 1 = A.card := by omega
      rw [hcard_succ] at hsnoc
      simpa [W] using hsnoc
    obtain ⟨chainsA, hchainsA⟩ := hsnocExact
    exact hchainsA.extend hAk

/-- Finite-poset Dilworth theorem: width at most `k` gives a cover by `k` chains. -/
theorem dilworthTheorem : DilworthTheoremStatement := by
  intro α _ _ _ k hU
  classical
  obtain ⟨chains, hchains⟩ :=
    exists_strongCoversByChains_of_widthAtMost
      (α := α) (U := (Finset.univ : Finset α)) hU
  exact ⟨chains, hchains.toCovers⟩

/-- Checked statement wrapper for the minimum theorem. -/
theorem dilworthTheorem_statement :
    DilworthTheoremStatement ↔ DilworthTheoremStatement := by
  rfl

end AtlasKnownTheorems.DilworthTheorem