mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ λ ∣ λ ^ (S.multiplicity - 1) * S.X

Tactic:
refine dvd_mul_of_dvd_left (dvd_pow_self _ (fun h ↦ ?_)) _
    rw [Nat.sub_eq_iff_eq_add (le_trans (by simp) S.two_le_multiplicity), zero_add] at h
    simpa [h] using S.two_le_multiplicity

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (∑ i_1, A (i, i_1) * x i_1)

Tactic:
fun_prop

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
H₀ : 1 ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x
hι' : Nonempty ι'
h : (fun j ↦ ∑ i, A (j, i) * x i) ≠ 0
hA : A ≠ 0
hx : x ≠ 0
⊢ Function.HasFiniteMulSupport fun i ↦ (⨆ i_1, ↑i (A i_1)) * ⨆ i_1, ↑i (x i_1)

Tactic:
fun_prop

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

Goal state before:
pp: 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 ι'
⊢ Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (constantCoeff (p i))

Tactic:
fun_prop

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

Goal state before:
pp: 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 ι'
⊢ Function.HasFiniteMulSupport fun v ↦ ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
fun_prop

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ ∀ b ∈ s, Function.HasFiniteMulSupport fun a ↦ max (↑a (x b)) 1

Tactic:
fun_prop

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ Function.HasFiniteMulSupport fun v ↦ max (↑v (∑ a ∈ s, x a)) 1

Tactic:
fun_prop

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ Function.HasFiniteMulSupport fun a ↦ ∏ b ∈ s, max (↑a (x b)) 1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : a ∈ Ioi 1
⊢ ↑a ≠ 1

Tactic:
← Complex.ofReal_one,

Goal state after:
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : a ∈ Ioi 1
⊢ ↑a ≠ ↑1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case refine_1
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableAt ℂ (fun s ↦ s - 1) s

Tactic:
fun_prop

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

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
⊢ Function.HasFiniteMulSupport fun v ↦ ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
fun_prop

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

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
⊢ Function.HasFiniteMulSupport fun i ↦ (⨆ i_1, ↑i (x i_1)) ^ N

Tactic:
fun_prop

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

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
⊢ Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v ((eval x) (p i))

Tactic:
fun_prop

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

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
this : Nonempty ι'
F : Function.HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)
⊢ Function.HasFiniteMulSupport fun i ↦ (⨆ j, max (⨆ s, ↑i (coeff (↑s) (p j))) 1) * (⨆ i_1, ↑i (x i_1)) ^ N

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case inl
⊢ riemannZeta ((starRingEnd ℂ) 1) = (starRingEnd ℂ) (riemannZeta 1)

Tactic:
have h : riemannZeta 1 = ((γ - Real.log (4 * π)) / 2 : ℝ) := by
      rw [riemannZeta_one, ofReal_div, ofReal_sub, ofReal_log (by positivity : (0 : ℝ) ≤ 4 * π)]
      norm_cast

Goal state after:
case inl
h : riemannZeta 1 = ↑((γ - Real.log (4 * π)) / 2)
⊢ riemannZeta ((starRingEnd ℂ) 1) = (starRingEnd ℂ) (riemannZeta 1)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ ∑ x ∈ univ \ {1}, χ (x / (1 - x)) + χ 0 = -χ (-1)

Tactic:
χ.map_zero,

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
⊢ ∑ x ∈ univ \ {1}, χ (x / (1 - x)) + 0 = -χ (-1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ Differentiable ℂ fun s ↦ 1 + (s - 1) * riemannZeta₀ s

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ DifferentiableAt ℂ (fun s ↦ s - 1) 1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ DifferentiableAt ℂ riemannZeta₀ 1

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ DifferentiableAt ℂ (fun s ↦ (s - 1)⁻¹) s

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ DifferentiableAt ℂ riemannZeta₀ s

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ DifferentiableAt ℂ (fun s ↦ s - 1) s

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ DifferentiableAt ℂ riemannZeta₁ s

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e'_3
s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ -(s - 1)⁻¹ ^ 2 * riemannZeta₁ s + (s - 1)⁻¹ * deriv riemannZeta₁ s = deriv (fun s ↦ (s - 1)⁻¹ * riemannZeta₁ s) s

pp: case convert_3
s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ riemannZeta =ᶠ[𝓝 s] fun s ↦ (s - 1)⁻¹ * riemannZeta₁ s

Tactic:
· rw [deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_inv'' (by fun_prop) (by exact this)]
    simp [field]

Goal state after:
case convert_3
s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ riemannZeta =ᶠ[𝓝 s] fun s ↦ (s - 1)⁻¹ * riemannZeta₁ s
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ Differentiable ℝ riemannZeta₀

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ ContinuousAt (fun x ↦ x) 1

Tactic:
fun_prop

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') h.root = h'.root

Tactic:
by simp [algEquiv_def]

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
U : Type u_2
inst✝¹ : Ring U
inst✝ : Algebra R U
h'' : IsAdjoinRoot U f
x : S
⊢ (h'.algEquiv h'') ((h.algEquiv h') x) = (h.algEquiv h'') x

