mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ gaussSum χ' ψ.char * gaussSum φ' ψ.char *
      (gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ *
        jacobiSum (χ.ringHomComp (algebraMap F' FF'))⁻¹ (φ.ringHomComp (algebraMap F' FF'))⁻¹) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ * (algebraMap F' FF') ↑(Fintype.card F)

Tactic:
jacobiSum_mul_nontrivial Hχφ',

Goal state after:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ gaussSum χ' ψ.char * gaussSum φ' ψ.char * (gaussSum χ'⁻¹ ψ.char⁻¹ * gaussSum φ'⁻¹ ψ.char⁻¹) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ * (algebraMap F' FF') ↑(Fintype.card F)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ (fun s ↦ (riemannZeta s)⁻¹ - (s - 1)) =O[𝓝[≠] 1] fun s ↦ (s - 1) ^ 2

Tactic:
suffices (fun s ↦ (s - 1) * ((riemannZeta₁ s)⁻¹ - 1)) =O[𝓝 1] (fun s ↦ (s - 1) ^ 2) by
    refine (this.mono nhdsWithin_le_nhds).congr' ?_ .rfl
    filter_upwards [inv_riemannZeta_eq_sub_mul]
    simp +contextual [field]
  suffices (fun s ↦ ((riemannZeta₁ s)⁻¹ - 1)) =O[𝓝 1] (· - 1) by
    simpa [pow_two] using (isBigO_refl ..).mul this
  simpa using ((differentiable_riemannZeta₁.differentiableAt (x := 1)).inv (by simp)).isBigO_sub

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
⊢ R[h.root] = ⊤

Tactic:
rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top, aeval_root_eq_map]
  exact h.map_surjective

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
H : ∀ (n : ℤ), v ↑n ≤ 1
f : ι → ℤ
i : ι
hf : 1 ≤ v ↑(x i) * v ↑(f i)
hi : v (↑(x i) * ↑(f i)) = ⨆ i, v (↑(x i) * ↑(f i))
⊢ ⨆ i, v ↑(x i) = 1

Tactic:
replace hf : 1 ≤ v (x i) := hf.trans <| mul_le_of_le_one_right (apply_nonneg v _) (H _)

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
H : ∀ (n : ℤ), v ↑n ≤ 1
f : ι → ℤ
i : ι
hi : v (↑(x i) * ↑(f i)) = ⨆ i, v (↑(x i) * ↑(f i))
hf : 1 ≤ v ↑(x i)
⊢ ⨆ i, v ↑(x i) = 1
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝¹ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.Even
n : ℕ
inst✝ : NeZero n
⊢ LFunction χ (-(2 * ↑n)) = 0

Tactic:
by
  obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)
  exact_mod_cast hχ.LFunction_neg_two_mul_nat_add_one m

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s ↦ (s - 1) * (↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j / ↑N))

Tactic:
(by ring : Φ j / N = Φ j * (1 / N * 1)),

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
j : ZMod N
x✝ : j ∈ Finset.univ
⊢ Tendsto (fun s ↦ (s - 1) * (↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s))) (𝓝[≠] 1) (𝓝 (Φ j * (1 / ↑N * 1)))
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
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ∫ (x : ℝ) in 0..(↑m)⁻¹,
      bernoulliFun (k + 1) (↑m * x) - ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m) =
    0

Tactic:
rw [intervalIntegral.integral_sub, intervalIntegral.integral_comp_mul_left _ m0', mul_zero,
        mul_inv_cancel₀ m0', integral_bernoulliFun_eq_zero (by lia), smul_zero, sub_eq_zero,
        intervalIntegral.integral_const_mul, eq_comm (a := 0), mul_eq_zero]

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
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ↑m ^ (k + 1) / ↑m = 0 ∨ ∫ (x : ℝ) in 0..(↑m)⁻¹, ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m) = 0

case hf
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
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (fun x ↦ bernoulliFun (k + 1) (↑m * x)) volume 0 (↑m)⁻¹

case hg
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
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (fun x ↦ ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m)) volume 0
    (↑m)⁻¹
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ ↑(Real.cos (↑k * π)) * (-1) ^ (k + 1) = -1

Tactic:
← sub_zero (k * π),

Goal state after:
case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ ↑(Real.cos (↑k * π - 0)) * (-1) ^ (k + 1) = -1
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
simp [k1]

Goal state after:
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 / 2) + (↑(bernoulli k) + 0))
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
zero_div,

Goal state after:
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)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ ↑(Real.cos (↑k * π)) * (-↑1) ^ (k + 1) = -↑1

Tactic:
← sub_zero (k * π),

