awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this_1 : Coprime 2 (2 * n + 1)
this : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
⊢ LE.le (α := Finset α) (Iio (↑n : α)) univ

Tactic:
subset_univ _

Premises used: Finset.subset_univ
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this_1 : Coprime 2 (2 * n + 1)
this : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
⊢ LE.le (α := Finset α) (Iio (↑n : α)) univ

Tactic:
exact subset_univ _

Premises used: Finset.subset_univ
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this_1 : Coprime 2 (2 * n + 1)
this : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
⊢ HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ) ≤ ruzsaSzemerediNumber (α ⊕ α ⊕ α)

Tactic:
addRothNumber_le_ruzsaSzemerediNumber _

Premises used: addRothNumber_le_ruzsaSzemerediNumber
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this_1 : Coprime 2 (2 * n + 1)
this : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
simp_rw : ruzsaSzemerediNumberNat (2 * n + 1 + (2 * n + 1 + (2 * n + 1))) = ruzsaSzemerediNumberNat (6 * n + 3)
⊢ ruzsaSzemerediNumber (α ⊕ α ⊕ α) = ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
simp_rw [← ruzsaSzemerediNumberNat_card, Fintype.card_sum, α, Fintype.card_fin]

Premises used: Fintype.card_fin, ruzsaSzemerediNumberNat_card, Fintype.card_sum
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this_1 : Coprime 2 (2 * n + 1)
this : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
⊢ ruzsaSzemerediNumberNat (2 * n + 1 + (2 * n + 1 + (2 * n + 1))) = ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
ring_nf
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this_1 : Coprime 2 (2 * n + 1)
this : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
n₁ :
  HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
    HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ)
n₂ :
  HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ) ≤
    HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ)
n₃ : ruzsaSzemerediNumber (α ⊕ α ⊕ α) = ruzsaSzemerediNumberNat (6 * n + 3)
⊢ HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
calc
    (2 * n + 1) * rothNumberNat n
    _ = Fintype.card α * addRothNumber (Iio (n : α)) := by
      rw [Fin.addRothNumber_eq_rothNumberNat le_rfl, Fintype.card_fin]
    _ ≤ Fintype.card α * addRothNumber (univ : Finset α) := by
      gcongr; exact subset_univ _
    _ ≤ ruzsaSzemerediNumber (Sum α (Sum α α)) := addRothNumber_le_ruzsaSzemerediNumber _
    _ = ruzsaSzemerediNumberNat (6 * n + 3) := by
      simp_rw [← ruzsaSzemerediNumberNat_card, Fintype.card_sum, α, Fintype.card_fin]
      ring_nf

Premises used: HMul.hMul, Finset.univ, Fintype.card, Sum, rothNumberNat, addRothNumber_le_ruzsaSzemerediNumber, HAdd.hAdd, ruzsaSzemerediNumber, ruzsaSzemerediNumberNat, addRothNumber, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this_1 : Coprime 2 (2 * n + 1)
this : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
open :
  HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
    HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ)
open₁ :
  HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ) ≤
    HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ)
open₂ : ruzsaSzemerediNumber (α ⊕ α ⊕ α) = ruzsaSzemerediNumberNat (6 * n + 3)
⊢ HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) ≤ ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
open scoped Fin.CommRing in
  calc
    (2 * n + 1) * rothNumberNat n
    _ = Fintype.card α * addRothNumber (Iio (n : α)) := by
      rw [Fin.addRothNumber_eq_rothNumberNat le_rfl, Fintype.card_fin]
    _ ≤ Fintype.card α * addRothNumber (univ : Finset α) := by
      gcongr; exact subset_univ _
    _ ≤ ruzsaSzemerediNumber (Sum α (Sum α α)) := addRothNumber_le_ruzsaSzemerediNumber _
    _ = ruzsaSzemerediNumberNat (6 * n + 3) := by
      simp_rw [← ruzsaSzemerediNumberNat_card, Fintype.card_sum, α, Fintype.card_fin]
      ring_nf

Premises used: HMul.hMul, Finset.univ, Fintype.card, Sum, rothNumberNat, addRothNumber_le_ruzsaSzemerediNumber, HAdd.hAdd, ruzsaSzemerediNumber, ruzsaSzemerediNumberNat, addRothNumber, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ (HDiv.hDiv (α := ℝ) (↑0 : ℝ) 3 - 2) * (↑((rothNumberNat : (a : ℕ) → ℕ) (HSub.hSub (α := ℕ) 0 3 / 6)) : ℝ) ≤
    (↑(ruzsaSzemerediNumberNat 0) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ (HDiv.hDiv (α := ℝ) (↑1 : ℝ) 3 - 2) * (↑((rothNumberNat : (a : ℕ) → ℕ) (HSub.hSub (α := ℕ) 1 3 / 6)) : ℝ) ≤
    (↑(ruzsaSzemerediNumberNat 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ (HDiv.hDiv (α := ℝ) (↑2 : ℝ) 3 - 2) * (↑((rothNumberNat : (a : ℕ) → ℕ) (HSub.hSub (α := ℕ) 2 3 / 6)) : ℝ) ≤
    (↑(ruzsaSzemerediNumberNat 2) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
⊢ (HDiv.hDiv (α := ℝ) (↑(n + 3) : ℝ) 3 - 2) * (↑((rothNumberNat : (a : ℕ) → ℕ) (n / 6)) : ℝ) ≤
    HMul.hMul (α := ℝ) (↑(2 * (n / 6) + 1) : ℝ) (↑((rothNumberNat : (a : ℕ) → ℕ) (n / 6)) : ℝ)

Tactic:
mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg _)

Premises used: Nat.cast_nonneg, mul_le_mul_of_nonneg_right
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
⊢ HMul.hMul (α := ℝ) (↑(2 * (n / 6) + 1) : ℝ) (↑((rothNumberNat : (a : ℕ) → ℕ) (n / 6)) : ℝ) ≤
    (↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3)) : ℝ)

Tactic:
?_
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
grw grw₁ : LE.le (α := ℝ) (↑(ruzsaSzemerediNumberNat (n + 3)) : ℝ) (↑(ruzsaSzemerediNumberNat (n + 3)) : ℝ)
⊢ LE.le (α := ℝ) (↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3)) : ℝ) (↑(ruzsaSzemerediNumberNat (n + 3)) : ℝ)

Tactic:
grw [Nat.mul_div_le]

Premises used: Nat.mul_div_le
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
calc_1 : HDiv.hDiv (α := ℝ) (↑(n + 3) : ℝ) 3 - 2 ≤ (↑(2 * (n / 6) + 1) : ℝ)
calc_2 :
  HMul.hMul (α := ℝ) (↑(2 * (n / 6) + 1) : ℝ) (↑((rothNumberNat : (a : ℕ) → ℕ) (n / 6)) : ℝ) ≤
    (↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3)) : ℝ)
⊢ (HDiv.hDiv (α := ℝ) (↑(n + 3) : ℝ) 3 - 2) * (↑((rothNumberNat : (a : ℕ) → ℕ) ((n + 3 - 3) / 6)) : ℝ) ≤
    (↑(ruzsaSzemerediNumberNat (n + 3)) : ℝ)

Tactic:
calc
      _ ≤ (↑(2 * (n / 6) + 1) : ℝ) * rothNumberNat (n / 6) :=
        mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg _)
      _ ≤ (ruzsaSzemerediNumberNat (6 * (n / 6) + 3) : ℝ) := ?_
      _ ≤ _ := by grw [Nat.mul_div_le]

Premises used: HMul.hMul, Nat.cast_nonneg, HDiv.hDiv, rothNumberNat, Nat.cast, mul_le_mul_of_nonneg_right, HAdd.hAdd, ruzsaSzemerediNumberNat, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
calc_1 : HAdd.hAdd (α := ℝ) (↑n : ℝ) 3 / 3 ≤ HMul.hMul (α := ℝ) 2 (↑(n / 6) : ℝ) + 1 + 2
⊢ HDiv.hDiv (α := ℝ) (↑(n + 3) : ℝ) 3 - 2 ≤ (↑(2 * (n / 6) + 1) : ℝ)

