mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ 1 * S.a + ↑η * S.b
⊢ p ∣ λ

Tactic:
have := dvd_mul_sub_mul_mul_gcd_of_dvd hpab hpaηb

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
p : 𝓞 K
hp : Prime p
hpab : p ∣ 1 * S.a + 1 * S.b
hpaηb : p ∣ 1 * S.a + ↑η * S.b
this : p ∣ (1 * ↑η - 1 * 1) * gcd S.a S.b
⊢ p ∣ λ
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
this : ∀ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal, a ≠ 0
⊢ (Multiset.map (fun x ↦ log x) (Multiset.map (fun v ↦ max (v x) 1) archAbsVal)).sum +
      log (∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1) =
    (Multiset.map (fun v ↦ log⁺ (v x)) archAbsVal).sum + ∑ᶠ (v : ↑nonarchAbsVal), log⁺ (↑v x)

Tactic:
Multiset.map_map,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
this : ∀ a ∈ Multiset.map (fun v ↦ max (v x) 1) archAbsVal, a ≠ 0
⊢ (Multiset.map ((fun x ↦ log x) ∘ fun v ↦ max (v x) 1) archAbsVal).sum + log (∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1) =
    (Multiset.map (fun v ↦ log⁺ (v x)) archAbsVal).sum + ∑ᶠ (v : ↑nonarchAbsVal), log⁺ (↑v x)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : λ ^ 2 ∣ λ ^ 4
X : 𝓞 K
hX : ↑S.u₅ * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = λ ^ 2 * X
Y : 𝓞 K
hY : S.Y ^ 3 + 1 = λ ^ 2 * Y
Z : 𝓞 K
hZ : S.Z ^ 3 - 1 = λ ^ 2 * Z
⊢ ∃ n, λ ^ 2 ∣ ↑S.u₄ - ↑n

Tactic:
refine ⟨1, X - Y - S.u₄ * Z, ?_⟩
    rw [show λ ^ 2 * (X - Y - S.u₄ * Z) = λ ^ 2 * X - λ ^ 2 * Y - S.u₄ * (λ ^ 2 * Z) by ring,
      ← hX, ← hY, ← hZ, ← formula2]
    ring

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₂
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
this : Nonempty ι'
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (constantCoeff (p i)) ≤
    ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
refine finprod_le_finprod (by fun_prop)
      (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass ..) (by fun_prop) ?_

