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
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
refine' ComponentCompl.ind fun v vnK => _
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
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
let C : G.ComponentCompl K := G.componentComplMk vnK
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
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
let dis := Set.disjoint_iff.mp C.disjoint_right
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, ck.fst ∈ componentComplMk G vnK ∧ ck.snd ∈ K ∧ Adj G ck.fst ck.snd
⊢ False
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
by_contra' h
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
⊢ False
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, ck.fst ∈ componentComplMk G vnK ∧ ck.snd ∈ K ∧ Adj G ck.fst ck.snd
⊢ False
simp only [not_exists, not_and] at h
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
⊢ Set.univ = ↑C
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
⊢ False
suffices Set.univ = (C : Set V) by exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
⊢ ↑C = Set.univ
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
⊢ Set.univ = ↑C
symm
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
⊢ ∀ (x : V), x ∈ ↑C
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
⊢ ↑C = Set.univ
rw [Set.eq_univ_iff_forall]
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
u : V
⊢ u ∈ ↑C
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
⊢ ∀ (x : V), x ∈ ↑C
rintro u
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
u : V
unC : ¬u ∈ ↑C
⊢ False
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
u : V
⊢ u ∈ ↑C
by_contra unC
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
u : V
unC : ¬u ∈ ↑C
p : Walk G v u
⊢ False
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
u : V
unC : ¬u ∈ ↑C
⊢ False
obtain ⟨p⟩ := Gc v u
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.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
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
u : V
unC : ¬u ∈ ↑C
p : Walk G v u
⊢ False
obtain ⟨⟨⟨x, y⟩, xy⟩, -, xC, ynC⟩ :=
  p.exists_boundary_dart (C : Set V) (G.componentComplMk_mem vnK) unC
no goals
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.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
exact ynC (mem_of_adj x y xC (fun yK : y ∈ K => h ⟨x, y⟩ xC yK xy) xy)
no goals
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 : ∀ (x : V × V), x.fst ∈ componentComplMk G vnK → x.snd ∈ K → ¬Adj G x.fst x.snd
this : Set.univ = ↑C
⊢ False
exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