awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
hx : Irrational x
a b : ℤ
p_nonzero :
  HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
      ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) ≠
    0
x_is_root :
  Eq (α := ℝ)
    ((aeval x : (a : ℤ[X]) → ℝ)
        (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
          ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
      ℝ)
    (0 : ℝ)
this : x * (↑a : ℝ) = -(↑b : ℝ)
ha : ¬a = 0
inr inr₁ inr₂ inr₃ :
  ∀
    (p_nonzero :
      ¬HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
            ((C : (a : ℤ) → ℤ[X]) b : ℤ[X]) =
          0)
    (x_is_root :
      Eq (α := ℝ)
        ((aeval x : (a : ℤ[X]) → ℝ)
            (HAdd.hAdd (β := ℤ[X]) (HMul.hMul (α := ℤ[X]) (β := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) a : ℤ[X]) X)
              ((C : (a : ℤ) → ℤ[X]) b : ℤ[X])) :
          ℝ)
        (0 : ℝ))
    (this : x * (↑a : ℝ) = (↑(-b) : ℝ)) (ha : ¬a = 0), ¬a = 0
⊢ Ne (α := ℝ) (↑a : ℝ) 0

Tactic:
assumption_mod_cast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
⊢ Irrational ((↑q : ℝ) + x) ↔ Irrational x

Tactic:
⟨of_ratCast_add q, ratCast_add q⟩

Premises used: Irrational.ratCast_add, Iff.intro, Irrational.of_ratCast_add
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
x : ℝ
⊢ Irrational ((↑m : ℝ) + x) ↔ Irrational x

Tactic:
⟨of_intCast_add m, fun h => h.intCast_add m⟩

Premises used: Irrational.intCast_add, Iff.intro, Irrational.of_intCast_add
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
x : ℝ
⊢ Irrational ((↑n : ℝ) + x) ↔ Irrational x

Tactic:
⟨of_natCast_add n, fun h => h.natCast_add n⟩

Premises used: Irrational.of_natCast_add, Irrational.natCast_add, Iff.intro
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
⊢ Irrational (x + (↑q : ℝ)) ↔ Irrational x

Tactic:
⟨of_add_ratCast q, add_ratCast q⟩

Premises used: Irrational.add_ratCast, Iff.intro, Irrational.of_add_ratCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
x : ℝ
⊢ Irrational (x + (↑m : ℝ)) ↔ Irrational x

Tactic:
⟨of_add_intCast m, fun h => h.add_intCast m⟩

Premises used: Irrational.of_add_intCast, Iff.intro, Irrational.add_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
x : ℝ
⊢ Irrational (x + (↑n : ℝ)) ↔ Irrational x

Tactic:
⟨of_add_natCast n, fun h => h.add_natCast n⟩

Premises used: Irrational.add_natCast, Iff.intro, Irrational.of_add_natCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
⊢ Irrational ((↑q : ℝ) - x) ↔ Irrational x

Tactic:
⟨of_ratCast_sub q, ratCast_sub q⟩

Premises used: Irrational.ratCast_sub, Irrational.of_ratCast_sub, Iff.intro
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
x : ℝ
⊢ Irrational ((↑m : ℝ) - x) ↔ Irrational x

Tactic:
⟨of_intCast_sub m, fun h => h.intCast_sub m⟩

Premises used: Irrational.of_intCast_sub, Irrational.intCast_sub, Iff.intro
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
x : ℝ
⊢ Irrational ((↑n : ℝ) - x) ↔ Irrational x

Tactic:
⟨of_natCast_sub n, fun h => h.natCast_sub n⟩

Premises used: Irrational.of_natCast_sub, Irrational.natCast_sub, Iff.intro
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
⊢ Irrational (x - (↑q : ℝ)) ↔ Irrational x

Tactic:
⟨of_sub_ratCast q, sub_ratCast q⟩

Premises used: Irrational.of_sub_ratCast, Irrational.sub_ratCast, Iff.intro
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
x : ℝ
⊢ Irrational (x - (↑m : ℝ)) ↔ Irrational x

Tactic:
⟨of_sub_intCast m, fun h => h.sub_intCast m⟩

Premises used: Irrational.sub_intCast, Iff.intro, Irrational.of_sub_intCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
x : ℝ
⊢ Irrational (x - (↑n : ℝ)) ↔ Irrational x

Tactic:
⟨of_sub_natCast n, fun h => h.sub_natCast n⟩

Premises used: Irrational.sub_natCast, Iff.intro, Irrational.of_sub_natCast
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
⊢ Irrational (-x) ↔ Irrational x

Tactic:
⟨of_neg, Irrational.neg⟩

Premises used: Irrational.neg, Irrational.of_neg, Iff.intro
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x : ℝ
⊢ Irrational x⁻¹ ↔ Irrational x

Tactic:
⟨of_inv, Irrational.inv⟩

Premises used: Irrational.inv, Iff.intro, Irrational.of_inv
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
⊢ Irrational ((↑q : ℝ) * x) ↔ q ≠ 0 ∧ Irrational x

Tactic:
⟨fun h => ⟨Rat.cast_ne_zero.1 <| left_ne_zero_of_mul h.ne_zero, h.of_ratCast_mul q⟩, fun h =>
    h.2.ratCast_mul h.1⟩

Premises used: Irrational.ratCast_mul, Irrational.of_ratCast_mul, Irrational.ne_zero, Rat.cast_ne_zero, And.right, And.left, And.intro, Iff.intro, left_ne_zero_of_mul, Iff.mp
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
rw : Irrational ((↑q : ℝ) * x) ↔ q ≠ 0 ∧ Irrational x
rw₁ rw₂ : q ≠ 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
⊢ Irrational (x * (↑q : ℝ)) ↔ q ≠ 0 ∧ Irrational x

Tactic:
rw [mul_comm, irrational_ratCast_mul_iff]

Premises used: irrational_ratCast_mul_iff, mul_comm
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
x : ℝ
rw : Irrational ((↑(↑m : ℚ) : ℝ) * x) ↔ m ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑m : ℚ) 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
rw₂ rw₃ : m ≠ 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
⊢ Irrational ((↑m : ℝ) * x) ↔ m ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_intCast, irrational_ratCast_mul_iff, Int.cast_ne_zero]

Premises used: Rat.cast_intCast, irrational_ratCast_mul_iff, Int.cast_ne_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
x : ℝ
rw : Irrational (x * (↑(↑m : ℚ) : ℝ)) ↔ m ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑m : ℚ) 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
rw₂ rw₃ : m ≠ 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
⊢ Irrational (x * (↑m : ℝ)) ↔ m ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_intCast, irrational_mul_ratCast_iff, Int.cast_ne_zero]

Premises used: Rat.cast_intCast, irrational_mul_ratCast_iff, Int.cast_ne_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
x : ℝ
rw : Irrational ((↑(↑n : ℚ) : ℝ) * x) ↔ n ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑n : ℚ) 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
rw₂ rw₃ : n ≠ 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
⊢ Irrational ((↑n : ℝ) * x) ↔ n ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_natCast, irrational_ratCast_mul_iff, Nat.cast_ne_zero]

Premises used: irrational_ratCast_mul_iff, Rat.cast_natCast, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
x : ℝ
rw : Irrational (x * (↑(↑n : ℚ) : ℝ)) ↔ n ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑n : ℚ) 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
rw₂ rw₃ : n ≠ 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
⊢ Irrational (x * (↑n : ℝ)) ↔ n ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_natCast, irrational_mul_ratCast_iff, Nat.cast_ne_zero]

Premises used: irrational_mul_ratCast_iff, Rat.cast_natCast, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
⊢ Irrational ((↑q : ℝ) / x) ↔ q ≠ 0 ∧ Irrational x

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
q : ℚ
x : ℝ
rw : Irrational (x * (↑q : ℝ)⁻¹) ↔ q ≠ 0 ∧ Irrational x
rw₁ : Irrational (x * (↑q⁻¹ : ℝ)) ↔ q ≠ 0 ∧ Irrational x
rw₂ : q⁻¹ ≠ 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
rw₃ : ¬q⁻¹ = 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
rw₄ rw₅ : ¬q = 0 ∧ Irrational x ↔ q ≠ 0 ∧ Irrational x
⊢ Irrational (x / (↑q : ℝ)) ↔ q ≠ 0 ∧ Irrational x

Tactic:
rw [div_eq_mul_inv, ← cast_inv, irrational_mul_ratCast_iff, Ne, inv_eq_zero]

Premises used: inv_eq_zero, irrational_mul_ratCast_iff, Ne, div_eq_mul_inv, Rat.cast_inv
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
x : ℝ
⊢ Irrational ((↑m : ℝ) / x) ↔ m ≠ 0 ∧ Irrational x

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
m : ℤ
x : ℝ
rw : Irrational (x / (↑(↑m : ℚ) : ℝ)) ↔ m ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑m : ℚ) 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
rw₂ rw₃ : m ≠ 0 ∧ Irrational x ↔ m ≠ 0 ∧ Irrational x
⊢ Irrational (x / (↑m : ℝ)) ↔ m ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_intCast, irrational_div_ratCast_iff, Int.cast_ne_zero]

Premises used: Rat.cast_intCast, irrational_div_ratCast_iff, Int.cast_ne_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
x : ℝ
⊢ Irrational ((↑n : ℝ) / x) ↔ n ≠ 0 ∧ Irrational x

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
n : ℕ
x : ℝ
rw : Irrational (x / (↑(↑n : ℚ) : ℝ)) ↔ n ≠ 0 ∧ Irrational x
rw₁ : Ne (α := ℚ) (↑n : ℚ) 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
rw₂ rw₃ : n ≠ 0 ∧ Irrational x ↔ n ≠ 0 ∧ Irrational x
⊢ Irrational (x / (↑n : ℝ)) ↔ n ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_natCast, irrational_div_ratCast_iff, Nat.cast_ne_zero]

Premises used: irrational_div_ratCast_iff, Rat.cast_natCast, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.Real.Irrational
Goal:
x y : ℝ
h : x < y
⊢ ∃ (r : ℝ), Irrational r ∧ x < r ∧ r < y

Tactic:
let ⟨q, ⟨hq1, hq2⟩⟩ := exists_rat_btwn ((sub_lt_sub_iff_right (√2)).mpr h)
  ⟨q + √2, irrational_sqrt_two.ratCast_add _, sub_lt_iff_lt_add.mp hq1, lt_sub_iff_add_lt.mp hq2⟩

Premises used: Iff.mpr, Exists, Rat.cast, sub_lt_sub_iff_right, exists_rat_btwn, _private.0.exists_irrational_btwn.match_1, Irrational.ratCast_add, And, Irrational, HAdd.hAdd, And.intro, LT.lt, Exists.intro, Iff.mp, sub_lt_iff_lt_add, Real.sqrt, lt_sub_iff_add_lt, OfNat.ofNat, irrational_sqrt_two
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : SelbergSieve
⊢ 1 ≤ s.level

Tactic:
s.one_le_level

Premises used: SelbergSieve.one_le_level
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
⊢ s.prodPrimes ≠ 0

Tactic:
Squarefree.ne_zero s.prodPrimes_squarefree

Premises used: BoundingSieve.prodPrimes_squarefree, Squarefree.ne_zero
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ Squarefree d

Tactic:
Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree

Premises used: BoundingSieve.prodPrimes_squarefree, Squarefree.squarefree_of_dvd
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∈ s.prodPrimes.divisors
⊢ d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0

Tactic:
simp only [Nat.mem_divisors] at hd

Premises used: Nat.mem_divisors
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0
⊢ Squarefree d

Tactic:
Squarefree.squarefree_of_dvd hd.left s.prodPrimes_squarefree

Premises used: BoundingSieve.prodPrimes_squarefree, Squarefree.squarefree_of_dvd, And.left
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes ∧ s.prodPrimes ≠ 0
⊢ Squarefree d

Tactic:
exact Squarefree.squarefree_of_dvd hd.left s.prodPrimes_squarefree

Premises used: BoundingSieve.prodPrimes_squarefree, Squarefree.squarefree_of_dvd, And.left
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
rw : Eq (α := ℝ) ((s.nu : (a : ℕ) → ℝ) (∏ a ∈ d.primeFactors, a) : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)
rw₁ rw₂ : Eq (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)
⊢ Eq (α := ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)

Tactic:
rw [← s.nu_mult.map_prod_of_subset_primeFactors _ _ subset_rfl,
    Nat.prod_primeFactors_of_squarefree <| Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree]

Premises used: ArithmeticFunction.IsMultiplicative.map_prod_of_subset_primeFactors, Nat.prod_primeFactors_of_squarefree, BoundingSieve.prodPrimes_squarefree, Squarefree.squarefree_of_dvd, BoundingSieve.nu_mult, subset_rfl
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
h0 : ∀ i ∈ d.primeFactors, LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) i : ℝ)
⊢ LT.lt (α := ℝ) 0 (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p)

Tactic:
apply prod_pos

Premises used: Finset.prod_pos
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
p : ℕ
hpd : p ∈ d.primeFactors
⊢ Nat.Prime p

Tactic:
have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : Nat.Prime p
⊢ p ∣ s.prodPrimes

Tactic:
have hp_dvd : p ∣ s.prodPrimes := (dvd_of_mem_primeFactors hpd).trans hd
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : Nat.Prime p
hp_dvd : p ∣ s.prodPrimes
⊢ LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) p : ℝ)

Tactic:
s.nu_pos_of_prime p hp_prime hp_dvd

Premises used: BoundingSieve.nu_pos_of_prime
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : Nat.Prime p
hp_dvd : p ∣ s.prodPrimes
⊢ LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) p : ℝ)

Tactic:
exact s.nu_pos_of_prime p hp_prime hp_dvd

Premises used: BoundingSieve.nu_pos_of_prime
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ Eq (α := ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)

Tactic:
prod_primeFactors_nu hd

Premises used: BoundingSieve.prod_primeFactors_nu
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
p : LT.lt (α := ℝ) 0 (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)

Tactic:
calc
    0 < ∏ p ∈ d.primeFactors, s.nu p := by
      apply prod_pos
      intro p hpd
      have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
      have hp_dvd : p ∣ s.prodPrimes := (dvd_of_mem_primeFactors hpd).trans hd
      exact s.nu_pos_of_prime p hp_prime hp_dvd
    _ = s.nu d := prod_primeFactors_nu hd

Premises used: Nat.primeFactors, DFunLike.coe, BoundingSieve.nu, BoundingSieve.prod_primeFactors_nu
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
h : LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)
⊢ Ne (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) (0 : ℝ)

Tactic:
apply _root_.ne_of_gt

Premises used: ne_of_gt
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)

Tactic:
nu_pos_of_dvd_prodPrimes hd

Premises used: BoundingSieve.nu_pos_of_dvd_prodPrimes
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ)

Tactic:
exact nu_pos_of_dvd_prodPrimes hd

Premises used: BoundingSieve.nu_pos_of_dvd_prodPrimes
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
⊢ Squarefree d

Tactic:
have hd_sq : Squarefree d := Squarefree.squarefree_of_dvd hdP s.prodPrimes_squarefree
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ d ≠ 0

Tactic:
have := hd_sq.ne_zero
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ Eq (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p : ℝ)

Tactic:
(prod_primeFactors_nu hdP).symm

Premises used: Eq.symm, BoundingSieve.prod_primeFactors_nu
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
hf : ∀ i ∈ d.primeFactors, LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) i : ℝ)
hfg : ∀ i ∈ d.primeFactors, LT.lt (α := ℝ) ((s.nu : (a : ℕ) → ℝ) i : ℝ) (1 : ℝ)
h_ne : d.primeFactors.Nonempty
⊢ LT.lt (α := ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p) (∏ p ∈ d.primeFactors, 1)

Tactic:
apply prod_lt_prod_of_nonempty

Premises used: Finset.prod_lt_prod_of_nonempty
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
hp : p ∈ d.primeFactors
⊢ Nat.Prime p ∧ p ∣ d ∧ d ≠ 0

Tactic:
simp only [mem_primeFactors] at hp

Premises used: Nat.mem_primeFactors
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
hp : Nat.Prime p ∧ p ∣ d ∧ d ≠ 0
⊢ LT.lt (α := ℝ) (0 : ℝ) ((s.nu : (a : ℕ) → ℝ) p : ℝ)

Tactic:
apply s.nu_pos_of_prime p hp.1 (hp.2.1.trans hdP)

Premises used: And.right, And.left, BoundingSieve.nu_pos_of_prime, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
hpd : p ∈ d.primeFactors
⊢ Nat.Prime p ∧ p ∣ d

Tactic:
rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd

Premises used: Nat.mem_primeFactors_of_ne_zero, Squarefree.ne_zero
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
hpd : Nat.Prime p ∧ p ∣ d
⊢ LT.lt (α := ℝ) ((s.nu : (a : ℕ) → ℝ) p : ℝ) (1 : ℝ)

Tactic:
apply s.nu_lt_one_of_prime p hpd.left (hpd.2.trans hdP)

Premises used: BoundingSieve.nu_lt_one_of_prime, And.right, And.left, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ 1 < d

Tactic:
lia
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ d.primeFactors.Nonempty

Tactic:
simp only [nonempty_primeFactors, show 1 < d by lia]

Premises used: Nat.nonempty_primeFactors
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ Eq (α := ℝ) (∏ p ∈ d.primeFactors, 1) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
d₁ : LT.lt (α := ℝ) (∏ p ∈ d.primeFactors, (s.nu : (a : ℕ) → ℝ) p) (∏ p ∈ d.primeFactors, 1)
d₂ : Eq (α := ℝ) (∏ p ∈ d.primeFactors, 1) 1
⊢ LT.lt (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) (1 : ℝ)

Tactic:
calc
    s.nu d = ∏ p ∈ d.primeFactors, s.nu p := (prod_primeFactors_nu hdP).symm
    _ < ∏ p ∈ d.primeFactors, 1 := by
      apply prod_lt_prod_of_nonempty
      · intro p hp
        simp only [mem_primeFactors] at hp
        apply s.nu_pos_of_prime p hp.1 (hp.2.1.trans hdP)
      · intro p hpd; rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd
        apply s.nu_lt_one_of_prime p hpd.left (hpd.2.trans hdP)
      · simp only [nonempty_primeFactors, show 1 < d by lia]
    _ = 1 := by
      simp

Premises used: Nat.primeFactors, Eq.symm, DFunLike.coe, BoundingSieve.nu, BoundingSieve.prod_primeFactors_nu
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
d : ℕ
⊢ (∑ n ∈ s.support, if d ∣ n then s.weights n else 0) =
    HMul.hMul (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) s.totalMass +
      ((∑ n ∈ s.support, if d ∣ n then s.weights n else 0) -
        HMul.hMul (α := ℝ) ((s.nu : (a : ℕ) → ℝ) d : ℝ) s.totalMass)

Tactic:
ring
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
simp_rw :
  Eq (α := ℝ) (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0)
    (∑ x ∈ s.support, if s.prodPrimes.gcd x = 1 then s.weights x * 1 else s.weights x * 0)
simp_rw₁ :
  Eq (α := ℝ) (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0)
    (∑ x ∈ s.support, if s.prodPrimes.gcd x = 1 then s.weights x else s.weights x * 0)
⊢ Eq (α := ℝ) (∑ d ∈ s.support, if s.prodPrimes.Coprime d then s.weights d else 0)
    (∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0)

Tactic:
simp_rw [mul_ite, mul_one, mul_zero]

Premises used: mul_ite, MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)

Tactic:
have hμ : ∀ n, (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d := h
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ siftedSum (s := s) ≤ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d

Tactic:
?caseA
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ Eq (α := ℝ) (∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
    (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)

Tactic:
?caseB
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
⊢ Eq (α := ℝ) (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)

Tactic:
?caseC
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
calc : siftedSum (s := s) ≤ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d
calc₁ :
  Eq (α := ℝ) (∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
    (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)
calc₂ :
  Eq (α := ℝ) (∑ n ∈ s.support, ∑ d ∈ s.prodPrimes.divisors, if d ∣ n then s.weights n * muPlus d else 0)
    (∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d)
⊢ siftedSum (s := s) ≤ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum (s := s) d

Tactic:
calc siftedSum ≤
    ∑ n ∈ s.support, s.weights n * ∑ d ∈ (Nat.gcd s.prodPrimes n).divisors, muPlus d := ?caseA
    _ = ∑ n ∈ s.support, ∑ d ∈ divisors s.prodPrimes,
        if d ∣ n then s.weights n * muPlus d else 0 := ?caseB
    _ = ∑ d ∈ divisors s.prodPrimes, muPlus d * multSum d := ?caseC

Premises used: BoundingSieve.siftedSum, BoundingSieve.support, BoundingSieve.prodPrimes, Nat.divisors
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
rw :
  LE.le (α := ℝ) (∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0)
    (∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
⊢ siftedSum (s := s) ≤ ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d

Tactic:
rw [siftedSum_eq_sum_support_mul_ite]

Premises used: BoundingSieve.siftedSum_eq_sum_support_mul_ite
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
h₁ :
  ∀ n ∈ s.support,
    LE.le (α := ℝ) (if s.prodPrimes.gcd n = 1 then 1 else 0) (∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)
⊢ LE.le (α := ℝ) (∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0)
    (∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)

Tactic:
gcongr with n
-- Module: Mathlib.NumberTheory.SelbergSieve
Goal:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), LE.le (α := ℝ) (if n = 1 then 1 else 0) (∑ d ∈ n.divisors, muPlus d)
n : ℕ
h_1 : n ∈ s.support
⊢ LE.le (α := ℝ) (if s.prodPrimes.gcd n = 1 then 1 else 0) (∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d)

Tactic:
hμ (Nat.gcd s.prodPrimes n)

Premises used: Nat.gcd, BoundingSieve.prodPrimes