mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_5
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
⊢ Complex.Gamma s * a i / ↑(p i) ^ s = ∫ (a_1 : ℝ) in Ioi 0, ↑a_1 ^ (s - 1) * a i * ↑(rexp (-p i * a_1)) ∂volume

Tactic:
mul_comm _ (a _),

Goal state after:
case e'_5
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
⊢ a i * Complex.Gamma s / ↑(p i) ^ s = ∫ (a_1 : ℝ) in Ioi 0, a i * ↑a_1 ^ (s - 1) * ↑(rexp (-p i * a_1)) ∂volume
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖↑n‖ ^ k * ‖rexp (-π * ((↑n + a) ^ 2 * t))‖ ≤
    ↑|↑n| ^ k * rexp (-π * (t * ↑↑n ^ 2 - 2 * (|a| * (t * ↑|↑n|))) + -π * (a ^ 2 * t))

Tactic:
Int.cast_abs,

Goal state after:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖↑n‖ ^ k * ‖rexp (-π * ((↑n + a) ^ 2 * t))‖ ≤
    |↑↑n| ^ k * rexp (-π * (t * ↑↑n ^ 2 - 2 * (|a| * (t * |↑↑n|))) + -π * (a ^ 2 * t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ π * |↑n ^ 2| * ‖ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ π * ↑|n| ^ 2

Tactic:
Int.cast_abs,

Goal state after:
case refine_2
n : ℤ
z τ : ℂ
hns : ∀ (a : ℂ) (f : ℂ × ℂ →L[ℂ] ℂ), ‖a • f‖ = ‖a‖ * ‖f‖
⊢ π * |↑n ^ 2| * ‖ContinuousLinearMap.snd ℂ ℂ ℂ‖ ≤ π * |↑n| ^ 2
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * ↑|n| ^ 2 = π * ‖↑n ^ 2‖

Tactic:
Int.cast_abs,

Goal state after:
n : ℤ
z τ : ℂ
this : ‖(jacobiTheta₂_term_fderiv n z τ) (0, 1)‖ ≤ ‖jacobiTheta₂_term_fderiv n z τ‖
⊢ π * |↑n| ^ 2 = π * ‖↑n ^ 2‖
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
⊢ ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • (((Ioi 1).indicator fun x ↦ P.f x) + (Ioo 0 1).indicator fun x ↦ P.f x) t =
    ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • P.f t

Tactic:
refine integral_congr_ae <| (ae_restrict_iff' measurableSet_Ioi).mpr ?_

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
s : ℂ
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioi 0 →
      (fun t ↦ ↑t ^ (s - 1) • (((Ioi 1).indicator fun x ↦ P.f x) + (Ioo 0 1).indicator fun x ↦ P.f x) t) x =
        (fun t ↦ ↑t ^ (s - 1) • P.f t) x
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
| ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)

Tactic:
enter [t, ht, 1, i]; rw [this]

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
t : ℝ
ht : t ∈ Ioi 0
i : ι
| if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - if ↑a = 0 then 1 else 0)

Tactic:
AddCircle.coe_eq_zero_iff,

Goal state after:
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t))
    (evenKernel (↑a) t - if ∃ n, n • 1 = a then 1 else 0)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case e_f
z τ : ℂ
n : ℤ
⊢ -((starRingEnd ℂ) ↑2 * (starRingEnd ℂ) ↑π * (starRingEnd ℂ) I * (starRingEnd ℂ) ↑↑n *
        cexp
          ((starRingEnd ℂ) ↑2 * (starRingEnd ℂ) ↑π * (starRingEnd ℂ) I * (starRingEnd ℂ) ↑↑n * (starRingEnd ℂ) z +
            (starRingEnd ℂ) ↑π * (starRingEnd ℂ) I * (starRingEnd ℂ) ↑↑n ^ 2 * (starRingEnd ℂ) τ)) =
    ↑2 * ↑π * I * ↑↑n * cexp (↑2 * ↑π * I * ↑↑n * -(starRingEnd ℂ) z + ↑π * I * ↑↑n ^ 2 * -(starRingEnd ℂ) τ)

