mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ |↑((Algebra.norm ℤ) a) / ↑((Algebra.norm ℤ) 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
⊢ |↑((Algebra.norm ℤ) a) / ↑((Algebra.norm ℤ) b)| =
    |↑((Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a / (algebraMap (𝓞 K) K) b))|
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight (![x, 1] * ![y, 1]) ≤ mulHeight ![x, 1] * mulHeight ![y, 1]

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight (![x, 1] * ![y, 1]) ≤ mulHeight ![x, 1] * mulHeight ![y, 1]
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
hb₀ : ↑((Algebra.norm ℤ) b) ≠ 0
⊢ (Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a) = (Algebra.norm ℚ) ↑a

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ log (mulHeight₁ (x * y)) ≤ log (mulHeight₁ x) + log (mulHeight₁ y)

Tactic:
pull (disch := positivity) log

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ log (mulHeight₁ (x * y)) ≤ log (mulHeight₁ x * mulHeight₁ y)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case insert
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
b : ι
s : Finset ι
hb : b ∉ s
ih : mulHeight₁ (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)
⊢ mulHeight₁ (x b * ∏ i ∈ s, x i) ≤ mulHeight₁ (x b) * mulHeight₁ (∏ i ∈ s, x i)

Tactic:
]

Goal state after:
case insert
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
b : ι
s : Finset ι
hb : b ∉ s
ih : mulHeight₁ (∏ i ∈ s, x i) ≤ ∏ i ∈ s, mulHeight₁ (x i)
⊢ mulHeight₁ (x b * ∏ i ∈ s, x i) ≤ mulHeight₁ (x b) * mulHeight₁ (∏ i ∈ s, x i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
s : Finset ι
x : ι → K
⊢ log (mulHeight₁ (∏ i ∈ s, x i)) ≤ log (∏ i ∈ s, mulHeight₁ (x i))

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
s : Finset ι
x : ι → K
⊢ log (mulHeight₁ (∏ i ∈ s, x i)) ≤ log (∏ i ∈ s, mulHeight₁ (x i))
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : CommSemiring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedRing S
inst✝ : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ v (∑ i ∈ s, x i) ≤ ∑ _x ∈ s, ∏ i ∈ s, max (v (x i)) 1

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : CommSemiring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedRing S
inst✝ : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ v (∑ i ∈ s, x i) ≤ ∑ _x ∈ s, ∏ i ∈ s, max (v (x i)) 1
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : CommSemiring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedRing S
inst✝ : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ ∑ i ∈ s, v (x i) ≤ ∑ _x ∈ s, ∏ i ∈ s, max (v (x i)) 1

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : CommSemiring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedRing S
inst✝ : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ ∑ i ∈ s, v (x i) ≤ ∑ _x ∈ s, ∏ i ∈ s, max (v (x i)) 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
]

Goal state after:
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, term (i + 1) s) atTop (𝓝 (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s))
Module: Mathlib.NumberTheory.Height.MvPolynomial

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

Tactic:
]

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

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommSemiring S
inst✝¹ : LinearOrder S
inst✝ : IsOrderedRing S
v : AbsoluteValue R S
hv : IsNonarchimedean ⇑v
ι : Type u_3
s : Finset ι
x : ι → R
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ v (x i)) ≤ ∏ i ∈ s, max (v (x i)) 1