Goal state after:
case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ ↑(Real.cos (↑k * π - 0)) * (-↑1) ^ (k + 1) = -↑1
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ ↑⟨↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx').symm)
            ⟨↑⟨span {↑⟨Polynomial.map (Ideal.Quotient.mk I) Q, hQ⟩}, ⋯⟩, ⋯⟩),
        ⋯⟩ =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
dsimp only

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
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ ↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv (quotMapEquivQuotQuotMap hx hx').symm)
        ⟨span {Polynomial.map (Ideal.Quotient.mk I) Q}, ⋯⟩) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ ↑((IsDedekindDomain.idealFactorsFunOfQuotHom ⋯) ⟨span {Polynomial.map (Ideal.Quotient.mk I) Q}, ⋯⟩) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
IsDedekindDomain.idealFactorsFunOfQuotHom_coe_coe

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
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (Ideal.map (↑(quotMapEquivQuotQuotMap hx hx').symm)
        (Ideal.map (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          ↑⟨span {Polynomial.map (Ideal.Quotient.mk I) Q}, ⋯⟩)) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (Ideal.map (↑(quotMapEquivQuotQuotMap hx hx').symm)
        (Ideal.map (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          ↑⟨span {Polynomial.map (Ideal.Quotient.mk I) Q}, ⋯⟩)) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
dsimp only

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
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (Ideal.map (↑(quotMapEquivQuotQuotMap hx hx').symm)
        (Ideal.map (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (span {Polynomial.map (Ideal.Quotient.mk I) Q}))) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (Ideal.map (↑(quotMapEquivQuotQuotMap hx hx').symm)
        (Ideal.map (Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
          (span {Polynomial.map (Ideal.Quotient.mk I) Q}))) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
map_span,

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
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (Ideal.map (↑(quotMapEquivQuotQuotMap hx hx').symm)
        (span
          (⇑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})) ''
            {Polynomial.map (Ideal.Quotient.mk I) Q}))) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: Φ : ZMod 1 → ℂ
s : ℂ
⊢ Φ 0 * completedRiemannZeta s = Φ 1 * completedRiemannZeta s

Tactic:
Subsingleton.elim 0 1

Goal state after:
Φ : ZMod 1 → ℂ
s : ℂ
⊢ Φ 1 * completedRiemannZeta s = Φ 1 * completedRiemannZeta s
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
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (Ideal.map (↑(quotMapEquivQuotQuotMap hx hx').symm)
        (span
          {(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
              (Polynomial.map (Ideal.Quotient.mk I) Q)})) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
map_span,

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
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (span
        (⇑↑(quotMapEquivQuotQuotMap hx hx').symm ''
          {(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
              (Polynomial.map (Ideal.Quotient.mk I) Q)})) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case inl
⊢ riemannZeta (2 * ↑0) = (-1) ^ (0 + 1) * 2 ^ (2 * ↑0 - 1) * ↑π ^ (2 * 0) * ↑(bernoulli (2 * 0)) / ↑(2 * 0)!

pp: case inr
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (2 * ↑k) = (-1) ^ (k + 1) * 2 ^ (2 * ↑k - 1) * ↑π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!

Tactic:
· simp [riemannZeta_zero]
    norm_num

Goal state after:
case inr
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (2 * ↑k) = (-1) ^ (k + 1) * 2 ^ (2 * ↑k - 1) * ↑π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr.refine_2.hf
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := ⋯
H : ℂ → ℂ := ⋯
this : B.F = G * H
⊢ ContinuousAt G 1

pp: case hg
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := ⋯
H : ℂ → ℂ := ⋯
this : B.F = G * H
⊢ ContinuousAt H 1

Tactic:
· simpa only [G, continuousAt_update_same] using riemannZeta_residue_one

Goal state after:
case hg
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := ⋯
H : ℂ → ℂ := ⋯
this : B.F = G * H
⊢ ContinuousAt H 1
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ Summable fun y ↦ (↑↑(p, y).1)⁻¹ ^ (p, y).2 * (↑↑(p, y).1)⁻¹ ^ (3 / 2)

Tactic:
dsimp only

Goal state after:
case refine_1
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
⊢ Summable fun y ↦ (↑↑p)⁻¹ ^ y * (↑↑p)⁻¹ ^ (3 / 2)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun x ↦ ∑' (y : ℕ), (↑↑(x, y).1)⁻¹ ^ (x, y).2 * (↑↑(x, y).1)⁻¹ ^ (3 / 2)

Tactic:
dsimp only

Goal state after:
case refine_2
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
⊢ Summable fun x ↦ ∑' (y : ℕ), (↑↑x)⁻¹ ^ y * (↑↑x)⁻¹ ^ (3 / 2)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
s : ℂ
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
n : ℕ
hn : n ≠ 0
⊢ (if n = 0 then 0 else f n) = f n

Tactic:
by simp_rw [if_neg hn]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ π ^ 4 / 90 = (-1) ^ (2 + 1) * 2 ^ (2 * 2 - 1) * π ^ (2 * 2) * ↑(bernoulli (2 * 2)) / ↑(2 * 2)!

Tactic:
simp only [Nat.reduceAdd, Nat.reduceMul, Nat.add_one_sub_one]

Goal state after:
⊢ π ^ 4 / 90 = (-1) ^ 3 * 2 ^ 3 * π ^ 4 * ↑(bernoulli 4) / ↑4!
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ J(4 * a / 4 | b) = J(4 * a | b)

Tactic:
have : Int.gcd (2 : ℕ) b = 1 := by
    rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right,
      Nat.gcd_one_right]

Goal state after:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : (↑2).gcd ↑b = 1
⊢ J(4 * a / 4 | b) = J(4 * a | b)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.inr.inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this✝ : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
this : (Set.Icc y⁻¹ x⁻¹).Finite
h : 1 < x
⊢ Set.Icc x y ⊆ (Set.Icc y⁻¹ x⁻¹)⁻¹

Tactic:
Set.inv_Icc

Goal state after:
case inr.inr.inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this✝ : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
this : (Set.Icc y⁻¹ x⁻¹).Finite
h : 1 < x
⊢ Set.Icc x y ⊆ Set.Icc x⁻¹⁻¹ y⁻¹⁻¹
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : ¬a % 2 = 0
⊢ J(a | b) =
    have this := ⋯;
    fastJacobiSym a (b / 2)

Tactic:
dsimp only

Goal state after:
case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : b % 2 = 0
ha2 : ¬a % 2 = 0
⊢ J(a | b) = fastJacobiSym a (b / 2)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.refine_1
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : K
hi : i ∈ ↑t
hi' : ↑↑z < v i
⊢ ⟨v i, ⋯⟩ ≠ 0

Tactic:
exact Subtype.coe_injective.ne_iff.mp (hi'.trans' z0).ne'

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case neg
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : v c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
j : K
hj : j ∈ t
hcj : ¬v j ≤ ↑↑z
hj' : c ∈ {w | v w = v j}
⊢ (if hi' : v j ≤ ↑↑z then z else Units.mk0 ⟨v j, ⋯⟩ ⋯) = i

Tactic:
simp only [Set.mem_ofPred_eq] at hj'
      rw [dif_neg hcj]
      simp [← hj', hc]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
hGH : 𝒢.relIndex ℋ ≠ 0
⊢ IsCusp c 𝒢

Tactic:
rw [← Subgroup.inf_relIndex_right] at hGH

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
hGH : (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0
⊢ IsCusp c 𝒢
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
⊢ (∀ γ ∈ Γ, f ∣[k] γ = f) ↔ ∀ γ ∈ s, f ∣[k] γ = f

Tactic:
by
  constructor <;> intro h γ hγ
  · exact h γ (hΓ ▸ Subgroup.mem_closure_of_mem hγ)
  · apply Subgroup.closure_induction (p := fun γ _ ↦ f ∣[k] γ = f) h (by simp)
    · simp +contextual [SlashAction.slash_mul]
    · intro x hx hf
      rw [← hf, ← SlashAction.slash_mul]
      simp [hf]
    · simpa [← hΓ]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
τ : ℍ
⊢ ‖f τ‖ ≤ √C / τ.im ^ (↑k / 2)

Tactic:
specialize hC τ

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ ‖f τ‖ ≤ √C / τ.im ^ (↑k / 2)
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ∀ (τ : ℍ), ‖petersson (↑k) (⇑f) (⇑f) τ‖ ≤ C * max τ.im (1 / τ.im) ^ ↑k
⊢ ‖f τ‖ ≤ √C * max 1 (1 / τ.im ^ ↑k)

Tactic:
specialize hC τ

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖petersson (↑k) (⇑f) (⇑f) τ‖ ≤ C * max τ.im (1 / τ.im) ^ ↑k
⊢ ‖f τ‖ ≤ √C * max 1 (1 / τ.im ^ ↑k)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable

Goal state before:
pp: case inr
k : ℤ
⊢ DifferentiableOn ℂ (fun z ↦ 0 ^ (-k)) {z | 0 < z.im}

Tactic:
apply differentiableOn_const

Goal state after: