awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∀ (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:
simp only [Finset.mem_biUnion, mem_neighborFinset, Set.mem_setOf_eq, implies_true]

Premises used: Set.mem_setOf_eq, SimpleGraph.mem_neighborFinset, implies_true, Finset.mem_biUnion
-- 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:
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]
-- 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
this : Finite.{u + 1} (↑(Set.range touch) : Type u)
⊢ Finite.{u + 1} (G.ComponentCompl (↑K : Set V))

Tactic:
apply Finite.of_injective_finite_range touch_inj

Premises used: Finite.of_injective_finite_range
-- 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 inr₁ : ∀ (h : K.Nonempty), Finite.{u + 1} (G.ComponentCompl (↑K : Set V))
⊢ Finite.{u + 1} (G.ComponentCompl (↑K : 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

Premises used: Finset.coe_empty, Set.compl_empty, SimpleGraph.ComponentCompl, rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
x : (Finset V)ᵒᵖ
h :
  ∀ (x_1 : G.ComponentCompl (↑(Opposite.unop x) : Set V)) (x_2 : V),
    x_2 ∈
        (TypeCat.Fun.toFun
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾ComponentCompl.hom (K := (↑(Opposite.unop x) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯))
              x_1).supp
          (K := (↑(Opposite.unop x) : Set V)) ↔
      x_2 ∈
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (G.ComponentCompl (↑(Opposite.unop x) : Set V)))).toFun x_1).supp
          (K := (↑(Opposite.unop x) : Set V))
⊢ ↾ComponentCompl.hom (K := (↑(Opposite.unop x) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯ =
    𝟙 (G.ComponentCompl (↑(Opposite.unop x) : Set V))

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
x : (Finset V)ᵒᵖ
x_1 : G.ComponentCompl (↑(Opposite.unop x) : Set V)
x_2 : V
⊢ x_2 ∈
      (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾ComponentCompl.hom (K := (↑(Opposite.unop x) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯))
            x_1).supp
        (K := (↑(Opposite.unop x) : Set V)) ↔
    x_2 ∈
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (G.ComponentCompl (↑(Opposite.unop x) : Set V)))).toFun x_1).supp
        (K := (↑(Opposite.unop x) : Set V))

Tactic:
simp [ComponentCompl.hom_refl]

Premises used: SimpleGraph.ComponentCompl.hom_refl
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
x Y Z : (Finset V)ᵒᵖ
h : x ⟶ Y
h' : Y ⟶ Z
h₁ :
  ∀ (C : G.ComponentCompl (↑(Opposite.unop x) : Set V)) (x_1 : V),
    x_1 ∈
        (TypeCat.Fun.toFun
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾ComponentCompl.hom (K := (↑(Opposite.unop Z) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯))
              C).supp
          (K := (↑(Opposite.unop Z) : Set V)) ↔
      x_1 ∈
        (TypeCat.Fun.toFun
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾ComponentCompl.hom (K := (↑(Opposite.unop Y) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯ ≫
                  ↾ComponentCompl.hom (K := (↑(Opposite.unop Z) : Set V)) (L := (↑(Opposite.unop Y) : Set V)) ⋯))
              C).supp
          (K := (↑(Opposite.unop Z) : Set V))
