awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h :
  ∀ (a : ℕ),
    ∃ b ≥ a,
      ∃ (G : SimpleGraph (Fin b)) (inst : DecidableRel G.Adj),
        (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(b.choose 2) : ℝ) ∧ IsEmpty.{u_1 + 1} (H.Copy G)
x : ℝ
h_1 :
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
    x
m : ℕ
hm : Membership.mem (γ := Set ℕ) (Set.Ici 2) m
hx : HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ) = x
n : ℕ
hn : n ≥ m
G : SimpleGraph (Fin n)
w : DecidableRel G.Adj
hcard_edges : (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(n.choose 2) : ℝ)
h_free : H.Free G
| (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) ≤ (↑(extremalNumber n H) : ℝ)
have enter : Fintype.card (Fin n)
Tactic: enter [2, 1, 1]
      rw [← Fintype.card_fin n]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h :
  ∀ (a : ℕ),
    ∃ b ≥ a,
      ∃ (G : SimpleGraph (Fin b)) (inst : DecidableRel G.Adj),
        (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(b.choose 2) : ℝ) ∧ IsEmpty.{u_1 + 1} (H.Copy G)
x : ℝ
h_1 :
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
    x
m : ℕ
hm : Membership.mem (γ := Set ℕ) (Set.Ici 2) m
hx : HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ) = x
n : ℕ
hn : n ≥ m
G : SimpleGraph (Fin n)
w : DecidableRel G.Adj
hcard_edges : (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(n.choose 2) : ℝ)
h_free : H.Free G
⊢ (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) ≤ (↑(extremalNumber n H) : ℝ)
have conv : (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) ≤ (↑(extremalNumber (Fintype.card (Fin n)) H) : ℝ)
Tactic: conv =>
      enter [2, 1, 1]
      rw [← Fintype.card_fin n]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
V : Type u_2
inst : Fintype V
h_verts : Fintype.card V ≥ H.turanDensityConst ε
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
⊢ (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑((Fintype.card V).choose 2) : ℝ) → H ⊑ G
have rw : (↑(Finset.card (α := Sym2 (Fin (Fintype.card V))) (edgeFinset (G.overFin sorry))) : ℝ) ≥
    (H.turanDensity + ε) * (↑((Fintype.card V).choose 2) : ℝ) →
  H.IsContained (β := Fin (Fintype.card V)) (G.overFin sorry)
Tactic: rw [(G.overFinIso rfl).card_edgeFinset_eq, isContained_congr Iso.refl (G.overFinIso rfl)]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
Goal:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
V : Type u_2
inst : Fintype V
h_verts : Fintype.card V ≥ H.turanDensityConst ε
G : SimpleGraph V
inst_1 : DecidableRel G.Adj
⊢ (↑(Finset.card (α := Sym2 (Fin (Fintype.card V))) (edgeFinset (G.overFin ⋯))) : ℝ) ≥
      (H.turanDensity + ε) * (↑((Fintype.card V).choose 2) : ℝ) →
    H.IsContained (β := Fin (Fintype.card V)) (G.overFin ⋯)
have a : Fintype.card V ≥
  Nat.find (p := fun (n : ℕ) ↦
    ∀ b ≥ n,
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(b.choose 2) : ℝ) → H ⊑ G)
    sorry
Tactic: apply Nat.find_spec <| eventually_atTop.mp <| eventually_isContained_of_card_edgeFinset H hε_pos
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst : Fintype (↑G₁.edgeSet : Type u_1)
inst_1 : Fintype (↑G₂.edgeSet : Type u_1)
⊢ Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂
have simp_rw : Disjoint (↑G₁.edgeFinset : Set (Sym2 V)) (↑G₂.edgeFinset : Set (Sym2 V)) ↔ Disjoint G₁ G₂
Tactic: simp_rw [← Finset.disjoint_coe, coe_edgeFinset, disjoint_edgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst : Fintype (↑G₁.edgeSet : Type u_1)
inst_1 : Fintype (↑G₂.edgeSet : Type u_1)
simp_rw : Disjoint (↑G₁.edgeFinset : Set (Sym2 V)) (↑G₂.edgeFinset : Set (Sym2 V)) ↔ Disjoint G₁ G₂
⊢ Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂
have simp_rw₁ : Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
Tactic: simp_rw [← Finset.disjoint_coe, coe_edgeFinset, disjoint_edgeSet]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
⊢ G.edgeFinset = ∅ ↔ G = ⊥
have rw : G.edgeFinset = edgeFinset ⊥ ↔ G = ⊥
Tactic: rw [← edgeFinset_bot, edgeFinset_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
rw : G.edgeFinset = edgeFinset ⊥ ↔ G = ⊥
⊢ G.edgeFinset = ∅ ↔ G = ⊥
have rw₁ : G = ⊥ ↔ G = ⊥
Tactic: rw [← edgeFinset_bot, edgeFinset_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
⊢ G.edgeFinset.Nonempty ↔ G ≠ ⊥
have rw : G.edgeFinset ≠ ∅ ↔ G ≠ ⊥
Tactic: rw [Finset.nonempty_iff_ne_empty, edgeFinset_eq_empty.ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
rw : G.edgeFinset ≠ ∅ ↔ G ≠ ⊥
⊢ G.edgeFinset.Nonempty ↔ G ≠ ⊥
have rw₁ : G ≠ ⊥ ↔ G ≠ ⊥
Tactic: rw [Finset.nonempty_iff_ne_empty, edgeFinset_eq_empty.ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
⊢ card.{u_1} (α := Sym2 V) (edgeFinset ⊤) = (Fintype.card V).choose 2
have simp_rw : card.{u_1} (α := Sym2 V) (Set.toFinset (edgeSet ⊤)) = (Fintype.card V).choose 2
Tactic: simp_rw [edgeFinset, Set.toFinset_card, edgeSet_top, ← Sym2.card_diagSet_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
simp_rw : card.{u_1} (α := Sym2 V) (Set.toFinset (edgeSet ⊤)) = (Fintype.card V).choose 2
⊢ card.{u_1} (α := Sym2 V) (edgeFinset ⊤) = (Fintype.card V).choose 2
have simp_rw₁ : Fintype.card.{u_1} (↑(edgeSet ⊤) : Type u_1) = (Fintype.card V).choose 2
Tactic: simp_rw [edgeFinset, Set.toFinset_card, edgeSet_top, ← Sym2.card_diagSet_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
simp_rw : card.{u_1} (α := Sym2 V) (Set.toFinset (edgeSet ⊤)) = (Fintype.card V).choose 2
simp_rw₁ : Fintype.card.{u_1} (↑(edgeSet ⊤) : Type u_1) = (Fintype.card V).choose 2
⊢ card.{u_1} (α := Sym2 V) (edgeFinset ⊤) = (Fintype.card V).choose 2
have simp_rw₂ : Fintype.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1) = (Fintype.card V).choose 2
Tactic: simp_rw [edgeFinset, Set.toFinset_card, edgeSet_top, ← Sym2.card_diagSet_compl]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
⊢ #G.edgeFinset ≤ (Fintype.card V).choose 2
have rw : #G.edgeFinset ≤ card.{u_1} (α := Sym2 V) (edgeFinset ⊤)
Tactic: rw [← card_edgeFinset_top_eq_card_choose_two]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
⊢ #G.edgeFinset ≤ (Fintype.card V).choose 2
have rw : #G.edgeFinset ≤ card.{u_1} (α := Sym2 V) (edgeFinset ⊤)
Tactic: classical
  rw [← card_edgeFinset_top_eq_card_choose_two]
  exact card_le_card (edgeFinset_mono le_top)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ 0 < G.degree v ↔ v ∈ G.support
have rw : (∃ (w : V), G.Adj v w) ↔ v ∈ G.support
Tactic: rw [G.degree_pos_iff_exists_adj v, mem_support]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ 0 < G.degree v ↔ v ∈ G.support
have rw₁ : (∃ (w : V), G.Adj v w) ↔ ∃ (w : V), G.Adj v w
Tactic: rw [G.degree_pos_iff_exists_adj v, mem_support]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ G.degree v = 0 ↔ v ∉ G.support
have rw : G.degree v = 0 ↔ ¬0 < G.degree v
Tactic: rw [← G.degree_pos_iff_mem_support v, Nat.pos_iff_ne_zero, not_ne_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.degree v = 0 ↔ v ∉ G.support
have rw₁ : G.degree v = 0 ↔ ¬G.degree v ≠ 0
Tactic: rw [← G.degree_pos_iff_mem_support v, Nat.pos_iff_ne_zero, not_ne_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.degree v = 0 ↔ v ∉ G.support
have rw₂ : G.degree v = 0 ↔ G.degree v = 0
Tactic: rw [← G.degree_pos_iff_mem_support v, Nat.pos_iff_ne_zero, not_ne_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : Subsingleton V
⊢ G.degree v = 0
have this : 0 < G.degree v ↔ ∃ (w : V), G.Adj v w
Tactic: have := G.degree_pos_iff_exists_adj v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ G.degree v = 1 ↔ ∃! w : V, G.Adj v w
have rw : (∃! a : V, a ∈ G.neighborFinset v) ↔ ∃! w : V, G.Adj v w
Tactic: rw [degree, Finset.card_eq_one, Finset.singleton_iff_unique_mem]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
h : G.degree v ≠ 0
⊢ Nontrivial V
have by_contra! : ∀ (this : Subsingleton V), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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 = Fintype.card V - 1 - G.degree v
have rw : Gᶜ.degree v = #((G.neighborSet v).toFinset ∪ (Gᶜ.neighborSet v).toFinset) - G.degree v
Tactic: rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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 = Fintype.card V - 1 - G.degree v
have rw : Gᶜ.degree v = #(G.neighborSet v ∪ Gᶜ.neighborSet v).toFinset - 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ Gᶜ.degree v = Fintype.card V - 1 - G.degree v
have rw₁ : Gᶜ.degree v = #((G.neighborSet v).toFinset ∪ (Gᶜ.neighborSet v).toFinset) - 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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
inst_1 : DecidableEq V
⊢ Fintype.card.{u_1} (↑(G.incidenceSet v) : Type u_1) = G.degree v
have rw : Fintype.card.{u_1} (↑(G.neighborSet v) : Type u_1) = G.degree v
Tactic: rw [Fintype.card_congr (G.incidenceSetEquivNeighborSet v), card_neighborSet_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ Fintype.card.{u_1} (↑(G.incidenceSet v) : Type u_1) = G.degree v
have rw₁ : G.degree v = G.degree v
Tactic: rw [Fintype.card_congr (G.incidenceSetEquivNeighborSet v), card_neighborSet_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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) = G.degree v
have rw : #(G.incidenceFinset v) = Fintype.card.{u_1} (↑(G.incidenceSet v) : Type u_1)
Tactic: rw [← G.card_incidenceSet_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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 = {e ∈ G.edgeFinset | v ∈ e}
have 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}
Tactic: ext ⟨⟨⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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.degree v ≤ #G.edgeFinset
have rw : #(G.incidenceFinset v) ≤ #G.edgeFinset
Tactic: rw [← card_incidenceFinset_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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.degree v ≤ #G.edgeFinset
have rw : #(G.incidenceFinset v) ≤ #G.edgeFinset
Tactic: classical
  rw [← card_incidenceFinset_eq_degree]
  exact card_le_card (G.incidenceFinset_subset v)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.degree v ≤ H.degree v
have simp_rw : Fintype.card.{u_1} (↑(G.neighborSet v) : Type u_1) ≤ Fintype.card.{u_1} (↑(H.neighborSet v) : Type u_1)
Tactic: simp_rw [← card_neighborSet_eq_degree]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ Gᶜ.degree v = Fintype.card V - 1 - k
have rw : Fintype.card V - 1 - G.degree v = Fintype.card V - 1 - k
Tactic: rw [degree_compl, h v]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ Gᶜ.degree v = Fintype.card V - 1 - k
have rw₁ : Fintype.card V - 1 - k = Fintype.card V - 1 - k
Tactic: rw [degree_compl, h v]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
v : V
inst_1 : DecidableRel G.Adj
⊢ G.neighborFinset v = {w : V | G.Adj v w}
have h : ∀ (a : V), a ∈ G.neighborFinset v ↔ Membership.mem (γ := Finset V) {w : V | G.Adj v w} a
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
v : V
⊢ (completeGraph V).degree v = Fintype.card V - 1
have simp_rw : #(erase univ v) = Fintype.card V - 1
Tactic: simp_rw [degree, neighborFinset_eq_filter, top_adj, filter_ne]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
v : V
⊢ #(erase univ v) = Fintype.card V - 1
have rw : card.{u_1} (α := V) univ - 1 = Fintype.card V - 1
Tactic: rw [card_erase_of_mem (mem_univ v), card_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ #(erase univ v) = Fintype.card V - 1
have rw₁ : Fintype.card V - 1 = Fintype.card V - 1
Tactic: rw [card_erase_of_mem (mem_univ v), card_univ]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
inst : Fintype V
v : V
⊢ degree ⊥ v = 0
have simp_rw : card.{u_1} (α := V) ∅ = 0
Tactic: simp_rw [degree, neighborFinset_eq_filter, bot_adj, filter_false]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
v : V
⊢ G.minDegree ≤ G.degree v
have obtain : ∀ (t : ℕ) (ht : Finset.min (image (fun (v : V) ↦ G.degree v) univ) = (↑t : WithTop ℕ)), 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))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (hypothesis)
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 ℕ)
⊢ G.minDegree ≤ G.degree v
have this : t ≤ G.degree v
Tactic: have := Finset.min_le_of_eq (mem_image_of_mem _ (mem_univ v)) ht
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.minDegree ≤ G.degree v
have rwa : WithTop.untopD 0 (Finset.min (image (fun (v : V) ↦ G.degree v) univ)) ≤ G.degree v
Tactic: rwa [minDegree, ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.minDegree ≤ G.degree v
have rwa₁ : WithTop.untopD 0 (↑t : WithTop ℕ) ≤ G.degree v
Tactic: rwa [minDegree, ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ k ≤ G.minDegree
have rcases : ∀ (v : V) (hv : G.minDegree = G.degree v), k ≤ G.minDegree
Tactic: rcases G.exists_minimal_degree_vertex with ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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.minDegree
have rw : k ≤ G.degree v
Tactic: rw [hv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : IsEmpty V
⊢ G.minDegree = 0
have 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)) ⊤
Tactic: rw [minDegree, WithTop.untopD_eq_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.minDegree ≤ H.minDegree
have inl : IsEmpty V → G.minDegree ≤ H.minDegree
Tactic: cases isEmpty_or_nonempty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.minDegree ≤ H.minDegree
have inr : Nonempty V → G.minDegree ≤ H.minDegree
Tactic: cases isEmpty_or_nonempty V
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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
⊢ G.minDegree ≤ H.minDegree
have inr : ∀ (v : V), G.minDegree ≤ H.degree v
Tactic: apply le_minDegree_of_forall_le_degree
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : Nonempty V
⊢ G.minDegree < Fintype.card V
have have : ∀ (v : V) (hv : G.minDegree = G.degree v), G.minDegree < Fintype.card V
Tactic: have ⟨v, hv⟩ := G.exists_minimal_degree_vertex
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
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.minDegree < Fintype.card V
have rw : G.degree v < Fintype.card V
Tactic: rw [hv]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : IsEmpty V
⊢ G.maxDegree = 0
have rw : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) univ))) 0
Tactic: rw [maxDegree, univ_eq_empty, image_empty, max_empty, WithBot.unbotD_bot]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : IsEmpty V
rw : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) univ))) 0
⊢ G.maxDegree = 0
have rw₁ : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) ∅))) 0
Tactic: rw [maxDegree, univ_eq_empty, image_empty, max_empty, WithBot.unbotD_bot]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : IsEmpty V
rw : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) univ))) 0
rw₁ : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) ∅))) 0
⊢ G.maxDegree = 0
have rw₂ : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max ∅)) 0
Tactic: rw [maxDegree, univ_eq_empty, image_empty, max_empty, WithBot.unbotD_bot]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : IsEmpty V
rw : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) univ))) 0
rw₁ : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) ∅))) 0
rw₂ : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max ∅)) 0
⊢ G.maxDegree = 0
have rw₃ : Eq (α := ℕ) (WithBot.unbotD 0 ⊥) 0
Tactic: rw [maxDegree, univ_eq_empty, image_empty, max_empty, WithBot.unbotD_bot]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Finite (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype V
inst_1 : DecidableRel G.Adj
inst_2 : IsEmpty V
rw : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) univ))) 0
rw₁ : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max (image (fun (v : V) ↦ G.degree v) ∅))) 0
rw₂ : Eq (α := ℕ) (WithBot.unbotD 0 (Finset.max ∅)) 0
rw₃ : Eq (α := ℕ) (WithBot.unbotD 0 ⊥) 0
⊢ G.maxDegree = 0
have rw₄ : Eq (α := ℕ) 0 0
Tactic: rw [maxDegree, univ_eq_empty, image_empty, max_empty, WithBot.unbotD_bot]