awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk (K := K) vnK
dis : K ∩ (↑C : Set V) ⊆ ∅ := ⋯
h : ∀ (ck : V × V) (_ : ck.1 ∈ G.componentComplMk (K := K) vnK) (_ : ck.2 ∈ K), ¬G.Adj ck.1 ck.2
symm : (↑C : Set V) = Set.univ
⊢ Set.univ = (↑C : Set V)

Tactic:
symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk (K := K) vnK
dis : K ∩ (↑C : Set V) ⊆ ∅ := ⋯
h : ∀ (ck : V × V) (_ : ck.1 ∈ G.componentComplMk (K := K) vnK) (_ : ck.2 ∈ K), ¬G.Adj ck.1 ck.2
rw : ∀ (x : V), x ∈ (↑C : Set V)
⊢ (↑C : Set V) = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk (K := K) vnK
dis : K ∩ (↑C : Set V) ⊆ ∅ := ⋯
h : ∀ (ck : V × V) (_ : ck.1 ∈ G.componentComplMk (K := K) vnK) (_ : ck.2 ∈ K), ¬G.Adj ck.1 ck.2
u : V
by_contra : ∀ (unC : u ∉ (↑C : Set V)), False
⊢ u ∈ (↑C : Set V)

Tactic:
by_contra unC
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk (K := K) vnK
dis : K ∩ (↑C : Set V) ⊆ ∅ := ⋯
h : ∀ (ck : V × V) (_ : ck.1 ∈ G.componentComplMk (K := K) vnK) (_ : ck.2 ∈ K), ¬G.Adj ck.1 ck.2
u : V
unC : u ∉ (↑C : Set V)
obtain : ∀ (p : G.Walk v u), False
⊢ False

Tactic:
obtain ⟨p⟩ := Gc v u
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk (K := K) vnK
dis : K ∩ (↑C : Set V) ⊆ ∅ := ⋯
h : ∀ (ck : V × V) (_ : ck.1 ∈ G.componentComplMk (K := K) vnK) (_ : ck.2 ∈ K), ¬G.Adj ck.1 ck.2
u : V
unC : u ∉ (↑C : Set V)
p : G.Walk v u
obtain :
  ∀ (x y : V) (xy : G.Adj (x, y).1 (x, y).2) (xC : { fst := x, snd := y, adj := xy : G.Dart }.toProd.1 ∈ (↑C : Set V))
    (ynC : { fst := x, snd := y, adj := xy : G.Dart }.toProd.2 ∉ (↑C : Set V)), False
⊢ False

Tactic:
obtain ⟨⟨⟨x, y⟩, xy⟩, -, xC, ynC⟩ :=
    p.exists_boundary_dart (C : Set V) (G.componentComplMk_mem vnK) unC

Premises used: SimpleGraph.Walk.exists_boundary_dart, SimpleGraph.componentComplMk_mem, SetLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk (K := K) vnK
dis : K ∩ (↑C : Set V) ⊆ ∅ := ⋯
h : ∀ (ck : V × V) (_ : ck.1 ∈ G.componentComplMk (K := K) vnK) (_ : ck.2 ∈ K), ¬G.Adj ck.1 ck.2
u : V
unC : u ∉ (↑C : Set V)
p : G.Walk v u
x y : V
xy : G.Adj (x, y).1 (x, y).2
xC : { fst := x, snd := y, adj := xy : G.Dart }.toProd.1 ∈ (↑C : Set V)
ynC : { fst := x, snd := y, adj := xy : G.Dart }.toProd.2 ∉ (↑C : Set V)
⊢ False

Tactic:
ynC (mem_of_adj x y xC (fun yK : y ∈ K => h ⟨x, y⟩ xC yK xy) xy)

Premises used: Prod.mk, SimpleGraph.ComponentCompl.mem_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
v : V
vnK : v ∉ K
C : G.ComponentCompl K := G.componentComplMk (K := K) vnK
dis : K ∩ (↑C : Set V) ⊆ ∅ := ⋯
h : ∀ (ck : V × V) (_ : ck.1 ∈ G.componentComplMk (K := K) vnK) (_ : ck.2 ∈ K), ¬G.Adj ck.1 ck.2
u : V
unC : u ∉ (↑C : Set V)
p : G.Walk v u
x y : V
xy : G.Adj (x, y).1 (x, y).2
xC : { fst := x, snd := y, adj := xy : G.Dart }.toProd.1 ∈ (↑C : Set V)
ynC : { fst := x, snd := y, adj := xy : G.Dart }.toProd.2 ∉ (↑C : Set V)
⊢ False

