mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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

Goal state before:
pp: h : Tendsto (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this : Tendsto ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ {z | 0 < z.re} ∈ 𝓝 1

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype R
inst✝ : CommRing R'
χ ψ : MulChar R R'
⊢ jacobiSum χ ψ = jacobiSum ψ χ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
inst✝³ : CommRing R
inst✝² : Fintype R
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ ψ : MulChar R R'
f : R' →+* R''
⊢ jacobiSum (χ.ringHomComp f) (ψ.ringHomComp f) = f (jacobiSum χ ψ)

Tactic:
by

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:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : AbsoluteValue K ℝ
⊢ v ∈ multisetInfinitePlace K ↔ IsInfinitePlace v

Tactic:
by

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ jacobiSum χ ψ = ∑ x ∈ univ \ {0, 1}, χ x * ψ (1 - x)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (AbsoluteValue K ℝ)
v : InfinitePlace K
⊢ Multiset.count (↑v) (multisetInfinitePlace K) = v.mult

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : CommMonoid M
f : AbsoluteValue K ℝ → M
v : InfinitePlace K
x✝ : v ∈ Finset.univ
⊢ ↑v ∈ (multisetInfinitePlace K).toFinset

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : CommMonoid M
f : AbsoluteValue K ℝ → M
w : AbsoluteValue K ℝ
hw : w ∈ (multisetInfinitePlace K).toFinset
⊢ f w ^ Multiset.count w (multisetInfinitePlace K) = f ↑⟨w, ⋯⟩ ^ InfinitePlace.mult ⟨w, ⋯⟩

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : CommMonoid M
f : AbsoluteValue K ℝ → M
⊢ (Multiset.map f (multisetInfinitePlace K)).prod = ∏ v, f ↑v ^ v.mult

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
v : AbsoluteValue K ℝ
hv : v ∈ {v | IsFinitePlace v}
⊢ ∃ v_1, place (FinitePlace.embedding v_1) = v

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : AddCommMonoid M
f : AbsoluteValue K ℝ → M
⊢ ∀ (a : AbsoluteValue K ℝ) (ha : a ∈ archAbsVal.toFinset), ⟨a, ⋯⟩ ∈ univ

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : AddCommMonoid M
f : AbsoluteValue K ℝ → M
⊢ ∀ a ∈ univ, ↑a ∈ archAbsVal.toFinset

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : AddCommMonoid M
f : AbsoluteValue K ℝ → M
⊢ ∀ (a : AbsoluteValue K ℝ) (ha : a ∈ archAbsVal.toFinset), ↑⟨a, ⋯⟩ = a

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : AddCommMonoid M
f : AbsoluteValue K ℝ → M
w : AbsoluteValue K ℝ
hw : w ∈ archAbsVal.toFinset
⊢ count w archAbsVal • f w = InfinitePlace.mult ⟨w, ⋯⟩ • f ↑⟨w, ⋯⟩

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : AddCommMonoid M
f : AbsoluteValue K ℝ → M
⊢ (Multiset.map f archAbsVal).sum = ∑ v, v.mult • f ↑v

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ mulHeight₁ x = (∏ v, max (v x) 1 ^ v.mult) * ∏ᶠ (v : FinitePlace K), max (v x) 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ logHeight₁ x = ∑ v, ↑v.mult * log⁺ (v x) + ∑ᶠ (v : FinitePlace K), log⁺ (v x)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
x : ι → K
hx : x ≠ 0
⊢ mulHeight x = (∏ v, (⨆ i, v (x i)) ^ v.mult) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (x i)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ totalWeight K = ∑ v, v.mult

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ totalWeight K = Module.finrank ℚ K

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 0 < totalWeight K

Tactic:
by

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

Goal state before:
pp: ⊢ Tendsto (fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))

Tactic:
by

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

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ jacobiSum χ ψ = ∑ x, χ x + ∑ x, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
by

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

Goal state before:
pp: ⊢ Tendsto (fun s ↦ riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 ((↑γ - Complex.log (4 * ↑π)) / 2))

Tactic:
by

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

