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
⊢ BddBelow (α := ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
have 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
Tactic: refine ⟨0, fun x ⟨_, _, hx⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
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 ≤ x
have rw : 0 ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber w H) : ℝ) (↑(w.choose 2) : ℝ)
Tactic: rw [← hx]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (hypothesis)
Goal:
W : Type u_1
H : SimpleGraph W
⊢ IsGLB
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
    H.turanDensity
have h_bdd : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
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
have refine : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop (𝓝 H.turanDensity)
Tactic: refine Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici ?_
    (antitoneOn_extremalNumber_div_choose_two H) h_bdd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (hypothesis)
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 (𝓝 H.turanDensity)
have 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)))
Tactic: have h_tto := Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici
    (antitoneOn_extremalNumber_div_choose_two H) h_bdd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
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)))
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop (𝓝 H.turanDensity)
have 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)
Tactic: rwa [← h_tto.limUnder_eq] at h_tto
Cleared hypotheses: h_tto
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (hypothesis)
Goal:
W : Type u_1
H : SimpleGraph W
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop (𝓝 H.turanDensity)
have 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)))
Tactic: have h_tendsto := Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici
    (antitoneOn_extremalNumber_div_choose_two H) (isGLB_turanDensity H).bddBelow
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
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)))
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop (𝓝 H.turanDensity)
have 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) : ℝ)))
Tactic: rwa [turanDensity, h_tendsto.limUnder_eq]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (hypothesis)
Goal:
W : Type u_1
H : SimpleGraph W
h : H.turanDensity ≠ 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(extremalNumber n H) : ℝ)) fun (n : ℕ) ↦
    H.turanDensity * (↑(n.choose 2) : ℝ)
have hπ : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)) atTop (𝓝 H.turanDensity)
Tactic: have hπ := tendsto_turanDensity H
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (hypothesis)
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)
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(extremalNumber n H) : ℝ)) fun (n : ℕ) ↦
    H.turanDensity * (↑(n.choose 2) : ℝ)
have hπ₁ : 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π
Cleared hypotheses: hπ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (hypothesis)
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))
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(extremalNumber n H) : ℝ)) fun (n : ℕ) ↦
    H.turanDensity * (↑(n.choose 2) : ℝ)
have hπ₁ : 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π
Cleared hypotheses: hπ
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
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
have rw : ∃ (a : ℕ), ∀ b ≥ a, H.turanDensity * (↑(b.choose 2) : ℝ) ≠ 0
Tactic: rw [eventually_atTop]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
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
have refine : ∀ (n : ℕ) (hn : n ≥ 2), H.turanDensity * (↑(n.choose 2) : ℝ) ≠ 0
Tactic: refine ⟨2, fun n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (hypothesis)
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)
⊢ IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑(extremalNumber n H) : ℝ)) fun (n : ℕ) ↦
    H.turanDensity * (↑(n.choose 2) : ℝ)
have hz : ∀ᶠ (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]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (hypothesis)
Goal:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) → H ⊑ G
have hπ : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
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
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ {G : SimpleGraph (Fin n)} [inst : DecidableRel G.Adj],
      (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) → H ⊑ G
have rw : ∃ (a : ℕ),
  ∀ b ≥ a,
    ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
      (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(b.choose 2) : ℝ) → H ⊑ G
Tactic: rw [eventually_atTop]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (goal)
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
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
        (↑(#G.edgeFinset) : ℝ) ≥ (H.turanDensity + ε) * (↑(b.choose 2) : ℝ) → H ⊑ G
have 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}
Tactic: contrapose! hπ with h
Cleared hypotheses: hπ
-- 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)
⊢ H.turanDensity <
    sInf
      {x : ℝ |
        ∃ (n : ℕ),
          Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
            HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
have apply : 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
-- 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)
⊢ H.turanDensity + ε ≤
    sInf
      {x : ℝ |
        ∃ (n : ℕ),
          Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
            HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
have refine_1 : Set.Nonempty (α := ℝ)
  {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⟩ ↦ ?_)
-- 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)
refine_1 :
  Set.Nonempty (α := ℝ)
    {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}
have 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
Tactic: refine le_csInf ?_ (fun x ⟨m, hm, hx⟩ ↦ ?_)
-- 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)
⊢ Set.Nonempty (α := ℝ)
    {x : ℝ |
      ∃ (n : ℕ),
        Membership.mem (γ := Set ℕ) (Set.Ici 2) n ∧
          HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) = x}
have refine_1 : Set.Nonempty (α := ℕ) (Set.Ici 2)
Tactic: rw [← Set.image, Set.image_nonempty]
-- 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
⊢ H.turanDensity + ε ≤ x
have refine_2 : H.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)
Tactic: rw [← hx]
-- 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
⊢ H.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)
have 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) : ℝ)
Tactic: have ⟨n, hn, G, _, hcard_edges, h_free⟩ := h m
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity (hypothesis)
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.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)
have h_free₁ : H.Free G
Tactic: replace h_free : H.Free G := not_nonempty_iff.mpr h_free
Cleared hypotheses: h_free
-- 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 + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)
have trans : H.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)
Tactic: trans (extremalNumber n H / n.choose 2)
-- 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
trans : H.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)
⊢ H.turanDensity + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)
have trans₁ : HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ) ≤
  HDiv.hDiv (α := ℝ) (↑(extremalNumber m H) : ℝ) (↑(m.choose 2) : ℝ)
Tactic: trans (extremalNumber n H / n.choose 2)
-- 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 + ε ≤ HDiv.hDiv (α := ℝ) (↑(extremalNumber n H) : ℝ) (↑(n.choose 2) : ℝ)
have rw : (H.turanDensity + ε) * (↑(n.choose 2) : ℝ) ≤ (↑(extremalNumber n H) : ℝ)
Tactic: rw [le_div_iff₀ <| mod_cast Nat.choose_pos (hm.trans hn)]
-- 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 : n
Tactic: enter [2, 1, 1]
-- 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
| n
have rw : Fintype.card (Fin n)
Tactic: rw [← Fintype.card_fin n]