awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)

Tactic:
simp only [Set.mem_setOf_eq, add_re, ofReal_re, one_re, hxy]

Premises used: Complex.add_re, Set.mem_setOf_eq, Complex.ofReal_re, Complex.one_re
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
⊢ Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)

Tactic:
have hys : (max x y + 1 : ℂ) ∈ {s | x < s.re} := by
    simp only [Set.mem_setOf_eq, add_re, ofReal_re, one_re, hxy]
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
⊢ 0 < f ((↑(max x y) : ℂ) + 1)

Tactic:
simpa only [hf' hys, ofReal_add, ofReal_one] using positive ha₀ ha₁ hxy'

Premises used: Complex.ofReal_add, Complex.ofReal_one, LSeries.positive
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
⊢ 0 < f ((↑(max x y) : ℂ) + 1)

Tactic:
have hfx : 0 < f (max x y + 1) := by
    simpa only [hf' hys, ofReal_add, ofReal_one] using positive ha₀ ha₁ hxy'
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
hfx : 0 < f ((↑(max x y) : ℂ) + 1)
⊢ 0 < f (↑y : ℂ)

Tactic:
(hfx.trans_le <| hf.apply_le_of_iteratedDeriv_alternating (fun n _ ↦ ?_) ?_)

Premises used: LT.lt.trans_le, Differentiable.apply_le_of_iteratedDeriv_alternating
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
hfx : 0 < f ((↑(max x y) : ℂ) + 1)
refine_1 : ∀ (n : ℕ), n ≠ 0 → 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n f ((↑(max x y) : ℂ) + 1)
refine_2 : (↑y : ℂ) ≤ (↑(max x y) : ℂ) + 1
⊢ 0 < f (↑y : ℂ)

Tactic:
refine (hfx.trans_le <| hf.apply_le_of_iteratedDeriv_alternating (fun n _ ↦ ?_) ?_)

Premises used: LT.lt.trans_le, Differentiable.apply_le_of_iteratedDeriv_alternating
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
hfx : 0 < f ((↑(max x y) : ℂ) + 1)
n : ℕ
h : n ≠ 0
⊢ IsOpen (X := ℂ) {s : ℂ | x < s.re}

Tactic:
have hs : IsOpen {s : ℂ | x < s.re} := continuous_re.isOpen_preimage _ isOpen_Ioi
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
hfx : 0 < f ((↑(max x y) : ℂ) + 1)
n : ℕ
h : n ≠ 0
hs : IsOpen (X := ℂ) {s : ℂ | x < s.re}
⊢ 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n f ((↑(max x y) : ℂ) + 1)

Tactic:
simpa only [hf'.iteratedDeriv_of_isOpen hs n hys, ofReal_add, ofReal_one] using
      iteratedDeriv_alternating ha₀ hxy' n

Premises used: Complex.ofReal_add, Complex.ofReal_one, LSeries.iteratedDeriv_alternating, Set.EqOn.iteratedDeriv_of_isOpen
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries a) {s : ℂ | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < (↑(max x y) : EReal) + 1
hys : Membership.mem (γ := Set ℂ) {s : ℂ | x < s.re} ((↑(max x y) : ℂ) + 1)
hfx : 0 < f ((↑(max x y) : ℂ) + 1)
⊢ (↑y : ℂ) ≤ (↑(max x y) : ℂ) + 1

Tactic:
exact_mod_cast (le_max_right x y).trans (lt_add_one _).le

Premises used: le_max_right, lt_add_one, LT.lt.le, LE.le.trans
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ArithmeticFunction ℂ
hn : ∀ (n : ℕ), LE.le (α := ℂ) (0 : ℂ) ((a : (a : ℕ) → ℂ) n : ℂ)
x : ℝ
h : LSeries.abscissaOfAbsConv (⇑a : (a : ℕ) → ℂ) < (↑x : EReal)
n : ℕ
⊢ 0 ≤ HPow.hPow (α := ℂ) (-1) n * iteratedDeriv n (LSeries fun (x : ℕ) ↦ (a : (a : ℕ) → ℂ) x) (↑x : ℂ)

Tactic:
LSeries.iteratedDeriv_alternating hn h n

Premises used: LSeries.iteratedDeriv_alternating
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
x : ℝ
hx : LSeries.abscissaOfAbsConv a < (↑x : EReal)
⊢ 0 < LSeries a (↑x : ℂ)

Tactic:
LSeries.positive ha₀ ha₁ hx

Premises used: LSeries.positive
-- Module: Mathlib.NumberTheory.LSeries.Positivity
Goal:
a : ArithmeticFunction ℂ
ha₀ : LE.le (α := ℕ → ℂ) 0 fun (x : ℕ) ↦ (a : (a : ℕ) → ℂ) x
ha₁ : LT.lt (α := ℂ) (0 : ℂ) ((a : (a : ℕ) → ℂ) 1 : ℂ)
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : LSeries.abscissaOfAbsConv (⇑a : (a : ℕ) → ℂ) ≤ (↑x : EReal)
hf' : Set.EqOn f (LSeries (⇑a : (a : ℕ) → ℂ)) {s : ℂ | x < s.re}
y : ℝ
⊢ 0 < f (↑y : ℂ)

Tactic:
LSeries.positive_of_differentiable_of_eqOn ha₀ ha₁ hf hx hf' y

Premises used: LSeries.positive_of_differentiable_of_eqOn
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
⊢ Multipliable.{u_1, 0} (α := α) (β := { n : ℕ // IsPrimePow n })
    ((fun (pk : Nat.Primes × ℕ) ↦ f ((↑pk.1 : ℕ) ^ (pk.2 + 1))) ∘
      (⇑prodNatEquiv.symm : (a : { n : ℕ // IsPrimePow n }) → Nat.Primes × ℕ))

Tactic:
simpa only [← coe_prodNatEquiv_apply, Prod.eta, Function.comp_def, Equiv.apply_symm_apply]
        using hfm.subtype _

Premises used: Equiv.apply_symm_apply, Multipliable.subtype, Prod.eta, Nat.Primes.coe_prodNatEquiv_apply, Function.comp_def
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
⊢ Multipliable.{u_1, 0} (α := α) fun (pk : Nat.Primes × ℕ) ↦ f ((↑pk.1 : ℕ) ^ (pk.2 + 1))

Tactic:
have hfm' : Multipliable fun pk : Nat.Primes × ℕ ↦ f (pk.fst ^ (pk.snd + 1)) :=
    prodNatEquiv.symm.multipliable_iff.mp <| by
      simpa only [← coe_prodNatEquiv_apply, Prod.eta, Function.comp_def, Equiv.apply_symm_apply]
        using hfm.subtype _
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfm' : Multipliable.{u_1, 0} (α := α) fun (pk : Nat.Primes × ℕ) ↦ f ((↑pk.1 : ℕ) ^ (pk.2 + 1))
simp :
  Eq.{u_1 + 1} (α := α)
    (∏' (c : Nat.Primes × ℕ), f (↑((prodNatEquiv : (a : Nat.Primes × ℕ) → { n : ℕ // IsPrimePow n }) c) : ℕ))
    (∏' (p : Nat.Primes × ℕ), f ((↑p.1 : ℕ) ^ (p.2 + 1)))
⊢ Eq.{u_1 + 1} (α := α) (∏' (n : ℕ), f n) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1)))

Tactic:
simp only [← tprod_subtype_eq_of_mulSupport_subset hf, Set.coe_setOf, ← prodNatEquiv.tprod_eq,
    ← hfm'.tprod_prod]

Premises used: Multipliable.tprod_prod, Equiv.tprod_eq, tprod_subtype_eq_of_mulSupport_subset, Nat.Primes.prodNatEquiv, Set.coe_setOf
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfm' : Multipliable.{u_1, 0} (α := α) fun (pk : Nat.Primes × ℕ) ↦ f ((↑pk.1 : ℕ) ^ (pk.2 + 1))
⊢ Eq.{u_1 + 1} (α := α)
    (∏' (c : Nat.Primes × ℕ), f (↑((prodNatEquiv : (a : Nat.Primes × ℕ) → { n : ℕ // IsPrimePow n }) c) : ℕ))
    (∏' (p : Nat.Primes × ℕ), f ((↑p.1 : ℕ) ^ (p.2 + 1)))

Tactic:
tprod_congr fun (p, k) ↦ congrArg f <| coe_prodNatEquiv_apply ..

Premises used: congrArg, _private.0.tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers.match_1, Prod.fst, tprod_congr, Nat.Primes.coe_prodNatEquiv_apply, HPow.hPow, HAdd.hAdd, Nat.Primes.prodNatEquiv, OfNat.ofNat, Subtype.val, Eq, Prod.snd, DFunLike.coe
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfm' : Multipliable.{u_1, 0} (α := α) fun (pk : Nat.Primes × ℕ) ↦ f ((↑pk.1 : ℕ) ^ (pk.2 + 1))
⊢ Eq.{u_1 + 1} (α := α)
    (∏' (c : Nat.Primes × ℕ), f (↑((prodNatEquiv : (a : Nat.Primes × ℕ) → { n : ℕ // IsPrimePow n }) c) : ℕ))
    (∏' (p : Nat.Primes × ℕ), f ((↑p.1 : ℕ) ^ (p.2 + 1)))

Tactic:
refine tprod_congr fun (p, k) ↦ congrArg f <| coe_prodNatEquiv_apply ..

Premises used: tprod_congr
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
rw :
  ∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1)) =
    HMul.hMul (α := α) (∏' (p : Nat.Primes), f (↑p : ℕ)) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2)))
⊢ ∏' (n : ℕ), f n =
    HMul.hMul (α := α) (∏' (p : Nat.Primes), f (↑p : ℕ)) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2)))

Tactic:
rw [tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers hfm hf]

Premises used: tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
⊢ ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))

Tactic:
have hfs' (p : Nat.Primes) : Multipliable fun k : ℕ ↦ f (p ^ (k + 1)) :=
    hfm.comp_injective <| (strictMono_nat_of_lt_succ
      fun k ↦ pow_lt_pow_right₀ p.prop.one_lt <| lt_add_one (k + 1)).injective
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
h : ∀ (p : Nat.Primes), ∏' (k : ℕ), f ((↑p : ℕ) ^ (k + 1))
| ∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1))

Tactic:
enter [1, p]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
p : Nat.Primes
h : f (↑p : ℕ) * ∏' (b : ℕ), f ((↑p : ℕ) ^ (b + 1 + 1))
| ∏' (k : ℕ), f ((↑p : ℕ) ^ (k + 1))

Tactic:
rw [(hfs' p).tprod_eq_zero_mul, zero_add, pow_one]

Premises used: Multipliable.tprod_eq_zero_mul, zero_add, pow_one
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
p : Nat.Primes
h : ∀ (k : ℕ), f ((↑p : ℕ) ^ (k + 1 + 1))
| f (↑p : ℕ) * ∏' (b : ℕ), f ((↑p : ℕ) ^ (b + 1 + 1))

Tactic:
enter [2, 1, k]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
p : Nat.Primes
k : ℕ
h : f ((↑p : ℕ) ^ (k + 2))
| f ((↑p : ℕ) ^ (k + 1 + 1))

Tactic:
rw [add_assoc, one_add_one_eq_two]

Premises used: add_assoc, one_add_one_eq_two
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
h : ∀ (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2))
| ∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1))

Tactic:
enter [1, p]; rw [(hfs' p).tprod_eq_zero_mul, zero_add, pow_one]
    enter [2, 1, k]; rw [add_assoc, one_add_one_eq_two]

Premises used: add_assoc, zero_add, one_add_one_eq_two, pow_one
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
conv_lhs :
  ∏' (p : Nat.Primes), f (↑p : ℕ) * ∏' (k : ℕ), f ((↑p : ℕ) ^ (k + 2)) =
    HMul.hMul (α := α) (∏' (p : Nat.Primes), f (↑p : ℕ)) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2)))
⊢ ∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 1)) =
    HMul.hMul (α := α) (∏' (p : Nat.Primes), f (↑p : ℕ)) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2)))

Tactic:
conv_lhs =>
    enter [1, p]; rw [(hfs' p).tprod_eq_zero_mul, zero_add, pow_one]
    enter [2, 1, k]; rw [add_assoc, one_add_one_eq_two]

Premises used: add_assoc, zero_add, one_add_one_eq_two, pow_one
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
⊢ ∏' (p : Nat.Primes), f (↑p : ℕ) * ∏' (k : ℕ), f ((↑p : ℕ) ^ (k + 2)) =
    HMul.hMul (α := α) (∏' (p : Nat.Primes), f (↑p : ℕ)) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2)))

Tactic:
(Multipliable.subtype hfm _).tprod_mul <|
    Multipliable.prod (f := fun (pk : Nat.Primes × ℕ) ↦ f (pk.1 ^ (pk.2 + 2))) <|
    hfm.comp_injective <| Subtype.val_injective |>.comp
    Nat.Primes.prodNatEquiv.injective |>.comp <|
    Function.Injective.prodMap (fun ⦃_ _⦄ a ↦ a) <| add_left_injective 1

Premises used: Function.Injective.prodMap, Multipliable.subtype, Subtype.val_injective, Nat.Primes, Function.Injective.comp, Multipliable.comp_injective, Nat.Primes.prodNatEquiv, add_left_injective, Multipliable.tprod_mul, Multipliable.prod, Equiv.injective, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : UniformSpace α
inst_2 : IsUniformGroup α
inst_3 : CompleteSpace α
inst_4 : T0Space α
f : ℕ → α
hfm : Multipliable f
hf : Function.mulSupport f ⊆ {n : ℕ | IsPrimePow n}
hfs' : ∀ (p : Nat.Primes), Multipliable.{u_1, 0} (α := α) fun (k : ℕ) ↦ f ((↑p : ℕ) ^ (k + 1))
⊢ ∏' (p : Nat.Primes), f (↑p : ℕ) * ∏' (k : ℕ), f ((↑p : ℕ) ^ (k + 2)) =
    HMul.hMul (α := α) (∏' (p : Nat.Primes), f (↑p : ℕ)) (∏' (p : Nat.Primes) (k : ℕ), f ((↑p : ℕ) ^ (k + 2)))

Tactic:
exact (Multipliable.subtype hfm _).tprod_mul <|
    Multipliable.prod (f := fun (pk : Nat.Primes × ℕ) ↦ f (pk.1 ^ (pk.2 + 2))) <|
    hfm.comp_injective <| Subtype.val_injective |>.comp
    Nat.Primes.prodNatEquiv.injective |>.comp <|
    Function.Injective.prodMap (fun ⦃_ _⦄ a ↦ a) <| add_left_injective 1

Premises used: Function.Injective.prodMap, Multipliable.subtype, Subtype.val_injective, Function.Injective.comp, Multipliable.comp_injective, Nat.Primes.prodNatEquiv, add_left_injective, Multipliable.tprod_mul, Multipliable.prod, Equiv.injective, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
n : ℕ
⊢ 0 ≤ residueClass a n

Tactic:
Set.indicator_apply_nonneg fun _ ↦ vonMangoldt_nonneg

Premises used: ArithmeticFunction.vonMangoldt_nonneg, Set.indicator_apply_nonneg
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
n : ℕ
⊢ residueClass a n ≤ (Λ : (a : ℕ) → ℝ) n

Tactic:
Set.indicator_apply_le' (fun _ ↦ le_rfl) (fun _ ↦ vonMangoldt_nonneg)

Premises used: le_rfl, Set.indicator_apply_le', ArithmeticFunction.vonMangoldt_nonneg
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
⊢ residueClass a 0 = 0

Tactic:
simp only [Set.indicator_apply_eq_zero, Set.mem_setOf_eq, Nat.cast_zero, map_zero,
    implies_true]

Premises used: Set.mem_setOf_eq, ArithmeticFunction.map_zero, implies_true, Nat.cast_zero, Set.indicator_apply_eq_zero
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) ≤ 1

Tactic:
abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable fun y hy ↦ ?_

Premises used: WithBot.some, LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable, Real.toEReal
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
refine : ∀ (y : ℝ) (hy : 1 < y), LSeriesSummable (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ)
⊢ (abscissaOfAbsConv fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) ≤ 1

Tactic:
refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable fun y hy ↦ ?_

Premises used: LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
⊢ 1 < (↑y : ℂ).re

Tactic:
simp only [ofReal_re, hy]

Premises used: Complex.ofReal_re
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
⊢ LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)

Tactic:
have := LSeriesSummable_vonMangoldt <| show 1 < (y : ℂ).re by simp only [ofReal_re, hy]
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)
⊢ Summable (Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)))

Tactic:
this.indicator {n : ℕ | (n : ZMod q) = a}

Premises used: setOf, Nat.cast, Summable.indicator, Eq
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)
h :
  term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) =
    Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ))
⊢ Summable (term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ))

Tactic:
convert! this.indicator {n : ℕ | (n : ZMod q) = a}

Premises used: setOf, Nat.cast, Summable.indicator, Eq
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)
h :
  ∀ (n : ℕ),
    term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
      Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n
⊢ term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) =
    Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ))

Tactic:
ext1 n
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)
n : ℕ
pos :
  ∀ (hn : (↑n : ZMod q) = a),
    term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
      Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n
neg :
  ∀ (hn : ¬(↑n : ZMod q) = a),
    term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
      Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n
⊢ term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
    Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n

Tactic:
by_cases hn : (n : ZMod q) = a

Premises used: Nat.cast
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)
n : ℕ
hn : (↑n : ZMod q) = a
⊢ term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
    Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n

Tactic:
simp +contextual only [term, Set.indicator, Set.mem_setOf_eq, hn, ↓reduceIte, apply_ite,
      ite_self]

Premises used: Set.indicator, ite_self, apply_ite, Set.mem_setOf_eq, reduceIte, LSeries.term
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)
n : ℕ
hn : ¬(↑n : ZMod q) = a
⊢ term (fun (n : ℕ) ↦ (↑(residueClass a n) : ℂ)) (↑y : ℂ) n =
    Set.indicator {n : ℕ | (↑n : ZMod q) = a} (term (fun (n : ℕ) ↦ (↑((Λ : (a : ℕ) → ℝ) n) : ℂ)) (↑y : ℂ)) n