Goal state before:
pp: ⊢ riemannZeta 1 = (↑γ - log (4 * ↑π)) / 2

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
m : ℕ
⊢ 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)

Tactic:
by

Goal state after:
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
⊢ ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1

Tactic:
by

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

Goal state before:
pp: ⊢ completedRiemannZeta₀ 1 = (↑γ - log (4 * ↑π)) / 2 + 1

Tactic:
by

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

Goal state before:
pp: this : (γ - Real.log (4 * π)) / 2 ≠ 0
⊢ 0 ≤ 4 * π

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
v : FinitePlace K
hn : ¬absNorm v.maximalIdeal.asIdeal = 0
h : ∀ {m : ℕ}, 0 < ↑(absNorm v.maximalIdeal.asIdeal ^ m)
⊢ 1 ≤ absNorm v.maximalIdeal.asIdeal

Tactic:
by

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

Goal state before:
pp: this : (γ - Real.log (4 * π)) / 2 ≠ 0
⊢ riemannZeta 1 ≠ 0

Tactic:
by

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

Goal state before:
pp: ⊢ 2 / 3 < 1

Tactic:
by

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

Goal state before:
pp: ⊢ 0 < 4 * π

Tactic:
by

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

Goal state before:
pp: ⊢ 2.7182818286 < 4 * 2

Tactic:
by

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

Goal state before:
pp: ⊢ 0 ≤ 4

Tactic:
by

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

Goal state before:
pp: ⊢ riemannZeta 1 ≠ 0

Tactic:
by

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

Goal state before:
pp: ⊢ 0 ≤ 4 * π

Tactic:
by

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

Goal state before:
pp: ⊢ riemannZeta 1 = ↑((γ - Real.log (4 * π)) / 2)

Tactic:
by

Goal state after:
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
this : ∀ x ∈ univ \ {0, 1}, (MulChar.trivial F R) x * (MulChar.trivial F R) (1 - x) = 1
⊢ ↑(#(univ \ {0, 1})) = ↑(Fintype.card F) - 2

Tactic:
by

Goal state after:
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
⊢ jacobiSum (MulChar.trivial F R) (MulChar.trivial F R) = ↑(Fintype.card F) - 2

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
⊢ 1 < ((starRingEnd ℂ) z).re

Tactic:
by

Goal state after:
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 \ {0, 1}, (1 x - 1) * (χ (1 - x) - 1) = 0

Tactic:
by

Goal state after:
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
⊢ jacobiSum 1 χ = -1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
⊢ ↑(absNorm (span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
n : ℕ
⊢ (↑n).arg ≠ π

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
n : ℕ
⊢ (starRingEnd ℂ) (1 / ↑n ^ (starRingEnd ℂ) z) = 1 / ↑n ^ z

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
⊢ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
ι : Type u_2
inst✝ : Finite ι
x : ι → 𝓞 K
hx : x ≠ 0
i₀ : ι
hi₀ : x i₀ ≠ 0 i₀
i' : { j // ↑(x j) ≠ 0 } := ⟨i₀, ⋯⟩
this : Nonempty { j // ↑(x j) ≠ 0 }
⊢ span (Set.range x) = span (Set.range fun i ↦ x ↑i)

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
hgz : ∀ (z : ℂ), 1 < z.re → (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z
⊢ 1 < Module.rank ℝ ℂ

Tactic:
by

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)
v : ↑nonarchAbsVal
x✝ : ι'
⊢ 0 ≤ max (⨆ s, ↑v (coeff (↑s) (p x✝))) 1

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
hgz : ∀ (z : ℂ), 1 < z.re → (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z
⊢ 2 ∈ {1}ᶜ

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
hgz : ∀ (z : ℂ), 1 < z.re → (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z
⊢ 2 ∈ {b | 1 < b.re}

Tactic:
by

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)
v : ↑nonarchAbsVal
⊢ 0 ≤ (⨆ i, ↑v (x i)) ^ N

Tactic:
by

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

Goal state before:
pp: s : ℂ
⊢ riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (riemannZeta s)

Tactic:
by

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
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N

Tactic:
by

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
⊢ max (mulHeightBound p) 1 > 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
ι : Type u_2
inst✝ : Finite ι
x : ι → 𝓞 K
hx : x ≠ 0
⊢ ↑(absNorm (span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ᶠ (s : ℂ) in 𝓝 1, riemannZeta s ≠ 0

Tactic:
by

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
⊢ 0 < mulHeight fun j ↦ (eval x) (p j)

Tactic:
by

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
⊢ (logHeight fun j ↦ (eval x) (p j)) ≤ log (max (mulHeightBound p) 1) + ↑N * logHeight x

Tactic:
by

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

Goal state before:
pp: ⊢ completedRiemannZeta₀ 0 = (↑γ - log (4 * ↑π)) / 2 + 1

Tactic:
by

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

Goal state before:
pp: K : Type u_6
inst✝² : Field K
ι : Type u_7
ι' : Type u_8
inst✝¹ : Fintype ι'
M N : ℕ
q : ι × ι' → MvPolynomial ι K
inst✝ : IsEmpty ι'
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
⊢ x = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
m n : ℕ
hn : n ≠ 0
a : 𝓞 K
f : 𝓞 K →ₗ[𝓞 K] 𝓞 K := LinearMap.mulLeft (𝓞 K) ↑n
x✝¹ : 𝓞 K
x✝ : f x✝¹ = 0
⊢ x✝¹ = 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
m n : ℕ
hn : n ≠ 0
a : 𝓞 K
f : 𝓞 K →ₗ[𝓞 K] 𝓞 K := LinearMap.mulLeft (𝓞 K) ↑n
hf : Function.Injective ⇑↑f
⊢ span {↑n * ↑m} = Submodule.map f (span {↑m})

Tactic:
by

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

Goal state before:
pp: ⊢ (1 - id) 0 ≠ 0

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
m n : ℕ
hn : n ≠ 0
a : 𝓞 K
f : 𝓞 K →ₗ[𝓞 K] 𝓞 K := LinearMap.mulLeft (𝓞 K) ↑n
hf : Function.Injective ⇑↑f
H₁ : span {↑n * ↑m} = Submodule.map f (span {↑m})
⊢ span {↑(n * m), ↑n * a} = Submodule.map f (span {↑m, a})

Tactic:
by

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

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
⊢ mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)

Tactic:
by

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

Goal state before:
pp: h₁ :
  HasDerivAt (id * completedRiemannZeta₀ - 1 - id / (1 - id))
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
      (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2)
    0
⊢ ↑π ∈ slitPlane

Tactic:
by

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

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ 0 < mulHeight x ^ M

Tactic:
by

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

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ 0 < max (mulHeightBound q) 1

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
m n : ℕ
hn : n ≠ 0
a : 𝓞 K
⊢ (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, a})) =
    (Submodule.toAddSubgroup (span {↑n * ↑m})).relIndex (Submodule.toAddSubgroup (span {↑(n * m), ↑n * a}))

Tactic:
by

Goal state after:
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)) = ∑ x ∈ univ \ {-1}, χ x

Tactic:
by

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

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
h✝ : Nonempty ι'
q' : ι × ι' → K := fun a ↦ (eval x) (q a)
H : mulHeight x ^ (M + N) ≤ ↑(Nat.card ι') ^ totalWeight K * mulHeight q' * mulHeight fun j ↦ (eval x) (p j)
⊢ (↑(Nat.card ι') ^ totalWeight K * (max (mulHeightBound q) 1 * mulHeight x ^ M) * mulHeight fun j ↦ (eval x) (p j)) =
    (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1 * mulHeight fun j ↦ (eval x) (p j)) * mulHeight x ^ M

Tactic:
by

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

Goal state before:
pp: K : Type u_6
inst✝³ : Field K
ι : Type u_7
ι' : Type u_8
inst✝² : Fintype ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι
M N : ℕ
q : ι × ι' → MvPolynomial ι K
hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M
p : ι' → MvPolynomial ι K
x : ι → K
h : ∀ (k : ι), ∑ j, (eval x) (q (k, j)) * (eval x) (p j) = x k ^ (M + N)
⊢ (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤ mulHeight fun j ↦ (eval x) (p j)

Tactic:
by

Goal state after: