[GOAL]
V : Type
G : SimpleGraph V
inst✝ : Finite V
⊢ ↑(SimpleGraph.end G) → False
[PROOFSTEP]
rintro ⟨s, _⟩
[GOAL]
case mk
V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
property✝ : s ∈ SimpleGraph.end G
⊢ False
[PROOFSTEP]
cases nonempty_fintype V
[GOAL]
case mk.intro
V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
property✝ : s ∈ SimpleGraph.end G
val✝ : Fintype V
⊢ False
[PROOFSTEP]
obtain ⟨v, h⟩ := (s <| Opposite.op Finset.univ).nonempty
[GOAL]
case mk.intro.intro
V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
property✝ : s ∈ SimpleGraph.end G
val✝ : Fintype V
v : V
h : v ∈ ↑(s (Opposite.op Finset.univ))
⊢ False
[PROOFSTEP]
exact Set.disjoint_iff.mp (s _).disjoint_right ⟨by simp only [Opposite.unop_op, Finset.coe_univ, Set.mem_univ], h⟩
[GOAL]
V : Type
G : SimpleGraph V
inst✝ : Finite V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
property✝ : s ∈ SimpleGraph.end G
val✝ : Fintype V
v : V
h : v ∈ ↑(s (Opposite.op Finset.univ))
⊢ v ∈ ↑(Opposite.op Finset.univ).unop
[PROOFSTEP]
simp only [Opposite.unop_op, Finset.coe_univ, Set.mem_univ]
[GOAL]
V : Type
G : SimpleGraph V
e : ↑(SimpleGraph.end G)
K : (Finset V)ᵒᵖ
⊢ Set.Infinite (ComponentCompl.supp (↑e K))
[PROOFSTEP]
refine (e.val K).infinite_iff_in_all_ranges.mpr (fun L h => ?_)
[GOAL]
V : Type
G : SimpleGraph V
e : ↑(SimpleGraph.end G)
K : (Finset V)ᵒᵖ
L : Finset V
h : K.unop ⊆ L
⊢ ∃ D, ComponentCompl.hom h D = ↑e K
[PROOFSTEP]
change Opposite.unop K ⊆ Opposite.unop (Opposite.op L) at h 
[GOAL]
V : Type
G : SimpleGraph V
e : ↑(SimpleGraph.end G)
K : (Finset V)ᵒᵖ
L : Finset V
h : K.unop ⊆ (Opposite.op L).unop
⊢ ∃ D, ComponentCompl.hom h D = ↑e K
[PROOFSTEP]
exact ⟨e.val (Opposite.op L), (e.prop (CategoryTheory.opHomOfLE h))⟩
[GOAL]
V : Type
G : SimpleGraph V
inst✝² : LocallyFinite G
inst✝¹ : Fact (Preconnected G)
inst✝ : Infinite V
⊢ Set.Nonempty (SimpleGraph.end G)
[PROOFSTEP]
classical apply nonempty_sections_of_finite_inverse_system G.componentComplFunctor
[GOAL]
V : Type
G : SimpleGraph V
inst✝² : LocallyFinite G
inst✝¹ : Fact (Preconnected G)
inst✝ : Infinite V
⊢ Set.Nonempty (SimpleGraph.end G)
[PROOFSTEP]
apply nonempty_sections_of_finite_inverse_system G.componentComplFunctor