Tactic:
simp only [cast_add, cast_ofNat, cast_mul, cast_one, tsub_le_iff_right]

Premises used: Nat.cast_ofNat, tsub_le_iff_right, Nat.cast_add, Nat.cast_mul, Nat.cast_one
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
calc_1 : (↑n : ℝ) ≤ HMul.hMul (α := ℝ) 2 3 * (↑(n / 6) : ℝ) + HMul.hMul (α := ℝ) 2 3
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 3 / 3 ≤ HMul.hMul (α := ℝ) 2 (↑(n / 6) : ℝ) + 1 + 2

Tactic:
rw [← div_add_one (three_ne_zero' ℝ), ← le_sub_iff_add_le, div_le_iff₀ (zero_lt_three' ℝ),
        add_assoc, add_sub_assoc, add_mul, mul_right_comm, add_sub_cancel_left]

Premises used: add_sub_assoc, add_mul, div_le_iff₀, Real, three_ne_zero', add_sub_cancel_left, add_assoc, zero_lt_three', div_add_one, mul_right_comm, le_sub_iff_add_le
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
calc_1 : n ≤ HMul.hMul (α := ℕ) 2 3 * (n / 6) + HMul.hMul (α := ℕ) 2 3
⊢ (↑n : ℝ) ≤ HMul.hMul (α := ℝ) 2 3 * (↑(n / 6) : ℝ) + HMul.hMul (α := ℝ) 2 3

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
⊢ 0 < HMul.hMul (α := ℕ) 2 3

Tactic:
simp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
⊢ n ≤ HMul.hMul (α := ℕ) 2 3 * (n / 6 + 1)

Tactic:
exact (Nat.lt_mul_div_succ _ <| by simp).le

Premises used: Nat.lt_mul_div_succ, LT.lt.le
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
calc_2 :
  HMul.hMul (β := ℕ) (2 * (n / 6) + 1) ((rothNumberNat : (a : ℕ) → ℕ) (n / 6) : ℕ) ≤
    ruzsaSzemerediNumberNat (6 * (n / 6) + 3)
⊢ HMul.hMul (α := ℝ) (↑(2 * (n / 6) + 1) : ℝ) (↑((rothNumberNat : (a : ℕ) → ℕ) (n / 6)) : ℝ) ≤
    (↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3)) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
⊢ HMul.hMul (β := ℕ) (2 * (n / 6) + 1) ((rothNumberNat : (a : ℕ) → ℕ) (n / 6) : ℕ) ≤
    ruzsaSzemerediNumberNat (6 * (n / 6) + 3)

Tactic:
rothNumberNat_le_ruzsaSzemerediNumberNat _

Premises used: rothNumberNat_le_ruzsaSzemerediNumberNat
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
⊢ HMul.hMul (β := ℕ) (2 * (n / 6) + 1) ((rothNumberNat : (a : ℕ) → ℕ) (n / 6) : ℕ) ≤
    ruzsaSzemerediNumberNat (6 * (n / 6) + 3)

Tactic:
exact rothNumberNat_le_ruzsaSzemerediNumberNat _

Premises used: rothNumberNat_le_ruzsaSzemerediNumberNat
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
rw :
  (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * ((↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))) ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)
⊢ (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ))) ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
inl :
  ∀ (hn : HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 ≤ 0),
    (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * ((↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))) ≤
      (↑(ruzsaSzemerediNumberNat n) : ℝ)
inr :
  ∀ (hn : 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2),
    (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * ((↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))) ≤
      (↑(ruzsaSzemerediNumberNat n) : ℝ)
⊢ (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * ((↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))) ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)

Tactic:
obtain hn | hn := le_total (n / 3 - 2 : ℝ) 0

Premises used: HSub.hSub, HDiv.hDiv, le_total, Nat.cast, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
hn : HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 ≤ 0
⊢ 0 ≤ (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))

