mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x - ↑n / x ^ 2 =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2

Tactic:
[

Goal state after:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x - ↑n / x ^ 2 =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ∫ (x : ℝ) in ↑n..↑n + 1, ↑n * (1 / x ^ 2) =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2

Tactic:
[

Goal state after:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ∫ (x : ℝ) in ↑n..↑n + 1, ↑n * (1 / x ^ 2) =
    (∫ (x : ℝ) in ↑n..↑n + 1, 1 / x) - ↑n * ∫ (x : ℝ) in ↑n..↑n + 1, 1 / x ^ 2
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * (((↑n + 1) ^ (-2 + 1) - ↑n ^ (-2 + 1)) / (-2 + 1)) =
    log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))

Tactic:
[

Goal state after:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
⊢ log (↑n + 1) - log ↑n - ↑n * (((↑n + 1) ^ (-2 + 1) - ↑n ^ (-2 + 1)) / (-2 + 1)) =
    log (↑n + 1) - log ↑n - ↑n * (1 / ↑n - 1 / (↑n + 1))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case zero
⊢ termSum 1 0 = log (↑0 + 1) - ↑(harmonic (0 + 1)) + 1

Tactic:
[

Goal state after:
case zero
⊢ termSum 1 0 = log (↑0 + 1) - ↑(harmonic (0 + 1)) + 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ Tendsto (fun N ↦ termSum 1 N) atTop (𝓝 (1 - γ))

Tactic:
[

Goal state after:
⊢ Tendsto (fun N ↦ termSum 1 N) atTop (𝓝 (1 - γ))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : Tendsto (fun x ↦ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) n = -↑(harmonic (n + 1)) + log (↑n + 1)

Tactic:
[

Goal state after:
this : Tendsto (fun x ↦ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -(eulerMascheroniSeq' ∘ fun a ↦ a + 1) n = -↑(harmonic (n + 1)) + log (↑n + 1)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ x⁻¹ = mulHeight₁ x

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ x⁻¹ = mulHeight₁ x
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ (fun I ↦ ∏ a, x a (I a)) ≠ 0

Tactic:
[

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ (fun I ↦ ∏ a, x a (I a)) ≠ 0
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ (Multiset.map (fun v ↦ ⨆ i, v (∏ a, x a (i a))) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∏ a, x a (i a)) =
    ∏ a, mulHeight (x a)

Tactic:
[

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
α : Type u
inst✝¹ : Fintype α
ι : α → Type v
inst✝ : ∀ (a : α), Finite (ι a)
x : (a : α) → ι a → K
hx : ∀ (a : α), x a ≠ 0
⊢ (Multiset.map (fun v ↦ ⨆ i, v (∏ a, x a (i a))) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (∏ a, x a (i a)) =
    ∏ a, mulHeight (x a)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ ∑ i ∈ p.support, v (coeff i p * ∏ i_1 ∈ i.support, x i_1 ^ i i_1) ≤
    ∑ i ∈ p.support, v (coeff i p) * (⨆ i, v (x i)) ^ N

Tactic:
[

Goal state after:
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ ∑ i ∈ p.support, v (coeff i p * ∏ i_1 ∈ i.support, x i_1 ^ i i_1) ≤
    ∑ i ∈ p.support, v (coeff i p) * (⨆ i, v (x i)) ^ N
Module: Mathlib.NumberTheory.Height.EllipticCurve

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
W : WeierstrassCurve K
inst✝ : W.IsElliptic
C₁ : ℝ
hC₁ : ∀ (x : Fin 3 → K), (logHeight fun j ↦ (eval x) (W.addSubMap j)) ≤ C₁ + ↑2 * logHeight x
C₂ : ℝ
h :
  ∀ (p : Fin 3 → MvPolynomial (Fin 3) K) {x : Fin 3 → K},
    (∀ (k : Fin 3), ∑ j, (eval x) (C ↑W.Δ'⁻¹ * W.addSubMapCoeff (k, j)) * (eval x) (p j) = x k ^ (2 + 2)) →
      C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (p j)
hC₂ : ∀ (x : Fin 3 → K), C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (W.addSubMap j)
⊢ ∃ C, ∀ (x : Fin 3 → K), |(logHeight fun i ↦ (eval x) (W.addSubMap i)) - 2 * logHeight x| ≤ C

Tactic:
refine ⟨max C₁ (-C₂), fun x ↦ abs_sub_le_iff.mpr ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
W : WeierstrassCurve K
inst✝ : W.IsElliptic
C₁ : ℝ
hC₁ : ∀ (x : Fin 3 → K), (logHeight fun j ↦ (eval x) (W.addSubMap j)) ≤ C₁ + ↑2 * logHeight x
C₂ : ℝ
h :
  ∀ (p : Fin 3 → MvPolynomial (Fin 3) K) {x : Fin 3 → K},
    (∀ (k : Fin 3), ∑ j, (eval x) (C ↑W.Δ'⁻¹ * W.addSubMapCoeff (k, j)) * (eval x) (p j) = x k ^ (2 + 2)) →
      C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (p j)
hC₂ : ∀ (x : Fin 3 → K), C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (W.addSubMap j)
x : Fin 3 → K
⊢ (logHeight fun i ↦ (eval x) (W.addSubMap i)) - 2 * logHeight x ≤ max C₁ (-C₂)

case refine_2
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
W : WeierstrassCurve K
inst✝ : W.IsElliptic
C₁ : ℝ
hC₁ : ∀ (x : Fin 3 → K), (logHeight fun j ↦ (eval x) (W.addSubMap j)) ≤ C₁ + ↑2 * logHeight x
C₂ : ℝ
h :
  ∀ (p : Fin 3 → MvPolynomial (Fin 3) K) {x : Fin 3 → K},
    (∀ (k : Fin 3), ∑ j, (eval x) (C ↑W.Δ'⁻¹ * W.addSubMapCoeff (k, j)) * (eval x) (p j) = x k ^ (2 + 2)) →
      C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (p j)
hC₂ : ∀ (x : Fin 3 → K), C₂ + ↑2 * logHeight x ≤ logHeight fun j ↦ (eval x) (W.addSubMap j)
x : Fin 3 → K
⊢ (2 * logHeight x - logHeight fun i ↦ (eval x) (W.addSubMap i)) ≤ max C₁ (-C₂)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ v (coeff s p * ∏ i ∈ s.support, x i ^ s i) ≤ (⨆ s, v (coeff (↑s) p)) * (⨆ i, v (x i)) ^ N

Tactic:
[

Goal state after:
case inr
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
s : ι →₀ ℕ
hs₁ : s ∈ p.support
hs₂ : v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ v (coeff s p * ∏ i ∈ s.support, x i ^ s i)
⊢ v (coeff s p * ∏ i ∈ s.support, x i ^ s i) ≤ (⨆ s, v (coeff (↑s) p)) * (⨆ i, v (x i)) ^ N
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
[

Goal state after:
case e_a
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ x ∈ Finset.range N, ↑(x + 1) / s * (1 / ↑(x + 1) ^ s - 1 / (↑(x + 1) + 1) ^ s) =
    1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) =
    ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|⁻¹

Tactic:
[

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a b : 𝓞 K
h_x_nezero : (algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b ≠ 0
hb : b ≠ 0
ha : a ≠ 0
⊢ ∏ᶠ (w : FinitePlace K), w ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b) =
    ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b)|⁻¹
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a.e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s
⊢ ∑ i ∈ Finset.range (N + 1), (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range (N + 1), 1 / (↑n + 1) ^ s - ↑(N + 1) / (↑(N + 1) + 1) ^ s

Tactic:
[

Goal state after:
case e_a.e_a.succ
s : ℝ
hs : 1 < s
N : ℕ
hN :
  ∑ i ∈ Finset.range N, (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s
⊢ ∑ i ∈ Finset.range (N + 1), (1 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) =
    ∑ n ∈ Finset.range (N + 1), 1 / (↑n + 1) ^ s - ↑(N + 1) / (↑(N + 1) + 1) ^ s
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ Tendsto (fun N ↦ termSum s N) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))

Tactic:
[

Goal state after:
s : ℝ
hs : 1 < s
⊢ Tendsto (fun N ↦ termSum s N) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / (s - 1) * (1 - 1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))

Tactic:
[

Goal state after:
case hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / (s - 1) * (1 - 1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1) ≤
    ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (1 + 1)

Tactic:
[

Goal state after:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1) ≤
    ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (1 + 1)
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:
rw [mem_compl_singleton_iff, ← Complex.ofReal_one, Ne, Complex.ofReal_inj]

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_2.refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x ↦ (f x - f 1) / (x - 1)⁻¹) (𝓝[≠] 1) (𝓝 0)

Tactic:
[

Goal state after:
case refine_2.refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun x ↦ (f x - f 1) / (x - 1)⁻¹) (𝓝[≠] 1) (𝓝 0)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case refine_2.refine_2.hf
f : ℂ → ℂ := ⋯
⊢ Tendsto (fun x ↦ f x * (x - 1)) (𝓝[≠] 1) (𝓝 (1 - 1))

Tactic:
[

Goal state after:
case refine_2.refine_2.hf
f : ℂ → ℂ := ⋯
⊢ Tendsto (fun x ↦ f x * (x - 1)) (𝓝[≠] 1) (𝓝 (1 - 1))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
[

Goal state after:
this :
  Tendsto (fun x ↦ riemannZeta x - 1 / (x - 1) + (1 / (x - 1) - 1 / x.Gammaℝ / (x - 1))) (𝓝[≠] 1)
    (𝓝 (↑γ + -(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ Tendsto (fun s ↦ riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 ((↑γ - Complex.log (4 * ↑π)) / 2))
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 }
hI : span (Set.range x) = span (Set.range fun i ↦ x ↑i)
hx₀ : (fun i ↦ ↑(x i)) ≠ 0
⊢ ↑(absNorm (span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1

Tactic:
[

Goal state after:
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 }
hI : span (Set.range x) = span (Set.range fun i ↦ x ↑i)
hx₀ : (fun i ↦ ↑(x i)) ≠ 0
⊢ ↑(absNorm (span (Set.range x))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(x i) = 1
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:
[

Goal state after:
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
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
ψ : AddChar F R
t : F
ht : t ∈ univ \ {0}
⊢ (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t

Tactic:
simp only [mem_sdiff, mem_univ, mem_singleton, true_and] at ht

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
ψ : AddChar F R
t : F
ht : ¬t = 0
⊢ (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
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
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, ∑ x_1, χ x_1 * φ (x - x_1) * ψ x

Tactic:
[

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
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, ∑ x_1, χ x_1 * φ (x - x_1) * ψ x
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
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ t ∈ univ \ {0}, (∑ x, χ t * (φ t * χ x * φ (1 - x))) * ψ t

Tactic:
[

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
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ t ∈ univ \ {0}, (∑ x, χ t * (φ t * χ x * φ (1 - x))) * ψ t
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
⊢ jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = ↑(Fintype.card F)

Tactic:
obtain ⟨n, hp, hc⟩ := FiniteField.card F (ringChar F)

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
⊢ jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = ↑(Fintype.card F)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
x : 𝓞 K
h : ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B
v : InfinitePlace K
⊢ ↑n ^ (totalWeight K - 1) * v ↑x ≤ ↑n ^ (totalWeight K - 1) * ⨆ i, v (![↑x, ↑n] i)

Tactic:
gcongr; exact Finite.le_ciSup_of_le 0 le_rfl

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

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

Tactic:
convert EventuallyEq.deriv_eq (f := fun s ↦ (s - 1)⁻¹ * riemannZeta₁ s) ?_

Goal state after:
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

case convert_3
s : ℂ
hs : s ≠ 1
this : s - 1 ≠ 0
⊢ riemannZeta =ᶠ[𝓝 s] fun s ↦ (s - 1)⁻¹ * riemannZeta₁ s
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
U : Type u_2
inst✝¹ : Ring U
inst✝ : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
⊢ ((h.ofAlgEquiv e).algEquiv h'') a = (e.symm.trans (h.algEquiv h'')) a

Tactic:
[

Goal state after:
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
U : Type u_2
inst✝¹ : Ring U
inst✝ : Algebra R U
h'' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
⊢ ((h.ofAlgEquiv e).algEquiv h'') a = (e.symm.trans (h.algEquiv h'')) a
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 : ι → ℤ
hf : v ↑(Finset.univ.gcd x) = v ↑(∑ a, x a * f a)
⊢ ⨆ i, v ↑(x i) = 1

Tactic:
[

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 : ι → ℤ
hf : v ↑(Finset.univ.gcd x) = v ↑(∑ a, x a * f a)
⊢ ⨆ i, v ↑(x i) = 1
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : Finset.univ.gcd x = 1
hx₀ : Int.cast ∘ x ≠ 0
⊢ mulHeight (Int.cast ∘ x) = ↑(⨆ i, |x i|)

Tactic:
[

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : Finset.univ.gcd x = 1
hx₀ : Int.cast ∘ x ≠ 0
⊢ mulHeight (Int.cast ∘ x) = ↑(⨆ i, |x i|)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC :
  ∀ {a b c d : K},
    ![a, b] ≠ 0 → ![c, d] ≠ 0 → C' * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ log (C' * mulHeight ![a✝, b✝] * mulHeight ![c✝, d✝]) ≤ log (mulHeight ![a✝ * c✝, a✝ * d✝ + b✝ * c✝, b✝ * d✝])

Tactic:
exact log_le_log (by positivity) (hC hab hcd)

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

Goal state before:
pp: case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) = ↑N ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Tactic:
rootNumber,

Goal state after:
case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) =
    ↑N ^ (s - 1 / 2) * ((gaussSum χ stdAddChar / I ^ if χ.Even then 0 else 1) / ↑N ^ (1 / 2)) * completedLFunction χ⁻¹ s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ContinuousOn (fun s ↦ -deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s)
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Tactic:
[

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ ContinuousOn (fun s ↦ -deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s)
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
⊢ ContinuousOn (fun s ↦ -(deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s))
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Tactic:
refine ((h.contDiff.continuous_deriv le_rfl).continuousOn.div
    h.continuous.continuousOn fun w hw ↦ ?_).neg

Goal state after:
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
w : ℂ
hw : w ∈ {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
⊢ LFunctionTrivChar₁ n w ≠ 0
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)! = (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ

Tactic:
[

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)! = (-1) ^ (k + 1) / (2 * ↑k) / (2 * ↑k).Gammaℂ
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ↑N ^ (-(1 - s)) *
      ∑ x,
        Φ x *
          (C *
            (cexp (-↑π * I * s / 2) * expZeta (toAddCircle x) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle x) s)) =
    ↑N ^ (s - 1) * C *
      (cexp (↑π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s)

Tactic:
[

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
⊢ ↑N ^ (-(1 - s)) *
      ∑ x,
        Φ x *
          (C *
            (cexp (-↑π * I * s / 2) * expZeta (toAddCircle x) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle x) s)) =
    ↑N ^ (s - 1) * C *
      (cexp (↑π * I * s / 2) * LFunction (𝓕 Φ) s + cexp (-↑π * I * s / 2) * LFunction (𝓕 fun x ↦ Φ (-x)) s)
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)! = (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ

Tactic:
[

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)! = (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