awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : CommRing α
s : Finset α
inst_2 : Fact (IsUnit.{u_1} (M := α) 2)
hs : ThreeAPFree (↑s : Set α)
inst_3 : DecidableEq α
this : NoAccidental (triangleIndices s)
rw : 3 * #((graph (triangleIndices s)).cliqueFinset 3) = 3 * Fintype.card α * #s
rw₁ : 3 * #(triangleIndices s) = 3 * Fintype.card α * #s
rw₂ : 3 * (Fintype.card α * #s) = 3 * Fintype.card α * #s
⊢ #(graph (triangleIndices s)).edgeFinset = 3 * Fintype.card α * #s
have rw₃ : 3 * (Fintype.card α * #s) = 3 * (Fintype.card α * #s)
Tactic: rw [(locallyLinear hs).card_edgeFinset, card_triangles, card_triangleIndices, mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : CommRing α
inst_3 : Fact (IsUnit.{u_1} (M := α) 2)
⊢ HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ) ≤
    ruzsaSzemerediNumber.{u_1} (α ⊕ α ⊕ α)
have obtain : ∀ (s : Finset α) (hscard : #s = (addRothNumber : (a : Finset α) → ℕ) univ) (hs : ThreeAPFree (↑s : Set α)),
  HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ) ≤
    ruzsaSzemerediNumber.{u_1} (α ⊕ α ⊕ α)
Tactic: obtain ⟨s, -, hscard, hs⟩ := addRothNumber_spec (univ : Finset α)
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : CommRing α
inst_3 : Fact (IsUnit.{u_1} (M := α) 2)
s : Finset α
hscard : #s = (addRothNumber : (a : Finset α) → ℕ) univ
hs : ThreeAPFree (↑s : Set α)
⊢ HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ) ≤
    ruzsaSzemerediNumber.{u_1} (α ⊕ α ⊕ α)
have this : NoAccidental (triangleIndices s)
Tactic: haveI := noAccidental hs
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : CommRing α
inst_3 : Fact (IsUnit.{u_1} (M := α) 2)
s : Finset α
hscard : #s = (addRothNumber : (a : Finset α) → ℕ) univ
hs : ThreeAPFree (↑s : Set α)
this : NoAccidental (triangleIndices s)
⊢ HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ) ≤
    ruzsaSzemerediNumber.{u_1} (α ⊕ α ⊕ α)
have rw : #((graph (triangleIndices s)).cliqueFinset 3) ≤ ruzsaSzemerediNumber.{u_1} (α ⊕ α ⊕ α)
Tactic: rw [← hscard, ← card_triangleIndices, ← card_triangles]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (hypothesis)
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
⊢ HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) ≤ ruzsaSzemerediNumberNat (6 * n + 3)
have this : Coprime 2 (2 * n + 1)
Tactic: have : Nat.Coprime 2 (2 * n + 1) := by simp
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (hypothesis)
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this : Coprime 2 (2 * n + 1)
⊢ HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) ≤ ruzsaSzemerediNumberNat (6 * n + 3)
have this₁ : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
Tactic: haveI : Fact (IsUnit (2 : Fin (2 * n + 1))) := ⟨by simpa using (ZMod.unitOfCoprime 2 this).isUnit⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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 (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
    HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ)
have rw : HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
  HMul.hMul (β := ℕ) (Fintype.card α) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ)
Tactic: rw [Fin.addRothNumber_eq_rothNumberNat le_rfl, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this_1 : Coprime 2 (2 * n + 1)
this : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
rw :
  HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
    HMul.hMul (β := ℕ) (Fintype.card α) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ)
⊢ HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
    HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ)
have rw₁ : HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
  HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ)
Tactic: rw [Fin.addRothNumber_eq_rothNumberNat le_rfl, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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 α) → ℕ) (Iio (↑n : α)) : ℕ) ≤
    HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ)
