[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
⊢ Function.Injective supp
[PROOFSTEP]
refine' ConnectedComponent.ind₂ _
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
⊢ ∀ (v w : ↑Kᶜ),
    supp (connectedComponentMk (induce Kᶜ G) v) = supp (connectedComponentMk (induce Kᶜ G) w) →
      connectedComponentMk (induce Kᶜ G) v = connectedComponentMk (induce Kᶜ G) w
[PROOFSTEP]
rintro ⟨v, hv⟩ ⟨w, hw⟩ h
[GOAL]
case mk.mk
V : Type u
G : SimpleGraph V
K L L' M : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h :
  supp (connectedComponentMk (induce Kᶜ G) { val := v, property := hv }) =
    supp (connectedComponentMk (induce Kᶜ G) { val := w, property := hw })
⊢ connectedComponentMk (induce Kᶜ G) { val := v, property := hv } =
    connectedComponentMk (induce Kᶜ G) { val := w, property := hw }
[PROOFSTEP]
simp only [Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq, ComponentCompl.supp] at h ⊢
[GOAL]
case mk.mk
V : Type u
G : SimpleGraph V
K L L' M : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h :
  ∀ (x : V),
    (∃ h, Reachable (induce Kᶜ G) { val := x, property := (_ : ¬x ∈ K) } { val := v, property := hv }) ↔
      ∃ h, Reachable (induce Kᶜ G) { val := x, property := (_ : ¬x ∈ K) } { val := w, property := hw }
⊢ Reachable (induce Kᶜ G) { val := v, property := hv } { val := w, property := hw }
[PROOFSTEP]
exact ((h v).mp ⟨hv, Reachable.refl _⟩).choose_spec
[GOAL]
V : Type u
G✝ : SimpleGraph V
K L L' M : Set V
G : SimpleGraph V
v w : V
vK : ¬v ∈ K
wK : ¬w ∈ K
a : Adj G v w
⊢ componentComplMk G vK = componentComplMk G wK
[PROOFSTEP]
rw [ConnectedComponent.eq]
[GOAL]
V : Type u
G✝ : SimpleGraph V
K L L' M : Set V
G : SimpleGraph V
v w : V
vK : ¬v ∈ K
wK : ¬w ∈ K
a : Adj G v w
⊢ Reachable (induce Kᶜ G) { val := v, property := vK } { val := w, property := wK }
[PROOFSTEP]
apply Adj.reachable
[GOAL]
case h
V : Type u
G✝ : SimpleGraph V
K L L' M : Set V
G : SimpleGraph V
v w : V
vK : ¬v ∈ K
wK : ¬w ∈ K
a : Adj G v w
⊢ Adj (induce Kᶜ G) { val := v, property := vK } { val := w, property := wK }
[PROOFSTEP]
exact a
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : Sort u_1
f : ⦃v : V⦄ → ¬v ∈ K → β
h : ∀ ⦃v w : V⦄ (hv : ¬v ∈ K) (hw : ¬w ∈ K), Adj G v w → f hv = f hw
v w : ↑Kᶜ
p : Walk (induce Kᶜ G) v w
⊢ Walk.IsPath p → (fun vv => f (_ : ↑vv ∈ Kᶜ)) v = (fun vv => f (_ : ↑vv ∈ Kᶜ)) w
[PROOFSTEP]
induction' p with _ u v w a q ih
[GOAL]
case nil
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : Sort u_1
f : ⦃v : V⦄ → ¬v ∈ K → β
h : ∀ ⦃v w : V⦄ (hv : ¬v ∈ K) (hw : ¬w ∈ K), Adj G v w → f hv = f hw
v w u✝ : ↑Kᶜ
⊢ Walk.IsPath Walk.nil → (fun vv => f (_ : ↑vv ∈ Kᶜ)) u✝ = (fun vv => f (_ : ↑vv ∈ Kᶜ)) u✝
[PROOFSTEP]
rintro _
[GOAL]
case nil
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : Sort u_1
f : ⦃v : V⦄ → ¬v ∈ K → β
h : ∀ ⦃v w : V⦄ (hv : ¬v ∈ K) (hw : ¬w ∈ K), Adj G v w → f hv = f hw
v w u✝ : ↑Kᶜ
a✝ : Walk.IsPath Walk.nil
⊢ (fun vv => f (_ : ↑vv ∈ Kᶜ)) u✝ = (fun vv => f (_ : ↑vv ∈ Kᶜ)) u✝
[PROOFSTEP]
rfl
[GOAL]
case cons
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : Sort u_1
f : ⦃v : V⦄ → ¬v ∈ K → β
h : ∀ ⦃v w : V⦄ (hv : ¬v ∈ K) (hw : ¬w ∈ K), Adj G v w → f hv = f hw
v✝ w✝ u v w : ↑Kᶜ
a : Adj (induce Kᶜ G) u v
q : Walk (induce Kᶜ G) v w
ih : Walk.IsPath q → (fun vv => f (_ : ↑vv ∈ Kᶜ)) v = (fun vv => f (_ : ↑vv ∈ Kᶜ)) w
⊢ Walk.IsPath (Walk.cons a q) → (fun vv => f (_ : ↑vv ∈ Kᶜ)) u = (fun vv => f (_ : ↑vv ∈ Kᶜ)) w
[PROOFSTEP]
rintro h'
[GOAL]
case cons
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : Sort u_1
f : ⦃v : V⦄ → ¬v ∈ K → β
h : ∀ ⦃v w : V⦄ (hv : ¬v ∈ K) (hw : ¬w ∈ K), Adj G v w → f hv = f hw
v✝ w✝ u v w : ↑Kᶜ
a : Adj (induce Kᶜ G) u v
q : Walk (induce Kᶜ G) v w
ih : Walk.IsPath q → (fun vv => f (_ : ↑vv ∈ Kᶜ)) v = (fun vv => f (_ : ↑vv ∈ Kᶜ)) w
h' : Walk.IsPath (Walk.cons a q)
⊢ (fun vv => f (_ : ↑vv ∈ Kᶜ)) u = (fun vv => f (_ : ↑vv ∈ Kᶜ)) w
[PROOFSTEP]
exact (h u.prop v.prop a).trans (ih h'.of_cons)
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : ComponentCompl G K → Prop
f : ∀ ⦃v : V⦄ (hv : ¬v ∈ K), β (componentComplMk G hv)
⊢ ∀ (C : ComponentCompl G K), β C
[PROOFSTEP]
apply ConnectedComponent.ind
[GOAL]
case h
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : ComponentCompl G K → Prop
f : ∀ ⦃v : V⦄ (hv : ¬v ∈ K), β (componentComplMk G hv)
⊢ ∀ (v : ↑Kᶜ), β (connectedComponentMk (induce Kᶜ G) v)
[PROOFSTEP]
exact fun ⟨v, vnK⟩ => f vnK
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
⊢ Disjoint K ↑C
[PROOFSTEP]
rw [Set.disjoint_iff]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
⊢ K ∩ ↑C ⊆ ∅
[PROOFSTEP]
exact fun v ⟨vK, vC⟩ => vC.choose vK
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
⊢ Pairwise fun C D => Disjoint ↑C ↑D
[PROOFSTEP]
rintro C D ne
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C D : ComponentCompl G K
ne : C ≠ D
⊢ Disjoint ↑C ↑D
[PROOFSTEP]
rw [Set.disjoint_iff]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C D : ComponentCompl G K
ne : C ≠ D
⊢ ↑C ∩ ↑D ⊆ ∅
[PROOFSTEP]
exact fun u ⟨uC, uD⟩ => ne (uC.choose_spec.symm.trans uD.choose_spec)
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
c d : V
x✝ : c ∈ C
dnK : ¬d ∈ K
cd : Adj G c d
cnK : ¬c ∈ K
h : componentComplMk G cnK = C
⊢ componentComplMk G dnK = C
[PROOFSTEP]
rw [← h, ConnectedComponent.eq]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
c d : V
x✝ : c ∈ C
dnK : ¬d ∈ K
cd : Adj G c d
cnK : ¬c ∈ K
h : componentComplMk G cnK = C
⊢ Reachable (induce Kᶜ G) { val := d, property := dnK } { val := c, property := cnK }
[PROOFSTEP]
exact Adj.reachable cd.symm
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
⊢ ∀ (C : ComponentCompl G K), ∃ ck, ck.fst ∈ C ∧ ck.snd ∈ K ∧ Adj G ck.fst ck.snd
[PROOFSTEP]
refine' ComponentCompl.ind fun v vnK => _
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
⊢ ∃ ck, ck.fst ∈ componentComplMk G vnK ∧ ck.snd ∈ K ∧ Adj G ck.fst ck.snd
[PROOFSTEP]
let C : G.ComponentCompl K := G.componentComplMk vnK
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
⊢ ∃ ck, ck.fst ∈ componentComplMk G vnK ∧ ck.snd ∈ K ∧ Adj G ck.fst ck.snd
[PROOFSTEP]
let dis := Set.disjoint_iff.mp C.disjoint_right
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
⊢ ∃ ck, ck.fst ∈ componentComplMk G vnK ∧ ck.snd ∈ K ∧ Adj G ck.fst ck.snd
[PROOFSTEP]
by_contra' h
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
⊢ False
[PROOFSTEP]
suffices Set.univ = (C : Set V) by exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
this : Set.univ = ↑C
⊢ False
[PROOFSTEP]
exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
⊢ Set.univ = ↑C
[PROOFSTEP]
symm
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
⊢ ↑C = Set.univ
[PROOFSTEP]
rw [Set.eq_univ_iff_forall]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
⊢ ∀ (x : V), x ∈ ↑C
[PROOFSTEP]
rintro u
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
u : V
⊢ u ∈ ↑C
[PROOFSTEP]
by_contra unC
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
u : V
unC : ¬u ∈ ↑C
⊢ False
[PROOFSTEP]
obtain ⟨p⟩ := Gc v u
[GOAL]
case intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
u : V
unC : ¬u ∈ ↑C
p : Walk G v u
⊢ False
[PROOFSTEP]
obtain ⟨⟨⟨x, y⟩, xy⟩, -, xC, ynC⟩ := p.exists_boundary_dart (C : Set V) (G.componentComplMk_mem vnK) unC
[GOAL]
case intro.intro.mk.mk.intro.intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
u : V
unC : ¬u ∈ ↑C
p : Walk G v u
x y : V
xy : Adj G (x, y).fst (x, y).snd
xC : { toProd := (x, y), is_adj := xy }.toProd.fst ∈ ↑C
ynC : ¬{ toProd := (x, y), is_adj := xy }.toProd.snd ∈ ↑C
⊢ False
[PROOFSTEP]
exact ynC (mem_of_adj x y xC (fun yK : y ∈ K => h ⟨x, y⟩ xC yK xy) xy)
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
⊢ ↑C ⊆ ↑(hom h C)
[PROOFSTEP]
rintro c ⟨cL, rfl⟩
[GOAL]
case intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
h : K ⊆ L
c : V
cL : ¬c ∈ L
⊢ c ∈ ↑(hom h (componentComplMk G cL))
[PROOFSTEP]
exact ⟨fun h' => cL (h h'), rfl⟩
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ hom h C = D ↔ ¬Disjoint ↑C ↑D
[PROOFSTEP]
rw [Set.not_disjoint_iff]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ hom h C = D ↔ ∃ x, x ∈ ↑C ∧ x ∈ ↑D
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ hom h C = D → ∃ x, x ∈ ↑C ∧ x ∈ ↑D
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
⊢ ∃ x, x ∈ ↑C ∧ x ∈ ↑(hom h C)
[PROOFSTEP]
refine C.ind fun x xnL => ?_
[GOAL]
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x : V
xnL : ¬x ∈ L
⊢ ∃ x_1, x_1 ∈ ↑(componentComplMk G xnL) ∧ x_1 ∈ ↑(hom h (componentComplMk G xnL))
[PROOFSTEP]
exact ⟨x, ⟨xnL, rfl⟩, ⟨fun xK => xnL (h xK), rfl⟩⟩
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ (∃ x, x ∈ ↑C ∧ x ∈ ↑D) → hom h C = D
[PROOFSTEP]
refine C.ind fun x xnL => ?_
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
x : V
xnL : ¬x ∈ L
⊢ (∃ x_1, x_1 ∈ ↑(componentComplMk G xnL) ∧ x_1 ∈ ↑D) → hom h (componentComplMk G xnL) = D
[PROOFSTEP]
rintro ⟨x, ⟨_, e₁⟩, _, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x✝ : V
xnL : ¬x✝ ∈ L
x : V
w✝¹ : ¬x ∈ L
e₁ : componentComplMk G w✝¹ = componentComplMk G xnL
w✝ : ¬x ∈ K
⊢ hom h (componentComplMk G xnL) = componentComplMk G w✝
[PROOFSTEP]
rw [← e₁]
[GOAL]
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x✝ : V
xnL : ¬x✝ ∈ L
x : V
w✝¹ : ¬x ∈ L
e₁ : componentComplMk G w✝¹ = componentComplMk G xnL
w✝ : ¬x ∈ K
⊢ hom h (componentComplMk G w✝¹) = componentComplMk G w✝
[PROOFSTEP]
rfl
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
⊢ hom (_ : L ⊆ L) C = C
[PROOFSTEP]
change C.map _ = C
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
⊢ ConnectedComponent.map (induceHom Hom.id (_ : Lᶜ ⊆ Lᶜ)) C = C
[PROOFSTEP]
erw [induceHom_id G Lᶜ, ConnectedComponent.map_id]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
h' : M ⊆ K
⊢ hom (_ : M ⊆ L) C = hom h' (hom h C)
[PROOFSTEP]
change C.map _ = (C.map _).map _
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom Hom.id (_ : Lᶜ ⊆ Mᶜ)) C =
    ConnectedComponent.map (induceHom Hom.id (_ : Kᶜ ⊆ Mᶜ)) (ConnectedComponent.map (induceHom Hom.id (_ : Lᶜ ⊆ Kᶜ)) C)