Tactic:
exact ynC (mem_of_adj x y xC (fun yK : y ∈ K => h ⟨x, y⟩ xC yK xy) xy)

Premises used: Prod.mk, SimpleGraph.ComponentCompl.mem_of_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
h : K ⊆ L
c : V
cL : c ∉ L
⊢ c ∈ (↑(hom (K := K) (L := L) h (G.componentComplMk (K := L) cL)) : Set V)

Tactic:
⟨fun h' => cL (h h'), rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, SimpleGraph.ComponentCompl.supp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
h : K ⊆ L
c : V
cL : c ∉ L
⊢ c ∈ (↑(hom (K := K) (L := L) h (G.componentComplMk (K := L) cL)) : Set V)

Tactic:
exact ⟨fun h' => cL (h h'), rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
K L : Set V
G : SimpleGraph V
v : V
vK : v ∉ K
h : L ⊆ K
⊢ v ∈ hom (K := L) (L := K) h (G.componentComplMk (K := K) vK)

Tactic:
subset_hom (G.componentComplMk vK) h (G.componentComplMk_mem vK)

Premises used: SimpleGraph.ComponentCompl.subset_hom, SimpleGraph.componentComplMk_mem, SimpleGraph.componentComplMk
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ hom (K := K) (L := L) h C = D ↔ (↑C : Set V) ⊆ (↑D : Set V)

Tactic:
⟨fun h' => h' ▸ C.subset_hom h, C.ind fun _ vnL vD => (vD ⟨vnL, rfl⟩).choose_spec⟩

Premises used: SimpleGraph.ComponentCompl.subset_hom, SimpleGraph.ComponentCompl.ind, Eq.rec, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
rw : hom (K := K) (L := L) h C = D ↔ ∃ x ∈ (↑C : Set V), x ∈ (↑D : Set V)
⊢ hom (K := K) (L := L) h C = D ↔ ¬Disjoint (↑C : Set V) (↑D : Set V)

Tactic:
rw [Set.not_disjoint_iff]

Premises used: Set.not_disjoint_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
mp : hom (K := K) (L := L) h C = D → ∃ x ∈ (↑C : Set V), x ∈ (↑D : Set V)
mpr : (∃ x ∈ (↑C : Set V), x ∈ (↑D : Set V)) → hom (K := K) (L := L) h C = D
⊢ hom (K := K) (L := L) h C = D ↔ ∃ x ∈ (↑C : Set V), x ∈ (↑D : Set V)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
⊢ ∃ x ∈ (↑C : Set V), x ∈ (↑(hom (K := K) (L := L) h C) : Set V)

Tactic:
C.ind fun x xnL => ?_

Premises used: SimpleGraph.ComponentCompl.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
mp :
  ∀ (x : V) (xnL : x ∉ L),
    ∃ x_1 ∈ (↑(G.componentComplMk (K := L) xnL) : Set V),
      x_1 ∈ (↑(hom (K := K) (L := L) h (G.componentComplMk (K := L) xnL)) : Set V)
⊢ ∃ x ∈ (↑C : Set V), x ∈ (↑(hom (K := K) (L := L) h C) : Set V)

Tactic:
refine C.ind fun x xnL => ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x : V
xnL : x ∉ L
⊢ ∃ x_1 ∈ (↑(G.componentComplMk (K := L) xnL) : Set V),
    x_1 ∈ (↑(hom (K := K) (L := L) h (G.componentComplMk (K := L) xnL)) : Set V)

Tactic:
⟨x, ⟨xnL, rfl⟩, ⟨fun xK => xnL (h xK), rfl⟩⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x : V
xnL : x ∉ L
⊢ ∃ x_1 ∈ (↑(G.componentComplMk (K := L) xnL) : Set V),
    x_1 ∈ (↑(hom (K := K) (L := L) h (G.componentComplMk (K := L) xnL)) : Set V)

