awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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 : IsEmpty.{u_1 + 1} (H.Copy G)
⊢ H.Free G

Tactic:
replace h_free : H.Free G := not_nonempty_iff.mpr h_free
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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
trans : H.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)
trans₁ :
  HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)
⊢ H.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)

Tactic:
trans (extremalNumber n H / n.choose 2)

Premises used: Nat.choose, SimpleGraph.extremalNumber, HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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
rw : (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) ≤ (↑(extremalNumber n H) : ℝ)
⊢ H.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)

Tactic:
rw [le_div_iff₀ <| mod_cast Nat.choose_pos (hm.trans hn)]

Premises used: Nat.choose_pos, LE.le.trans, le_div_iff₀
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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
enter : n
| (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) ≤ (↑(extremalNumber n H) : ℝ)

Tactic:
enter [2, 1, 1]
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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
rw : Fintype.card (Fin n)
| n

Tactic:
rw [← Fintype.card_fin n]

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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
enter : Fintype.card (Fin n)
| (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) ≤ (↑(extremalNumber n H) : ℝ)

Tactic:
enter [2, 1, 1]
      rw [← Fintype.card_fin n]

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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
conv : (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) ≤ (↑(extremalNumber (Fintype.card (Fin n)) H) : ℝ)
⊢ (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) ≤ (↑(extremalNumber n H) : ℝ)

Tactic:
conv =>
      enter [2, 1, 1]
      rw [← Fintype.card_fin n]

Premises used: Fintype.card_fin
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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 (Fintype.card (Fin n)) H) : ℝ)

Tactic:
hcard_edges.trans (mod_cast card_edgeFinset_le_extremalNumber h_free)

Premises used: SimpleGraph.card_edgeFinset_le_extremalNumber, cast, Nat.cast_le._simp_1, LE.le.trans, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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 (Fintype.card (Fin n)) H) : ℝ)

Tactic:
exact hcard_edges.trans (mod_cast card_edgeFinset_le_extremalNumber h_free)

Premises used: LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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
⊢ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)

Tactic:
antitoneOn_extremalNumber_div_choose_two H hm (hm.trans hn) hn

Premises used: SimpleGraph.antitoneOn_extremalNumber_div_choose_two, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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
⊢ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)

Tactic:
exact antitoneOn_extremalNumber_div_choose_two H hm (hm.trans hn) hn

Premises used: SimpleGraph.antitoneOn_extremalNumber_div_choose_two, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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
rw :
  (↑(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 ⋯)
⊢ (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑((Fintype.card V).choose 2) : ℝ) → H ⊑ G

Tactic:
rw [(G.overFinIso rfl).card_edgeFinset_eq, isContained_congr Iso.refl (G.overFinIso rfl)]

Premises used: SimpleGraph.Iso.refl, SimpleGraph.overFinIso, SimpleGraph.Iso.card_edgeFinset_eq, SimpleGraph.isContained_congr, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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
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)
      ⋯
⊢ (↑(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 ⋯)

Tactic:
apply Nat.find_spec <| eventually_atTop.mp <| eventually_isContained_of_card_edgeFinset H hε_pos

Premises used: SimpleGraph.eventually_isContained_of_card_edgeFinset, Iff.mp, Filter.eventually_atTop, Nat.find_spec
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
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
⊢ 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)
      ⋯

Tactic:
simpa only [turanDensityConst, hε_pos, ↓reduceDIte] using h_verts

Premises used: reduceDIte, SimpleGraph.turanDensityConst
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
⊢ (↑G.edgeFinset : Set (Sym2 V)) = G.edgeSet

Tactic:
Set.coe_toFinset _

Premises used: setOf, Set.coe_toFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
e : Sym2 V
inst : Fintype (↑G.edgeSet : Type u_1)
⊢ e ∈ G.edgeFinset ↔ e ∈ G.edgeSet

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
e : Sym2 V
inst : Fintype (↑G.edgeSet : Type u_1)
⊢ e ∈ G.edgeFinset → ¬e.IsDiag

Tactic:
not_isDiag_of_mem_edgeSet _ ∘ mem_edgeFinset.1

Premises used: Function.comp, SimpleGraph.mem_edgeFinset, Iff.mp, SimpleGraph.not_isDiag_of_mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : DecidableEq V
e : ↥G.edgeFinset
⊢ #(↑e : Sym2 V).toFinset = 2