Tactic:
conj_ofReal,

Goal state after:
case e_f
z τ : ℂ
n : ℤ
⊢ -(↑2 * ↑π * (starRingEnd ℂ) I * ↑↑n *
        cexp
          (↑2 * ↑π * (starRingEnd ℂ) I * ↑↑n * (starRingEnd ℂ) z +
            ↑π * (starRingEnd ℂ) I * ↑↑n ^ 2 * (starRingEnd ℂ) τ)) =
    ↑2 * ↑π * I * ↑↑n * cexp (↑2 * ↑π * I * ↑↑n * -(starRingEnd ℂ) z + ↑π * I * ↑↑n ^ 2 * -(starRingEnd ℂ) τ)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case e_f
z τ : ℂ
n : ℤ
⊢ -(starRingEnd ℂ) (jacobiTheta₂'_term n z τ) = jacobiTheta₂'_term n (-(starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, map_mul, ← Complex.exp_conj, map_add, map_mul,
    ← ofReal_intCast, ← ofReal_ofNat, map_pow, conj_ofReal, conj_I]

Goal state after:
case e_f
z τ : ℂ
n : ℤ
⊢ -(↑2 * ↑π * -I * ↑↑n * cexp (↑2 * ↑π * -I * ↑↑n * (starRingEnd ℂ) z + ↑π * -I * ↑↑n ^ 2 * (starRingEnd ℂ) τ)) =
    ↑2 * ↑π * I * ↑↑n * cexp (↑2 * ↑π * I * ↑↑n * -(starRingEnd ℂ) z + ↑π * I * ↑↑n ^ 2 * -(starRingEnd ℂ) τ)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2) =
    1 / (-I * τ) ^ (1 / 2) * cexp (↑π * I * (-1 / τ) * z ^ 2) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Tactic:
mul_assoc _ (cexp _),

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2) =
    1 / (-I * τ) ^ (1 / 2) *
      (cexp (↑π * I * (-1 / τ) * z ^ 2) * ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
r p : ℝ
hp : 0 < p
hp' : (fun x ↦ cosKernel a x - 1) =O[atTop] fun x ↦ rexp (-p * x)
⊢ (fun x ↦ (ofReal ∘ cosKernel a) x - 1) =O[atTop] fun x ↦ x ^ r

Tactic:
simpa using isBigO_ofReal_left.mpr <| hp'.trans (isLittleO_exp_neg_mul_rpow_atTop hp r).isBigO

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_f
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.g =
    ofReal ∘ evenKernel 0

Tactic:
simp [evenKernel_eq_cosKernel_of_zero]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_g
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.f =
    ofReal ∘ cosKernel 0

Tactic:
simp [evenKernel_eq_cosKernel_of_zero]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_ε
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
          hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
          hf_top := ⋯, hg_top := ⋯ }.ε⁻¹ =
    1

Tactic:
simp [evenKernel_eq_cosKernel_of_zero]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_f₀
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.g₀ =
    if 0 = 0 then 1 else 0

Tactic:
simp [evenKernel_eq_cosKernel_of_zero]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_g₀
⊢ { f := ofReal ∘ evenKernel 0, g := ofReal ∘ cosKernel 0, k := 1 / 2, ε := 1, f₀ := if 0 = 0 then 1 else 0, g₀ := 1,
        hf_int := ⋯, hg_int := ⋯, hk := hurwitzEvenFEPair._proof_7, hε := hurwitzEvenFEPair._proof_8, h_feq := ⋯,
        hf_top := ⋯, hg_top := ⋯ }.f₀ =
    1

Tactic:
simp [evenKernel_eq_cosKernel_of_zero]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
J : ℂ
⊢ J = (↑x ^ (↑3 / ↑2))⁻¹ * (-2 * ↑π * ↑x ^ (3 / 2) * J / (-2 * ↑π))

Tactic:
ofReal_ofNat,

Goal state after:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
J : ℂ
⊢ J = (↑x ^ (3 / ↑2))⁻¹ * (-2 * ↑π * ↑x ^ (3 / 2) * J / (-2 * ↑π))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
J : ℂ
⊢ J = (↑x ^ (3 / ↑2))⁻¹ * (-2 * ↑π * ↑x ^ (3 / 2) * J / (-2 * ↑π))

Tactic:
ofReal_ofNat,

Goal state after:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
J : ℂ
⊢ J = (↑x ^ (3 / 2))⁻¹ * (-2 * ↑π * ↑x ^ (3 / 2) * J / (-2 * ↑π))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : -1 / (I * ↑(1 / x)) = I * ↑x
h2 : -I * (I * ↑(1 / x)) = 1 / ↑x
h3 : ↑x ^ (3 / 2) ≠ 0
h4 : (↑x).arg ≠ π
J : ℂ
⊢ J = ↑(1 / x ^ (3 / 2)) * (-2 * ↑π / (1 / ↑x) ^ (3 / 2) * J / (-2 * ↑π))

Tactic:
rw [one_div (x : ℂ), inv_cpow _ _ h4, div_inv_eq_mul, one_div, ofReal_inv, ofReal_cpow hx.le,
    ofReal_div, ofReal_ofNat, ofReal_ofNat, ← mul_div_assoc _ _ (-2 * π : ℂ),
    eq_div_iff <| mul_ne_zero (neg_ne_zero.mpr two_ne_zero) (ofReal_ne_zero.mpr pi_ne_zero),
    ← div_eq_inv_mul, eq_div_iff h3, mul_comm J _, mul_right_comm]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case e_a
a : UnitAddCircle
s : ℂ
⊢ ((hurwitzEvenFEPair a).symm.ε / (↑(hurwitzEvenFEPair a).symm.k - s / 2)) • (hurwitzEvenFEPair a).symm.g₀ / 2 =
    (if a = 0 then 1 else 0) / (1 - s)

Tactic:
simp_rw [WeakFEPair.symm, hurwitzEvenFEPair, push_cast, inv_one, smul_eq_mul,
      mul_comm _ (if _ then _ else _), mul_div_assoc, div_div, ← sub_div,
      div_mul_cancel₀ _ (two_ne_zero' ℂ), mul_one_div]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedCosZeta₀ a (1 - s) = completedHurwitzZetaEven₀ a s

Tactic:
← completedHurwitzZetaEven₀_one_sub,

Goal state after:
a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaEven₀ a (1 - (1 - s)) = completedHurwitzZetaEven₀ a s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ ↑2 * ↑n * ↑(Real.sin (2 * π * a * ↑n)) * ↑(rexp (-π * ↑n ^ 2 * t)) =
    -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) +
      -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n)) * ↑(rexp (-π * ↑n ^ 2 * t))

Tactic:
ofReal_ofNat,

Goal state after:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      -I * ↑↑n * cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        -I * ↑(-↑n) * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    ↑(sinKernel (↑a) t)
n : ℕ
⊢ 2 * ↑n * ↑(Real.sin (2 * π * a * ↑n)) * ↑(rexp (-π * ↑n ^ 2 * t)) =
    -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) +
      -(-I * ↑n) * cexp (-(2 * ↑π * I * ↑a * ↑n)) * ↑(rexp (-π * ↑n ^ 2 * t))
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk :
  ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n) x ∈ Iio (1 / 2)
⊢ False

Tactic:
indicator_indicator,

Goal state after:
h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p} ∩ {p | Nat.Prime p}).indicator (fun n ↦ 1 / ↑n) x ∈ Iio (1 / 2)
⊢ False
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
⊢ L (fun n ↦ ↑(ζ n)) s = L 1 s

