case mp
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
⊢ Set.Infinite (supp C) → ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C

case mpr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
⊢ (∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C) → Set.Infinite (supp C)
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
⊢ Set.Infinite (supp C) ↔ ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
constructor
case mp
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
Cinf : Set.Infinite (supp C)
L : Finset V
h : K ⊆ L
⊢ ∃ D, hom h D = C
case mp
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
⊢ Set.Infinite (supp C) → ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
rintro Cinf L h
case mp.intro.intro.intro
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
K L : Finset V
h : K ⊆ L
v : V
vL : ¬v ∈ ↑L
vK : ¬v ∈ ↑K
Cinf : Set.Infinite (supp (componentComplMk G vK))
⊢ ∃ D, hom h D = componentComplMk G vK
case mp
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
Cinf : Set.Infinite (supp C)
L : Finset V
h : K ⊆ L
⊢ ∃ D, hom h D = C
obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.diff Cinf L.finite_toSet)
no goals
case mp.intro.intro.intro
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
K L : Finset V
h : K ⊆ L
v : V
vL : ¬v ∈ ↑L
vK : ¬v ∈ ↑K
Cinf : Set.Infinite (supp (componentComplMk G vK))
⊢ ∃ D, hom h D = componentComplMk G vK
exact ⟨componentComplMk _ vL, rfl⟩
case mpr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
⊢ False
case mpr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
⊢ (∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C) → Set.Infinite (supp C)
rintro h Cfin
case mpr.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
⊢ False
case mpr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
⊢ False
obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) (Finset.subset_union_left K Cfin.toFinset)
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
v : V
vD : v ∈ ↑D
⊢ False
case mpr.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
⊢ False
obtain ⟨v, vD⟩ := D.nonempty
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
v : V
vD : v ∈ ↑D
Ddis : Disjoint ↑(K ∪ Set.Finite.toFinset Cfin) ↑D := ComponentCompl.disjoint_right D
⊢ False
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
v : V
vD : v ∈ ↑D
⊢ False
let Ddis := D.disjoint_right
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
v : V
vD : v ∈ ↑D
Ddis : ↑K ∩ ↑D ⊆ ∅ ∧ supp C ∩ ↑D ⊆ ∅
⊢ False
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
v : V
vD : v ∈ ↑D
Ddis : Disjoint ↑(K ∪ Set.Finite.toFinset Cfin) ↑D := ComponentCompl.disjoint_right D
⊢ False
simp_rw [Finset.coe_union, Set.Finite.coe_toFinset, Set.disjoint_union_left,
  Set.disjoint_iff] at Ddis
no goals
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
v : V
vD : v ∈ ↑D
Ddis : ↑K ∩ ↑D ⊆ ∅ ∧ supp C ∩ ↑D ⊆ ∅
⊢ False
exact Ddis.right ⟨(ComponentCompl.hom_eq_iff_le _ _ _).mp e vD, vD⟩