awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ Fintype.card.{u_1} (↑(G.neighborSet v) : Type u_1) = G.degree v

Tactic:
(Set.toFinset_card _).symm

Premises used: SimpleGraph.neighborFinset, Set.toFinset_card, SimpleGraph.degree, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ G.degree v = 0 ↔ G.IsIsolated v

Tactic:
simp [← card_neighborFinset_eq_degree]

Premises used: SimpleGraph.card_neighborFinset_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ 0 < G.degree v ↔ ¬G.IsIsolated v

Tactic:
simp [← card_neighborFinset_eq_degree]

Premises used: SimpleGraph.card_neighborFinset_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ 0 < G.degree v ↔ ∃ (w : V), G.Adj v w

Tactic:
simp only [degree, card_pos, Finset.Nonempty, mem_neighborFinset]

Premises used: SimpleGraph.mem_neighborFinset, Finset.Nonempty, Finset.card_pos, SimpleGraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ 0 < G.degree v ↔ (G.neighborSet v).Nonempty

Tactic:
G.degree_pos_iff_exists_adj v

Premises used: Set.Mem, setOf, SimpleGraph.degree_pos_iff_exists_adj, SimpleGraph.neighborSet, Set.Nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
w : V
h : G.Adj v w
⊢ 0 < G.degree v

Tactic:
G.degree_pos_iff_nonempty.mpr ⟨_, h⟩

Premises used: Iff.mpr, SimpleGraph.degree_pos_iff_nonempty, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
w : V
h : G.Adj w v
⊢ 0 < G.degree v

Tactic:
h.symm.degree_pos_left

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Adj.degree_pos_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
rw : (∃ (w : V), G.Adj v w) ↔ v ∈ G.support
rw₁ rw₂ : (∃ (w : V), G.Adj v w) ↔ ∃ (w : V), G.Adj v w
⊢ 0 < G.degree v ↔ v ∈ G.support

Tactic:
rw [G.degree_pos_iff_exists_adj v, mem_support]

Premises used: SimpleGraph.mem_support, SimpleGraph.degree_pos_iff_exists_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
rw : G.degree v = 0 ↔ ¬0 < G.degree v
rw₁ : G.degree v = 0 ↔ ¬G.degree v ≠ 0
rw₂ rw₃ : G.degree v = 0 ↔ G.degree v = 0
⊢ G.degree v = 0 ↔ v ∉ G.support

Tactic:
rw [← G.degree_pos_iff_mem_support v, Nat.pos_iff_ne_zero, not_ne_iff]

Premises used: Nat.pos_iff_ne_zero, not_ne_iff, SimpleGraph.degree_pos_iff_mem_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : Subsingleton V
⊢ 0 < G.degree v ↔ ∃ (w : V), G.Adj v w

Tactic:
have := G.degree_pos_iff_exists_adj v
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : Subsingleton V
this : 0 < G.degree v ↔ ∃ (w : V), G.Adj v w
⊢ G.degree v = 0

Tactic:
simp_all [subsingleton_iff_forall_eq v]

Premises used: subsingleton_iff_forall_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
rw : (∃! a : V, a ∈ G.neighborFinset v) ↔ ∃! w : V, G.Adj v w
⊢ G.degree v = 1 ↔ ∃! w : V, G.Adj v w

Tactic:
rw [degree, Finset.card_eq_one, Finset.singleton_iff_unique_mem]

Premises used: Finset.card_eq_one, SimpleGraph.degree, Finset.singleton_iff_unique_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ (∃! a : V, a ∈ G.neighborFinset v) ↔ ∃! w : V, G.Adj v w

Tactic:
simp only [mem_neighborFinset]

Premises used: SimpleGraph.mem_neighborFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.degree v ≠ 0
by_contra! : ∀ (this : Subsingleton V), False
⊢ Nontrivial V

Tactic:
by_contra!
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.degree v ≠ 0
this : Subsingleton V
⊢ False

Tactic:
simp_all [degree_eq_zero_of_subsingleton]

Premises used: SimpleGraph.degree_eq_zero_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : Fintype (↑(Gᶜ.neighborSet v) : Type u_1)
inst_2 : Fintype V
rw : Gᶜ.degree v = #((G.neighborSet v).toFinset ∪ (Gᶜ.neighborSet v).toFinset) - G.degree v
⊢ Gᶜ.degree v = Fintype.card V - 1 - G.degree v