Tactic:
positivity
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
hn : HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2 ≤ 0
⊢ (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * ((↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))) ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)

Tactic:
exact (mul_nonpos_of_nonpos_of_nonneg hn <| by positivity).trans (Nat.cast_nonneg _)

Premises used: mul_nonpos_of_nonpos_of_nonneg, Nat.cast_nonneg, LE.le.trans
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
hn : 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
⊢ (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * ((↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))) ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)

Tactic:
(mul_le_mul_of_nonneg_left Behrend.roth_lower_bound hn).trans
      (rothNumberNat_le_ruzsaSzemerediNumberNat' _)

Premises used: Behrend.roth_lower_bound, LE.le.trans, rothNumberNat_le_ruzsaSzemerediNumberNat', mul_le_mul_of_nonneg_left
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
hn : 0 ≤ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
⊢ (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * ((↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))) ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)

Tactic:
exact
    (mul_le_mul_of_nonneg_left Behrend.roth_lower_bound hn).trans
      (rothNumberNat_le_ruzsaSzemerediNumberNat' _)

Premises used: Behrend.roth_lower_bound, LE.le.trans, rothNumberNat_le_ruzsaSzemerediNumberNat', mul_le_mul_of_nonneg_left
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
trans :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * rexp (-4 * √(Real.log (↑n : ℝ)))) fun (n : ℕ) ↦
    (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))
trans₁ :
  IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ))))
    fun (n : ℕ) ↦ (↑(ruzsaSzemerediNumberNat n) : ℝ)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * rexp (-4 * √(Real.log (↑n : ℝ)))) fun (n : ℕ) ↦
    (↑(ruzsaSzemerediNumberNat n) : ℝ)

Tactic:
trans fun n ↦ (n / 3 - 2) * ↑((n - 3) / 6) * exp (-4 * √(log ↑((n - 3) / 6)))

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Real.exp, Real.log, Real.sqrt, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
simp_rw :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ) * rexp (-4 * √(Real.log (↑n : ℝ))))
    fun (n : ℕ) ↦
    (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * rexp (-4 * √(Real.log (↑n : ℝ)))) fun (n : ℕ) ↦
    (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))

Tactic:
simp_rw [sq]

Premises used: sq
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ) * rexp (-4 * √(Real.log (↑n : ℝ))))
    fun (n : ℕ) ↦
    (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))

Tactic:
(IsBigO.mul ?_ ?_).mul ?_

Premises used: Asymptotics.IsBigO.mul
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
refine_1 : IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
refine_2 : IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)
refine_3 :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ rexp (-4 * √(Real.log (↑n : ℝ)))) fun (n : ℕ) ↦
    rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ) * rexp (-4 * √(Real.log (↑n : ℝ))))
    fun (n : ℕ) ↦
    (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))

Tactic:
refine (IsBigO.mul ?_ ?_).mul ?_

Premises used: Asymptotics.IsBigO.mul
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
trans : IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3
trans₁ :
  IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3) fun (n : ℕ) ↦
    HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
⊢ IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2

Tactic:
trans fun n ↦ n / 3

Premises used: HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
simp_rw : IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HMul.hMul (α := ℝ) 3⁻¹ (↑n : ℝ)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3

Tactic:
simp_rw [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ Ne (α := ℝ) 3⁻¹ 0

Tactic:
simp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HMul.hMul (α := ℝ) 3⁻¹ (↑n : ℝ)

Tactic:
exact (isBigO_refl ..).const_mul_right (by simp)

Premises used: Asymptotics.IsBigO.const_mul_right, Asymptotics.isBigO_refl
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3) fun (n : ℕ) ↦
    HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2

Tactic:
IsLittleO.right_isBigO_sub ?_

Premises used: Asymptotics.IsLittleO.right_isBigO_sub
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ 2) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3) fun (n : ℕ) ↦
    HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2

Tactic:
refine IsLittleO.right_isBigO_sub ?_