Tactic:
simp +contextual only [term, Set.mem_setOf_eq, hn, not_false_eq_true, Set.indicator_of_notMem,
      ofReal_zero, zero_div, ite_self]

Premises used: ite_self, zero_div, Set.mem_setOf_eq, Complex.ofReal_zero, Set.indicator_of_notMem, LSeries.term, not_false_eq_true
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
simp :
  Eq (α := Set ℕ) {x : ℕ | (Nat.Prime x ∧ (↑x : ZMod q) = a ∧ ¬Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) x : ℝ) (0 : ℝ)) ∧ ¬x = 0}
    {p : ℕ | Nat.Prime p ∧ (↑p : ZMod q) = a}
⊢ Eq (α := Set ℕ) (Function.support (M := ℝ) fun (n : ℕ) ↦ (if Nat.Prime n then residueClass a n else 0) / (↑n : ℝ))
    {p : ℕ | Nat.Prime p ∧ (↑p : ZMod q) = a}

Tactic:
simp only [Function.support, ne_eq, div_eq_zero_iff, ite_eq_right_iff,
    Set.indicator_apply_eq_zero, Set.mem_setOf_eq, Nat.cast_eq_zero, not_or, Classical.not_imp]

Premises used: Set.mem_setOf_eq, ne_eq, not_or, Nat.cast_eq_zero, ite_eq_right_iff, Classical.not_imp, Function.support, Set.indicator_apply_eq_zero, div_eq_zero_iff
-- Module: Mathlib.NumberTheory.LSeries.PrimesInAP
Goal:
q : ℕ
a : ZMod q
h :
  ∀ (p : ℕ),
    Membership.mem (γ := Set ℕ)
        {x : ℕ | (Nat.Prime x ∧ (↑x : ZMod q) = a ∧ ¬Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) x : ℝ) (0 : ℝ)) ∧ ¬x = 0} p ↔
      Membership.mem (γ := Set ℕ) {p : ℕ | Nat.Prime p ∧ (↑p : ZMod q) = a} p
⊢ Eq (α := Set ℕ) {x : ℕ | (Nat.Prime x ∧ (↑x : ZMod q) = a ∧ ¬Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) x : ℝ) (0 : ℝ)) ∧ ¬x = 0}
    {p : ℕ | Nat.Prime p ∧ (↑p : ZMod q) = a}

Tactic:
ext1 p