awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ G.center.Nonempty

Tactic:
exists_eccent_eq_radius

Premises used: Set.Mem, setOf, SimpleGraph.center, Set.Nonempty, SimpleGraph.exists_eccent_eq_radius
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
u : α
⊢ u ∈ G.center ↔ G.eccent u = G.radius

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SimpleGraph.center
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
rw : Set.univ ⊆ G.center ↔ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
⊢ G.center = Set.univ ↔ G.radius = G.ediam

Tactic:
rw [radius_eq_ediam_iff, ← Set.univ_subset_iff]

Premises used: Set.univ_subset_iff, SimpleGraph.radius_eq_ediam_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
⊢ Set.univ ⊆ G.center ↔ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
refine_1 : ∀ (h : Set.univ ⊆ G.center), ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
refine_2 : ∀ (h : ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e), Set.univ ⊆ G.center
⊢ Set.univ ⊆ G.center ↔ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : Set.univ ⊆ G.center
h₁ : ∀ (u : α), G.eccent u = G.radius
⊢ ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e

Tactic:
use G.radius

Premises used: SimpleGraph.radius
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : Set.univ ⊆ G.center
⊢ ∀ (u : α), G.eccent u = G.radius

Tactic:
fun _ ↦ h trivial

Premises used: trivial, Set.Mem, setOf, SimpleGraph.center
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : Set.univ ⊆ G.center
⊢ ∀ (u : α), G.eccent u = G.radius

Tactic:
exact fun _ ↦ h trivial

Premises used: trivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
h : ∃ (e : ℕ∞), ∀ (u : α), G.eccent u = e
refine_2 : ∀ (e : ℕ∞) (h : ∀ (u : α), G.eccent u = e), Set.univ ⊆ G.center
⊢ Set.univ ⊆ G.center

Tactic:
obtain ⟨e, h⟩ := h
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
u : α
hu : Membership.mem (γ := Set α) Set.univ u
refine_2 : e = G.radius
⊢ u ∈ G.center

Tactic:
rw [mem_center_iff, h u]

Premises used: SimpleGraph.mem_center_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
u : α
hu : Membership.mem (γ := Set α) Set.univ u
⊢ e = G.radius

Tactic:
le_antisymm (le_iInf fun u ↦ (h u).ge) ((h Classical.ofNonempty) ▸ radius_le_eccent)

Premises used: Classical.ofNonempty, Eq.ge, le_iInf, Eq.rec, le_antisymm, SimpleGraph.radius_le_eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Nonempty α
e : ℕ∞
h : ∀ (u : α), G.eccent u = e
u : α
hu : Membership.mem (γ := Set α) Set.univ u
⊢ e = G.radius

Tactic:
exact le_antisymm (le_iInf fun u ↦ (h u).ge) ((h Classical.ofNonempty) ▸ radius_le_eccent)

Premises used: Classical.ofNonempty, Eq.ge, le_iInf, Eq.rec, le_antisymm, SimpleGraph.radius_le_eccent
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Subsingleton α
rw : ∀ (x : α), x ∈ G.center
⊢ G.center = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Subsingleton α
u : α
rw : Nonempty α ∧ Subsingleton α
⊢ u ∈ G.center

Tactic:
rw [mem_center_iff, eccent_eq_zero_of_subsingleton u, eq_comm, radius_eq_zero_iff]

Premises used: SimpleGraph.radius_eq_zero_iff, SimpleGraph.mem_center_iff, eq_comm, SimpleGraph.eccent_eq_zero_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
G : SimpleGraph α
inst : Subsingleton α
u : α
left : Nonempty α
right : Subsingleton α
left₁ left₂ left₃ left₄ left₅ : Nonempty α
⊢ Nonempty α ∧ Subsingleton α

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inl : Subsingleton α → Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ
inr : Nontrivial α → Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ

Tactic:
cases subsingleton_or_nontrivial α

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Subsingleton α
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ

Tactic:
center_eq_univ_of_subsingleton

Premises used: SimpleGraph.center_eq_univ_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Subsingleton α
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ

Tactic:
exact center_eq_univ_of_subsingleton