have bc : LE.le (α := Finset α) (Iio (↑n : α)) univ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
α : Type := Fin (2 * n + 1)
this_1 : Coprime 2 (2 * n + 1)
this : Fact (IsUnit (M := Fin (2 * n + 1)) 2)
⊢ ruzsaSzemerediNumber (α ⊕ α ⊕ α) = ruzsaSzemerediNumberNat (6 * n + 3)
have simp_rw : ruzsaSzemerediNumberNat (2 * n + 1 + (2 * n + 1 + (2 * n + 1))) = ruzsaSzemerediNumberNat (6 * n + 3)
Tactic: simp_rw [← ruzsaSzemerediNumberNat_card, Fintype.card_sum, α, Fintype.card_fin]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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 (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) ≤ ruzsaSzemerediNumberNat (6 * n + 3)
have n₁ : HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
  HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ)
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
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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 : α)) : ℕ)
⊢ HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) ≤ ruzsaSzemerediNumberNat (6 * n + 3)
have n₂ : HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ) ≤
  HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ)
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
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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 : ℕ)
⊢ HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) ≤ ruzsaSzemerediNumberNat (6 * n + 3)
have n₃ : ruzsaSzemerediNumber (α ⊕ α ⊕ α) = 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
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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 (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) ≤ ruzsaSzemerediNumberNat (6 * n + 3)
have open : HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) =
  HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ)
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
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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 : α)) : ℕ)
⊢ HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) ≤ ruzsaSzemerediNumberNat (6 * n + 3)
have open₁ : HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) (Iio (↑n : α)) : ℕ) ≤
  HMul.hMul (β := ℕ) (Fintype.card α) ((addRothNumber : (a : Finset α) → ℕ) univ : ℕ)
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
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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 : ℕ)
⊢ HMul.hMul (β := ℕ) (2 * n + 1) ((rothNumberNat : (a : ℕ) → ℕ) n : ℕ) ≤ ruzsaSzemerediNumberNat (6 * n + 3)
have open₂ : ruzsaSzemerediNumber (α ⊕ α ⊕ α) = 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
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
⊢ LE.le (α := ℝ) (↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3)) : ℝ) (↑(ruzsaSzemerediNumberNat (n + 3)) : ℝ)
have grw : LE.le (α := ℝ) (↑(ruzsaSzemerediNumberNat (n + 3)) : ℝ) (↑(ruzsaSzemerediNumberNat (n + 3)) : ℝ)
Tactic: grw [Nat.mul_div_le]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
⊢ (HDiv.hDiv (α := ℝ) (↑(n + 3) : ℝ) 3 - 2) * (↑((rothNumberNat : (a : ℕ) → ℕ) ((n + 3 - 3) / 6)) : ℝ) ≤
    (↑(ruzsaSzemerediNumberNat (n + 3)) : ℝ)
have calc_1 : HDiv.hDiv (α := ℝ) (↑(n + 3) : ℝ) 3 - 2 ≤ (↑(2 * (n / 6) + 1) : ℝ)
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
calc_1 : HDiv.hDiv (α := ℝ) (↑(n + 3) : ℝ) 3 - 2 ≤ (↑(2 * (n / 6) + 1) : ℝ)
⊢ (HDiv.hDiv (α := ℝ) (↑(n + 3) : ℝ) 3 - 2) * (↑((rothNumberNat : (a : ℕ) → ℕ) ((n + 3 - 3) / 6)) : ℝ) ≤
    (↑(ruzsaSzemerediNumberNat (n + 3)) : ℝ)
have calc_2 : HMul.hMul (α := ℝ) (↑(2 * (n / 6) + 1) : ℝ) (↑((rothNumberNat : (a : ℕ) → ℕ) (n / 6)) : ℝ) ≤
  (↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑(n + 3) : ℝ) 3 - 2 ≤ (↑(2 * (n / 6) + 1) : ℝ)
have calc_1 : HAdd.hAdd (α := ℝ) (↑n : ℝ) 3 / 3 ≤ HMul.hMul (α := ℝ) 2 (↑(n / 6) : ℝ) + 1 + 2
Tactic: simp only [cast_add, cast_ofNat, cast_mul, cast_one, tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 3 / 3 ≤ HMul.hMul (α := ℝ) 2 (↑(n / 6) : ℝ) + 1 + 2
have calc_1 : (↑n : ℝ) ≤ HMul.hMul (α := ℝ) 2 3 * (↑(n / 6) : ℝ) + HMul.hMul (α := ℝ) 2 3
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
⊢ (↑n : ℝ) ≤ HMul.hMul (α := ℝ) 2 3 * (↑(n / 6) : ℝ) + HMul.hMul (α := ℝ) 2 3
have calc_1 : n ≤ HMul.hMul (α := ℕ) 2 3 * (n / 6) + HMul.hMul (α := ℕ) 2 3
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
⊢ HMul.hMul (α := ℝ) (↑(2 * (n / 6) + 1) : ℝ) (↑((rothNumberNat : (a : ℕ) → ℕ) (n / 6)) : ℝ) ≤
    (↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3)) : ℝ)