Tactic:
]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : CommSemiring S
inst✝¹ : LinearOrder S
inst✝ : IsOrderedRing S
v : AbsoluteValue R S
hv : IsNonarchimedean ⇑v
ι : Type u_3
s : Finset ι
x : ι → R
hs : s.Nonempty
⊢ (s.sup' hs fun i ↦ v (x i)) ≤ ∏ i ∈ s, max (v (x i)) 1
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: case hg
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / s * (∑ n ∈ Finset.range x, 1 / (↑n + 1) ^ s - ↑x / (↑x + 1) ^ s)) atTop
    (𝓝 (1 / s * (∑' (n : ℕ), 1 / (↑n + 1) ^ s - 0)))

Tactic:
]

Goal state after:
case hg
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / s * (∑ n ∈ Finset.range x, 1 / (↑n + 1) ^ s - ↑x / (↑x + 1) ^ s)) atTop
    (𝓝 (1 / s * (∑' (n : ℕ), 1 / (↑n + 1) ^ s - 0)))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ 𝓝 0 = 𝓝 0

pp: s : ℝ
hs : 1 < s
⊢ s - 1 ≠ 0

Tactic:
]

Goal state after:
s : ℝ
hs : 1 < s
⊢ s - 1 ≠ 0
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
]

Goal state after:
case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n ↦ (1 / ↑(n + 1)) ^ (s - 1)) atTop (𝓝 (0 ^ (s - 1)))
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
⊢ (Multiset.map (fun v ↦ max (v (∑ a ∈ s, x a)) 1) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), max (↑v (∑ a ∈ s, x a)) 1 ≤
    (Multiset.map (fun i ↦ Function.const (AbsoluteValue K ℝ) (↑(#s)) i * ∏ a ∈ s, max (i (x a)) 1) archAbsVal).prod *
      ∏ᶠ (a : ↑nonarchAbsVal), ∏ b ∈ s, max (↑a (x b)) 1

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
hs : s.Nonempty
x : α → K
⊢ (Multiset.map (fun v ↦ max (v (∑ a ∈ s, x a)) 1) archAbsVal).prod *
      ∏ᶠ (v : ↑nonarchAbsVal), max (↑v (∑ a ∈ s, x a)) 1 ≤
    (Multiset.map (fun i ↦ Function.const (AbsoluteValue K ℝ) (↑(#s)) i * ∏ a ∈ s, max (i (x a)) 1) archAbsVal).prod *
      ∏ᶠ (a : ↑nonarchAbsVal), ∏ b ∈ s, max (↑a (x b)) 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = ↑(n + 1) / ↑(n + 1) ^ s

pp: case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 ≤ ↑(n + 1)

pp: case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0

Tactic:
]

Goal state after:
s : ℝ
hs : 1 < s
n : ℕ
⊢ (↑n + 1) / (↑n + 1) ^ s = ↑(n + 1) / ↑(n + 1) ^ s

case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 0 ≤ ↑(n + 1)

case hx
s : ℝ
hs : 1 < s
n : ℕ
⊢ 1 / ↑(n + 1) ≠ 0
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s)

Tactic:
]

Goal state after:
s : ℝ
hs : 1 < s
⊢ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * (1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inl
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
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ 1 * mulHeight x ^ N

Tactic:
]

Goal state after:
case inr.inl
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
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ 1 * mulHeight x ^ N
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case h_bound
n : ℕ
s : ℝ
hs : 1 ≤ s
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1) → ‖(x - ↑(n + 1)) / x ^ (s + 1)‖ ≤ (x - ↑(n + 1)) / x ^ 2

Tactic:
]

Goal state after:
case h_bound
n : ℕ
s : ℝ
hs : 1 ≤ s
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1) → ‖(x - ↑(n + 1)) / x ^ (s + 1)‖ ≤ (x - ↑(n + 1)) / x ^ 2
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case h_bound
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 1 < x
⊢ (x - (↑n + 1)) / x ^ (s + 1) ≤ (x - (↑n + 1)) / x ^ 2

Tactic:
]

Goal state after:
case h_bound
n : ℕ
s : ℝ
hs : 1 ≤ s
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 1 < x
⊢ (x - (↑n + 1)) / x ^ (s + 1) ≤ (x - (↑n + 1)) / x ^ 2
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight₁ (Finset.univ.sum ![x, y]) ≤ 2 ^ totalWeight K * (mulHeight₁ x * mulHeight₁ y)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight₁ (Finset.univ.sum ![x, y]) ≤ 2 ^ totalWeight K * (mulHeight₁ x * mulHeight₁ y)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ ↑Finset.univ.card ^ totalWeight K * ∏ a, mulHeight₁ (![x, y] a) ≤ 2 ^ totalWeight K * (mulHeight₁ x * mulHeight₁ y)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ ↑Finset.univ.card ^ totalWeight K * ∏ a, mulHeight₁ (![x, y] a) ≤ 2 ^ totalWeight K * (mulHeight₁ x * mulHeight₁ y)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ log (mulHeight₁ (x + y)) ≤ ↑(totalWeight K) * log 2 + log (mulHeight₁ x) + log (mulHeight₁ y)

Tactic:
pull (disch := positivity) log

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ log (mulHeight₁ (x + y)) ≤ log (2 ^ totalWeight K * mulHeight₁ x * mulHeight₁ y)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case bound_integrable
n : ℕ
⊢ IntervalIntegrable (fun x ↦ (x - ↑(n + 1)) / x ^ 2) volume (↑(n + 1)) (↑(n + 1) + 1)

Tactic:
]

Goal state after:
case bound_integrable
n : ℕ
⊢ IntervalIntegrable (fun x ↦ (x - ↑(n + 1)) / x ^ 2) volume (↑(n + 1)) (↑(n + 1) + 1)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight₁ (x + -y) ≤ 2 ^ totalWeight K * mulHeight₁ x * mulHeight₁ (-y)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ mulHeight₁ (x + -y) ≤ 2 ^ totalWeight K * mulHeight₁ x * mulHeight₁ (-y)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ logHeight₁ (x + -y) ≤ ↑(totalWeight K) * log 2 + logHeight₁ x + logHeight₁ (-y)

Tactic:
]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ logHeight₁ (x + -y) ≤ ↑(totalWeight K) * log 2 + logHeight₁ x + logHeight₁ (-y)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case h_cont
n : ℕ
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1) → ContinuousOn (fun x_1 ↦ (x - ↑(n + 1)) / x ^ (x_1 + 1)) (Ici 1)