[PROOFSTEP]
erw [ConnectedComponent.map_comp, induceHom_comp]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom Hom.id (_ : Lᶜ ⊆ Mᶜ)) C =
    ConnectedComponent.map (induceHom (Hom.comp Hom.id Hom.id) (_ : Set.MapsTo (↑Hom.id ∘ fun x => ↑Hom.id x) Lᶜ Mᶜ)) C
[PROOFSTEP]
rfl
[GOAL]
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
[PROOFSTEP]
classical
constructor
· rintro Cinf L h
  obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.diff Cinf L.finite_toSet)
  exact ⟨componentComplMk _ vL, rfl⟩
· rintro h Cfin
  obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) (Finset.subset_union_left K Cfin.toFinset)
  obtain ⟨v, vD⟩ := D.nonempty
  let Ddis := D.disjoint_right
  simp_rw [Finset.coe_union, Set.Finite.coe_toFinset, Set.disjoint_union_left, Set.disjoint_iff] at Ddis 
  exact Ddis.right ⟨(ComponentCompl.hom_eq_iff_le _ _ _).mp e vD, vD⟩
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rintro Cinf L h
[GOAL]
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
[PROOFSTEP]
obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.diff Cinf L.finite_toSet)
[GOAL]
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
[PROOFSTEP]
exact ⟨componentComplMk _ vL, rfl⟩
[GOAL]
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)
[PROOFSTEP]
rintro h Cfin
[GOAL]
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
[PROOFSTEP]
obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) (Finset.subset_union_left K Cfin.toFinset)
[GOAL]
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
[PROOFSTEP]
obtain ⟨v, vD⟩ := D.nonempty
[GOAL]
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
[PROOFSTEP]
let Ddis := D.disjoint_right
[GOAL]
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
[PROOFSTEP]
simp_rw [Finset.coe_union, Set.Finite.coe_toFinset, Set.disjoint_union_left, Set.disjoint_iff] at Ddis 
[GOAL]
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
[PROOFSTEP]
exact Ddis.right ⟨(ComponentCompl.hom_eq_iff_le _ _ _).mp e vD, vD⟩
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
classical
rcases K.eq_empty_or_nonempty with rfl | h
· dsimp [ComponentCompl]
  rw [Finset.coe_empty, Set.compl_empty]
  have := Gpc.out.subsingleton_connectedComponent
  exact Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm
· let touch (C : G.ComponentCompl K) : {v : V | ∃ k : V, k ∈ K ∧ G.Adj k v} :=
    let p := C.exists_adj_boundary_pair Gpc.out h
    ⟨p.choose.1, p.choose.2, p.choose_spec.2.1, p.choose_spec.2.2.symm⟩
      -- `touch` is injective
  have touch_inj : touch.Injective := fun C D h' =>
    ComponentCompl.pairwise_disjoint.eq
      (Set.not_disjoint_iff.mpr
        ⟨touch C, (C.exists_adj_boundary_pair Gpc.out h).choose_spec.1,
          h'.symm ▸ (D.exists_adj_boundary_pair Gpc.out h).choose_spec.1⟩)
        -- `touch` has finite range
  have : Finite (Set.range touch) :=
    by
    refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _
    apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))
    simp only [Finset.mem_biUnion, mem_neighborFinset, Set.mem_setOf_eq, implies_true]
      -- hence `touch` has a finite domain
  apply Finite.of_injective_finite_range touch_inj
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
rcases K.eq_empty_or_nonempty with rfl | h
[GOAL]
case inl
V : Type u
G : SimpleGraph V
K L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
⊢ Finite (ComponentCompl G ↑∅)
[PROOFSTEP]
dsimp [ComponentCompl]
[GOAL]
case inl
V : Type u
G : SimpleGraph V
K L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
⊢ Finite (ConnectedComponent (induce (↑∅)ᶜ G))
[PROOFSTEP]
rw [Finset.coe_empty, Set.compl_empty]
[GOAL]
case inl
V : Type u
G : SimpleGraph V
K L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
⊢ Finite (ConnectedComponent (induce Set.univ G))
[PROOFSTEP]
have := Gpc.out.subsingleton_connectedComponent
[GOAL]
case inl
V : Type u
G : SimpleGraph V
K L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
this : Subsingleton (ConnectedComponent G)
⊢ Finite (ConnectedComponent (induce Set.univ G))
[PROOFSTEP]
exact Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm
[GOAL]
case inr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
let touch (C : G.ComponentCompl K) : {v : V | ∃ k : V, k ∈ K ∧ G.Adj k v} :=
  let p := C.exists_adj_boundary_pair Gpc.out h
  ⟨p.choose.1, p.choose.2, p.choose_spec.2.1, p.choose_spec.2.2.symm⟩
    -- `touch` is injective
[GOAL]
case inr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
have touch_inj : touch.Injective := fun C D h' =>
  ComponentCompl.pairwise_disjoint.eq
    (Set.not_disjoint_iff.mpr
      ⟨touch C, (C.exists_adj_boundary_pair Gpc.out h).choose_spec.1,
        h'.symm ▸ (D.exists_adj_boundary_pair Gpc.out h).choose_spec.1⟩)
      -- `touch` has finite range
[GOAL]
case inr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
touch_inj : Function.Injective touch
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
have : Finite (Set.range touch) :=
  by
  refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _
  apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))
  simp only [Finset.mem_biUnion, mem_neighborFinset, Set.mem_setOf_eq, implies_true]
    -- hence `touch` has a finite domain
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
touch_inj : Function.Injective touch
⊢ Finite ↑(Set.range touch)
[PROOFSTEP]
refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
touch_inj : Function.Injective touch
⊢ Set.Finite {v | ∃ k, k ∈ K ∧ Adj G k v}
[PROOFSTEP]
apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
touch_inj : Function.Injective touch
⊢ ∀ (x : V), (x ∈ Finset.biUnion K fun v => neighborFinset G v) ↔ x ∈ {v | ∃ k, k ∈ K ∧ Adj G k v}
[PROOFSTEP]
simp only [Finset.mem_biUnion, mem_neighborFinset, Set.mem_setOf_eq, implies_true]
  -- hence `touch` has a finite domain