Tactic:
rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]

Premises used: Set.toFinset_union, SimpleGraph.card_neighborSet_union_compl_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : Fintype (↑(Gᶜ.neighborSet v) : Type u_1)
inst_2 : Fintype V
⊢ Gᶜ.degree v = #((G.neighborSet v).toFinset ∪ (Gᶜ.neighborSet v).toFinset) - G.degree v

Tactic:
simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v)),
      card_neighborSet_eq_degree]

Premises used: Iff.mpr, SimpleGraph.card_neighborSet_eq_degree, Set.disjoint_toFinset, SimpleGraph.compl_neighborSet_disjoint, Finset.card_union_of_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : Fintype (↑(Gᶜ.neighborSet v) : Type u_1)
inst_2 : Fintype V
rw : Gᶜ.degree v = #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset - G.degree v
rw₁ rw₂ rw₃ : Gᶜ.degree v = #((G.neighborSet v).toFinset ∪ (Gᶜ.neighborSet v).toFinset) - G.degree v
⊢ Gᶜ.degree v = Fintype.card V - 1 - G.degree v

Tactic:
classical
    rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
    simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v)),
      card_neighborSet_eq_degree]

Premises used: Set.toFinset_union, SimpleGraph.card_neighborSet_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableEq V
rw : Fintype.card.{u_1} (↑(G.neighborSet v) : Type u_1) = G.degree v
rw₁ rw₂ : G.degree v = G.degree v
⊢ Fintype.card.{u_1} (↑(G.incidenceSet v) : Type u_1) = G.degree v

Tactic:
rw [Fintype.card_congr (G.incidenceSetEquivNeighborSet v), card_neighborSet_eq_degree]

Premises used: Fintype.card_congr, SimpleGraph.incidenceSetEquivNeighborSet, SimpleGraph.card_neighborSet_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableEq V
⊢ (↑(G.incidenceFinset v) : Set (Sym2 V)) = G.incidenceSet v

Tactic:
simp [incidenceFinset]

Premises used: SimpleGraph.incidenceFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableEq V
rw : #(G.incidenceFinset v) = Fintype.card.{u_1} (↑(G.incidenceSet v) : Type u_1)
⊢ #(G.incidenceFinset v) = G.degree v

Tactic:
rw [← G.card_incidenceSet_eq_degree]

Premises used: SimpleGraph.card_incidenceSet_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableEq V
⊢ #(G.incidenceFinset v) = Fintype.card.{u_1} (↑(G.incidenceSet v) : Type u_1)

Tactic:
apply Set.toFinset_card

Premises used: Set.toFinset_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableEq V
e : Sym2 V
⊢ e ∈ G.incidenceFinset v ↔ e ∈ G.incidenceSet v

Tactic:
Set.mem_toFinset

Premises used: Set.Mem, setOf, Set.mem_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableEq V
inst_2 : Fintype (↑G.edgeSet : Type u_1)
h :
  ∀ (a : Sym2 V) (fst snd : V),
    Quot.mk (Sym2.Rel V) (fst, snd) ∈ G.incidenceFinset v ↔ Quot.mk (Sym2.Rel V) (fst, snd) ∈ {e ∈ G.edgeFinset | v ∈ e}
⊢ G.incidenceFinset v = {e ∈ G.edgeFinset | v ∈ e}

Tactic:
ext ⟨⟨⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableEq V
inst_2 : Fintype (↑G.edgeSet : Type u_1)
a : Sym2 V
fst snd : V
⊢ Quot.mk (Sym2.Rel V) (fst, snd) ∈ G.incidenceFinset v ↔ Quot.mk (Sym2.Rel V) (fst, snd) ∈ {e ∈ G.edgeFinset | v ∈ e}

Tactic:
simp [mk'_mem_incidenceSet_iff]

Premises used: SimpleGraph.mk'_mem_incidenceSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableEq V
inst_2 : Fintype (↑G.edgeSet : Type u_1)
⊢ G.incidenceFinset v ⊆ G.edgeFinset

Tactic:
Set.toFinset_subset_toFinset.mpr (G.incidenceSet_subset v)

Premises used: Iff.mpr, Set.Mem, setOf, Set.toFinset_subset_toFinset, SimpleGraph.incidenceSet_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : Fintype (↑G.edgeSet : Type u_1)
rw : #(G.incidenceFinset v) ≤ #G.edgeFinset
⊢ G.degree v ≤ #G.edgeFinset

Tactic:
rw [← card_incidenceFinset_eq_degree]

Premises used: SimpleGraph.card_incidenceFinset_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : Fintype (↑G.edgeSet : Type u_1)
⊢ #(G.incidenceFinset v) ≤ #G.edgeFinset

Tactic:
card_le_card (G.incidenceFinset_subset v)

Premises used: Finset.card_le_card, SimpleGraph.incidenceFinset_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : Fintype (↑G.edgeSet : Type u_1)
⊢ #(G.incidenceFinset v) ≤ #G.edgeFinset

Tactic:
exact card_le_card (G.incidenceFinset_subset v)

Premises used: Finset.card_le_card, SimpleGraph.incidenceFinset_subset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : Fintype (↑G.edgeSet : Type u_1)
rw rw₁ rw₂ : #(G.incidenceFinset v) ≤ #G.edgeFinset
⊢ G.degree v ≤ #G.edgeFinset

Tactic:
classical
  rw [← card_incidenceFinset_eq_degree]
  exact card_le_card (G.incidenceFinset_subset v)

Premises used: SimpleGraph.card_incidenceFinset_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
H : SimpleGraph V
inst_1 : Fintype (↑(H.neighborSet v) : Type u_1)
hle : G ≤ H
simp_rw : Fintype.card.{u_1} (↑(G.neighborSet v) : Type u_1) ≤ Fintype.card.{u_1} (↑(H.neighborSet v) : Type u_1)
⊢ G.degree v ≤ H.degree v

Tactic:
simp_rw [← card_neighborSet_eq_degree]

Premises used: SimpleGraph.card_neighborSet_eq_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
H : SimpleGraph V
inst_1 : Fintype (↑(H.neighborSet v) : Type u_1)
hle : G ≤ H
⊢ Fintype.card.{u_1} (↑(G.neighborSet v) : Type u_1) ≤ Fintype.card.{u_1} (↑(H.neighborSet v) : Type u_1)

Tactic:
Set.card_le_card fun v hv => hle hv

Premises used: Set.card_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
H : SimpleGraph V
inst_1 : Fintype (↑(H.neighborSet v) : Type u_1)
hle : G ≤ H
⊢ Fintype.card.{u_1} (↑(G.neighborSet v) : Type u_1) ≤ Fintype.card.{u_1} (↑(H.neighborSet v) : Type u_1)

Tactic:
exact Set.card_le_card fun v hv => hle hv

Premises used: Set.card_le_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
⊢ G.degree v < Fintype.card V

Tactic:
Finset.card_lt_univ_of_notMem <| G.notMem_neighborFinset_self v

Premises used: SimpleGraph.notMem_neighborFinset_self, Finset.card_lt_univ_of_notMem, SimpleGraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
d : ℕ
h : G.IsRegularOfDegree d
v : V
⊢ G.degree v = d

Tactic:
h v
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
inst_1 : IsEmpty V
d : ℕ
⊢ G.IsRegularOfDegree d

Tactic:
IsEmpty.elim ‹_›

Premises used: IsEmpty.elim, SimpleGraph.IsRegularOfDegree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
G : SimpleGraph V
inst_2 : DecidableRel G.Adj
k : ℕ
h : G.IsRegularOfDegree k
v : V
rw : Fintype.card V - 1 - G.degree v = Fintype.card V - 1 - k
rw₁ rw₂ : Fintype.card V - 1 - k = Fintype.card V - 1 - k
⊢ Gᶜ.degree v = Fintype.card V - 1 - k

Tactic:
rw [degree_compl, h v]

Premises used: SimpleGraph.degree_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
v : V
inst_1 : DecidableRel G.Adj
h : ∀ (a : V), a ∈ G.neighborFinset v ↔ Membership.mem (γ := Finset V) {w : V | G.Adj v w} a
⊢ G.neighborFinset v = {w : V | G.Adj v w}

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
v : V
inst_1 : DecidableRel G.Adj
a : V
⊢ a ∈ G.neighborFinset v ↔ Membership.mem (γ := Finset V) {w : V | G.Adj v w} a

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
v : V
⊢ Gᶜ.neighborFinset v = (G.neighborFinset v)ᶜ \ {v}

Tactic:
simp only [neighborFinset, neighborSet_compl, Set.toFinset_diff, Set.toFinset_compl,
    Set.toFinset_singleton]

Premises used: Set.toFinset_compl, Set.toFinset_diff, SimpleGraph.neighborFinset, SimpleGraph.neighborSet_compl, Set.toFinset_singleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
v : V
simp_rw : #(erase univ v) = Fintype.card V - 1
⊢ (completeGraph V).degree v = Fintype.card V - 1

Tactic:
simp_rw [degree, neighborFinset_eq_filter, top_adj, filter_ne]

Premises used: Finset.filter_ne, SimpleGraph.top_adj, SimpleGraph.neighborFinset_eq_filter, SimpleGraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
v : V
rw : card.{u_1} (α := V) univ - 1 = Fintype.card V - 1
rw₁ rw₂ : Fintype.card V - 1 = Fintype.card V - 1
⊢ #(erase univ v) = Fintype.card V - 1

Tactic:
rw [card_erase_of_mem (mem_univ v), card_univ]

Premises used: Finset.mem_univ, Finset.card_univ, Finset.card_erase_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
v : V
simp_rw : card.{u_1} (α := V) ∅ = 0
⊢ degree ⊥ v = 0

Tactic:
simp_rw [degree, neighborFinset_eq_filter, bot_adj, filter_false]

Premises used: Finset.filter_false, SimpleGraph.bot_adj, SimpleGraph.neighborFinset_eq_filter, SimpleGraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
v : V
⊢ card.{u_1} (α := V) ∅ = 0

Tactic:
Finset.card_empty

Premises used: Finset.card_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
v : V
⊢ card.{u_1} (α := V) ∅ = 0

Tactic:
exact Finset.card_empty

Premises used: Finset.card_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
⊢ IsRegularOfDegree.{u_1} (V := V) ⊤ (Fintype.card V - 1)

Tactic:
simp [IsRegularOfDegree]

Premises used: SimpleGraph.IsRegularOfDegree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
⊢ IsRegularOfDegree.{u_1} (V := V) ⊥ 0

Tactic:
bot_degree

Premises used: SimpleGraph.bot_degree, SimpleGraph.IsRegularOfDegree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
⊢ ∃ (v : V), G.minDegree = G.degree v

Tactic:
grind [minDegree, WithTop.untopD_coe, min_mem_image_coe <| univ_nonempty.image (G.degree ·)]

Premises used: Finset.Nonempty.image, Finset.univ_nonempty, SimpleGraph.minDegree, Finset.min_mem_image_coe, SimpleGraph.degree, WithTop.untopD_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
obtain :
  ∀ (t : ℕ) (ht : Finset.min (image (fun (v : V) ↦ G.degree v) univ) = (↑t : WithTop ℕ)), G.minDegree ≤ G.degree v
⊢ G.minDegree ≤ G.degree v

Tactic:
obtain ⟨t, ht⟩ := Finset.min_of_mem (mem_image_of_mem (fun v => G.degree v) (mem_univ v))

Premises used: Finset.mem_univ, Finset.min_of_mem, Finset.mem_image_of_mem, SimpleGraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
t : ℕ
ht : Finset.min (image (fun (v : V) ↦ G.degree v) univ) = (↑t : WithTop ℕ)
⊢ t ≤ G.degree v

Tactic:
have := Finset.min_le_of_eq (mem_image_of_mem _ (mem_univ v)) ht
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
t : ℕ
ht : Finset.min (image (fun (v : V) ↦ G.degree v) univ) = (↑t : WithTop ℕ)
this : t ≤ G.degree v
rwa : WithTop.untopD 0 (Finset.min (image (fun (v : V) ↦ G.degree v) univ)) ≤ G.degree v
rwa₁ rwa₂ rwa₃ rwa₄ : WithTop.untopD 0 (↑t : WithTop ℕ) ≤ G.degree v
⊢ G.minDegree ≤ G.degree v

Tactic:
rwa [minDegree, ht]

Premises used: SimpleGraph.minDegree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
rcases : ∀ (v : V) (hv : G.minDegree = G.degree v), k ≤ G.minDegree
⊢ k ≤ G.minDegree

Tactic:
rcases G.exists_minimal_degree_vertex with ⟨v, hv⟩

Premises used: SimpleGraph.exists_minimal_degree_vertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
rw : k ≤ G.degree v
⊢ k ≤ G.minDegree

Tactic:
rw [hv]
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
k : ℕ
h : ∀ (v : V), k ≤ G.degree v
v : V
hv : G.minDegree = G.degree v
⊢ k ≤ G.degree v

Tactic:
apply h
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : IsEmpty V
rw :
  Eq (α := WithTop ℕ) (Finset.min (image (fun (v : V) ↦ G.degree v) univ)) (↑0 : WithTop ℕ) ∨
    Eq (α := WithTop ℕ) (Finset.min (image (fun (v : V) ↦ G.degree v) univ)) ⊤
⊢ G.minDegree = 0

Tactic:
rw [minDegree, WithTop.untopD_eq_self_iff]

Premises used: SimpleGraph.minDegree, WithTop.untopD_eq_self_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : IsEmpty V
⊢ Eq (α := WithTop ℕ) (Finset.min (image (fun (v : V) ↦ G.degree v) univ)) (↑0 : WithTop ℕ) ∨
    Eq (α := WithTop ℕ) (Finset.min (image (fun (v : V) ↦ G.degree v) univ)) ⊤

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
H : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
hle : G ≤ H
inl : IsEmpty V → G.minDegree ≤ H.minDegree
inr : Nonempty V → G.minDegree ≤ H.minDegree
⊢ G.minDegree ≤ H.minDegree

Tactic:
cases isEmpty_or_nonempty V

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
H : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
hle : G ≤ H
h : IsEmpty V
⊢ G.minDegree ≤ H.minDegree

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
H : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
hle : G ≤ H
h : Nonempty V
inr : ∀ (v : V), G.minDegree ≤ H.degree v
⊢ G.minDegree ≤ H.minDegree

Tactic:
apply le_minDegree_of_forall_le_degree

Premises used: SimpleGraph.le_minDegree_of_forall_le_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
H : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
hle : G ≤ H
h : Nonempty V
⊢ ∀ (v : V), G.minDegree ≤ H.degree v

Tactic:
fun v ↦ (G.minDegree_le_degree v).trans (G.degree_le_of_le hle)

Premises used: SimpleGraph.degree_le_of_le, LE.le.trans, SimpleGraph.minDegree_le_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
H : SimpleGraph V
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
hle : G ≤ H
h : Nonempty V
⊢ ∀ (v : V), G.minDegree ≤ H.degree v

Tactic:
exact fun v ↦ (G.minDegree_le_degree v).trans (G.degree_le_of_le hle)

Premises used: SimpleGraph.degree_le_of_le, LE.le.trans, SimpleGraph.minDegree_le_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
have : ∀ (v : V) (hv : G.minDegree = G.degree v), G.minDegree < Fintype.card V
⊢ G.minDegree < Fintype.card V

Tactic:
have ⟨v, hv⟩ := G.exists_minimal_degree_vertex
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
v : V
hv : G.minDegree = G.degree v
rw : G.degree v < Fintype.card V
⊢ G.minDegree < Fintype.card V

Tactic:
rw [hv]
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
v : V
hv : G.minDegree = G.degree v
⊢ G.degree v < Fintype.card V

Tactic:
apply degree_lt_card_verts

Premises used: SimpleGraph.degree_lt_card_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
⊢ ∃ (v : V), G.maxDegree = G.degree v

Tactic:
grind [maxDegree, WithBot.unbotD_coe, max_mem_image_coe <| univ_nonempty.image (G.degree ·)]

Premises used: SimpleGraph.maxDegree, Finset.Nonempty.image, Finset.univ_nonempty, Finset.max_mem_image_coe, WithBot.unbotD_coe, SimpleGraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
⊢ G.degree v ≤ G.maxDegree

Tactic:
WithBot.le_unbotD <| Finset.le_max <| mem_image_of_mem (G.degree ·) <| mem_univ v

Premises used: SimpleGraph.maxDegree, Finset.mem_univ, Finset.mem_image_of_mem, WithBot.le_unbotD, SimpleGraph.degree, Finset.le_max