Tactic:
exact ⟨x, ⟨xnL, rfl⟩, ⟨fun xK => xnL (h xK), rfl⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
⊢ (∃ x ∈ (↑C : Set V), x ∈ (↑D : Set V)) → hom (K := K) (L := L) h C = D

Tactic:
C.ind fun x xnL => ?_

Premises used: SimpleGraph.ComponentCompl.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
D : G.ComponentCompl K
mpr :
  ∀ (x : V) (xnL : x ∉ L),
    (∃ x_1 ∈ (↑(G.componentComplMk (K := L) xnL) : Set V), x_1 ∈ (↑D : Set V)) →
      hom (K := K) (L := L) h (G.componentComplMk (K := L) xnL) = D
⊢ (∃ x ∈ (↑C : Set V), x ∈ (↑D : Set V)) → hom (K := K) (L := L) h C = D

Tactic:
refine C.ind fun x xnL => ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x_1 : V
xnL : x_1 ∉ L
x : V
w : x ∉ L
e₁ : G.componentComplMk (K := L) w = G.componentComplMk (K := L) xnL
w_1 : x ∉ K
mpr : hom (K := K) (L := L) h (G.componentComplMk (K := L) w) = G.componentComplMk (K := K) w_1
⊢ hom (K := K) (L := L) h (G.componentComplMk (K := L) xnL) = G.componentComplMk (K := K) w_1

Tactic:
rw [← e₁]
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
x_1 : V
xnL : x_1 ∉ L
x : V
w : x ∉ L
e₁ : G.componentComplMk (K := L) w = G.componentComplMk (K := L) xnL
w_1 : x ∉ K
⊢ hom (K := K) (L := L) h (G.componentComplMk (K := L) w) = G.componentComplMk (K := K) w_1

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
L : Set V
C : G.ComponentCompl L
rw : ConnectedComponent.map Hom.id C = C
rw₁ rw₂ : C = C
⊢ ConnectedComponent.map (induceHom (s := Lᶜ) (t := Lᶜ) Hom.id ⋯) C = C

Tactic:
rw [induceHom_id G Lᶜ, ConnectedComponent.map_id]

Premises used: Compl.compl, SimpleGraph.induceHom_id, SimpleGraph.ConnectedComponent.map_id
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
rw :
  ConnectedComponent.map (induceHom (s := Lᶜ) (t := Mᶜ) Hom.id ⋯) C =
    ConnectedComponent.map (induceHom (s := Lᶜ) (t := Mᶜ) (Hom.comp Hom.id Hom.id) ⋯) C
⊢ Eq (α := (induce Mᶜ G).ConnectedComponent) (ConnectedComponent.map (induceHom (s := Lᶜ) (t := Mᶜ) Hom.id ⋯) C)
    (ConnectedComponent.map (V := (↑Kᶜ : Type u)) (induceHom (s := Kᶜ) (t := Mᶜ) Hom.id ⋯)
      (ConnectedComponent.map (induceHom (s := Lᶜ) (t := Kᶜ) Hom.id ⋯) C))

Tactic:
rw [ConnectedComponent.map_comp, induceHom_comp]

Premises used: SimpleGraph.ConnectedComponent.map_comp, SimpleGraph.induceHom_comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom (s := Lᶜ) (t := Mᶜ) Hom.id ⋯) C =
    ConnectedComponent.map (induceHom (s := Lᶜ) (t := Mᶜ) (Hom.comp Hom.id Hom.id) ⋯) C

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
v : V
vnL : v ∉ L
h : K ⊆ L
⊢ hom (K := K) (L := L) h (G.componentComplMk (K := L) vnL) = G.componentComplMk (K := K) ⋯

Tactic:
rfl

Premises used: Subtype.map, SimpleGraph.connectedComponentMk, SimpleGraph.ConnectedComponent.map, Set.MapsTo.restrict, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Set V
C : G.ComponentCompl L
h : K ⊆ L
Cinf : (↑C : Set V).Infinite
⊢ (↑(hom (K := K) (L := L) h C) : Set V).Infinite

Tactic:
Set.Infinite.mono (C.subset_hom h) Cinf