⊢ Eq (α := G.ComponentCompl (↑(Opposite.unop x) : Set V) ⟶ G.ComponentCompl (↑(Opposite.unop Z) : Set V))
    (↾ComponentCompl.hom (K := (↑(Opposite.unop Z) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯)
    (↾ComponentCompl.hom (K := (↑(Opposite.unop Y) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯ ≫
      ↾ComponentCompl.hom (K := (↑(Opposite.unop Z) : Set V)) (L := (↑(Opposite.unop Y) : Set V)) ⋯)

Tactic:
ext C
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K L M : Set V
x Y Z : (Finset V)ᵒᵖ
h : x ⟶ Y
h' : Y ⟶ Z
C : G.ComponentCompl (↑(Opposite.unop x) : Set V)
x_1 : V
⊢ x_1 ∈
      (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾ComponentCompl.hom (K := (↑(Opposite.unop Z) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯))
            C).supp
        (K := (↑(Opposite.unop Z) : Set V)) ↔
    x_1 ∈
      (TypeCat.Fun.toFun
            (ConcreteCategory.hom (FC := TypeCat.Fun)
              (↾ComponentCompl.hom (K := (↑(Opposite.unop Y) : Set V)) (L := (↑(Opposite.unop x) : Set V)) ⋯ ≫
                ↾ComponentCompl.hom (K := (↑(Opposite.unop Z) : Set V)) (L := (↑(Opposite.unop Y) : Set V)) ⋯))
            C).supp
        (K := (↑(Opposite.unop Z) : Set V))

Tactic:
simp [C.hom_trans (le_of_op_hom h) (le_of_op_hom h')]

Premises used: SimpleGraph.ComponentCompl.hom_trans, CategoryTheory.le_of_op_hom
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
sec : s ∈ G.end
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : v ∉ Opposite.unop L
hs : s L = G.componentComplMk (K := (↑(Opposite.unop L) : Set V)) vnL
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (G.componentComplFunctor.map h) :
        (a : (fun (X : Type u) ↦ X) (G.componentComplFunctor.obj L)) →
          (fun (X : Type u) ↦ X) (G.componentComplFunctor.obj K))
      (G.componentComplMk (K := (↑(Opposite.unop L) : Set V)) vnL) =
    G.componentComplMk (K := (↑(Opposite.unop K) : Set V)) ⋯
⊢ s K = G.componentComplMk (K := (↑(Opposite.unop K) : Set V)) ⋯

Tactic:
rw [← sec h, hs]
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
sec : s ∈ G.end
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : v ∉ Opposite.unop L
hs : s L = G.componentComplMk (K := (↑(Opposite.unop L) : Set V)) vnL
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (G.componentComplFunctor.map h) :
        (a : (fun (X : Type u) ↦ X) (G.componentComplFunctor.obj L)) →
          (fun (X : Type u) ↦ X) (G.componentComplFunctor.obj K))
      (G.componentComplMk (K := (↑(Opposite.unop L) : Set V)) vnL) =
    G.componentComplMk (K := (↑(Opposite.unop K) : Set V)) ⋯

Tactic:
apply ComponentCompl.hom_mk _ (le_of_op_hom h : _ ⊆ _)

Premises used: SimpleGraph.ComponentCompl.hom_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : (Finset V)ᵒᵖ
C : G.componentComplFunctor.obj K
simp :
  (∀ (L : Finset V) (h : Opposite.unop K ⊆ L),
      ∃ (D : G.ComponentCompl (↑L : Set V)),
        ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑L : Set V)) h D = C) ↔
    ∀ (i : (Finset V)ᵒᵖ) (i_1 : i ⟶ K),
      ∃ (y : G.componentComplFunctor.obj i),
        (ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑(Opposite.unop i) : Set V)) ⋯) :
              (a : G.componentComplFunctor.obj i) → G.componentComplFunctor.obj K)
            y =
          C
⊢ (ComponentCompl.supp (K := (↑(Opposite.unop K) : Set V)) C).Infinite ↔ C ∈ G.componentComplFunctor.eventualRange K

Tactic:
simp only [C.infinite_iff_in_all_ranges, CategoryTheory.Functor.eventualRange, Set.mem_iInter,
    Set.mem_range, componentComplFunctor_map]

Premises used: Set.mem_range, Set.mem_iInter, SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges, CategoryTheory.Functor.eventualRange, SimpleGraph.componentComplFunctor_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : (Finset V)ᵒᵖ
C : G.componentComplFunctor.obj K
⊢ (∀ (L : Finset V) (h : Opposite.unop K ⊆ L),
      ∃ (D : G.ComponentCompl (↑L : Set V)),
        ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑L : Set V)) h D = C) ↔
    ∀ (i : (Finset V)ᵒᵖ) (i_1 : i ⟶ K),
      ∃ (y : G.componentComplFunctor.obj i),
        (ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑(Opposite.unop i) : Set V)) ⋯) :
              (a : G.componentComplFunctor.obj i) → G.componentComplFunctor.obj K)
            y =
          C

Tactic:
⟨fun h Lop KL => h Lop.unop (le_of_op_hom KL), fun h L KL =>
      h (Opposite.op L) (opHomOfLE KL)⟩

Premises used: CategoryTheory.le_of_op_hom, CategoryTheory.opHomOfLE, Opposite.op, Iff.intro, Opposite.unop
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs
Goal:
V : Type u
G : SimpleGraph V
K : (Finset V)ᵒᵖ
C : G.componentComplFunctor.obj K
⊢ (∀ (L : Finset V) (h : Opposite.unop K ⊆ L),
      ∃ (D : G.ComponentCompl (↑L : Set V)),
        ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑L : Set V)) h D = C) ↔
    ∀ (i : (Finset V)ᵒᵖ) (i_1 : i ⟶ K),
      ∃ (y : G.componentComplFunctor.obj i),
        (ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑(Opposite.unop i) : Set V)) ⋯) :
              (a : G.componentComplFunctor.obj i) → G.componentComplFunctor.obj K)
            y =
          C

Tactic:
exact
    ⟨fun h Lop KL => h Lop.unop (le_of_op_hom KL), fun h L KL =>
      h (Opposite.op L) (opHomOfLE KL)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
inst : Finite V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
property : s ∈ G.end
intro : ∀ (val : Fintype V), False
⊢ False

Tactic:
cases nonempty_fintype V

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
inst : Finite V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
property : s ∈ G.end
val : Fintype V
intro : ∀ (v : V) (h : v ∈ (↑(s (Opposite.op Finset.univ)) : Set V)), False
⊢ False

Tactic:
obtain ⟨v, h⟩ := (s <| Opposite.op Finset.univ).nonempty

Premises used: Finset.univ, Opposite.op, SimpleGraph.ComponentCompl.nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
inst : Finite V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
property : s ∈ G.end
val : Fintype V
v : V
h : v ∈ (↑(s (Opposite.op Finset.univ)) : Set V)
⊢ v ∈ (↑(Opposite.unop (Opposite.op Finset.univ)) : Set V)

Tactic:
simp only [Finset.coe_univ, Set.mem_univ]

Premises used: Finset.coe_univ, Set.mem_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
inst : Finite V
s : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j
property : s ∈ G.end
val : Fintype V
v : V
h : v ∈ (↑(s (Opposite.op Finset.univ)) : Set V)
⊢ False

Tactic:
exact Set.disjoint_iff.mp (s _).disjoint_right
        ⟨by simp only [Finset.coe_univ, Set.mem_univ], h⟩

Premises used: SimpleGraph.ComponentCompl.disjoint_right, And.intro, Iff.mp, Set.disjoint_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
e : (↑G.end : Type)
K : (Finset V)ᵒᵖ
⊢ (ComponentCompl.supp (K := (↑(Opposite.unop K) : Set V))
      ((↑e : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j) K)).Infinite

Tactic:
(e.val K).infinite_iff_in_all_ranges.mpr (fun L h => ?_)

Premises used: Iff.mpr, SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
e : (↑G.end : Type)
K : (Finset V)ᵒᵖ
refine :
  ∀ (L : Finset V) (h : Opposite.unop K ⊆ L),
    ∃ (D : G.ComponentCompl (↑L : Set V)),
      ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑L : Set V)) h D =
        (↑e : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j) K
⊢ (ComponentCompl.supp (K := (↑(Opposite.unop K) : Set V))
      ((↑e : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j) K)).Infinite

Tactic:
refine (e.val K).infinite_iff_in_all_ranges.mpr (fun L h => ?_)

Premises used: Iff.mpr, SimpleGraph.ComponentCompl.infinite_iff_in_all_ranges, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
e : (↑G.end : Type)
K : (Finset V)ᵒᵖ
L : Finset V
h : Opposite.unop K ⊆ L
⊢ Opposite.unop K ⊆ Opposite.unop (Opposite.op L)

Tactic:
change Opposite.unop K ⊆ Opposite.unop (Opposite.op L) at h

Premises used: Opposite.op, Opposite.unop
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
e : (↑G.end : Type)
K : (Finset V)ᵒᵖ
L : Finset V
h : Opposite.unop K ⊆ Opposite.unop (Opposite.op L)
⊢ ∃ (D : G.ComponentCompl (↑L : Set V)),
    ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑L : Set V)) h D =
      (↑e : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j) K

Tactic:
⟨e.val (Opposite.op L), (e.prop (CategoryTheory.opHomOfLE h))⟩

Premises used: CategoryTheory.opHomOfLE, Opposite.op, Subtype.prop, Exists.intro, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
e : (↑G.end : Type)
K : (Finset V)ᵒᵖ
L : Finset V
h : Opposite.unop K ⊆ Opposite.unop (Opposite.op L)
⊢ ∃ (D : G.ComponentCompl (↑L : Set V)),
    ComponentCompl.hom (K := (↑(Opposite.unop K) : Set V)) (L := (↑L : Set V)) h D =
      (↑e : (j : (Finset V)ᵒᵖ) → G.componentComplFunctor.obj j) K

Tactic:
exact ⟨e.val (Opposite.op L), (e.prop (CategoryTheory.opHomOfLE h))⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
inst : Infinite V
K : (Finset V)ᵒᵖ
⊢ Nonempty (G.componentComplFunctor.obj K)

Tactic:
G.componentCompl_nonempty_of_infinite K.unop

Premises used: SimpleGraph.ConnectedComponent, Opposite.unop, SimpleGraph.componentCompl_nonempty_of_infinite
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
inst : G.LocallyFinite
inst_1 : Fact G.Preconnected
K : (Finset V)ᵒᵖ
⊢ Finite (G.componentComplFunctor.obj K)

Tactic:
G.componentCompl_finite K.unop

Premises used: SimpleGraph.ConnectedComponent, SimpleGraph.componentCompl_finite, Opposite.unop
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
inst : G.LocallyFinite
inst_1 : Fact G.Preconnected
inst_2 : Infinite V
⊢ G.end.Nonempty

Tactic:
apply nonempty_sections_of_finite_inverse_system G.componentComplFunctor

Premises used: nonempty_sections_of_finite_inverse_system, SimpleGraph.componentComplFunctor
-- Module: Mathlib.Combinatorics.SimpleGraph.Ends.Properties
Goal:
V : Type
G : SimpleGraph V
inst : G.LocallyFinite
inst_1 : Fact G.Preconnected
inst_2 : Infinite V
⊢ G.end.Nonempty

Tactic:
classical
  apply nonempty_sections_of_finite_inverse_system G.componentComplFunctor

Premises used: nonempty_sections_of_finite_inverse_system, SimpleGraph.componentComplFunctor
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
p : SimpleGraph V → Prop
h : G.IsExtremal p
⊢ p G

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
⊢ (∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p) ↔ ∃ (G : SimpleGraph V), p G

Tactic:
⟨fun ⟨_, _, h⟩ ↦ ⟨_, h.1⟩, fun ⟨G, hp⟩ ↦ ?_⟩

Premises used: _private.0.SimpleGraph.exists_isExtremal_iff_exists.match_1, Exists, SimpleGraph.IsExtremal, And.left, _private.0.SimpleGraph.exists_isExtremal_iff_exists.match_2, Iff.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
refine :
  (∃ (G : SimpleGraph V), p G) →
    ∀ (G : SimpleGraph V) (hp : p G), ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p
⊢ (∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p) ↔ ∃ (G : SimpleGraph V), p G

Tactic:
refine ⟨fun ⟨_, _, h⟩ ↦ ⟨_, h.1⟩, fun ⟨G, hp⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp : p G
apply : Finset.Nonempty.{u_1} (α := SimpleGraph V) {G : SimpleGraph V | p G}
⊢ ∃ (x : SimpleGraph V),
    Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x ∧
      ∀ (x' : SimpleGraph V),
        Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x' → #x'.edgeFinset ≤ #x.edgeFinset

Tactic:
apply exists_max_image { G | p G } (#·.edgeFinset)

Premises used: Finset.univ, Finset.exists_max_image, SimpleGraph.edgeFinset, Finset.card, Finset.filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp : p G
⊢ Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} G

Tactic:
simpa using hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h_1 : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp : p G
w : SimpleGraph V
h : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} G
⊢ Finset.Nonempty.{u_1} (α := SimpleGraph V) {G : SimpleGraph V | p G}

Tactic:
use G, by simpa using hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp : p G
obtain :
  ∀ (G' : SimpleGraph V) (hp' : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} G')
    (h :
      ∀ (x' : SimpleGraph V),
        Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x' → #x'.edgeFinset ≤ #G'.edgeFinset),
    ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p
⊢ ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p

Tactic:
obtain ⟨G', hp', h⟩ := by
    apply exists_max_image { G | p G } (#·.edgeFinset)
    use G, by simpa using hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h_1 : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp : p G
G' : SimpleGraph V
hp' : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} G'
h :
  ∀ (x' : SimpleGraph V),
    Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x' → #x'.edgeFinset ≤ #G'.edgeFinset
h₁ : G'.IsExtremal p
⊢ ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal p

Tactic:
use G', inferInstanceAs (DecidableRel G'.Adj)
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h_1 : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp : p G
G' : SimpleGraph V
hp' : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} G'
h :
  ∀ (x' : SimpleGraph V),
    Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x' → #x'.edgeFinset ≤ #G'.edgeFinset
⊢ p G'

Tactic:
simpa using hp'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h_1 : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp_1 : p G
G' : SimpleGraph V
hp' : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} G'
h :
  ∀ (x' : SimpleGraph V),
    Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x' → #x'.edgeFinset ≤ #G'.edgeFinset
x : SimpleGraph V
x_1 : DecidableRel x.Adj
hp : p x
⊢ Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x

Tactic:
simpa using hp
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h_1 : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp_1 : p G
G' : SimpleGraph V
hp' : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} G'
h :
  ∀ (x' : SimpleGraph V),
    Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x' → #x'.edgeFinset ≤ #G'.edgeFinset
x : SimpleGraph V
x_1 : DecidableRel x.Adj
hp : p x
⊢ #x.edgeFinset ≤ #G'.edgeFinset

Tactic:
convert! h _ (by simpa using hp)
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
p : SimpleGraph V → Prop
h_1 : ∃ (G : SimpleGraph V), p G
G : SimpleGraph V
hp : p G
G' : SimpleGraph V
hp' : Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} G'
h :
  ∀ (x' : SimpleGraph V),
    Membership.mem (γ := Finset (SimpleGraph V)) {G : SimpleGraph V | p G} x' → #x'.edgeFinset ≤ #G'.edgeFinset
⊢ G'.IsExtremal p

Tactic:
exact ⟨by simpa using hp', fun _ _ hp ↦ by convert! h _ (by simpa using hp)⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
Goal:
V : Type u_1
inst : Fintype V
W : Type u_2
H : SimpleGraph W
h : H ≠ ⊥
⊢ ∃ (G : SimpleGraph V) (x : DecidableRel G.Adj), G.IsExtremal H.Free

Tactic:
(exists_isExtremal_iff_exists H.Free).mpr ⟨⊥, free_bot h⟩

Premises used: Iff.mpr, SimpleGraph.Free, SimpleGraph.free_bot, Bot.bot, SimpleGraph.exists_isExtremal_iff_exists, Exists.intro