Tactic:
]

Goal state after:
case h_cont
n : ℕ
⊢ ∀ᵐ (x : ℝ), x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1) → ContinuousOn (fun x_1 ↦ (x - ↑(n + 1)) / x ^ (x_1 + 1)) (Ici 1)
Module: Mathlib.NumberTheory.Height.Projectivization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : Projectivization K (ι → K)
⊢ log (Height.mulHeight x.rep) = log (Height.mulHeight x.rep)

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : Projectivization K (ι → K)
⊢ 1 ≤ Height.mulHeight x.rep

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : Projectivization K (ι → K)
⊢ 1 ≤ Height.mulHeight x.rep
Module: Mathlib.NumberTheory.Height.Projectivization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : Projectivization K (ι → K)
⊢ 0 ≤ log x.mulHeight

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : Projectivization K (ι → K)
⊢ 0 ≤ log x.mulHeight
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inr
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
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((eval x) (p i))) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i)) ≤
    ((Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod *
        ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) *
      ((Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) ^ N

Tactic:
]

Goal state after:
case inr.inr
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
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((eval x) (p i))) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i)) ≤
    ((Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod *
        ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) *
      ((Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) ^ N
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)

pp: n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ 0 ≤ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 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)

n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ 0 ≤ ∫ (x : ℝ) in ↑(n + 1)..↑(n + 1) + 1, (x - ↑(n + 1)) / x ^ (s + 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case h₁
n : ℕ
s : ℝ
hs : s ∈ Ici 1
x : ℝ
hx : x ∈ Ioc (↑(n + 1)) (↑(n + 1) + 1)
this : 1 ≤ x
⊢ 1 ≤ s

Tactic:
exact hs

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) * (X - C 1) = (∑ i ∈ range (n + 1), X ^ i) * (X - 1)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) * (X - C 1) = (∑ i ∈ range (n + 1), X ^ i) * (X - 1)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
]

Goal state after:
n : ℕ
s : ℝ
hs : s ∈ Ici 1
⊢ 0 ≤ ∫ (x : ℝ) in Ioc (↑(n + 1)) (↑(n + 1) + 1), (x - ↑(n + 1)) / x ^ (s + 1) ∂volume
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
⊢ Tendsto (fun s ↦ riemannZeta ↑s - 1 / (↑s - 1)) (𝓝[>] 1) (𝓝 ↑γ)

Tactic:
apply ((Complex.continuous_ofReal.tendsto _).comp this).congr'

Goal state after:
this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
⊢ (Complex.ofReal ∘ fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) =ᶠ[𝓝[>] 1] fun s ↦ riemannZeta ↑s - 1 / (↑s - 1)
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
⊢ (-1) ^ n = (-1) ^ n

Tactic:
]

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

Goal state before:
pp: this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ ∑' (a : ℕ), 1 / ↑((↑a + 1) ^ s) = ∑' (n : ℕ), 1 / (↑n + 1) ^ ↑s

Tactic:
]

Goal state after:
this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ ∑' (a : ℕ), 1 / ↑((↑a + 1) ^ s) = ∑' (n : ℕ), 1 / (↑n + 1) ^ ↑s
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inr
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
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((eval x) (p i))) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i)) ≤
    (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod *
        (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod ^ N *
      ((∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) *
        (∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) ^ N)

Tactic:
]

Goal state after:
case inr.inr
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
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((eval x) (p i))) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i)) ≤
    (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod *
        (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod ^ N *
      ((∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) *
        (∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) ^ N)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_f
this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
n : ℕ
⊢ 1 / ↑(↑n + 1) ^ ↑s = 1 / (↑n + 1) ^ ↑s

Tactic:
]

Goal state after:
case e_f
this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
n : ℕ
⊢ 1 / ↑(↑n + 1) ^ ↑s = 1 / (↑n + 1) ^ ↑s
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: aux2 : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - termTSum 1))
this : γ = 1 - termTSum 1
⊢ Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Tactic:
]

Goal state after:
aux2 : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - termTSum 1))
this : γ = 1 - termTSum 1
⊢ Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case h
⊢ Tendsto (fun x ↦ x * termTSum x) (𝓝[>] 1) (𝓝 (1 * termTSum 1))

Tactic:
]

Goal state after:
case h
⊢ Tendsto (fun x ↦ x * termTSum x) (𝓝[>] 1) (𝓝 (1 * termTSum 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:
]

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