awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
pos : ∀ (hvOdd : Odd (Nat.card V)), ∃ (u : Set V), G.IsTutteViolator u
neg : ∀ (hvOdd : ¬Odd (Nat.card V)), ∃ (u : Set V), G.IsTutteViolator u
⊢ ∃ (u : Set V), G.IsTutteViolator u

Tactic:
by_cases hvOdd : Odd (Nat.card V)

Premises used: Odd, Nat.card
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvOdd : Odd (Nat.card V)
⊢ ∃ (u : Set V), G.IsTutteViolator u

Tactic:
⟨∅, .empty hvOdd⟩

Premises used: Exists.intro, SimpleGraph.IsTutteViolator.empty, EmptyCollection.emptyCollection
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvOdd : Odd (Nat.card V)
⊢ ∃ (u : Set V), G.IsTutteViolator u

Tactic:
exact ⟨∅, .empty hvOdd⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvOdd : ¬Odd (Nat.card V)
⊢ ∃ (u : Set V), G.IsTutteViolator u

Tactic:
exists_isTutteViolator h (Nat.not_odd_iff_even.mp hvOdd)

Premises used: Nat.not_odd_iff_even, SimpleGraph.exists_isTutteViolator, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching
hvOdd : ¬Odd (Nat.card V)
⊢ ∃ (u : Set V), G.IsTutteViolator u

Tactic:
exact exists_isTutteViolator h (Nat.not_odd_iff_even.mp hvOdd)

Premises used: Nat.not_odd_iff_even, SimpleGraph.exists_isTutteViolator, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Tutte
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
refine : (∀ (u : Set V), ¬G.IsTutteViolator u) → ∃ (M : G.Subgraph), M.IsPerfectMatching
refine₁ refine₂ : ∀ (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching), ∃ (u : Set V), G.IsTutteViolator u
pos : ∀ (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching) (hvOdd : Odd (Nat.card V)), ∃ (u : Set V), G.IsTutteViolator u
neg neg₁ :
  ∀ (h : ∀ (M : G.Subgraph), ¬M.IsPerfectMatching) (hvOdd : ¬Odd (Nat.card V)), ∃ (u : Set V), G.IsTutteViolator u
⊢ (∃ (M : G.Subgraph), M.IsPerfectMatching) ↔ ∀ (u : Set V), ¬G.IsTutteViolator u

Tactic:
classical
  refine ⟨by rintro ⟨M, hM⟩; apply not_isTutteViolator_of_isPerfectMatching hM, ?_⟩
  contrapose!
  intro h
  by_cases hvOdd : Odd (Nat.card V)
  · exact ⟨∅, .empty hvOdd⟩
  · exact exists_isTutteViolator h (Nat.not_odd_iff_even.mp hvOdd)

Premises used: Odd, Nat.card
-- Module: Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
E : Type u_3
inst : MetricSpace E
p : V ↪ E
⊢ ∀ {u v : V} (ha : Adj ⊥ u v), dist.{u_3} (α := E) ((p : (a : V) → E) u : E) ((p : (a : V) → E) v : E) = 1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
E : Type u_3
inst : MetricSpace E
inst_1 : Subsingleton V
x : E
u v : V
ha : G.Adj u v
⊢ G.Adj v v

Tactic:
have := Subsingleton.elim u v ▸ ha
-- Module: Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
E : Type u_3
inst : MetricSpace E
inst_1 : Subsingleton V
x : E
u v : V
ha : G.Adj u v
this : G.Adj v v
⊢ dist.{u_3} (α := E) (({ toFun := fun (x_1 : V) ↦ x, inj' := ⋯ : V ↪ E } : (a : V) → E) u : E)
      (({ toFun := fun (x_1 : V) ↦ x, inj' := ⋯ : V ↪ E } : (a : V) → E) v : E) =
    1

Tactic:
simp at this
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsVertexCover ∅ ↔ G = ⊥

Tactic:
simp [IsVertexCover, eq_bot_iff_forall_not_adj]

Premises used: SimpleGraph.IsVertexCover, SimpleGraph.eq_bot_iff_forall_not_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsVertexCover Set.univ

Tactic:
simp [IsVertexCover]

Premises used: SimpleGraph.IsVertexCover
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
c : Set V
⊢ IsVertexCover ⊥ c

Tactic:
simp [IsVertexCover]

Premises used: SimpleGraph.IsVertexCover
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
c d : Set V
hcd : c ⊆ d
hc : G.IsVertexCover c
⊢ G.IsVertexCover d

Tactic:
grind [IsVertexCover]

Premises used: SimpleGraph.IsVertexCover
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G G' : SimpleGraph V
c : Set V
hG : G ≤ G'
hc : G'.IsVertexCover c
⊢ G.IsVertexCover c

Tactic:
fun _ _ hadj ↦ hc (hG hadj)

Premises used: SimpleGraph.IsVertexCover
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
c : Set V
⊢ G.IsVertexCover c → G.IsIndepSet cᶜ

Tactic:
grind [IsVertexCover, Set.Pairwise]

Premises used: Set.Pairwise, SimpleGraph.IsVertexCover
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
c : Set V
refine : ∀ (hi : G.IsIndepSet cᶜ) (v w : V) (hadj : G.Adj v w), v ∈ c ∨ w ∈ c
⊢ G.IsIndepSet cᶜ ↔ G.IsVertexCover c

Tactic:
refine ⟨fun hi v w hadj ↦ ?_, by grind [IsVertexCover, Set.Pairwise]⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
c : Set V
hi : G.IsIndepSet cᶜ
v w : V
hadj : G.Adj v w
by_contra! : ∀ (hh : v ∉ c ∧ w ∉ c), False
⊢ v ∈ c ∨ w ∈ c

Tactic:
by_contra! hh
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
c : Set V
hi : G.IsIndepSet cᶜ
v w : V
hadj : G.Adj v w
hh : v ∉ c ∧ w ∉ c
⊢ False

Tactic:
hi hh.1 hh.2 (Adj.ne hadj) hadj

Premises used: SimpleGraph.Adj.ne, And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
c : Set V
hi : G.IsIndepSet cᶜ
v w : V
hadj : G.Adj v w
hh : v ∉ c ∧ w ∉ c
⊢ False

Tactic:
exact hi hh.1 hh.2 (Adj.ne hadj) hadj

Premises used: SimpleGraph.Adj.ne, And.right, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
c : Set V
⊢ G.IsVertexCover cᶜ ↔ G.IsIndepSet c

Tactic:
simp [← isIndepSet_compl_iff_isVertexCover]

Premises used: SimpleGraph.isIndepSet_compl_iff_isVertexCover
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
F : Type u_3
inst : FunLike F V W
inst_1 : HomClass F G H
f : F
c : Set W
hc : H.IsVertexCover c
⊢ G.IsVertexCover ((⇑f : (a : V) → W) ⁻¹' c)

Tactic:
fun _ _ hadj ↦ hc (map_rel f hadj)

Premises used: Set.Mem, setOf, SimpleGraph.IsVertexCover, Set.preimage, RelHomClass.map_rel
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ≃g H
c : Set W
h : G.IsVertexCover ((⇑f : (a : V) → W) ⁻¹' c)
⊢ H.IsVertexCover c

Tactic:
simpa [← RelIso.image_eq_preimage_symm, Set.image_preimage_eq _ f.surjective]
      using h.preimage f.symm

Premises used: Set.image_preimage_eq, RelIso.surjective, RelIso.image_eq_preimage_symm, SimpleGraph.Iso.symm, SimpleGraph.IsVertexCover.preimage
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ≃g H
c : Set V
⊢ H.IsVertexCover ((⇑f : (a : V) → W) '' c) ↔ G.IsVertexCover c

Tactic:
simp [RelIso.image_eq_preimage_symm]

Premises used: RelIso.image_eq_preimage_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
n : ℕ∞
⊢ G.vertexCoverNum ≤ n ↔ ∀ (m : ℕ∞), (∀ (s : Set V), G.IsVertexCover s → m ≤ s.encard) → m ≤ n

Tactic:
simp [vertexCoverNum, iInf_le_iff]

Premises used: SimpleGraph.vertexCoverNum, iInf_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
c : Set V
hc : G.IsVertexCover c
⊢ G.vertexCoverNum ≤ c.encard

Tactic:
vertexCoverNum_le_iff.mpr fun _ hm ↦ hm c hc

Premises used: Iff.mpr, SimpleGraph.vertexCoverNum_le_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsVertexCover Set.univ

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
⊢ Nonempty.{max 1 (u_1 + 1)} { s : Set V // G.IsVertexCover s }

Tactic:
have : Nonempty {s : Set V // IsVertexCover G s} := nonempty_subtype.mpr ⟨Set.univ, by simp⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
this : Nonempty.{max 1 (u_1 + 1)} { s : Set V // G.IsVertexCover s }
obtain :
  ∀ (s : { s : Set V // G.IsVertexCover s })
    (hs : (↑s : Set V).encard = ⨅ (x : { s : Set V // G.IsVertexCover s }), (↑x : Set V).encard),
    ∃ (s : Set V), s.encard = G.vertexCoverNum ∧ G.IsVertexCover s
⊢ ∃ (s : Set V), s.encard = G.vertexCoverNum ∧ G.IsVertexCover s

Tactic:
obtain ⟨s, hs⟩ := @ENat.exists_eq_iInf _ this (·.val.encard)

Premises used: Set.encard, ENat.exists_eq_iInf, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
this : Nonempty.{max 1 (u_1 + 1)} { s : Set V // G.IsVertexCover s }
s : { s : Set V // G.IsVertexCover s }
hs : (↑s : Set V).encard = ⨅ (x : { s : Set V // G.IsVertexCover s }), (↑x : Set V).encard
⊢ ∃ (s : Set V), s.encard = G.vertexCoverNum ∧ G.IsVertexCover s

Tactic:
⟨s.val, hs ▸ iInf_subtype, s.property⟩

Premises used: iInf_subtype, Eq.rec, And.intro, Exists.intro, Eq.symm, Subtype.val, Subtype.property
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
this : Nonempty.{max 1 (u_1 + 1)} { s : Set V // G.IsVertexCover s }
s : { s : Set V // G.IsVertexCover s }
hs : (↑s : Set V).encard = ⨅ (x : { s : Set V // G.IsVertexCover s }), (↑x : Set V).encard
⊢ ∃ (s : Set V), s.encard = G.vertexCoverNum ∧ G.IsVertexCover s

Tactic:
exact ⟨s.val, hs ▸ iInf_subtype, s.property⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ (↑n : ℕ∞)
h₂ : (↑n : ℕ∞) ≤ ENat.card V
obtain :
  ∀ (s : Set V) (hs₁ : s.encard = G.vertexCoverNum) (hs₂ : G.IsVertexCover s),
    ∃ (s : Set V), s.encard = (↑n : ℕ∞) ∧ G.IsVertexCover s
⊢ ∃ (s : Set V), s.encard = (↑n : ℕ∞) ∧ G.IsVertexCover s

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := vertexCoverNum_exists G

Premises used: SimpleGraph.vertexCoverNum_exists
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ (↑n : ℕ∞)
h₂ : (↑n : ℕ∞) ≤ ENat.card V
s : Set V
hs₁ : s.encard = G.vertexCoverNum
hs₂ : G.IsVertexCover s
⊢ s ⊆ Set.univ

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ (↑n : ℕ∞)
h₂ : (↑n : ℕ∞) ≤ ENat.card V
s : Set V
hs₁ : s.encard = G.vertexCoverNum
hs₂ : G.IsVertexCover s
obtain :
  ∀ (r : Set V) (hr₁ : s ⊆ r),
    r ⊆ Set.univ → ∀ (hr₃ : r.encard = (↑n : ℕ∞)), ∃ (s : Set V), s.encard = (↑n : ℕ∞) ∧ G.IsVertexCover s
⊢ ∃ (s : Set V), s.encard = (↑n : ℕ∞) ∧ G.IsVertexCover s

Tactic:
obtain ⟨r, hr₁, _, hr₃⟩ :=
    Set.exists_superset_subset_encard_eq (by simp) (le_of_eq_of_le hs₁ h₁) (Set.encard_univ _ ▸ h₂)

Premises used: le_of_eq_of_le, Set.exists_superset_subset_encard_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ (↑n : ℕ∞)
h₂ : (↑n : ℕ∞) ≤ ENat.card V
s : Set V
hs₁ : s.encard = G.vertexCoverNum
hs₂ : G.IsVertexCover s
r : Set V
hr₁ : s ⊆ r
left : r ⊆ Set.univ
hr₃ : r.encard = (↑n : ℕ∞)
⊢ ∃ (s : Set V), s.encard = (↑n : ℕ∞) ∧ G.IsVertexCover s

Tactic:
⟨r, hr₃, hs₂.subset hr₁⟩

Premises used: SimpleGraph.IsVertexCover.subset, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
n : ℕ
h₁ : G.vertexCoverNum ≤ (↑n : ℕ∞)
h₂ : (↑n : ℕ∞) ≤ ENat.card V
s : Set V
hs₁ : s.encard = G.vertexCoverNum
hs₂ : G.IsVertexCover s
r : Set V
hr₁ : s ⊆ r
left : r ⊆ Set.univ
hr₃ : r.encard = (↑n : ℕ∞)
⊢ ∃ (s : Set V), s.encard = (↑n : ℕ∞) ∧ G.IsVertexCover s

Tactic:
exact ⟨r, hr₃, hs₂.subset hr₁⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
⊢ IsVertexCover.{u_1} (V := V) ⊥ ∅

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
inst : Subsingleton V
⊢ G.vertexCoverNum = 0

Tactic:
simp [SimpleGraph.subsingleton_iff.mpr _ |>.allEq G ⊥]

Premises used: Bot.bot, Subsingleton.allEq
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G = ⊥ → G.vertexCoverNum = 0

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
refine : ∀ (h : G.vertexCoverNum = 0), G = ⊥
⊢ G.vertexCoverNum = 0 ↔ G = ⊥

Tactic:
refine ⟨fun h ↦ ?_, by simp_all⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h : G.vertexCoverNum = 0
⊢ G = ⊥

Tactic:
simpa [h] using vertexCoverNum_exists G

Premises used: SimpleGraph.vertexCoverNum_exists
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
⊢ Nontrivial V

Tactic:
nontriviality V
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h : Nontrivial V
obtain : ∀ (x : V), G.vertexCoverNum ≤ ENat.card V - 1
⊢ G.vertexCoverNum ≤ ENat.card V - 1

Tactic:
obtain ⟨x⟩ := not_subsingleton_iff_nontrivial.mp (not_subsingleton V) |>.to_nonempty

Premises used: Nontrivial.to_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h : Nontrivial V
x : V
⊢ G.vertexCoverNum ≤ ENat.card V - 1

Tactic:
ENat.forall_natCast_le_iff_le.mp fun n hn ↦ ?_

Premises used: ENat.forall_natCast_le_iff_le, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h : Nontrivial V
x : V
refine : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ G.vertexCoverNum), (↑n : ℕ∞) ≤ ENat.card V - 1
⊢ G.vertexCoverNum ≤ ENat.card V - 1

Tactic:
refine ENat.forall_natCast_le_iff_le.mp fun n hn ↦ ?_

Premises used: ENat.forall_natCast_le_iff_le, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h : Nontrivial V
x : V
n : ℕ
hn : (↑n : ℕ∞) ≤ G.vertexCoverNum
⊢ ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard

Tactic:
simp only [vertexCoverNum, le_iInf_iff] at hn

Premises used: SimpleGraph.vertexCoverNum, le_iInf_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h : Nontrivial V
x : V
n : ℕ
hn : ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard
⊢ G.IsVertexCover (Set.univ \ {x})

Tactic:
grind [IsVertexCover, Adj.ne']

Premises used: SimpleGraph.Adj.ne', SimpleGraph.IsVertexCover
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h : Nontrivial V
x : V
n : ℕ
hn : ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard
⊢ (↑n : ℕ∞) ≤ Set.encard (α := V) (Set.univ \ {x})

Tactic:
have := hn (Set.univ \ {x}) (by grind [IsVertexCover, Adj.ne'])
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h : Nontrivial V
x : V
n : ℕ
hn : ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard
this : (↑n : ℕ∞) ≤ Set.encard (α := V) (Set.univ \ {x})
⊢ (↑n : ℕ∞) ≤ ENat.card V - 1

Tactic:
simpa [Set.encard_diff_singleton_of_mem (Set.mem_univ _)] using this

Premises used: Set.mem_univ, Set.encard_diff_singleton_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
⊢ ENat.card V - 1 ≠ ⊤

Tactic:
simpa
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nonempty V
inst_1 : Finite V
⊢ G.vertexCoverNum < ENat.card V

Tactic:
(ENat.add_one_le_iff vertexCoverNum_ne_top_of_finite).mp ?_

Premises used: ENat.add_one_le_iff, Iff.mp, SimpleGraph.vertexCoverNum_ne_top_of_finite
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nonempty V
inst_1 : Finite V
refine : G.vertexCoverNum + 1 ≤ ENat.card V
⊢ G.vertexCoverNum < ENat.card V

Tactic:
refine (ENat.add_one_le_iff vertexCoverNum_ne_top_of_finite).mp ?_

Premises used: ENat.add_one_le_iff, Iff.mp, SimpleGraph.vertexCoverNum_ne_top_of_finite
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nonempty V
inst_1 : Finite V
grw : HSub.hSub (α := ℕ∞) (↑(Nat.card V) : ℕ∞) 1 + 1 ≤ (↑(Nat.card V) : ℕ∞)
⊢ G.vertexCoverNum + 1 ≤ ENat.card V

Tactic:
grw [vertexCoverNum_le_card_sub_one, ENat.card_eq_coe_natCard]

Premises used: SimpleGraph.vertexCoverNum_le_card_sub_one, ENat.card_eq_coe_natCard
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nonempty V
inst_1 : Finite V
enat_to_nat : Nat.card V - 1 + 1 ≤ Nat.card V
⊢ HSub.hSub (α := ℕ∞) (↑(Nat.card V) : ℕ∞) 1 + 1 ≤ (↑(Nat.card V) : ℕ∞)

Tactic:
enat_to_nat
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nonempty V
inst_1 : Finite V
⊢ Nat.card V - 1 + 1 ≤ Nat.card V

Tactic:
Nat.add_le_of_le_sub (Order.one_le_iff_pos.mpr Nat.card_pos) (le_refl _)

Premises used: Iff.mpr, le_refl, Nat.card_pos, Nat.add_le_of_le_sub, Order.one_le_iff_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
inst : Nonempty V
inst_1 : Finite V
⊢ Nat.card V - 1 + 1 ≤ Nat.card V

Tactic:
exact Nat.add_le_of_le_sub (Order.one_le_iff_pos.mpr Nat.card_pos) (le_refl _)

Premises used: Iff.mpr, le_refl, Nat.card_pos, Nat.add_le_of_le_sub, Order.one_le_iff_pos
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
pos : ∀ (h' : G.edgeSet = ∅), G.vertexCoverNum ≤ G.edgeSet.encard
neg : ∀ (h' : ¬G.edgeSet = ∅), G.vertexCoverNum ≤ G.edgeSet.encard
⊢ G.vertexCoverNum ≤ G.edgeSet.encard

Tactic:
by_cases h' : G.edgeSet = ∅

Premises used: SimpleGraph.edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h' : G.edgeSet = ∅
⊢ G.vertexCoverNum ≤ G.edgeSet.encard

Tactic:
simp [h', SimpleGraph.edgeSet_eq_empty.mp]

Premises used: Iff.mp, SimpleGraph.edgeSet_eq_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
⊢ G.vertexCoverNum ≤ G.edgeSet.encard

Tactic:
ENat.forall_natCast_le_iff_le.mp fun n hn ↦ ?_

Premises used: ENat.forall_natCast_le_iff_le, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
neg : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ G.vertexCoverNum), (↑n : ℕ∞) ≤ G.edgeSet.encard
⊢ G.vertexCoverNum ≤ G.edgeSet.encard

Tactic:
refine ENat.forall_natCast_le_iff_le.mp fun n hn ↦ ?_

Premises used: ENat.forall_natCast_le_iff_le, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : (↑n : ℕ∞) ≤ G.vertexCoverNum
⊢ ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard

Tactic:
simp only [vertexCoverNum, le_iInf_iff] at hn

Premises used: SimpleGraph.vertexCoverNum, le_iInf_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard
v w : V
h : G.Adj v w
⊢ Membership.mem (γ := Set V) ((fun (x : Sym2 V) ↦ (Quot.out (r := Sym2.Rel V) x).1) '' G.edgeSet) v ∨
    Membership.mem (γ := Set V) ((fun (x : Sym2 V) ↦ (Quot.out (r := Sym2.Rel V) x).1) '' G.edgeSet) w

Tactic:
grind [Sym2.out_fst_mem s(v, w), mem_edgeSet]

Premises used: Sym2.mk, Sym2.out_fst_mem, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard
⊢ (↑n : ℕ∞) ≤ Set.encard (α := V) ((fun (x : Sym2 V) ↦ (Quot.out (r := Sym2.Rel V) x).1) '' G.edgeSet)

Tactic:
have := hn ((·.out.1) '' G.edgeSet)
    (fun v w _ ↦ by grind [Sym2.out_fst_mem s(v, w), mem_edgeSet])
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h' : ¬G.edgeSet = ∅
n : ℕ
hn : ∀ (i : Set V) (i_1 : G.IsVertexCover i), (↑n : ℕ∞) ≤ i.encard
this : (↑n : ℕ∞) ≤ Set.encard (α := V) ((fun (x : Sym2 V) ↦ (Quot.out (r := Sym2.Rel V) x).1) '' G.edgeSet)
⊢ (↑n : ℕ∞) ≤ G.edgeSet.encard

Tactic:
grind [Set.encard_image_le]

Premises used: Set.encard_image_le
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
G : SimpleGraph V
h : G.edgeSet.Finite
⊢ G.vertexCoverNum ≠ ⊤

Tactic:
ne_top_of_le_ne_top (Set.encard_ne_top_iff.mpr h) vertexCoverNum_le_encard_edgeSet

Premises used: Iff.mpr, SimpleGraph.vertexCoverNum_le_encard_edgeSet, ne_top_of_le_ne_top, Set.encard_ne_top_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
⊢ Nontrivial V

Tactic:
nontriviality V using tsub_eq_zero_of_le

Premises used: tsub_eq_zero_of_le
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
⊢ (completeGraph V).vertexCoverNum = ENat.card V - 1

Tactic:
ENat.eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩

Premises used: ENat.eq_of_forall_natCast_le_iff, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
refine_1 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ (completeGraph V).vertexCoverNum), (↑n : ℕ∞) ≤ ENat.card V - 1
refine_2 : ∀ (n : ℕ) (hn : (↑n : ℕ∞) ≤ ENat.card V - 1), (↑n : ℕ∞) ≤ (completeGraph V).vertexCoverNum
⊢ (completeGraph V).vertexCoverNum = ENat.card V - 1

Tactic:
refine ENat.eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩

Premises used: ENat.eq_of_forall_natCast_le_iff, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ (completeGraph V).vertexCoverNum
refine_1 : (completeGraph V).vertexCoverNum ≤ ENat.card V - 1
refine_1₁ refine_1₂ : ENat.card V - 1 ≤ ENat.card V - 1
⊢ (↑n : ℕ∞) ≤ ENat.card V - 1

Tactic:
grw [hn, vertexCoverNum_le_card_sub_one]

Premises used: SimpleGraph.vertexCoverNum_le_card_sub_one
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
refine_2 : ∀ (hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)), False
⊢ (↑n : ℕ∞) ≤ (completeGraph V).vertexCoverNum

Tactic:
by_contra! hh
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
grw : ENat.card V - 1 ≤ ENat.card V + 1
⊢ HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V

Tactic:
grw [tsub_le_iff_right, hn]

Premises used: tsub_le_iff_right
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
⊢ ENat.card V - 1 ≤ ENat.card V + 1

Tactic:
simp [add_assoc, one_add_one_eq_two]

Premises used: add_assoc, one_add_one_eq_two
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
⊢ HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V

Tactic:
have : n - 1 ≤ ENat.card V := by
    grw [tsub_le_iff_right, hn]
    simp [add_assoc, one_add_one_eq_two]
-- Module: Mathlib.Combinatorics.SimpleGraph.VertexCover
Goal:
V : Type u_1
h : Nontrivial V
n : ℕ
hn : (↑n : ℕ∞) ≤ ENat.card V - 1
hh : (completeGraph V).vertexCoverNum < (↑n : ℕ∞)
this : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 ≤ ENat.card V
refine_2 : ∀ (t : Set V) (ht₁ : t.encard = (↑(n - 1) : ℕ∞)) (ht₂ : (completeGraph V).IsVertexCover t), False
⊢ False

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := exists_of_le_vertexCoverNum (n - 1) (ENat.le_sub_one_of_lt hh) this

Premises used: HSub.hSub, ENat.le_sub_one_of_lt, OfNat.ofNat, SimpleGraph.exists_of_le_vertexCoverNum