Theorem: Aux.sum_pow_cardDistinctFactors_div_self_le_log_pow (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) ≤ (1 + x.log) ^ k
Tactic:
have hx_pos : 0 < x := by
  linarith
State after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) ≤ (1 + x.log) ^ k

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) ≤ (1 + x.log) ^ k
Tactic:
calc
  _ = ∑ d in P.divisors,
        ∑ a in Fintype.piFinset fun _i : Fin k => P.divisors,
          if ∏ i, a i = d ∧ d ∣ P then if ↑d ≤ x then (d : ℝ)⁻¹ else 0 else 0 := ?_
  _ = ∑ a in Fintype.piFinset fun _i : Fin k => P.divisors,
        if ∏ i, a i ∣ P then if ↑(∏ i, a i) ≤ x then ∏ i, (a i : ℝ)⁻¹ else 0 else 0 := ?_
  _ ≤ ∑ a in Fintype.piFinset fun _i : Fin k => P.divisors,
        if ↑(∏ i, a i) ≤ x then ∏ i, (a i : ℝ)⁻¹ else 0 := ?_ _ ≤ ∑ a in Fintype.piFinset fun _i : Fin k => P.divisors,
        ∏ i, if ↑(a i) ≤ x then (a i : ℝ)⁻¹ else 0 := ?_
  _ = ∏ _i : Fin k, ∑ d in P.divisors, if ↑d ≤ x then (d : ℝ)⁻¹ else 0 := by rw [prod_univ_sum]
  _ = (∑ d in P.divisors, if ↑d ≤ x then (d : ℝ)⁻¹ else 0) ^ k := by rw [prod_const, card_fin]
  _ ≤ (1 + Real.log x) ^ k := ?_
State after:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) =
    ∑ d ∈ P.divisors,
      ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
        if ∏ i : Fin k, a i = d ∧ d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0

case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ d ∈ P.divisors,
      ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
        if ∏ i : Fin k, a i = d ∧ d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0) =
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0

case calc_3
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors, if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0

case calc_4
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ Fintype.piFinset fun _i => P.divisors, if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0) ≤
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors, ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0

case calc_5
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then (↑d)⁻¹ else 0) ^ k ≤ (1 + x.log) ^ k

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
⊢ 0 < x
Tactic:
linarith
State after:
no goals

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ Fintype.piFinset fun _i => P.divisors, ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0) =
    ∏ _i : Fin k, ∑ d ∈ P.divisors, if ↑d ≤ x then (↑d)⁻¹ else 0
Tactic:
rw [prod_univ_sum]
State after:
no goals

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∏ _i : Fin k, ∑ d ∈ P.divisors, if ↑d ≤ x then (↑d)⁻¹ else 0) = (∑ d ∈ P.divisors, if ↑d ≤ x then (↑d)⁻¹ else 0) ^ k
Tactic:
rw [prod_const, card_fin]
State after:
no goals

State before:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) =
    ∑ d ∈ P.divisors,
      ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
        if ∏ i : Fin k, a i = d ∧ d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0
Tactic:
apply sum_congr rfl
State after:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ x_1 ∈ P.divisors,
    (if ↑x_1 ≤ x then ↑k ^ ω x_1 / ↑x_1 else 0) =
      ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
        if ∏ i : Fin k, a i = x_1 ∧ x_1 ∣ P then if ↑x_1 ≤ x then (↑x_1)⁻¹ else 0 else 0

State before:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ x_1 ∈ P.divisors,
    (if ↑x_1 ≤ x then ↑k ^ ω x_1 / ↑x_1 else 0) =
      ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
        if ∏ i : Fin k, a i = x_1 ∧ x_1 ∣ P then if ↑x_1 ≤ x then (↑x_1)⁻¹ else 0 else 0
Tactic:
intro d hd
State after:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors
⊢ (if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) =
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i = d ∧ d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0

State before:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors
⊢ (if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) =
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i = d ∧ d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0
Tactic:
rw [mem_divisors] at hd
State after:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ (if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) =
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i = d ∧ d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0

State before:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ (if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) =
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i = d ∧ d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0
Tactic:
simp_rw [ite_and]
State after:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ (if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) =
    ∑ x_1 ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, x_1 i = d then if d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0 else 0

State before:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ (if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) =
    ∑ x_1 ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, x_1 i = d then if d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0 else 0
Tactic:
rw [←sum_filter, Finset.sum_const, ←finMulAntidiagonal_univ_eq hd.1 hd.2, card_finMulAntidiagonal
  <| hP.squarefree_of_dvd hd.1, if_pos hd.1]
State after:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ (if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) = k ^ ω d • if ↑d ≤ x then (↑d)⁻¹ else 0

State before:
case calc_1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ (if ↑d ≤ x then ↑k ^ ω d / ↑d else 0) = k ^ ω d • if ↑d ≤ x then (↑d)⁻¹ else 0
Tactic:
simp only [div_eq_mul_inv, one_mul, nsmul_eq_mul, cast_pow, mul_ite, mul_zero]
State after:
no goals

State before:
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ d ∈ P.divisors,
      ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
        if ∏ i : Fin k, a i = d ∧ d ∣ P then if ↑d ≤ x then (↑d)⁻¹ else 0 else 0) =
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0
Tactic:
rw [sum_comm]
State after:
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ y ∈ Fintype.piFinset fun _i => P.divisors,
      ∑ x_1 ∈ P.divisors, if ∏ i : Fin k, y i = x_1 ∧ x_1 ∣ P then if ↑x_1 ≤ x then (↑x_1)⁻¹ else 0 else 0) =
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0

State before:
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ y ∈ Fintype.piFinset fun _i => P.divisors,
      ∑ x_1 ∈ P.divisors, if ∏ i : Fin k, y i = x_1 ∧ x_1 ∣ P then if ↑x_1 ≤ x then (↑x_1)⁻¹ else 0 else 0) =
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0
Tactic:
apply sum_congr rfl
State after:
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ x_1 ∈ Fintype.piFinset fun _i => P.divisors,
    (∑ x_2 ∈ P.divisors, if ∏ i : Fin k, x_1 i = x_2 ∧ x_2 ∣ P then if ↑x_2 ≤ x then (↑x_2)⁻¹ else 0 else 0) =
      if ∏ i : Fin k, x_1 i ∣ P then if ↑(∏ i : Fin k, x_1 i) ≤ x then ∏ i : Fin k, (↑(x_1 i))⁻¹ else 0 else 0

State before:
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ x_1 ∈ Fintype.piFinset fun _i => P.divisors,
    (∑ x_2 ∈ P.divisors, if ∏ i : Fin k, x_1 i = x_2 ∧ x_2 ∣ P then if ↑x_2 ≤ x then (↑x_2)⁻¹ else 0 else 0) =
      if ∏ i : Fin k, x_1 i ∣ P then if ↑(∏ i : Fin k, x_1 i) ≤ x then ∏ i : Fin k, (↑(x_1 i))⁻¹ else 0 else 0
Tactic:
intro a _
State after:
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (∑ x_1 ∈ P.divisors, if ∏ i : Fin k, a i = x_1 ∧ x_1 ∣ P then if ↑x_1 ≤ x then (↑x_1)⁻¹ else 0 else 0) =
    if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0

State before:
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (∑ x_1 ∈ P.divisors, if ∏ i : Fin k, a i = x_1 ∧ x_1 ∣ P then if ↑x_1 ≤ x then (↑x_1)⁻¹ else 0 else 0) =
    if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0
Tactic:
rw [sum_eq_single (∏ i, a i)]
State after:
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (if ∏ i : Fin k, a i = ∏ i : Fin k, a i ∧ ∏ i : Fin k, a i ∣ P then
      if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0
    else 0) =
    if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0

case calc_2.h₀
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∀ b ∈ P.divisors,
    b ≠ ∏ i : Fin k, a i → (if ∏ i : Fin k, a i = b ∧ b ∣ P then if ↑b ≤ x then (↑b)⁻¹ else 0 else 0) = 0

case calc_2.h₁
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∉ P.divisors →
    (if ∏ i : Fin k, a i = ∏ i : Fin k, a i ∧ ∏ i : Fin k, a i ∣ P then
        if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0
      else 0) =
      0

State before:
case calc_2
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (if ∏ i : Fin k, a i = ∏ i : Fin k, a i ∧ ∏ i : Fin k, a i ∣ P then
      if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0
    else 0) =
    if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0
Tactic:
apply if_ctx_congr _ _ (fun _ => rfl)
State after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i = ∏ i : Fin k, a i ∧ ∏ i : Fin k, a i ∣ P ↔ ∏ i : Fin k, a i ∣ P

P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∣ P →
    (if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0) =
      if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i = ∏ i : Fin k, a i ∧ ∏ i : Fin k, a i ∣ P ↔ ∏ i : Fin k, a i ∣ P

P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∣ P →
    (if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0) =
      if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
rw [Iff.comm, iff_and_self]
State after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∣ P → ∏ i : Fin k, a i = ∏ i : Fin k, a i

P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∣ P →
    (if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0) =
      if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∣ P → ∏ i : Fin k, a i = ∏ i : Fin k, a i

P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∣ P →
    (if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0) =
      if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
exact fun _ => rfl
State after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∣ P →
    (if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0) =
      if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∣ P →
    (if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0) =
      if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
intro
State after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝¹ : a ∈ Fintype.piFinset fun _i => P.divisors
a✝ : ∏ i : Fin k, a i ∣ P
⊢ (if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0) =
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝¹ : a ∈ Fintype.piFinset fun _i => P.divisors
a✝ : ∏ i : Fin k, a i ∣ P
⊢ (if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0) =
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
rw [cast_prod, ← prod_inv_distrib]
State after:
no goals

State before:
case calc_2.h₀
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∀ b ∈ P.divisors,
    b ≠ ∏ i : Fin k, a i → (if ∏ i : Fin k, a i = b ∧ b ∣ P then if ↑b ≤ x then (↑b)⁻¹ else 0 else 0) = 0
Tactic:
exact fun d _ hd_ne ↦ if_neg fun h => hd_ne.symm h.1
State after:
no goals

State before:
case calc_2.h₁
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ ∏ i : Fin k, a i ∉ P.divisors →
    (if ∏ i : Fin k, a i = ∏ i : Fin k, a i ∧ ∏ i : Fin k, a i ∣ P then
        if ↑(∏ i : Fin k, a i) ≤ x then (↑(∏ i : Fin k, a i))⁻¹ else 0
      else 0) =
      0
Tactic:
exact fun h ↦ if_neg fun h' => h (mem_divisors.mpr ⟨h'.2, hP.ne_zero⟩)
State after:
no goals

State before:
case calc_3
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ Fintype.piFinset fun _i => P.divisors,
      if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors, if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
apply sum_le_sum
State after:
case calc_3.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Fintype.piFinset fun _i => P.divisors,
    (if ∏ i_1 : Fin k, i i_1 ∣ P then if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0 else 0) ≤
      if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0

State before:
case calc_3.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Fintype.piFinset fun _i => P.divisors,
    (if ∏ i_1 : Fin k, i i_1 ∣ P then if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0 else 0) ≤
      if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0
Tactic:
intro a _
State after:
case calc_3.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0

State before:
case calc_3.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
by_cases h : (∏ i, a i ∣ P)
State after:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ∏ i : Fin k, a i ∣ P
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0

case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0

State before:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
rw [if_neg h]
State after:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
⊢ 0 ≤ if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0

State before:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
⊢ 0 ≤ if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
split_ifs with h'
State after:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ ∏ i : Fin k, (↑(a i))⁻¹

case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ 0

State before:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ∏ i : Fin k, a i ∣ P
⊢ (if ∏ i : Fin k, a i ∣ P then if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0 else 0) ≤
    if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0
Tactic:
rw [if_pos h]
State after:
no goals

State before:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ ∏ i : Fin k, (↑(a i))⁻¹
Tactic:
apply prod_nonneg
State after:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ (↑(a i))⁻¹

State before:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ (↑(a i))⁻¹
Tactic:
intro i _
State after:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝¹ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
a✝ : i ∈ univ
⊢ 0 ≤ (↑(a i))⁻¹

State before:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝¹ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
a✝ : i ∈ univ
⊢ 0 ≤ (↑(a i))⁻¹
Tactic:
norm_num
State after:
no goals

State before:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
a✝ : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬∏ i : Fin k, a i ∣ P
h' : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ 0
Tactic:
rfl
State after:
no goals

State before:
case calc_4
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ Fintype.piFinset fun _i => P.divisors, if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0) ≤
    ∑ a ∈ Fintype.piFinset fun _i => P.divisors, ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
apply sum_le_sum
State after:
case calc_4.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Fintype.piFinset fun _i => P.divisors,
    (if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0) ≤
      ∏ i_1 : Fin k, if ↑(i i_1) ≤ x then (↑(i i_1))⁻¹ else 0

State before:
case calc_4.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Fintype.piFinset fun _i => P.divisors,
    (if ↑(∏ i_1 : Fin k, i i_1) ≤ x then ∏ i_1 : Fin k, (↑(i i_1))⁻¹ else 0) ≤
      ∏ i_1 : Fin k, if ↑(i i_1) ≤ x then (↑(i i_1))⁻¹ else 0
Tactic:
intro a ha
State after:
case calc_4.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0) ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0

State before:
case calc_4.h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
⊢ (if ↑(∏ i : Fin k, a i) ≤ x then ∏ i : Fin k, (↑(a i))⁻¹ else 0) ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
split_ifs with h
State after:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∏ i : Fin k, (↑(a i))⁻¹ ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0

case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0

State before:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∏ i : Fin k, (↑(a i))⁻¹ ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
gcongr with i hi
State after:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ (↑(a i))⁻¹

case pos.h1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ (↑(a i))⁻¹ ≤ if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0

State before:
case pos.h1
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ (↑(a i))⁻¹ ≤ if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
rw [if_pos]
State after:
case pos.h1.hc
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ↑(a i) ≤ x

State before:
case pos.h1.hc
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ↑(a i) ≤ x
Tactic:
apply le_trans _ h
State after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ↑(a i) ≤ ↑(∏ i : Fin k, a i)

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ↑(a i) ≤ ↑(∏ i : Fin k, a i)
Tactic:
norm_cast
State after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ a i ≤ ∏ i : Fin k, a i

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ a i ≤ ∏ i : Fin k, a i
Tactic:
rw [←prod_erase_mul (a:=i) (h:= hi)]
State after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ a i ≤ (∏ x ∈ univ.erase i, a x) * a i

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ a i ≤ (∏ x ∈ univ.erase i, a x) * a i
Tactic:
apply Nat.le_mul_of_pos_left
State after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ 0 < ∏ x ∈ univ.erase i, a x

State before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ 0 < ∏ x ∈ univ.erase i, a x
Tactic:
rw [Fintype.mem_piFinset] at ha
State after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ 0 < ∏ x ∈ univ.erase i, a x

State before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ 0 < ∏ x ∈ univ.erase i, a x
Tactic:
apply prod_pos
State after:
case h.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ∀ i_1 ∈ univ.erase i, 0 < a i_1

State before:
case h.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
⊢ ∀ i_1 ∈ univ.erase i, 0 < a i_1
Tactic:
intro j _
State after:
case h.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
j : Fin k
a✝ : j ∈ univ.erase i
⊢ 0 < a j

State before:
case h.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : ∀ (a_1 : Fin k), a a_1 ∈ P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
i : Fin k
hi : i ∈ univ
j : Fin k
a✝ : j ∈ univ.erase i
⊢ 0 < a j
Tactic:
apply pos_of_mem_divisors (ha j)
State after:
no goals

State before:
case pos.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ (↑(a i))⁻¹
Tactic:
norm_num
State after:
no goals

State before:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ 0 ≤ ∏ i : Fin k, if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
apply prod_nonneg
State after:
case neg.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0

State before:
case neg.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
⊢ ∀ i ∈ univ, 0 ≤ if ↑(a i) ≤ x then (↑(a i))⁻¹ else 0
Tactic:
intro j _
State after:
case neg.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
⊢ 0 ≤ if ↑(a j) ≤ x then (↑(a j))⁻¹ else 0

State before:
case neg.h0
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
⊢ 0 ≤ if ↑(a j) ≤ x then (↑(a j))⁻¹ else 0
Tactic:
split_ifs
State after:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
h✝ : ↑(a j) ≤ x
⊢ 0 ≤ (↑(a j))⁻¹

case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
h✝ : ¬↑(a j) ≤ x
⊢ 0 ≤ 0

State before:
case pos
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
h✝ : ↑(a j) ≤ x
⊢ 0 ≤ (↑(a j))⁻¹
Tactic:
norm_num
State after:
no goals

State before:
case neg
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
a : Fin k → ℕ
ha : a ∈ Fintype.piFinset fun _i => P.divisors
h : ¬↑(∏ i : Fin k, a i) ≤ x
j : Fin k
a✝ : j ∈ univ
h✝ : ¬↑(a j) ≤ x
⊢ 0 ≤ 0
Tactic:
rfl
State after:
no goals

State before:
case calc_5
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ d ∈ P.divisors, if ↑d ≤ x then (↑d)⁻¹ else 0) ^ k ≤ (1 + x.log) ^ k
Tactic:
rw [←sum_filter]
State after:
case calc_5
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹) ^ k ≤ (1 + x.log) ^ k

State before:
case calc_5
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ (∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹) ^ k ≤ (1 + x.log) ^ k
Tactic:
gcongr
State after:
case calc_5.hab
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹ ≤ 1 + x.log

State before:
case calc_5.hab
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹ ≤ 1 + x.log
Tactic:
trans (∑ d in Icc 1 (floor x), (d:ℝ)⁻¹)
State after:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹ ≤ ∑ d ∈ Icc 1 ⌊x⌋₊, (↑d)⁻¹

P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ d ∈ Icc 1 ⌊x⌋₊, (↑d)⁻¹ ≤ 1 + x.log

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ d ∈ Icc 1 ⌊x⌋₊, (↑d)⁻¹ ≤ 1 + x.log
Tactic:
apply sum_inv_le_log_real
State after:
case hy
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ 1 ≤ x

State before:
case hy
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ 1 ≤ x
Tactic:
linarith
State after:
no goals

State before:
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∑ a ∈ filter (fun d => ↑d ≤ x) P.divisors, (↑a)⁻¹ ≤ ∑ d ∈ Icc 1 ⌊x⌋₊, (↑d)⁻¹
Tactic:
apply sum_le_sum_of_subset_of_nonneg
State after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ filter (fun d => ↑d ≤ x) P.divisors ⊆ Icc 1 ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹

State before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ filter (fun d => ↑d ≤ x) P.divisors ⊆ Icc 1 ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Tactic:
intro d
State after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
⊢ d ∈ filter (fun d => ↑d ≤ x) P.divisors → d ∈ Icc 1 ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹

State before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
⊢ d ∈ filter (fun d => ↑d ≤ x) P.divisors → d ∈ Icc 1 ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Tactic:
rw[mem_filter, mem_Icc]
State after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
⊢ d ∈ P.divisors ∧ ↑d ≤ x → 1 ≤ d ∧ d ≤ ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹

State before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
⊢ d ∈ P.divisors ∧ ↑d ≤ x → 1 ≤ d ∧ d ≤ ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Tactic:
intro hd
State after:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 1 ≤ d ∧ d ≤ ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹

State before:
case h
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 1 ≤ d ∧ d ≤ ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Tactic:
constructor
State after:
case h.left
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 1 ≤ d

case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ d ≤ ⌊x⌋₊

case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹

State before:
case hf
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
⊢ ∀ i ∈ Icc 1 ⌊x⌋₊, i ∉ filter (fun d => ↑d ≤ x) P.divisors → 0 ≤ (↑i)⁻¹
Tactic:
norm_num
State after:
no goals

State before:
case h.left
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 1 ≤ d
Tactic:
rw [Nat.succ_le]
State after:
case h.left
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 < d

State before:
case h.left
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 < d
Tactic:
exact pos_of_mem_divisors hd.1
State after:
no goals

State before:
case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ d ≤ ⌊x⌋₊
Tactic:
rw [le_floor_iff]
State after:
case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ ↑d ≤ x

case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 ≤ x

State before:
case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ ↑d ≤ x

case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 ≤ x
Tactic:
exact hd.2
State after:
case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 ≤ x

State before:
case h.right
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 ≤ x
Tactic:
apply le_of_lt
State after:
case h.right.a
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 < x

State before:
case h.right.a
P k : ℕ
x : ℝ
hx : 1 ≤ x
hP : Squarefree P
hx_pos : 0 < x
d : ℕ
hd : d ∈ P.divisors ∧ ↑d ≤ x
⊢ 0 < x
Tactic:
exact hx_pos
State after:
no goals