Premises used: SimpleGraph.center_eq_univ_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Nontrivial α
inr : ∀ (x : α), Membership.mem (γ := Set α) (center ⊥) x
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊥) Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Nontrivial α
u : α
inr : eccent ⊥ u = radius.{u_1} (α := α) ⊥
inr₁ : ⊤ = radius.{u_1} (α := α) ⊥
inr₂ inr₃ : Eq (α := ℕ∞) ⊤ ⊤
⊢ Membership.mem (γ := Set α) (center ⊥) u

Tactic:
rw [mem_center_iff, eccent_bot, radius_bot]

Premises used: SimpleGraph.eccent_bot, SimpleGraph.mem_center_iff, SimpleGraph.radius_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
inl : Subsingleton α → Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ
inr : Nontrivial α → Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ

Tactic:
cases subsingleton_or_nontrivial α

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Subsingleton α
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ

Tactic:
center_eq_univ_of_subsingleton

Premises used: SimpleGraph.center_eq_univ_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Subsingleton α
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ

Tactic:
exact center_eq_univ_of_subsingleton

Premises used: SimpleGraph.center_eq_univ_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Nontrivial α
inr : ∀ (x : α), Membership.mem (γ := Set α) (center ⊤) x
⊢ Eq.{u_1 + 1} (α := Set α) (center ⊤) Set.univ

Tactic:
rw [Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Diam
Goal:
α : Type u_1
h : Nontrivial α
u : α
inr : eccent ⊤ u = radius.{u_1} (α := α) ⊤
inr₁ : 1 = radius.{u_1} (α := α) ⊤
inr₂ inr₃ : Eq (α := ℕ∞) 1 1
⊢ Membership.mem (γ := Set α) (center ⊤) u

Tactic:
rw [mem_center_iff, eccent_top, radius_top]

Premises used: SimpleGraph.mem_center_iff, SimpleGraph.radius_top, SimpleGraph.eccent_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
⊢ Function.Injective.{u + 1, u + 1} (α := G.ComponentCompl K) (supp (K := K))

Tactic:
ConnectedComponent.ind₂ ?_

Premises used: SimpleGraph.ConnectedComponent.ind₂, Function.Injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
refine :
  ∀ (v w : (↑Kᶜ : Type u)),
    supp (K := K) ((induce Kᶜ G).connectedComponentMk v) = supp (K := K) ((induce Kᶜ G).connectedComponentMk w) →
      (induce Kᶜ G).connectedComponentMk v = (induce Kᶜ G).connectedComponentMk w
⊢ Function.Injective.{u + 1, u + 1} (α := G.ComponentCompl K) (supp (K := K))

Tactic:
refine ConnectedComponent.ind₂ ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h :
  supp (K := K) ((induce Kᶜ G).connectedComponentMk (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv)) =
    supp (K := K) ((induce Kᶜ G).connectedComponentMk (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw))
simp :
  ∀
    (h :
      ∀ (x : V),
        (∃ (h : x ∉ K),
            (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) x ⋯)
              (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv)) ↔
          ∃ (h : x ∉ K),
            (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) x ⋯)
              (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw)),
    (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw)
⊢ (induce Kᶜ G).connectedComponentMk (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv) =
    (induce Kᶜ G).connectedComponentMk (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw)

Tactic:
simp only [Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq, ComponentCompl.supp] at h ⊢

Premises used: Set.mem_setOf_eq, SimpleGraph.ConnectedComponent.eq, Set.ext_iff, SimpleGraph.ComponentCompl.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h :
  ∀ (x : V),
    (∃ (h : x ∉ K),
        (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) x ⋯)
          (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv)) ↔
      ∃ (h : x ∉ K),
        (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) x ⋯)
          (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw)
⊢ (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw)

Tactic:
((h v).mp ⟨hv, Reachable.refl _⟩).choose_spec

Premises used: Exists.choose_spec, Exists.intro, Iff.mp, SimpleGraph.Reachable.refl
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h :
  ∀ (x : V),
    (∃ (h : x ∉ K),
        (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) x ⋯)
          (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv)) ↔
      ∃ (h : x ∉ K),
        (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) x ⋯)
          (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw)
⊢ (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v hv) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w hw)

Tactic:
exact ((h v).mp ⟨hv, Reachable.refl _⟩).choose_spec

Premises used: Exists.choose_spec, Exists.intro, Iff.mp, SimpleGraph.Reachable.refl
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
⊢ C.supp (K := K) = D.supp (K := K) ↔ C = D

Tactic:
ComponentCompl.supp_injective.eq_iff

Premises used: Function.Injective.eq_iff, SimpleGraph.ComponentCompl.supp_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
v : V
C : G.ComponentCompl K
⊢ v ∈ C ↔ ∃ (vK : v ∉ K), G.componentComplMk (K := K) vK = C

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, SimpleGraph.ComponentCompl.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
K : Set V
G : SimpleGraph V
v : V
vK : v ∉ K
⊢ v ∈ G.componentComplMk (K := K) vK

Tactic:
⟨vK, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, SimpleGraph.ComponentCompl.supp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
rw : (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v vK) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w wK)
⊢ G.componentComplMk (K := K) vK = G.componentComplMk (K := K) wK

Tactic:
rw [ConnectedComponent.eq]

Premises used: SimpleGraph.ConnectedComponent.eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
h : (induce Kᶜ G).Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v vK) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w wK)
⊢ (induce Kᶜ G).Reachable (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v vK) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w wK)

Tactic:
apply Adj.reachable

Premises used: SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ (induce Kᶜ G).Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v vK) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w wK)

Tactic:
a
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
K : Set V
G : SimpleGraph V
v w : V
vK : v ∉ K
wK : w ∉ K
a : G.Adj v w
⊢ (induce Kᶜ G).Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) v vK) (Subtype.mk (p := fun (x : V) ↦ x ∈ Kᶜ) w wK)

Tactic:
exact a
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G_1 : SimpleGraph V
K_1 L M : Set V
G : SimpleGraph V
inst : Infinite V
K : Finset V
⊢ Nonempty.{u + 1} (G.ComponentCompl (↑K : Set V))

Tactic:
let ⟨_, kK⟩ := K.finite_toSet.infinite_compl.nonempty
  ⟨componentComplMk _ kK⟩

Premises used: Set.Infinite.nonempty, Nonempty.intro, SetLike.coe, Set.Finite.infinite_compl, Nonempty, SimpleGraph.ComponentCompl, Finset.finite_toSet, SimpleGraph.componentComplMk, _private.0.SimpleGraph.componentCompl_nonempty_of_infinite.match_1
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
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 u : (↑Kᶜ : Type u)
h_1 : 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)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
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_1 w_1 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 ⋯) v) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) w)
h' : (Walk.cons a q).IsPath
⊢ Eq.{u_1} (α := β) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) u) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) w)

Tactic:
(h u.prop v.prop a).trans (ih h'.of_cons)

Premises used: SimpleGraph.Walk.IsPath.of_cons, Subtype.prop, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
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_1 w_1 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 ⋯) v) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) w)
h' : (Walk.cons a q).IsPath
⊢ Eq.{u_1} (α := β) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) u) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) w)

Tactic:
exact (h u.prop v.prop a).trans (ih h'.of_cons)

Premises used: SimpleGraph.Walk.IsPath.of_cons, Subtype.prop, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
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)
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 ⋯) v) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) w)),
    (Walk.cons a q).IsPath →
      Eq.{u_1} (α := β) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) u) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) w)
⊢ p.IsPath → Eq.{u_1} (α := β) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) v) ((fun (vv : (↑Kᶜ : Type u)) ↦ f ⋯) 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)
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
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)
h : ∀ (v : (↑Kᶜ : Type u)), β ((induce Kᶜ G).connectedComponentMk v)
⊢ ∀ (C : G.ComponentCompl K), β C

Tactic:
apply ConnectedComponent.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
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)
⊢ ∀ (v : (↑Kᶜ : Type u)), β ((induce Kᶜ G).connectedComponentMk v)

Tactic:
fun ⟨v, vnK⟩ => f vnK

Premises used: SimpleGraph.connectedComponentMk, Compl.compl, _private.0.SimpleGraph.ComponentCompl.ind.match_1, SimpleGraph.induce
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
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)
⊢ ∀ (v : (↑Kᶜ : Type u)), β ((induce Kᶜ G).connectedComponentMk v)

Tactic:
exact fun ⟨v, vnK⟩ => f vnK
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
⊢ (↑C : Set V) = (↑D : Set V) ↔ C = D

Tactic:
SetLike.coe_set_eq

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
⊢ (↑C : Set V).Nonempty

Tactic:
C.ind fun v vnK => ⟨v, vnK, rfl⟩

Premises used: SimpleGraph.ComponentCompl.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
⊢ ∃ (v : V) (h : v ∉ K), G.componentComplMk (K := K) h = C

Tactic:
C.nonempty

Premises used: Set.Mem, setOf, Set.Nonempty, SimpleGraph.ComponentCompl.nonempty, SimpleGraph.ComponentCompl.supp
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
rw : K ∩ (↑C : Set V) ⊆ ∅
⊢ Disjoint K (↑C : Set V)

Tactic:
rw [Set.disjoint_iff]

Premises used: Set.disjoint_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
⊢ K ∩ (↑C : Set V) ⊆ ∅

Tactic:
fun v ⟨vK, vC⟩ => vC.choose vK

Premises used: Membership.mem, Set.Subset, Exists.choose, _private.0.SimpleGraph.ComponentCompl.disjoint_right.match_1, EmptyCollection.emptyCollection
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
⊢ K ∩ (↑C : Set V) ⊆ ∅

Tactic:
exact fun v ⟨vK, vC⟩ => vC.choose vK
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
c : V
cC : c ∈ C
⊢ c ∉ K

Tactic:
fun cK =>
  Set.disjoint_iff.mp C.disjoint_right ⟨cK, cC⟩

Premises used: SimpleGraph.ComponentCompl.disjoint_right, Set.Mem, And.intro, Iff.mp, Not, Set.disjoint_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
ne : C ≠ D
rw : (↑C : Set V) ∩ (↑D : Set V) ⊆ ∅
⊢ Disjoint (↑C : Set V) (↑D : Set V)

Tactic:
rw [Set.disjoint_iff]

Premises used: Set.disjoint_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
ne : C ≠ D
⊢ (↑C : Set V) ∩ (↑D : Set V) ⊆ ∅

Tactic:
fun u ⟨uC, uD⟩ => ne (uC.choose_spec.symm.trans uD.choose_spec)

Premises used: Exists.choose_spec, Membership.mem, Set.Subset, EmptyCollection.emptyCollection, Eq.symm, _private.0.SimpleGraph.ComponentCompl.pairwise_disjoint.match_1, Eq.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
ne : C ≠ D
⊢ (↑C : Set V) ∩ (↑D : Set V) ⊆ ∅

Tactic:
exact fun u ⟨uC, uD⟩ => ne (uC.choose_spec.symm.trans uD.choose_spec)
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
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
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)
⊢ G.componentComplMk (K := K) dnK = C

Tactic:
rw [← h, ConnectedComponent.eq]

Premises used: SimpleGraph.ConnectedComponent.eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
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
⊢ (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:
Adj.reachable cd.symm

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
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
⊢ (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:
exact Adj.reachable cd.symm

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Adj.reachable
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
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

Tactic:
ComponentCompl.ind fun v vnK => ?_

Premises used: SimpleGraph.ComponentCompl.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
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
⊢ ∀ (C : G.ComponentCompl K), ∃ (ck : V × V), ck.1 ∈ C ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2

Tactic:
refine ComponentCompl.ind fun v vnK => ?_
-- 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) ⊆ ∅ := ⋯
by_contra! : ∀ (h : ∀ (ck : V × V) (_ : ck.1 ∈ G.componentComplMk (K := K) vnK) (_ : ck.2 ∈ K), ¬G.Adj ck.1 ck.2), False
⊢ ∃ (ck : V × V), ck.1 ∈ G.componentComplMk (K := K) vnK ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2

Tactic:
by_contra! h
-- 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
this : Set.univ = (↑C : Set V)
⊢ False

Tactic:
dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩

Premises used: Exists.choose_spec, Set.Mem, Eq.rec, And.intro, Set.mem_univ, Set.Nonempty.some
-- 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
this : Set.univ = (↑C : Set V)
⊢ False

Tactic:
exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩

Premises used: Exists.choose_spec, Eq.rec, And.intro, Set.mem_univ, Set.Nonempty.some
-- 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
suffices : Set.univ = (↑C : Set V)
⊢ False

Tactic:
suffices Set.univ = (C : Set V) by exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