[GOAL]
case inr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
touch_inj : Function.Injective touch
this : Finite ↑(Set.range touch)
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
apply Finite.of_injective_finite_range touch_inj
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
sec : s ∈ SimpleGraph.end G
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : ¬v ∈ L.unop
hs : s L = componentComplMk G vnL
⊢ s K = componentComplMk G (_ : ¬v ∈ fun a => a ∈ K.unop.val)
[PROOFSTEP]
rw [← sec h, hs]
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
sec : s ∈ SimpleGraph.end G
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : ¬v ∈ L.unop
hs : s L = componentComplMk G vnL
⊢ (componentComplFunctor G).map h (componentComplMk G vnL) = componentComplMk G (_ : ¬v ∈ fun a => a ∈ K.unop.val)
[PROOFSTEP]
apply ComponentCompl.hom_mk _ (le_of_op_hom h : _ ⊆ _)
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : (Finset V)ᵒᵖ
C : (componentComplFunctor G).obj K
⊢ Set.Infinite (ComponentCompl.supp C) ↔ C ∈ Functor.eventualRange (componentComplFunctor G) K
[PROOFSTEP]
simp only [C.infinite_iff_in_all_ranges, CategoryTheory.Functor.eventualRange, Set.mem_iInter, Set.mem_range,
  componentComplFunctor_map]
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : (Finset V)ᵒᵖ
C : (componentComplFunctor G).obj K
⊢ (∀ (L : Finset V) (h : K.unop ⊆ L), ∃ D, ComponentCompl.hom h D = C) ↔
    ∀ (i : (Finset V)ᵒᵖ) (i_1 : i ⟶ K), ∃ y, ComponentCompl.hom (_ : K.unop ≤ i.unop) y = C
[PROOFSTEP]
exact ⟨fun h Lop KL => h Lop.unop (le_of_op_hom KL), fun h L KL => h (Opposite.op L) (opHomOfLE KL)⟩