Premises used: Asymptotics.IsLittleO.right_isBigO_sub
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ 3 * HMul.hMul (α := ℝ) 3⁻¹ (↑x : ℝ)) atTop atTop

Tactic:
simp [tendsto_natCast_atTop_atTop]

Premises used: tendsto_natCast_atTop_atTop
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ 2) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3

Tactic:
simpa [div_eq_inv_mul, Function.comp_def] using
        .atTop_of_const_mul₀ zero_lt_three (by simp [tendsto_natCast_atTop_atTop])

Premises used: Function.comp_def, div_eq_inv_mul
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
refine_2 : ∃ (c : ℝ), IsBigOWith (E := ℝ) (F := ℝ) c atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)

Tactic:
rw [IsBigO_def]

Premises used: Asymptotics.IsBigO_def
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ ∃ (c : ℝ), IsBigOWith (E := ℝ) (F := ℝ) c atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)

Tactic:
⟨12, ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
refine_2 : IsBigOWith (E := ℝ) (F := ℝ) 12 atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)
⊢ ∃ (c : ℝ), IsBigOWith (E := ℝ) (F := ℝ) c atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)

Tactic:
refine ⟨12, ?_⟩
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
refine_2 : ∃ (a : ℕ), ∀ b ≥ a, (↑b : ℝ) ≤ HMul.hMul (α := ℝ) 12 (↑((b - 3) / 6) : ℝ)
⊢ IsBigOWith (E := ℝ) (F := ℝ) 12 atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)

Tactic:
simp only [IsBigOWith, norm_natCast, eventually_atTop]

Premises used: Asymptotics.IsBigOWith, Real.norm_natCast, Filter.eventually_atTop
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
x : ℕ
hx : x ≥ 15
norm_cast : x ≤ 12 * ((x - 3) / 6)
⊢ (↑x : ℝ) ≤ HMul.hMul (α := ℝ) 12 (↑((x - 3) / 6) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
x : ℕ
hx : x ≥ 15
⊢ x ≤ 12 * ((x - 3) / 6)

Tactic:
lia
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ ∃ (a : ℕ), ∀ b ≥ a, (↑b : ℝ) ≤ HMul.hMul (α := ℝ) 12 (↑((b - 3) / 6) : ℝ)

Tactic:
exact ⟨15, fun x hx ↦ by norm_cast; lia⟩
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
refine_3 :
  IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop
    (HSub.hSub (α := ℕ → ℝ) (fun (n : ℕ) ↦ -4 * √(Real.log (↑n : ℝ))) fun (n : ℕ) ↦
      -4 * √(Real.log (↑((n - 3) / 6) : ℝ)))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ rexp (-4 * √(Real.log (↑n : ℝ)))) fun (n : ℕ) ↦
    rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))

Tactic:
rw [isBigO_exp_comp_exp_comp]

Premises used: Real.isBigO_exp_comp_exp_comp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop
    (HSub.hSub (α := ℕ → ℝ) (fun (n : ℕ) ↦ -4 * √(Real.log (↑n : ℝ))) fun (n : ℕ) ↦
      -4 * √(Real.log (↑((n - 3) / 6) : ℝ)))

Tactic:
⟨0, ?_⟩