Tactic:
exact (LSeries_congr const_one_eq_zeta s).symm

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
⊢ ↑1 < ↑s.re

Tactic:
EReal.coe_lt_coe_iff

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
hχ : LSeriesSummable (fun n ↦ χ ↑n) s
⊢ 1 < s.re
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
⊢ [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE

Tactic:
by
  tfae_have 1 → 2
  | h, a, b, c, ha, hb, hc, habc => by
    obtain hn | hn := n.even_or_odd
    · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [hn.pow_abs, habc]
    obtain ha | ha := ha.lt_or_gt <;> obtain hb | hb := hb.lt_or_gt <;>
      obtain hc | hc := hc.lt_or_gt
    · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_neg, neg_pow a, neg_pow b, neg_pow c, ← mul_add, *]
    · exact (by positivity : 0 < c ^ n).not_gt <| habc.symm.trans_lt <| add_neg (hn.pow_neg ha) <|
        hn.pow_neg hb
    · refine h b.natAbs c.natAbs a.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, add_neg_eq_iff_eq_add,
        eq_neg_add_iff_add_eq, *]
    · refine h a.natAbs c.natAbs b.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, neg_add_eq_iff_eq_add,
        *]
    · refine h c.natAbs a.natAbs b.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, neg_add_eq_iff_eq_add,
        eq_add_neg_iff_add_eq, *]
    · refine h c.natAbs b.natAbs a.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, abs_of_neg, hn.neg_pow, add_neg_eq_iff_eq_add,
        *]
    · exact (by positivity : 0 < a ^ n + b ^ n).not_gt <| habc.trans_lt <| hn.pow_neg hc
    · refine h a.natAbs b.natAbs c.natAbs (by positivity) (by positivity) (by positivity)
        (Int.natCast_inj.1 ?_)
      push_cast
      simp only [abs_of_pos, *]
  tfae_have 2 → 3
  | h, a, b, c, ha, hb, hc, habc => by
    rw [← Rat.num_ne_zero] at ha hb hc
    refine h (a.num * b.den * c.den) (a.den * b.num * c.den) (a.den * b.den * c.num)
      (by positivity) (by positivity) (by positivity) ?_
    have : (a.den * b.den * c.den : ℚ) ^ n ≠ 0 := by positivity
    refine Int.cast_injective <| (div_left_inj' this).1 ?_
    push_cast
    simp only [add_div, ← div_pow, mul_div_mul_comm, div_self (by positivity : (a.den : ℚ) ≠ 0),
      div_self (by positivity : (b.den : ℚ) ≠ 0), div_self (by positivity : (c.den : ℚ) ≠ 0),
      one_mul, mul_one, Rat.num_div_den, habc]
  tfae_have 3 → 1
  | h, a, b, c => mod_cast h a b c
  tfae_finish

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ↑n ^ (-s.re) = (↑n ^ s.re)⁻¹

Tactic:
Real.rpow_neg <| Nat.cast_nonneg n

Goal state after:
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (↑n ^ s.re)⁻¹ = (↑n ^ s.re)⁻¹
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun n ↦ (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / ↑n ^ s / 2) (cosZeta (↑a) s)
⊢ HasSum (fun n ↦ ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (cosZeta (↑a) s)

Tactic:
div_right_comm _ _ (2 : ℂ)

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
this : HasSum (fun n ↦ (cexp (2 * ↑π * I * ↑a * ↑n) + cexp (-(2 * ↑π * I * ↑a * ↑n))) / 2 / ↑n ^ s) (cosZeta (↑a) s)
⊢ HasSum (fun n ↦ ↑(Real.cos (2 * π * a * ↑n)) / ↑n ^ s) (cosZeta (↑a) s)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 2 ∣ x.natAbs

Tactic:
apply Int.natCast_dvd.1
      apply Int.dvd_of_emod_eq_zero hx

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := ⋯
⊢ Summable f

Tactic:
apply of_norm_bounded_eventually_nat (g := (↑· ^ (-s.re)))

Goal state after:
case hg
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := ⋯
⊢ Summable fun x ↦ ↑x ^ (-s.re)

case h
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := ⋯
⊢ ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ ↑i ^ (-s.re)
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hs : b' ^ 2 = -d ^ 2 * m
hd : r * s = d ^ 2 ∨ r * s = -d ^ 2
h1 : r * s = -d ^ 2
⊢ -(d ^ 2 * m) ≤ 0

Tactic:
exact neg_nonpos.mpr ((mul_nonneg_iff_of_pos_right h4).mpr (sq_nonneg d))

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
n : ℕ
hn : 1 < n
this : 0 < Real.log ↑n
⊢ ‖↑n ^ (-s)‖ ≤ ↑n ^ (-s.re)

Tactic:
← ofReal_natCast n,

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
n : ℕ
hn : 1 < n
this : 0 < Real.log ↑n
⊢ ‖↑↑n ^ (-s)‖ ≤ ↑n ^ (-s.re)
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a : k[X]
⊢ divRadical a ∣ derivative a

Tactic:
induction a using induction_on_coprime

Goal state after:
case h0
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
⊢ divRadical 0 ∣ derivative 0

case h1
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ : k[X]
a✝ : IsUnit x✝
⊢ divRadical x✝ ∣ derivative x✝

case hpr
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p✝ : k[X]
i✝ : ℕ
a✝ : Prime p✝
⊢ divRadical (p✝ ^ i✝) ∣ derivative (p✝ ^ i✝)

case hcp
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ y✝ : k[X]
a✝² : IsRelPrime x✝ y✝
a✝¹ : divRadical x✝ ∣ derivative x✝
a✝ : divRadical y✝ ∣ derivative y✝
⊢ divRadical (x✝ * y✝) ∣ derivative (x✝ * y✝)
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case pos
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a = 0
⊢ radical a ∣ a

Tactic:
rw [ha]
    apply dvd_zero

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
a✝ : Nontrivial M
⊢ radical (a * b) ∣ radical a * radical b

Tactic:
simp [radical_dvd_iff_primeFactors_subset, primeFactors_mul_eq_union,
    primeFactors_mul_eq_union ha hb, primeFactors_radical]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ⋯
w : ℚ := ⋯
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := ⋯
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ⋯
n : ℤ := ⋯
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 1
⊢ (m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1

Tactic:
apply coprime_sq_sub_sq_add_of_even_odd hmncp hm2 hn2

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I J : FractionalIdeal R⁰ K
⊢ ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / ↑|(Algebra.norm ℤ) ↑I.den * (Algebra.norm ℤ) ↑J.den| =
    ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / (↑|(Algebra.norm ℤ) ↑I.den| * ↑|(Algebra.norm ℤ) ↑J.den|)

Tactic:
Int.cast_abs,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I J : FractionalIdeal R⁰ K
⊢ ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / |↑((Algebra.norm ℤ) ↑I.den * (Algebra.norm ℤ) ↑J.den)| =
    ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / (↑|(Algebra.norm ℤ) ↑I.den| * ↑|(Algebra.norm ℤ) ↑J.den|)
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I J : FractionalIdeal R⁰ K
⊢ ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / |↑((Algebra.norm ℤ) ↑I.den * (Algebra.norm ℤ) ↑J.den)| =
    ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / (↑|(Algebra.norm ℤ) ↑I.den| * ↑|(Algebra.norm ℤ) ↑J.den|)

Tactic:
Int.cast_abs,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I J : FractionalIdeal R⁰ K
⊢ ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / |↑((Algebra.norm ℤ) ↑I.den * (Algebra.norm ℤ) ↑J.den)| =
    ↑(Ideal.absNorm I.num) * ↑(Ideal.absNorm J.num) / (|↑((Algebra.norm ℤ) ↑I.den)| * ↑|(Algebra.norm ℤ) ↑J.den|)