Goal state after:
case h₂
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
this : Nonempty ι'
⊢ (fun v ↦ ⨆ i, ↑v (constantCoeff (p i))) ≤ fun v ↦ ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hg
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / s * (∑ n ∈ Finset.range x, 1 / (↑n + 1) ^ s - ↑x / (↑x + 1) ^ s)) atTop
    (𝓝 (1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Tactic:
rw [← sub_zero (tsum _)]
    apply (((Summable.hasSum ?_).tendsto_sum_nat).sub ?_).const_mul
    · exact_mod_cast (summable_nat_add_iff 1).mpr (summable_one_div_nat_rpow.mpr hs)
    · apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
              (h := fun n : ℕ ↦ (1 / ↑(n + 1) : ℝ) ^ (s - 1))
      · rw [show 𝓝 (0 : ℝ) = 𝓝 (0 ^ (s - 1)) by rw [zero_rpow]; linarith]
        refine Tendsto.rpow_const ?_ (Or.inr <| by linarith)
        exact (tendsto_const_div_atTop_nhds_zero_nat _).comp (tendsto_add_atTop_nat _)
      · intro n
        positivity
      · intro n
        dsimp only
        transitivity (n + 1) / (n + 1) ^ s
        · gcongr
          linarith
        · apply le_of_eq
          rw [rpow_sub_one, ← div_mul, div_one, mul_comm, one_div, inv_rpow, ← div_eq_mul_inv]
          · norm_cast
          all_goals positivity

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring S
f : R[X]
inst✝² : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝¹ : Ring T
inst✝ : Algebra R T
h' : IsAdjoinRoot T f
⊢ (↑(h.algEquiv h')).comp h.map = h'.map

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ ∀ (m : ℕ), f.natDegree ≤ m → { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.coeff m = 0

Tactic:
intro m

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
⊢ f.natDegree ≤ m → { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.coeff m = 0
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ (quotMapEquivQuotQuotMap hx hx')
      ((quotMapEquivQuotQuotMap hx hx').symm
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (Polynomial.map (Ideal.Quotient.mk I) Q))) =
    (quotMapEquivQuotQuotMap hx hx') ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))

Tactic:
quotMapEquivQuotQuotMap,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
Q : R[X]
⊢ ((quotAdjoinEquivQuotMap hx ⋯).symm.trans
        (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯)))
      (((quotAdjoinEquivQuotMap hx ⋯).symm.trans
            (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯))).symm
        ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (Polynomial.map (Ideal.Quotient.mk I) Q))) =
    ((quotAdjoinEquivQuotMap hx ⋯).symm.trans
        (((adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans (quotEquivOfEq ⋯)))
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
⊢ h.coeff h.root = Pi.single 1 1

Tactic:
rw [← h.coeff_root_pow hdeg, pow_one]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : R[α] = ⊤
⊢ (mkOfAdjoinEqTop hα hα₂).root = α

Tactic:
simp [IsAdjoinRoot.root]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : Free R S
α : S
hα : R[α] = ⊤
⊢ (mkOfAdjoinEqTop' hα).root = α

Tactic:
simp [IsAdjoinRoot.root]

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
⊢ Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count J
      (Multiset.map (fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)

Tactic:
by_cases hJ : J ∈ normalizedFactors (I.map (algebraMap R S))

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
⊢ Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count J
      (Multiset.map (fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)

case neg
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∉ normalizedFactors (Ideal.map (algebraMap R S) I)
⊢ Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count J
      (Multiset.map (fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
        (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach)
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: χ : DirichletCharacter ℂ 1
⊢ LFunction χ = riemannZeta

Tactic:
ext; rw [LFunction, ZMod.LFunction_modOne_eq, (by rfl : (0 : ZMod 1) = 1), map_one, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ bernoulliFun k 0 = ↑(bernoulli k)

Tactic:
bernoulliFun,

Goal state after:
k : ℕ
⊢ Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = ↑(bernoulli k)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 1
⊢ bernoulliFun k 1 = ↑(bernoulli k)

Tactic:
bernoulliFun,

Goal state after:
k : ℕ
hk : k ≠ 1
⊢ Polynomial.eval 1 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = ↑(bernoulli k)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
⊢ bernoulliFun k 1 = bernoulliFun k 0 + if k = 1 then 1 else 0

Tactic:
bernoulliFun,

Goal state after:
k : ℕ
⊢ Polynomial.eval 1 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) =
    bernoulliFun k 0 + if k = 1 then 1 else 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ cosZeta (↑x) (2 * ↑k) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
rw [← (hasSum_nat_cosZeta x (?_ : 1 < re (2 * k))).tsum_eq]

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ∑' (b : ℕ), ↑(Real.cos (2 * π * x * ↑b)) / ↑b ^ (2 * ↑k) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < (2 * ↑k).re
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case neg
k : ℕ
h : ¬k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli' k) + 0

Tactic:
add_zero,

Goal state after:
case neg
k : ℕ
h : ¬k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli' k)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x✝ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
⊢ HasDerivAt (f (k + 1)) (↑m * (↑k + 1) * f k x) x

Tactic:
simp only [f, mul_sub, Finset.mul_sum, pow_succ, mul_div_cancel_right₀ _ m0',
        ← mul_assoc, mul_comm _ (_ / _), div_mul_cancel₀ _ m0']

Goal state after:
m : ℕ
m0 : m ≠ 0
x✝ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
⊢ HasDerivAt
    (fun x ↦ bernoulliFun (k + 1) (↑m * x) - ∑ x_1 ∈ Finset.range m, ↑m ^ k * bernoulliFun (k + 1) (x + ↑x_1 / ↑m))
    (↑m * (↑k + 1) * bernoulliFun k (↑m * x) -
      ∑ x_1 ∈ Finset.range m, ↑m ^ k * (↑k + 1) * bernoulliFun k (x + ↑x_1 / ↑m))
    x
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / (2 * ↑k * Complex.Gamma (2 * ↑k)) =
    (-1) ^ (k + 1) / (2 * ↑k) / (2 * (2 * ↑π) ^ (-(2 * ↑k)) * Complex.Gamma (2 * ↑k))

Tactic:
cpow_neg,

Goal state after:
case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / (2 * ↑k * Complex.Gamma (2 * ↑k)) =
    (-1) ^ (k + 1) / (2 * ↑k) / (2 * ((2 * ↑π) ^ (2 * ↑k))⁻¹ * Complex.Gamma (2 * ↑k))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ cosZeta (↑x) (2 * ↑k) =
    (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
rw [cosZeta_two_mul_nat hk hx]
  congr 1
  have : (2 * k)! = (2 * k) * Complex.Gamma (2 * k) := by
    rw [(by { norm_cast; lia } : 2 * (k : ℂ) = ↑(2 * k - 1) + 1), Complex.Gamma_nat_eq_factorial,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ, Nat.sub_add_cancel (by lia)]
  simp_rw [this, Gammaℂ, cpow_neg, ← div_div, div_inv_eq_mul, div_mul_eq_mul_div, div_div,
    mul_right_comm (2 : ℂ) (k : ℂ)]
  norm_cast

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

Goal state before:
pp: case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ((2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)) =
    (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * (2 * ↑π) ^ (-(2 * ↑k + 1)) * Complex.Gamma (2 * ↑k + 1))

Tactic:
cpow_neg,

Goal state after:
case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ((2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)) =
    (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ((2 * ↑π) ^ (2 * ↑k + 1))⁻¹ * Complex.Gamma (2 * ↑k + 1))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case neg
k : ℕ
k1 : ¬k = 1
m : ↑(bernoulli k) + 0 = 2 ^ k / 2 * (0 + bernoulliFun k (1 / 2 + 0) + (↑(bernoulli k) + 0))
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
add_zero,

Goal state after:
case neg
k : ℕ
k1 : ¬k = 1
m : ↑(bernoulli k) = 2 ^ k / 2 * (0 + bernoulliFun k (1 / 2) + ↑(bernoulli k))
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaOdd (↑x) (1 - 2 * ↑k) = 0
⊢ hurwitzZetaEven (↑x) (1 - 2 * ↑k) + 0 =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
add_zero,

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaOdd (↑x) (1 - 2 * ↑k) = 0
⊢ hurwitzZetaEven (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e_a.e_a
k : ℕ
n : ℤ
hn : n ≠ 0
⊢ ↑(if k = 1 then 1 else 0) = if k = 1 then 1 else 0

Tactic:
split_ifs <;> simp only [ofReal_one, ofReal_zero]

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

Goal state before:
pp: ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
hf : ∀ i ∈ S, LSeriesSummable (f i) s
⊢ LSeries (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries (f i) s

Tactic:
by
  simpa [LSeries, term_sum] using Summable.tsum_finsetSum hf

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
⊢ (fun x ↦ LFunctionTrivChar N (1 + ↑x)) =O[𝓝[>] 0] fun x ↦ 1 / ↑x

Tactic:
have : (fun w : ℂ ↦ LFunctionTrivChar N (1 + w)) =O[𝓝[≠] 0] (1 / ·) := by
    have H : Tendsto (fun w ↦ w * LFunctionTrivChar N (1 + w)) (𝓝[≠] 0)
        (𝓝 <| ∏ p ∈ N.primeFactors, (1 - (p : ℂ)⁻¹)) := by
      convert! (LFunctionTrivChar_residue_one (N := N)).comp (f := fun w ↦ 1 + w) ?_ using 1
      · simp only [Function.comp_def, add_sub_cancel_left]
      · simpa only [tendsto_iff_comap, Homeomorph.coe_addLeft, add_zero, map_le_iff_le_comap] using
          ((Homeomorph.addLeft (1 : ℂ)).map_punctured_nhds_eq 0).le
    exact (isBigO_mul_iff_isBigO_div eventually_mem_nhdsWithin).mp <| H.isBigO_one ℂ

Goal state after:
N : ℕ
inst✝ : NeZero N
this : (fun w ↦ LFunctionTrivChar N (1 + w)) =O[𝓝[≠] 0] fun x ↦ 1 / x
⊢ (fun x ↦ LFunctionTrivChar N (1 + ↑x)) =O[𝓝[>] 0] fun x ↦ 1 / ↑x
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ↑(residueClass a n)) s = -(↑q.totient)⁻¹ * ∑ χ, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s)

Tactic:
simp only [deriv_LFunction_eq_deriv_LSeries _ hs, LFunction_eq_LSeries _ hs, neg_mul, ← mul_neg,
    ← Finset.sum_neg_distrib, ← neg_div, ← LSeries_twist_vonMangoldt_eq _ hs]

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ↑(residueClass a n)) s = (↑q.totient)⁻¹ * ∑ x, x a⁻¹ * L ((fun x_1 ↦ x ↑x_1) * fun n ↦ ↑(Λ n)) s
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ (↑q.totient)⁻¹ *
      (-(deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s) -
        ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s) =
    -(↑q.totient)⁻¹ * ∑ χ, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) - (↑q.totient)⁻¹ / (s - 1)

Tactic:
← neg_add',

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ (↑q.totient)⁻¹ *
      -(deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
          ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s) =
    -(↑q.totient)⁻¹ * ∑ χ, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) - (↑q.totient)⁻¹ / (s - 1)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
help : ∀ (x : ℝ), (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
H₀ :
  (fun x ↦ 1) =O[𝓝[>] 0] fun x ↦
    LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑t) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑t)
H : (fun x ↦ 1) =O[𝓝[>] 0] fun x ↦ ‖x‖
⊢ False

Tactic:
exact isLittleO_irrefl (.of_forall (fun _ ↦ one_ne_zero)) <|
    H.of_norm_right.trans_isLittleO <| isLittleO_id_one.mono nhdsWithin_le_nhds

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

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
⊢ False

Tactic:
rcases le_or_gt (C + C') 0 with h₀ | h₀

Goal state after:
case inl
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : C + C' ≤ 0
⊢ False

case inr
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : 0 < C + C'
⊢ False
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
⊢ ContinuousOn (fun t ↦ t ^ (-s - 1)) (Set.Ici 1)

Tactic:
exact fun t ht ↦ (Real.continuousAt_rpow_const _ _
      <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
hD : IsDiscrete R
hN : IsNontrivial R
hM : MulArchimedean (ValueGroupWithZero R)
⊢ Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))

Tactic:
isNontrivial_iff_nontrivial_units

Goal state after:
case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
hD : IsDiscrete R
hN : Nontrivial (ValueGroupWithZero R)ˣ
hM : MulArchimedean (ValueGroupWithZero R)
⊢ Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : ¬DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R

Tactic:
isNontrivial_iff_nontrivial_units

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : Nontrivial (ValueGroupWithZero R)ˣ
H : ¬DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : ¬IsNontrivial R
⊢ IsDiscrete R

Tactic:
isNontrivial_iff_nontrivial_units

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : ¬Nontrivial (ValueGroupWithZero R)ˣ
⊢ IsDiscrete R
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
⊢ ContinuousOn (fun t ↦ t ^ (-1 - 1)) (Set.Ici 1)

Tactic:
exact fun t ht ↦ (Real.continuousAt_rpow_const _ _
      <| Or.inl (zero_lt_one.trans_le ht).ne').continuousWithinAt

Goal state after: