awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v w : (↑Kᶜ : Type u)
p : (induce Kᶜ G).Walk v w
nil :
  ∀ {u : (↑Kᶜ : Type u)},
    Walk.IsPath.{u} (V := (↑Kᶜ : Type u)) (G := induce Kᶜ G) (u := u) Walk.nil →
      Eq.{u_1} (α := β) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) u) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) u)
⊢ p.IsPath → Eq.{u_1} (α := β) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) v) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) w)
have cons : ∀ {u v w : (↑Kᶜ : Type u)} (a : (induce Kᶜ G).Adj u v) (q : (induce Kᶜ G).Walk v w)
  (ih : q.IsPath → Eq.{u_1} (α := β) ((fun (vv : (↑Kᶜ : Type u)) ↦ f sorry) v) ((fun (vv : (↑Kᶜ : Type u)) ↦ f sorry) w)),
  (Walk.cons a q).IsPath → Eq.{u_1} (α := β) ((fun (vv : (↑Kᶜ : Type u)) ↦ f sorry) u) ((fun (vv : (↑Kᶜ : Type u)) ↦ f sorry) w)
Tactic: induction p with
    | nil => rintro _; rfl
    | cons a q ih => rename_i u v w; rintro h'; exact (h u.prop v.prop a).trans (ih h'.of_cons)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K : Set V
β : G.ComponentCompl K → Prop
f : ∀ ⦃v : V⦄ (hv : v ∉ K), β (G.componentComplMk (K := K) hv)
⊢ ∀ (C : G.ComponentCompl K), β C
have h : ∀ (v : (↑Kᶜ : Type u)), β ((induce Kᶜ G).connectedComponentMk v)
Tactic: apply ConnectedComponent.ind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
⊢ Disjoint K (↑C : Set V)
have rw : K ∩ (↑C : Set V) ⊆ ∅
Tactic: rw [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
ne : C ≠ D
⊢ Disjoint (↑C : Set V) (↑D : Set V)
have rw : (↑C : Set V) ∩ (↑D : Set V) ⊆ ∅
Tactic: rw [Set.disjoint_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
c d : V
h_1 : c ∈ C
dnK : d ∉ K
cd : G.Adj c d
cnK : c ∉ K
h : G.componentComplMk (K := K) cnK = C
⊢ G.componentComplMk (K := K) dnK = C
have rw : (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) d dnK) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) c cnK)
Tactic: rw [← h, ConnectedComponent.eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
⊢ ∀ (C : G.ComponentCompl K), ∃ (ck : V × V), ck.1 ∈ C ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2
have refine : ∀ (v : V) (vnK : v ∉ K), ∃ (ck : V × V), ck.1 ∈ G.componentComplMk (K := K) vnK ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2
Tactic: refine ComponentCompl.ind fun v vnK => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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) ⊆ ∅ := ⋯
⊢ ∃ (ck : V × V), ck.1 ∈ G.componentComplMk (K := K) vnK ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2
have by_contra! : ∀ (h : ∀ (ck : V × V) (_ : ck.1 ∈ G.componentComplMk (K := K) vnK) (_ : ck.2 ∈ K), ¬G.Adj ck.1 ck.2), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
⊢ False
have suffices : Set.univ = (↑C : Set V)
Tactic: suffices Set.univ = (C : Set V) by exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
⊢ Set.univ = (↑C : Set V)
have symm : (↑C : Set V) = Set.univ
Tactic: symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
⊢ (↑C : Set V) = Set.univ
have rw : ∀ (x : V), x ∈ (↑C : Set V)
Tactic: rw [Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
⊢ u ∈ (↑C : Set V)
have by_contra : ∀ (unC : u ∉ (↑C : Set V)), False
Tactic: by_contra unC
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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)
⊢ False
have obtain : ∀ (p : G.Walk v u), False
Tactic: obtain ⟨p⟩ := Gc v u
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
⊢ False
have 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
Tactic: obtain ⟨⟨⟨x, y⟩, xy⟩, -, xC, ynC⟩ :=
    p.exists_boundary_dart (C : Set V) (G.componentComplMk_mem vnK) unC
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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 ↔ ¬Disjoint (↑C : Set V) (↑D : Set V)
have rw : hom (K := K) (L := L) h C = D ↔ ∃ x ∈ (↑C : Set V), x ∈ (↑D : Set V)
Tactic: rw [Set.not_disjoint_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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 ↔ ∃ x ∈ (↑C : Set V), x ∈ (↑D : Set V)
have mp : hom (K := K) (L := L) h C = D → ∃ x ∈ (↑C : Set V), x ∈ (↑D : Set V)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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)
⊢ hom (K := K) (L := L) h C = D ↔ ∃ x ∈ (↑C : Set V), x ∈ (↑D : Set V)
have mpr : (∃ x ∈ (↑C : Set V), x ∈ (↑D : Set V)) → hom (K := K) (L := L) h C = D
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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)
have 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)
Tactic: refine C.ind fun x xnL => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
have 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
Tactic: refine C.ind fun x xnL => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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) xnL) = G.componentComplMk (K := K) w_1
have mpr : hom (K := K) (L := L) h (G.componentComplMk (K := L) w) = G.componentComplMk (K := K) w_1
Tactic: rw [← e₁]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
L : Set V
C : G.ComponentCompl L
⊢ ConnectedComponent.map (induceHom (s := Lᶜ) (t := Lᶜ) Hom.id ⋯) C = C
have rw : ConnectedComponent.map Hom.id C = C
Tactic: rw [induceHom_id G Lᶜ, ConnectedComponent.map_id]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
L : Set V
C : G.ComponentCompl L
rw : ConnectedComponent.map Hom.id C = C
⊢ ConnectedComponent.map (induceHom (s := Lᶜ) (t := Lᶜ) Hom.id ⋯) C = C
have rw₁ : C = C
Tactic: rw [induceHom_id G Lᶜ, ConnectedComponent.map_id]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
⊢ 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))
have rw : ConnectedComponent.map (induceHom (s := Lᶜ) (t := Mᶜ) Hom.id sorry) C =
  ConnectedComponent.map (induceHom (s := Lᶜ) (t := Mᶜ) (Hom.comp Hom.id Hom.id) sorry) C
Tactic: rw [ConnectedComponent.map_comp, induceHom_comp]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl (↑K : Set V)
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
⊢ ∃ (D : G.ComponentCompl (↑L : Set V)), hom (K := (↑K : Set V)) (L := (↑L : Set V)) h D = C
have 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
Tactic: obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.diff Cinf L.finite_toSet)
Cleared hypotheses: C, Cinf
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
⊢ False
have 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)) sorry D = C), False
Tactic: obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) Finset.subset_union_left
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
⊢ False
have mpr : ∀ (v : V) (vD : v ∈ (↑D : Set V)), False
Tactic: obtain ⟨v, vD⟩ := D.nonempty
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (hypothesis)
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) := ⋯
⊢ False
have Ddis₁ : (↑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
Cleared hypotheses: Ddis
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K : Finset V
C : G.ComponentCompl (↑K : Set V)
⊢ 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
have 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
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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
⊢ 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
have 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
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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K_1 L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
⊢ Finite.{u + 1} (G.ComponentCompl (↑K : Set V))
have inl : Finite.{u + 1} (G.ComponentCompl (↑∅ : Set V))
Tactic: rcases K.eq_empty_or_nonempty with rfl | h
Cleared hypotheses: K
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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))
⊢ Finite.{u + 1} (G.ComponentCompl (↑K : Set V))
have inr : ∀ (h : K.Nonempty), Finite.{u + 1} (G.ComponentCompl (↑K : Set V))
Tactic: rcases K.eq_empty_or_nonempty with rfl | h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
⊢ Finite.{u + 1} (induce (↑∅ : Set V)ᶜ G).ConnectedComponent
have inl : Finite.{u + 1} (ConnectedComponent (V := (↑Set.univ : Type u)) (induce Set.univ G))
Tactic: rw [Finset.coe_empty, Set.compl_empty]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (hypothesis)
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
⊢ Finite.{u + 1} (ConnectedComponent (V := (↑Set.univ : Type u)) (induce Set.univ G))
have this : Subsingleton.{u + 1} G.ConnectedComponent
Tactic: have := Gpc.out.subsingleton_connectedComponent
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (hypothesis)
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 ⋯
⊢ Finite.{u + 1} (G.ComponentCompl (↑K : Set V))
have touch_inj : 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⟩)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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)
have refine : Set.Finite.{u} (α := V) {v : V | ∃ k ∈ K, G.Adj k v}
Tactic: refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
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
⊢ Set.Finite.{u} (α := V) {v : V | ∃ k ∈ K, G.Adj k v}
have 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
Tactic: apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (hypothesis)
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} (G.ComponentCompl (↑K : Set V))
have this : Finite.{u + 1} (↑(Set.range touch) : Type u)
Tactic: 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Ends.Defs (goal)
Goal:
V : Type u
G : SimpleGraph V
K_1 L M : Set V
inst : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
⊢ Finite.{u + 1} (G.ComponentCompl (↑K : Set V))
have inl : Finite.{u + 1} (G.ComponentCompl (↑∅ : Set V))
Tactic: classical
  rcases K.eq_empty_or_nonempty with rfl | h
  -- If K is empty, then removing K doesn't change the graph, which is connected, hence has a
  -- single connected component
  · dsimp [ComponentCompl]
    rw [Finset.coe_empty, Set.compl_empty]
    have := Gpc.out.subsingleton_connectedComponent
    exact Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm
  -- Otherwise, we consider the function `touch` mapping a connected component to one of its
  -- vertices adjacent to `K`.
  · 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
Cleared hypotheses: K