awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
rw : Finset.card (α := Fin (n + 1)) univ * extremalNumber n H
| (n + 1) * extremalNumber n H

Tactic:
rw [← Fintype.card_fin (n + 1), ← card_univ]

Premises used: Finset.card_univ, Fintype.card_fin, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
hf : #G.edgeFinset * (n - 1) ≤ Finset.card (α := Fin (n + 1)) univ * extremalNumber n H
⊢ #G.edgeFinset * (n - 1) ≤ (n + 1) * extremalNumber n H

Tactic:
conv_rhs =>
    rw [← Fintype.card_fin (n + 1), ← card_univ]

Premises used: Finset.card_univ, Fintype.card_fin, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
hf :
  ∀ b ∈ G.edgeFinset,
    n - 1 ≤
      (↑(Finset.card (α := Fin (n + 1))
            (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ b)) :
        ℕ)
hf₁ :
  ∀ (a : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) univ a →
      (↑(#(bipartiteAbove (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) G.edgeFinset a)) : ℕ) ≤
        extremalNumber n H
⊢ #G.edgeFinset * (n - 1) ≤ Finset.card (α := Fin (n + 1)) univ * extremalNumber n H

Tactic:
apply card_nsmul_le_card_nsmul' (r := fun v e ↦ v ∉ e)

Premises used: Membership.mem, Not, Finset.card_nsmul_le_card_nsmul'
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
e : Sym2 (Fin (n + 1))
he : e ∈ G.edgeFinset
hf :
  n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e.toFinset) univ e)) :
      ℕ)
hf₁ : n - 1 ≤ (↑(Finset.card (α := Fin (n + 1)) {x : Fin (n + 1) | x ∉ e.toFinset}) : ℕ)
hf₂ : n - 1 ≤ (↑(#(univ \ filter (Membership.mem e.toFinset) univ)) : ℕ)
hf₃ : n - 1 ≤ (↑(#(univ \ (univ ∩ e.toFinset))) : ℕ)
hf₄ : n - 1 ≤ (↑(#(univ \ e.toFinset)) : ℕ)
hf₅ : n - 1 ≤ (↑(#e.toFinsetᶜ) : ℕ)
hf₆ : n - 1 ≤ (↑(Fintype.card (Fin (n + 1)) - #e.toFinset) : ℕ)
hf₇ : n - 1 ≤ (↑(n + 1 - #e.toFinset) : ℕ)
hf₈ : n - 1 ≤ (↑(n + 1 - 2) : ℕ)
hf₉ : n - 1 ≤ n + 1 - 2
hf₁₀ : n - 1 ≤ n - 1
⊢ n - 1 ≤
    (↑(Finset.card (α := Fin (n + 1))
          (bipartiteBelow (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) univ e)) :
      ℕ)

Tactic:
simp_rw [← Sym2.mem_toFinset, bipartiteBelow, filter_not, filter_mem_eq_inter, univ_inter,
      ← compl_eq_univ_sdiff, card_compl, Fintype.card_fin, card_toFinset_mem_edgeFinset ⟨e, he⟩,
      Nat.cast_id, Nat.reduceSubDiff, le_refl]

Premises used: le_refl, Finset.compl_eq_univ_sdiff, Fintype.card_fin, Nat.cast_id, Finset.card_compl, Nat.reduceSubDiff, Subtype.mk, Sym2.mem_toFinset, Finset.univ_inter, Finset.filter_not, SimpleGraph.card_toFinset_mem_edgeFinset, Finset.bipartiteBelow, Finset.filter_mem_eq_inter
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst : DecidableRel G.Adj
h : H.Free G
v : Fin (n + 1)
hv : Membership.mem (γ := Finset (Fin (n + 1))) univ v
⊢ (↑(#(bipartiteAbove (fun (v : Fin (n + 1)) (e : Sym2 (Fin (n + 1))) ↦ v ∉ e) G.edgeFinset v)) : ℕ) ≤
    extremalNumber n H

Tactic:
simpa [edgeFinset_deleteIncidenceSet_eq_filter]
      using card_edgeFinset_deleteIncidenceSet_le_extremalNumber h v

Premises used: SimpleGraph.card_edgeFinset_deleteIncidenceSet_le_extremalNumber, SimpleGraph.edgeFinset_deleteIncidenceSet_eq_filter
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
⊢ BddBelow (α := ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}

Tactic:
⟨0, fun x ⟨_, _, hx⟩ ↦ ?_⟩

Premises used: _private.0.SimpleGraph.isGLB_turanDensity.match_1, LE.le, Set.Nonempty, BddBelow, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
refine :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ)
        {x : ℝ |
          ∃ (n : ℕ),
            Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
              HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
        x →
      ∀ (w : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) w →
          ∀ (hx : HDiv.hDiv (α := ℝ) (↑(extremalNumber w H) : ℝ) (↑(w.choose 2) : ℝ) = x), 0 ≤ x
⊢ BddBelow (α := ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}

Tactic:
refine ⟨0, fun x ⟨_, _, hx⟩ ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
x : ℝ
h :
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
    x
w : ℕ
left : Membership.mem (γ := Set ℕ) (Set.Ici 2) w
hx : HDiv.hDiv (α := ℝ) (↑(extremalNumber w H) : ℝ) (↑(w.choose 2) : ℝ) = x
rw : 0 ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber w H) : ℝ) (↑(w.choose 2) : ℝ)
⊢ 0 ≤ x

Tactic:
rw [← hx]
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
x : ℝ
h :
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
    x
w : ℕ
left : Membership.mem (γ := Set ℕ) (Set.Ici 2) w
hx : HDiv.hDiv (α := ℝ) (↑(extremalNumber w H) : ℝ) (↑(w.choose 2) : ℝ) = x
⊢ 0 ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber w H) : ℝ) (↑(w.choose 2) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
⊢ BddBelow (α := ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}

Tactic:
have h_bdd : BddBelow { (extremalNumber n H / n.choose 2 : ℝ) | n ∈ Set.Ici 2 } := by
    refine ⟨0, fun x ⟨_, _, hx⟩ ↦ ?_⟩
    rw [← hx]
    positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h_bdd :
  BddBelow (α := ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
⊢ IsGLB
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
    H.turanDensity

Tactic:
Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici ?_
    (antitoneOn_extremalNumber_div_choose_two H) h_bdd

Premises used: SimpleGraph.antitoneOn_extremalNumber_div_choose_two, setOf, Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici, Set.image
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h_bdd :
  BddBelow (α := ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
refine :
  Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop (𝓝 H.turanDensity)
⊢ IsGLB
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
    H.turanDensity

Tactic:
refine Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici ?_
    (antitoneOn_extremalNumber_div_choose_two H) h_bdd

Premises used: SimpleGraph.antitoneOn_extremalNumber_div_choose_two, Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h_bdd :
  BddBelow (α := ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop
    (𝓝 (sInf ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) '' Set.Ici 2)))

Tactic:
have h_tto := Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici
    (antitoneOn_extremalNumber_div_choose_two H) h_bdd
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h_bdd :
  BddBelow (α := ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
h_tto :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop
    (𝓝 (sInf ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) '' Set.Ici 2)))
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h_tto :
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop
        (𝓝 (limUnder atTop fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)))),
    Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop (𝓝 H.turanDensity)
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop (𝓝 H.turanDensity)

Tactic:
rwa [← h_tto.limUnder_eq] at h_tto

Premises used: Filter.Tendsto.limUnder_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
⊢ H.turanDensity =
    sInf
      {x : ℝ |
        ∃ (n : ℕ),
          Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
            HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}

Tactic:
have h := isGLB_turanDensity H
  (h.csInf_eq h.nonempty).symm

Premises used: IsGLB.csInf_eq, IsGLB.nonempty, SimpleGraph.isGLB_turanDensity, Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop
    (𝓝 (sInf ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) '' Set.Ici 2)))

Tactic:
have h_tendsto := Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici
    (antitoneOn_extremalNumber_div_choose_two H) (isGLB_turanDensity H).bddBelow
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h_tendsto :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop
    (𝓝 (sInf ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) '' Set.Ici 2)))
rwa :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop
    (𝓝 (limUnder atTop fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)))
rwa₁ rwa₂ rwa₃ rwa₄ :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop
    (𝓝 (sInf ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) '' Set.Ici 2)))
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop (𝓝 H.turanDensity)

Tactic:
rwa [turanDensity, h_tendsto.limUnder_eq]

Premises used: SimpleGraph.turanDensity, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop (𝓝 H.turanDensity)

Tactic:
have hπ := tendsto_turanDensity H
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop (𝓝 H.turanDensity)
⊢ Tendsto (fun (x : ℕ) ↦ 1 / H.turanDensity * HDiv.hDiv (α := ℝ) (↑(extremalNumber x H) : ℝ) (↑(x.choose 2) : ℝ)) atTop
    (𝓝 (1 / H.turanDensity * H.turanDensity))

Tactic:
apply Tendsto.const_mul (1 / turanDensity H : ℝ) at hπ

Premises used: SimpleGraph.turanDensity, HDiv.hDiv, Filter.Tendsto.const_mul, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ :
  Tendsto (fun (x : ℕ) ↦ 1 / H.turanDensity * HDiv.hDiv (α := ℝ) (↑(extremalNumber x H) : ℝ) (↑(x.choose 2) : ℝ)) atTop
    (𝓝 (1 / H.turanDensity * H.turanDensity))
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑(extremalNumber x H) : ℝ) / (H.turanDensity * (↑(x.choose 2) : ℝ))) atTop (𝓝 1)

Tactic:
simp_rw [one_div_mul_cancel h, div_mul_div_comm, one_mul] at hπ

Premises used: div_mul_div_comm, one_div_mul_cancel, one_mul
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑(extremalNumber x H) : ℝ) / (H.turanDensity * (↑(x.choose 2) : ℝ))) atTop (𝓝 1)
rw : ∃ (a : ℕ), ∀ b ≥ a, H.turanDensity * (↑(b.choose 2) : ℝ) ≠ 0
⊢ ∀ᶠ (x : ℕ) in atTop, H.turanDensity * (↑(x.choose 2) : ℝ) ≠ 0

Tactic:
rw [eventually_atTop]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑(extremalNumber x H) : ℝ) / (H.turanDensity * (↑(x.choose 2) : ℝ))) atTop (𝓝 1)
⊢ ∃ (a : ℕ), ∀ b ≥ a, H.turanDensity * (↑(b.choose 2) : ℝ) ≠ 0

Tactic:
⟨2, fun n hn ↦ ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑(extremalNumber x H) : ℝ) / (H.turanDensity * (↑(x.choose 2) : ℝ))) atTop (𝓝 1)
refine : ∀ (n : ℕ) (hn : n ≥ 2), H.turanDensity * (↑(n.choose 2) : ℝ) ≠ 0
⊢ ∃ (a : ℕ), ∀ b ≥ a, H.turanDensity * (↑(b.choose 2) : ℝ) ≠ 0

Tactic:
refine ⟨2, fun n hn ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑(extremalNumber x H) : ℝ) / (H.turanDensity * (↑(x.choose 2) : ℝ))) atTop (𝓝 1)
n : ℕ
hn : n ≥ 2
⊢ H.turanDensity * (↑(n.choose 2) : ℝ) ≠ 0

Tactic:
simpa [h, Nat.choose_eq_zero_iff]

Premises used: Nat.choose_eq_zero_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑(extremalNumber x H) : ℝ) / (H.turanDensity * (↑(x.choose 2) : ℝ))) atTop (𝓝 1)
⊢ ∀ᶠ (x : ℕ) in atTop, H.turanDensity * (↑(x.choose 2) : ℝ) ≠ 0

Tactic:
have hz : ∀ᶠ (x : ℕ) in atTop, turanDensity H * x.choose 2 ≠ 0 := by
    rw [eventually_atTop]
    refine ⟨2, fun n hn ↦ ?_⟩
    simpa [h, Nat.choose_eq_zero_iff]
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
hπ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ (↑(extremalNumber x H) : ℝ) / (H.turanDensity * (↑(x.choose 2) : ℝ))) atTop (𝓝 1)
hz : ∀ᶠ (x : ℕ) in atTop, H.turanDensity * (↑(x.choose 2) : ℝ) ≠ 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(extremalNumber n H) : ℝ)) fun (n : ℕ) ↦
    H.turanDensity * (↑(n.choose 2) : ℝ)

Tactic:
simpa [isEquivalent_iff_tendsto_one hz] using hπ

Premises used: Asymptotics.isEquivalent_iff_tendsto_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
⊢ sInf
      {x : ℝ |
        ∃ (n : ℕ),
          Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
            HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x} ≤
    H.turanDensity

Tactic:
have hπ := (turanDensity_eq_csInf H).ge
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
hπ :
  sInf
      {x : ℝ |
        ∃ (n : ℕ),
          Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
            HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x} ≤
    H.turanDensity
rw :
  ∃ (a : ℕ),
    ∀ b ≥ a,
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(b.choose 2) : ℝ) → H ⊑ G
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) → H ⊑ G

Tactic:
rw [eventually_atTop]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
Goal:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
hπ :
  sInf
      {x : ℝ |
        ∃ (n : ℕ),
          Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
            HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x} ≤
    H.turanDensity
contrapose! :
  ∀
    (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)),
    H.turanDensity <
      sInf
        {x : ℝ |
          ∃ (n : ℕ),
            Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
              HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(b.choose 2) : ℝ) → H ⊑ G

Tactic:
contrapose! hπ with h
-- 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)
apply :
  H.turanDensity + ε ≤
    sInf
      {x : ℝ |
        ∃ (n : ℕ),
          Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
            HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
⊢ H.turanDensity <
    sInf
      {x : ℝ |
        ∃ (n : ℕ),
          Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
            HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}

Tactic:
apply lt_of_lt_of_le <| lt_add_of_pos_right (turanDensity H) hε_pos

Premises used: lt_add_of_pos_right, SimpleGraph.turanDensity, lt_of_lt_of_le
-- 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)
⊢ H.turanDensity + ε ≤
    sInf
      {x : ℝ |
        ∃ (n : ℕ),
          Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
            HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}

Tactic:
le_csInf ?_ (fun x ⟨m, hm, hx⟩ ↦ ?_)

Premises used: le_csInf, _private.0.SimpleGraph.eventually_isContained_of_card_edgeFinset.match_1, SimpleGraph.turanDensity, LE.le, HAdd.hAdd
-- 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)
refine_1 :
  Set.Nonempty (α := ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
refine_2 :
  ∀ (x : ℝ),
    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), H.turanDensity + ε ≤ x
⊢ H.turanDensity + ε ≤
    sInf
      {x : ℝ |
        ∃ (n : ℕ),
          Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
            HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}

Tactic:
refine le_csInf ?_ (fun x ⟨m, hm, hx⟩ ↦ ?_)
-- 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)
refine_1 : Set.Nonempty (α := ℕ) (Set.Ici 2)
⊢ Set.Nonempty (α := ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}

Tactic:
rw [← Set.image, Set.image_nonempty]

Premises used: Set.image_nonempty, Set.image
-- 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)
⊢ Set.Nonempty (α := ℕ) (Set.Ici 2)

Tactic:
Set.nonempty_Ici

Premises used: Set.nonempty_Ici
-- 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)
⊢ Set.Nonempty (α := ℕ) (Set.Ici 2)

Tactic:
exact Set.nonempty_Ici

Premises used: Set.nonempty_Ici
-- 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
refine_2 : H.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)
⊢ H.turanDensity + ε ≤ x

Tactic:
rw [← hx]
-- 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
refine_2 :
  ∀ (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.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)
⊢ H.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)

Tactic:
have ⟨n, hn, G, _, hcard_edges, h_free⟩ := h m