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
V : Type u
G : SimpleGraph V
K L L' M : Set V
⊢ Function.Injective supp
refine' ConnectedComponent.ind₂ _
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 }
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
rintro ⟨v, hv⟩ ⟨w, hw⟩ h
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 }
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 }
simp only [Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq, ComponentCompl.supp] at h⊢
no goals
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 }
exact ((h v).mp ⟨hv, Reachable.refl _⟩).choose_spec