have calc_2 : HMul.hMul (β := ℕ) (2 * (n / 6) + 1) ((rothNumberNat : (a : ℕ) → ℕ) (n / 6) : ℕ) ≤
  ruzsaSzemerediNumberNat (6 * (n / 6) + 3)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
⊢ (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * (↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ))) ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)
have rw : (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * ((↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))) ≤
  (↑(ruzsaSzemerediNumberNat n) : ℝ)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
n : ℕ
⊢ (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * ((↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))) ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)
have 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) : ℝ)
Tactic: obtain hn | hn := le_total (n / 3 - 2 : ℝ) 0
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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) : ℝ)
⊢ (HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2) * ((↑((n - 3) / 6) : ℝ) * rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))) ≤
    (↑(ruzsaSzemerediNumberNat n) : ℝ)
have 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) : ℝ)
Tactic: obtain hn | hn := le_total (n / 3 - 2 : ℝ) 0
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * rexp (-4 * √(Real.log (↑n : ℝ)))) fun (n : ℕ) ↦
    (↑(ruzsaSzemerediNumberNat n) : ℝ)
have 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) : ℝ)))
Tactic: trans fun n ↦ (n / 3 - 2) * ↑((n - 3) / 6) * exp (-4 * √(log ↑((n - 3) / 6)))
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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) : ℝ)))
⊢ IsBigO (E := ℝ) (F := ℝ) atTop
    (fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (β := ℕ) (↑n : ℝ) 2 * rexp (-4 * √(Real.log (↑n : ℝ)))) fun (n : ℕ) ↦
    (↑(ruzsaSzemerediNumberNat n) : ℝ)
have 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) : ℝ)
Tactic: trans fun n ↦ (n / 3 - 2) * ↑((n - 3) / 6) * exp (-4 * √(log ↑((n - 3) / 6)))
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ 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) : ℝ)))
have 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) : ℝ)))
Tactic: simp_rw [sq]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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) : ℝ)))
have refine_1 : IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
Tactic: refine (IsBigO.mul ?_ ?_).mul ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
refine_1 : IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
⊢ 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) : ℝ)))
have refine_2 : IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)
Tactic: refine (IsBigO.mul ?_ ?_).mul ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
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) : ℝ)
⊢ 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) : ℝ)))
have refine_3 : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ rexp (-4 * √(Real.log (↑n : ℝ)))) fun (n : ℕ) ↦
  rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))
Tactic: refine (IsBigO.mul ?_ ?_).mul ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
have trans : IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3
Tactic: trans fun n ↦ n / 3
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
trans : IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3
⊢ IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
have trans₁ : IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3) fun (n : ℕ) ↦
  HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
Tactic: trans fun n ↦ n / 3
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3
have simp_rw : IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ HMul.hMul (α := ℝ) 3⁻¹ (↑n : ℝ)
Tactic: simp_rw [div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3) fun (n : ℕ) ↦
    HDiv.hDiv (α := ℝ) (↑n : ℝ) 3 - 2
have refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ 2) fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑n : ℝ) 3
Tactic: refine IsLittleO.right_isBigO_sub ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)
have refine_2 : ∃ (c : ℝ), IsBigOWith (E := ℝ) (F := ℝ) c atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)
Tactic: rw [IsBigO_def]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ ∃ (c : ℝ), IsBigOWith (E := ℝ) (F := ℝ) c atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)
have refine_2 : IsBigOWith (E := ℝ) (F := ℝ) 12 atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)
Tactic: refine ⟨12, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ IsBigOWith (E := ℝ) (F := ℝ) 12 atTop Nat.cast fun (n : ℕ) ↦ (↑((n - 3) / 6) : ℝ)
have refine_2 : ∃ (a : ℕ), ∀ b ≥ a, (↑b : ℝ) ≤ HMul.hMul (α := ℝ) 12 (↑((b - 3) / 6) : ℝ)
Tactic: simp only [IsBigOWith, norm_natCast, eventually_atTop]
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
x : ℕ
hx : x ≥ 15
⊢ (↑x : ℝ) ≤ HMul.hMul (α := ℝ) 12 (↑((x - 3) / 6) : ℝ)
have norm_cast : x ≤ 12 * ((x - 3) / 6)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Combinatorics.Extremal.RuzsaSzemeredi (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ rexp (-4 * √(Real.log (↑n : ℝ)))) fun (n : ℕ) ↦
    rexp (-4 * √(Real.log (↑((n - 3) / 6) : ℝ)))
have 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) : ℝ)))
Tactic: rw [isBigO_exp_comp_exp_comp]