Tactic:
by simp [algEquiv_def]

Goal state after:
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

Tactic:
jacobiSum_eq_aux,

Goal state after:
case neg
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
⊢ ∃ z ∈ ℤ[μ],
    ∑ x, χ x + ∑ x, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1) = -1 + z * (μ - 1) ^ 2
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
x y : S
hxy : ∀ i < f.natDegree, h.coeff x i = h.coeff y i
i : Fin f.natDegree
⊢ h.basis.equivFun x i = h.basis.equivFun y i

Tactic:
rw [Basis.equivFun_apply, ← h.coeff_apply_coe, Basis.equivFun_apply, ← h.coeff_apply_coe,
        hxy i i.prop]

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

Goal state before:
pp: case refine_2
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s✝ : ℂ
hs✝ : s✝ ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
s : ℂ
hs : s ∈ {1}ᶜ
i : ℕ
h : i ∈ N.primeFactors
this : NeZero i
⊢ DifferentiableAt ℂ (fun s ↦ 1 - χ ↑i * ↑i ^ (-s)) s

Tactic:
fun_prop

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (fun s ↦ ↑N ^ (-s)) s

Tactic:
fun_prop

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

Goal state before:
pp: M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ : (changeLevel hMN) χ ≠ 1
p : ℕ
hp : p ∈ N.primeFactors
this : NeZero p
⊢ Continuous fun s ↦ 1 - χ ↑p * ↑p ^ (-s)

Tactic:
fun_prop

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
p : ℕ
hp : p ∈ N.primeFactors
this : NeZero p
⊢ Continuous fun s ↦ 1 - ↑p ^ (-s)

Tactic:
fun_prop

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
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
J' : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
hJ' : (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J'
⊢ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J') = J

Tactic:
rw [← hJ', Equiv.symm_apply_apply _ _, Subtype.coe_mk]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
⊢ LFunction (fun k ↦ 𝕖 (j * k)) s = expZeta (toAddCircle j) s

Tactic:
have hUc : IsPreconnected U := by
    by_cases h : j = 0
    · simpa only [h, ↓reduceIte, U] using!
        (isConnected_compl_singleton_of_one_lt_rank (by simp) _).isPreconnected
    · simpa only [h, ↓reduceIte, U] using isPreconnected_univ

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
⊢ LFunction (fun k ↦ 𝕖 (j * k)) s = expZeta (toAddCircle j) s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
s : ℂ
hs : s ≠ 1
H : deriv (LFunctionTrivChar₁ n) s = deriv (fun w ↦ (w - 1) * LFunctionTrivChar n w) s
⊢ DifferentiableAt ℂ (fun w ↦ w - 1) s

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
x y : ℝ
⊢ Continuous fun t ↦ ↑(k + 1) * bernoulliFun k t

Tactic:
fun_prop

Goal state after:
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
k✝ : ℕ
a✝ : k✝ < m
⊢ Continuous (bernoulliFun (k + 1))

Tactic:
fun_prop

Goal state after:
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
i✝ : ℕ
a✝ : i✝ ∈ Finset.range m
⊢ Continuous fun x ↦ bernoulliFun (k + 1) (x + ↑i✝ / ↑m)

Tactic:
fun_prop

Goal state after:
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
⊢ Continuous fun x ↦ bernoulliFun (k + 1) (↑m * x)

Tactic:
fun_prop

Goal state after:
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
⊢ Continuous fun x ↦ ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k 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)
⊢ ∀ (x : ℝ), f k x = 0