Premises used: SimpleGraph.ComponentCompl.subset_hom, Set.Infinite.mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl (↑K : Set V)
mp :
  C.supp (K := (↑K : Set V)).Infinite →
    ∀ (L : Finset V) (h : K ⊆ L),
      ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C
mpr :
  (∀ (L : Finset V) (h : K ⊆ L),
      ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C) →
    C.supp (K := (↑K : Set V)).Infinite
⊢ C.supp (K := (↑K : Set V)).Infinite ↔
    ∀ (L : Finset V) (h : K ⊆ L),
      ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl (↑K : Set V)
Cinf : C.supp (K := (↑K : Set V)).Infinite
L : Finset V
h : K ⊆ L
mp :
  ∀ (v : V) (vL : v ∉ (↑L : Set V)) (vK : v ∉ (↑K : Set V))
    (Cinf : (G.componentComplMk (K := (↑K : Set V)) vK).supp (K := (↑K : Set V)).Infinite),
    ∃ (D : G.ComponentCompl (↑L : Set V)),
      hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = G.componentComplMk (K := (↑K : Set V)) vK
⊢ ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C

Tactic:
obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.diff Cinf L.finite_toSet)

Premises used: Set.Infinite.nonempty, Finset.finite_toSet, rfl, Set.Infinite.diff
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Finset V
h : K ⊆ L
v : V
vL : v ∉ (↑L : Set V)
vK : v ∉ (↑K : Set V)
Cinf : (G.componentComplMk (K := (↑K : Set V)) vK).supp (K := (↑K : Set V)).Infinite
⊢ ∃ (D : G.ComponentCompl (↑L : Set V)),
    hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = G.componentComplMk (K := (↑K : Set V)) vK

Tactic:
⟨componentComplMk _ vL, rfl⟩

Premises used: Exists.intro, SimpleGraph.componentComplMk, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L : Finset V
h : K ⊆ L
v : V
vL : v ∉ (↑L : Set V)
vK : v ∉ (↑K : Set V)
Cinf : (G.componentComplMk (K := (↑K : Set V)) vK).supp (K := (↑K : Set V)).Infinite
⊢ ∃ (D : G.ComponentCompl (↑L : Set V)),
    hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = G.componentComplMk (K := (↑K : Set V)) vK

Tactic:
exact ⟨componentComplMk _ vL, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl (↑K : Set V)
h :
  ∀ (L : Finset V) (h : K ⊆ L),
    ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C
Cfin : C.supp (K := (↑K : Set V)).Finite
mpr :
  ∀ (D : G.ComponentCompl (↑(K ∪ Cfin.toFinset (s := C.supp (K := (↑K : Set V)))) : Set V))
    (e : hom (K := (↑K : Set V)) (L := (↑(K ∪ Cfin.toFinset (s := C.supp (K := (↑K : Set V)))) : Set V)) ⋯ D = C), False
⊢ False

Tactic:
obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) Finset.subset_union_left

Premises used: Finset.subset_union_left, Set.Finite.toFinset, Union.union
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl (↑K : Set V)
h :
  ∀ (L : Finset V) (h : K ⊆ L),
    ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C
Cfin : C.supp (K := (↑K : Set V)).Finite
D : G.ComponentCompl (↑(K ∪ Cfin.toFinset (s := C.supp (K := (↑K : Set V)))) : Set V)
e : hom (K := (↑K : Set V)) (L := (↑(K ∪ Cfin.toFinset (s := C.supp (K := (↑K : Set V)))) : Set V)) ⋯ D = C
mpr : ∀ (v : V) (vD : v ∈ (↑D : Set V)), False
⊢ False

Tactic:
obtain ⟨v, vD⟩ := D.nonempty

Premises used: SimpleGraph.ComponentCompl.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl (↑K : Set V)
h :
  ∀ (L : Finset V) (h : K ⊆ L),
    ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C
Cfin : C.supp (K := (↑K : Set V)).Finite
D : G.ComponentCompl (↑(K ∪ Cfin.toFinset (s := C.supp (K := (↑K : Set V)))) : Set V)
e : hom (K := (↑K : Set V)) (L := (↑(K ∪ Cfin.toFinset (s := C.supp (K := (↑K : Set V)))) : Set V)) ⋯ D = C
v : V
vD : v ∈ (↑D : Set V)
Ddis : Disjoint (↑(K ∪ Cfin.toFinset (s := C.supp (K := (↑K : Set V)))) : Set V) (↑D : Set V) := ⋯
⊢ (↑K : Set V) ∩ (↑D : Set V) ⊆ ∅ ∧ C.supp (K := (↑K : Set V)) ∩ (↑D : Set V) ⊆ ∅

Tactic:
simp_rw [Finset.coe_union, Set.Finite.coe_toFinset, Set.disjoint_union_left,
        Set.disjoint_iff] at Ddis

Premises used: Set.Finite.coe_toFinset, Set.disjoint_union_left, Set.disjoint_iff, Finset.coe_union
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl (↑K : Set V)
h :
  ∀ (L : Finset V) (h : K ⊆ L),
    ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C
Cfin : C.supp (K := (↑K : Set V)).Finite
D : G.ComponentCompl (↑(K ∪ Cfin.toFinset (s := C.supp (K := (↑K : Set V)))) : Set V)
e : hom (K := (↑K : Set V)) (L := (↑(K ∪ Cfin.toFinset (s := C.supp (K := (↑K : Set V)))) : Set V)) ⋯ D = C
v : V
vD : v ∈ (↑D : Set V)
Ddis : (↑K : Set V) ∩ (↑D : Set V) ⊆ ∅ ∧ C.supp (K := (↑K : Set V)) ∩ (↑D : Set V) ⊆ ∅
⊢ False

Tactic:
Ddis.right ⟨(ComponentCompl.hom_eq_iff_le _ _ _).mp e vD, vD⟩

Premises used: Set.Mem, And.right, SimpleGraph.ComponentCompl.hom_eq_iff_le, And.intro, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl (↑K : Set V)
h :
  ∀ (L : Finset V) (h : K ⊆ L),
    ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C
Cfin : C.supp (K := (↑K : Set V)).Finite
D : G.ComponentCompl (↑(K ∪ Cfin.toFinset (s := C.supp (K := (↑K : Set V)))) : Set V)
e : hom (K := (↑K : Set V)) (L := (↑(K ∪ Cfin.toFinset (s := C.supp (K := (↑K : Set V)))) : Set V)) ⋯ D = C
v : V
vD : v ∈ (↑D : Set V)
Ddis : (↑K : Set V) ∩ (↑D : Set V) ⊆ ∅ ∧ C.supp (K := (↑K : Set V)) ∩ (↑D : Set V) ⊆ ∅
⊢ False

Tactic:
exact Ddis.right ⟨(ComponentCompl.hom_eq_iff_le _ _ _).mp e vD, vD⟩

Premises used: And.right, SimpleGraph.ComponentCompl.hom_eq_iff_le, And.intro, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl (↑K : Set V)
mp :
  C.supp (K := (↑K : Set V)).Infinite →
    ∀ (L : Finset V) (h : K ⊆ L),
      ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C
mpr mpr₁ :
  (∀ (L : Finset V) (h : K ⊆ L),
      ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C) →
    C.supp (K := (↑K : Set V)).Infinite
⊢ C.supp (K := (↑K : Set V)).Infinite ↔
    ∀ (L : Finset V) (h : K ⊆ L),
      ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C

Tactic:
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
      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⟩

Premises used: Set.Finite.coe_toFinset, Set.disjoint_union_left, rfl, Set.disjoint_iff, Finset.coe_union
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K_1 L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
inl : Finite.{u + 1} (G.ComponentCompl (↑∅ : Set V))
inr : ∀ (h : K.Nonempty), Finite.{u + 1} (G.ComponentCompl (↑K : Set V))
⊢ Finite.{u + 1} (G.ComponentCompl (↑K : Set V))

Tactic:
rcases K.eq_empty_or_nonempty with rfl | h

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
inl : Finite.{u + 1} (ConnectedComponent (V := (↑Set.univ : Type u)) (induce Set.univ G))
⊢ Finite.{u + 1} (induce (↑∅ : Set V)ᶜ G).ConnectedComponent

Tactic:
rw [Finset.coe_empty, Set.compl_empty]

Premises used: Finset.coe_empty, Set.compl_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
⊢ Subsingleton.{u + 1} G.ConnectedComponent

Tactic:
have := Gpc.out.subsingleton_connectedComponent
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
this : Subsingleton.{u + 1} G.ConnectedComponent
⊢ Finite.{u + 1} (ConnectedComponent (V := (↑Set.univ : Type u)) (induce Set.univ G))

Tactic:
Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm

Premises used: Finite.of_equiv, SimpleGraph.induceUnivIso, SimpleGraph.Iso.connectedComponentEquiv, Equiv.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
this : Subsingleton.{u + 1} G.ConnectedComponent
⊢ Finite.{u + 1} (ConnectedComponent (V := (↑Set.univ : Type u)) (induce Set.univ G))

Tactic:
exact Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm

Premises used: Finite.of_equiv, SimpleGraph.induceUnivIso, SimpleGraph.Iso.connectedComponentEquiv, Equiv.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K_1 L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
h : K.Nonempty
touch : (C : G.ComponentCompl (↑K : Set V)) → (↑{v : V | ∃ k ∈ K, G.Adj k v} : Type u) :=
  fun (C : G.ComponentCompl (↑K : Set V)) ↦
    let p := ⋯;
    Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {v : V | ∃ k ∈ K, G.Adj k v} x)
      p.choose (p := fun (ck : V × V) ↦ ck.1 ∈ C ∧ ck.2 ∈ (↑K : Set V) ∧ G.Adj ck.1 ck.2).1 ⋯
⊢ Function.Injective touch

Tactic:
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⟩)
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K_1 L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
h : K.Nonempty
touch : (C : G.ComponentCompl (↑K : Set V)) → (↑{v : V | ∃ k ∈ K, G.Adj k v} : Type u) :=
  fun (C : G.ComponentCompl (↑K : Set V)) ↦
    let p := ⋯;
    Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {v : V | ∃ k ∈ K, G.Adj k v} x)
      p.choose (p := fun (ck : V × V) ↦ ck.1 ∈ C ∧ ck.2 ∈ (↑K : Set V) ∧ G.Adj ck.1 ck.2).1 ⋯
touch_inj : Function.Injective touch
⊢ Finite.{u + 1} (↑(Set.range touch) : Type u)

Tactic:
@Subtype.finite _ (Set.Finite.to_subtype ?_) _

Premises used: Subtype.finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K_1 L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
h : K.Nonempty
touch : (C : G.ComponentCompl (↑K : Set V)) → (↑{v : V | ∃ k ∈ K, G.Adj k v} : Type u) :=
  fun (C : G.ComponentCompl (↑K : Set V)) ↦
    let p := ⋯;
    Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {v : V | ∃ k ∈ K, G.Adj k v} x)
      p.choose (p := fun (ck : V × V) ↦ ck.1 ∈ C ∧ ck.2 ∈ (↑K : Set V) ∧ G.Adj ck.1 ck.2).1 ⋯
touch_inj : Function.Injective touch
refine : Set.Finite.{u} (α := V) {v : V | ∃ k ∈ K, G.Adj k v}
⊢ Finite.{u + 1} (↑(Set.range touch) : Type u)

Tactic:
refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _

Premises used: Subtype.finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K_1 L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
h : K.Nonempty
touch : (C : G.ComponentCompl (↑K : Set V)) → (↑{v : V | ∃ k ∈ K, G.Adj k v} : Type u) :=
  fun (C : G.ComponentCompl (↑K : Set V)) ↦
    let p := ⋯;
    Subtype.mk (p := fun (x : V) ↦ Membership.mem (γ := Set V) {v : V | ∃ k ∈ K, G.Adj k v} x)
      p.choose (p := fun (ck : V × V) ↦ ck.1 ∈ C ∧ ck.2 ∈ (↑K : Set V) ∧ G.Adj ck.1 ck.2).1 ⋯
touch_inj : Function.Injective touch
apply :
  ∀ (x : V),
    Membership.mem (γ := Finset V) (K.biUnion fun (v : V) ↦ G.neighborFinset v) x ↔
      Membership.mem (γ := Set V) {v : V | ∃ k ∈ K, G.Adj k v} x
⊢ Set.Finite.{u} (α := V) {v : V | ∃ k ∈ K, G.Adj k v}

Tactic:
apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))

Premises used: SimpleGraph.neighborFinset, Finset.biUnion, Set.Finite.ofFinset