Premises used: Filter.IsBounded, Exists.intro, OfNat.ofNat, Filter.IsBoundedUnder
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
refine_3 :
  ∀ᶠ (x : ℝ) in
    Filter.map
      (HSub.hSub (α := ℕ → ℝ) (fun (n : ℕ) ↦ -4 * √(Real.log (↑n : ℝ))) fun (n : ℕ) ↦
        -4 * √(Real.log (↑((n - 3) / 6) : ℝ)))
      atTop,
    (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x 0
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop
    (HSub.hSub (α := ℕ → ℝ) (fun (n : ℕ) ↦ -4 * √(Real.log (↑n : ℝ))) fun (n : ℕ) ↦
      -4 * √(Real.log (↑((n - 3) / 6) : ℝ)))

Tactic:
refine ⟨0, ?_⟩
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
refine_3 : ∃ (a : ℕ), ∀ b ≥ a, 4 * √(Real.log (↑((b - 3) / 6) : ℝ)) ≤ 4 * √(Real.log (↑b : ℝ))
⊢ ∀ᶠ (x : ℝ) in
    Filter.map
      (HSub.hSub (α := ℕ → ℝ) (fun (n : ℕ) ↦ -4 * √(Real.log (↑n : ℝ))) fun (n : ℕ) ↦
        -4 * √(Real.log (↑((n - 3) / 6) : ℝ)))
      atTop,
    (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x 0

Tactic:
simp only [neg_mul, eventually_map, Pi.sub_apply, sub_neg_eq_add, neg_add_le_iff_le_add,
        add_zero, eventually_atTop]

Premises used: neg_add_le_iff_le_add, Filter.eventually_map, neg_mul, add_zero, Filter.eventually_atTop, sub_neg_eq_add, Pi.sub_apply
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ ∃ (a : ℕ), ∀ b ≥ a, 4 * √(Real.log (↑((b - 3) / 6) : ℝ)) ≤ 4 * √(Real.log (↑b : ℝ))

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

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
refine_3 : ∀ (x : ℕ) (hx : x ≥ 9), 4 * √(Real.log (↑((x - 3) / 6) : ℝ)) ≤ 4 * √(Real.log (↑x : ℝ))
⊢ ∃ (a : ℕ), ∀ b ≥ a, 4 * √(Real.log (↑((b - 3) / 6) : ℝ)) ≤ 4 * √(Real.log (↑b : ℝ))

Tactic:
refine ⟨9, fun x hx ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
x : ℕ
hx : x ≥ 9
refine_3 : LT.lt (α := ℝ) 0 (↑((x - 3) / 6) : ℝ)
refine_3₁ : (x - 3) / 6 ≤ x
⊢ 4 * √(Real.log (↑((x - 3) / 6) : ℝ)) ≤ 4 * √(Real.log (↑x : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
x : ℕ
hx : x ≥ 9
refine_3 : 6 ≤ x - 3
⊢ LT.lt (α := ℝ) 0 (↑((x - 3) / 6) : ℝ)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
x : ℕ
hx : x ≥ 9
⊢ 6 ≤ x - 3

Tactic:
lia
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
x : ℕ
hx : x ≥ 9
⊢ (x - 3) / 6 ≤ x

Tactic:
lia
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ))))
    fun (n : ℕ) ↦ (↑(ruzsaSzemerediNumberNat n) : ℝ)

Tactic:
.of_norm_eventuallyLE ?_

Premises used: Asymptotics.IsBigO.of_norm_eventuallyLE
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
refine :
  EventuallyLE (β := ℝ) atTop
    (fun (x : ℕ) ↦
      ‖(HDiv.hDiv (α := ℝ) (↑x : ℝ) 3 - 2) * (↑((x - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((x - 3) / 6) : ℝ)))‖)
    fun (n : ℕ) ↦ (↑(ruzsaSzemerediNumberNat n) : ℝ)
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦
      (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ))))
    fun (n : ℕ) ↦ (↑(ruzsaSzemerediNumberNat n) : ℝ)

Tactic:
refine .of_norm_eventuallyLE ?_
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
h :
  ∀ (n : ℕ) (hn : 6 ≤ n),
    ‖(HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))‖ ≤
      (↑(ruzsaSzemerediNumberNat n) : ℝ)
⊢ EventuallyLE (β := ℝ) atTop
    (fun (x : ℕ) ↦
      ‖(HDiv.hDiv (α := ℝ) (↑x : ℝ) 3 - 2) * (↑((x - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((x - 3) / 6) : ℝ)))‖)
    fun (n : ℕ) ↦ (↑(ruzsaSzemerediNumberNat n) : ℝ)

Tactic:
filter_upwards [eventually_ge_atTop 6] with n hn

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
Goal:
n : ℕ
hn : 6 ≤ n
⊢ LE.le (α := ℝ) 6 (↑n : ℝ)

Tactic:
rify at hn