Tactic:
Sym2.card_toFinset_of_not_isDiag e.val (G.not_isDiag_of_mem_edgeFinset e.prop)

Premises used: Sym2.card_toFinset_of_not_isDiag, SimpleGraph.not_isDiag_of_mem_edgeFinset, Subtype.prop, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst : Fintype (↑G₁.edgeSet : Type u_1)
inst_1 : Fintype (↑G₂.edgeSet : Type u_1)
⊢ G₁.edgeFinset = G₂.edgeFinset ↔ G₁ = G₂

Tactic:
simp [edgeFinset]

Premises used: SimpleGraph.edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst : Fintype (↑G₁.edgeSet : Type u_1)
inst_1 : Fintype (↑G₂.edgeSet : Type u_1)
⊢ G₁.edgeFinset ⊆ G₂.edgeFinset ↔ G₁ ≤ G₂

Tactic:
simp [edgeFinset]

Premises used: SimpleGraph.edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst : Fintype (↑G₁.edgeSet : Type u_1)
inst_1 : Fintype (↑G₂.edgeSet : Type u_1)
⊢ G₁.edgeFinset ⊂ G₂.edgeFinset ↔ G₁ < G₂

Tactic:
simp [edgeFinset]

Premises used: SimpleGraph.edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
⊢ Eq.{u_1 + 1} (α := Finset (Sym2 V)) (edgeFinset ⊥) ∅

Tactic:
simp [edgeFinset]

Premises used: SimpleGraph.edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst : Fintype (↑G₁.edgeSet : Type u_1)
inst_1 : Fintype (↑G₂.edgeSet : Type u_1)
inst_2 : Fintype (↑(G₁ ⊔ G₂).edgeSet : Type u_1)
inst_3 : DecidableEq V
⊢ (G₁ ⊔ G₂).edgeFinset = G₁.edgeFinset ∪ G₂.edgeFinset

Tactic:
simp [edgeFinset]

Premises used: SimpleGraph.edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst : Fintype (↑G₁.edgeSet : Type u_1)
inst_1 : Fintype (↑G₂.edgeSet : Type u_1)
inst_2 : DecidableEq V
⊢ (G₁ ⊓ G₂).edgeFinset = G₁.edgeFinset ∩ G₂.edgeFinset

Tactic:
simp [edgeFinset]

Premises used: SimpleGraph.edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst : Fintype (↑G₁.edgeSet : Type u_1)
inst_1 : Fintype (↑G₂.edgeSet : Type u_1)
inst_2 : DecidableEq V
⊢ (G₁ \ G₂).edgeFinset = G₁.edgeFinset \ G₂.edgeFinset

Tactic:
simp [edgeFinset]

Premises used: SimpleGraph.edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
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₂
simp_rw₁ : Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
⊢ Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂

Tactic:
simp_rw [← Finset.disjoint_coe, coe_edgeFinset, disjoint_edgeSet]

Premises used: Finset.disjoint_coe, SimpleGraph.coe_edgeFinset, SimpleGraph.disjoint_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
rw : G.edgeFinset = edgeFinset ⊥ ↔ G = ⊥
rw₁ rw₂ : G = ⊥ ↔ G = ⊥
⊢ G.edgeFinset = ∅ ↔ G = ⊥

Tactic:
rw [← edgeFinset_bot, edgeFinset_inj]

Premises used: SimpleGraph.edgeFinset_inj, SimpleGraph.edgeFinset_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
rw : G.edgeFinset ≠ ∅ ↔ G ≠ ⊥
rw₁ rw₂ : G ≠ ⊥ ↔ G ≠ ⊥
⊢ G.edgeFinset.Nonempty ↔ G ≠ ⊥

Tactic:
rw [Finset.nonempty_iff_ne_empty, edgeFinset_eq_empty.ne]

Premises used: Finset.nonempty_iff_ne_empty, Iff.ne, SimpleGraph.edgeFinset_eq_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
⊢ #G.edgeFinset = Fintype.card.{u_1} (↑G.edgeSet : Type u_1)

Tactic:
Set.toFinset_card _

Premises used: Set.toFinset_card, SimpleGraph.edgeFinset
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
⊢ Fintype.card.{u_1} (↑G.edgeSet : Type u_1) = #G.edgeFinset

Tactic:
.symm <| Set.toFinset_card _

Premises used: Set.toFinset_card, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
⊢ card.{u_1} (α := (↑G.edgeSet : Type u_1)) univ = #G.edgeFinset

Tactic:
simp [card_edgeSet]

Premises used: SimpleGraph.card_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
inst : Fintype V
inst_1 : DecidableEq V
⊢ Eq.{u_1 + 1} (α := Finset (Sym2 V)) (edgeFinset ⊤) (Set.toFinset Sym2.diagSetᶜ)

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
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
simp_rw₂ : Fintype.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1) = (Fintype.card V).choose 2
⊢ card.{u_1} (α := Sym2 V) (edgeFinset ⊤) = (Fintype.card V).choose 2

Tactic:
simp_rw [edgeFinset, Set.toFinset_card, edgeSet_top, ← Sym2.card_diagSet_compl]

Premises used: SimpleGraph.edgeSet_top, Set.toFinset_card, SimpleGraph.edgeFinset, Sym2.card_diagSet_compl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
rw : #G.edgeFinset ≤ card.{u_1} (α := Sym2 V) (edgeFinset ⊤)
⊢ #G.edgeFinset ≤ (Fintype.card V).choose 2

Tactic:
rw [← card_edgeFinset_top_eq_card_choose_two]

Premises used: SimpleGraph.card_edgeFinset_top_eq_card_choose_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
⊢ #G.edgeFinset ≤ card.{u_1} (α := Sym2 V) (edgeFinset ⊤)

Tactic:
card_le_card (edgeFinset_mono le_top)

Premises used: SimpleGraph.edgeFinset_mono, Finset.card_le_card, le_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
⊢ #G.edgeFinset ≤ card.{u_1} (α := Sym2 V) (edgeFinset ⊤)

Tactic:
exact card_le_card (edgeFinset_mono le_top)

Premises used: SimpleGraph.edgeFinset_mono, Finset.card_le_card, le_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
inst : Fintype (↑G.edgeSet : Type u_1)
inst_1 : Fintype V
rw rw₁ rw₂ : #G.edgeFinset ≤ card.{u_1} (α := Sym2 V) (edgeFinset ⊤)
⊢ #G.edgeFinset ≤ (Fintype.card V).choose 2

Tactic:
classical
  rw [← card_edgeFinset_top_eq_card_choose_two]
  exact card_le_card (edgeFinset_mono le_top)

Premises used: SimpleGraph.edgeFinset_mono, Finset.card_le_card, SimpleGraph.card_edgeFinset_top_eq_card_choose_two, le_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ G.neighborFinset v = (G.neighborSet v).toFinset

Tactic:
rfl

Premises used: SimpleGraph.neighborFinset, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ (↑(G.neighborFinset v) : Set V) = G.neighborSet v

Tactic:
Set.coe_toFinset _

Premises used: setOf, Set.coe_toFinset
-- 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
⊢ w ∈ G.neighborFinset v ↔ G.Adj v w

Tactic:
Set.mem_toFinset

Premises used: Set.Mem, setOf, SimpleGraph.neighborSet, 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)
⊢ v ∉ G.neighborFinset v

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ Disjoint (G.neighborFinset v) {v}

Tactic:
Finset.disjoint_singleton_right.mpr <| notMem_neighborFinset_self _ _

Premises used: Iff.mpr, SimpleGraph.notMem_neighborFinset_self, Finset.disjoint_singleton_right
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ Disjoint {v} (G.neighborFinset v)

Tactic:
Finset.disjoint_singleton_left.mpr <| notMem_neighborFinset_self _ _

Premises used: Iff.mpr, SimpleGraph.notMem_neighborFinset_self, Finset.disjoint_singleton_left
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ G.neighborFinset v = ∅ ↔ G.IsIsolated v

Tactic:
simp [neighborFinset, IsIsolated, Set.ext_iff]

Premises used: SimpleGraph.neighborFinset, Set.ext_iff, SimpleGraph.IsIsolated
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ (G.neighborFinset v).Nonempty ↔ ¬G.IsIsolated v

Tactic:
simp [nonempty_iff_ne_empty]

Premises used: Finset.nonempty_iff_ne_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Finite
Goal:
V : Type u_1
G : SimpleGraph V
v : V
inst : Fintype (↑(G.neighborSet v) : Type u_1)
⊢ #(G.neighborFinset v) = G.degree v

Tactic:
rfl

Premises used: SimpleGraph.degree, rfl