Tactic:
induction k with
  | zero =>
    intro x
    simp only [f, bernoulliFun_zero, pow_zero, one_div, Finset.sum_const, Finset.card_range,
      nsmul_eq_mul, mul_one, sub_eq_zero]
    rw [inv_mul_cancel₀ (Nat.cast_ne_zero.mpr m0)]
  | succ k h =>
    have d (x) : HasDerivAt (f (k + 1)) (m * (k + 1) * f k x) x := by
      simp only [f, mul_sub, Finset.mul_sum, pow_succ, mul_div_cancel_right₀ _ m0',
        ← mul_assoc, mul_comm _ (_ / _), div_mul_cancel₀ _ m0']
      apply HasDerivAt.sub
      · rw [mul_assoc, mul_comm (m : ℝ) _, ← Nat.cast_add_one]
        exact (hasDerivAt_bernoulliFun _ _).comp _ (hasDerivAt_const_mul ..)
      · refine HasDerivAt.fun_sum fun i _ ↦ ?_
        simp only [mul_assoc, ← Nat.cast_add_one]
        apply HasDerivAt.const_mul
        rw [← mul_one (_ * _)]
        exact (hasDerivAt_bernoulliFun _ _).comp _ ((hasDerivAt_id' _).add_const _)
    simp only [h, mul_zero] at d
    have fc (x) : f (k + 1) x = f (k + 1) 0 :=
      is_const_of_deriv_eq_zero (fun _ ↦ (d _).differentiableAt) (fun _ ↦ (d _).deriv) x 0
    generalize f (k + 1) 0 = c at fc
    have i : ∫ x in (0 : ℝ)..m⁻¹, f (k + 1) x = 0 := by
      simp only [f]
      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]
      · right
        rw [intervalIntegral.integral_finsetSum]
        · simp only [intervalIntegral.integral_comp_add_right, zero_add, ← one_div, ← add_div,
            add_comm (1 : ℝ), ← Nat.cast_add_one]
          rw [intervalIntegral.sum_integral_adjacent_intervals]
          · simp [div_self m0', integral_bernoulliFun_eq_zero]
          · intros; exact Continuous.intervalIntegrable (by fun_prop) _ _
        · intros; exact Continuous.intervalIntegrable (by fun_prop) _ _
      · exact Continuous.intervalIntegrable (by fun_prop) _ _
      · exact Continuous.intervalIntegrable (by fun_prop) _ _
    simp only [fc, intervalIntegral.integral_const, sub_zero, smul_eq_mul, mul_eq_zero, inv_eq_zero,
      Nat.cast_eq_zero, m0, false_or] at i
    simpa only [i] using fc

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

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaOdd (↑x) (1 - 2 * (↑k + 1)) = 0

Tactic:
show (1 : ℂ) - 2 * (k + 1) = -2 * k - 1 by ring,

Goal state after:
x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaOdd (↑x) (-2 * ↑k - 1) = 0
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Differentiable ℂ fun s ↦ ↑N ^ (-s)

Tactic:
fun_prop

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
⊢ DifferentiableAt ℂ (fun x ↦ ↑N ^ (-x)) s

Tactic:
fun_prop

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : s ≠ 1
⊢ DifferentiableAt ℂ (fun x ↦ ∑ j, Φ j) s

Tactic:
fun_prop

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs₀ : s ≠ 0 ∨ Φ 0 = 0
hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0
h : s ≠ 1
⊢ DifferentiableAt ℂ (HSub.hSub 1) s

Tactic:
fun_prop

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
⊢ ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
rw [ContinuousMap.coe_mk]

Goal state after:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
⊢ ∀ (n : ℤ), fourierCoeff (ofReal ∘ periodizedBernoulli k) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case inr.inr
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
x : ℝ
m : ℕ
hm : m ≠ n + 1
H : n + 1 < m
⊢ F x m = (↑n + 1) ^ ↑x * term f (↑x) m

Tactic:
· simp [H, term, (n.zero_lt_succ.trans H).ne', F, cpow_mul_div_cpow_eq_div_div_cpow]

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (0 + (1 + I * ↑y))
⊢ ContinuousAt (fun x ↦ ↑x + (1 + I * ↑y)) 0

Tactic:
fun_prop

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
y : ℝ
hy : y ≠ 0 ∨ χ ≠ 1
this : ContinuousAt (LFunction χ) (0 + (1 + I * ↑y))
⊢ (fun x ↦ LFunction χ (↑x + (1 + I * ↑y))) =O[𝓝 0] fun x ↦ 1

Tactic:
exact this.comp (f := fun x : ℝ ↦ x + (1 + I * y)) (x := 0) (by fun_prop) |>.tendsto.isBigO_one ℂ

Goal state after: