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

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
h : n < 0
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ↑n * (((↑n + 1) ^ (-(s + 1) + 1) - ↑n ^ (-(s + 1) + 1)) / (-(s + 1) + 1)) = ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)

Tactic:
·

Goal state after:
case e_a
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n) (↑n + 1), 0 < x
this : 0 ∉ uIcc (↑n) (↑n + 1)
⊢ ↑n * (((↑n + 1) ^ (-(s + 1) + 1) - ↑n ^ (-(s + 1) + 1)) / (-(s + 1) + 1)) = ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Solution'_descent.multiplicity = S.multiplicity - 1

Tactic:
refine multiplicity_eq_of_dvd_of_not_dvd
    (by simp [Solution'_descent]) (fun h ↦ S.lambda_not_dvd_X ?_)
  obtain ⟨k, hk : λ ^ (S.multiplicity - 1) * S.X = λ ^ (S.multiplicity - 1 + 1) * k⟩ := h
  rw [pow_succ, mul_assoc] at hk
  simp only [mul_eq_mul_left_iff, pow_eq_zero_iff', hζ.zeta_sub_one_prime'.ne_zero, ne_eq,
    false_and, or_false] at hk
  simp [hk]

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

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : IsEmpty ι
⊢ (logHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(totalWeight K) * log ↑(Nat.card ι) + logHeight A + logHeight x

pp: case inr
K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : Nonempty ι
⊢ (logHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(totalWeight K) * log ↑(Nat.card ι) + logHeight A + logHeight x

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝³ : Field K
ι : Type u_2
ι' : Type u_3
inst✝² : Fintype ι
inst✝¹ : Finite ι'
inst✝ : AdmissibleAbsValues K
A : ι' × ι → K
x : ι → K
hι : IsEmpty ι
⊢ (logHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(totalWeight K) * log ↑(Nat.card ι) + logHeight A + logHeight x
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inl
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
N : ℕ
x : ι → K
hp : IsHomogeneous 0 N
⊢ v ((eval x) 0) ≤ (⨆ s, v (coeff (↑s) 0)) * (⨆ i, v (x i)) ^ N

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
⊢ v ((eval x) p) ≤ (⨆ s, v (coeff (↑s) p)) * (⨆ i, v (x i)) ^ N

Tactic:
·

Goal state after:
case inl
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
N : ℕ
x : ι → K
hp : IsHomogeneous 0 N
⊢ v ((eval x) 0) ≤ (⨆ s, v (coeff (↑s) 0)) * (⨆ 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, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1))

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, 1 / (s - 1) * (1 / ↑(x + 1) ^ (s - 1) - 1 / (↑(x + 1) + 1) ^ (s - 1)) =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
hN,

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

Goal state before:
pp: case e_a.e_f
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
v : AbsoluteValue K ℝ
⊢ ⨆ i, v (x i.1 * y i.2) = (⨆ i, v (x i)) * ⨆ i, v (y i)

pp: case e_a
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
v : ↑nonarchAbsVal
⊢ ⨆ i, ↑v (x i.1 * y i.2) = (⨆ i, ↑v (x i)) * ⨆ i, ↑v (y i)

Tactic:
·

Goal state after:
case e_a.e_f
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
v : AbsoluteValue K ℝ
⊢ ⨆ i, v (x i.1 * y i.2) = (⨆ i, v (x i)) * ⨆ i, v (y i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case e_a
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
v : ↑nonarchAbsVal
⊢ ⨆ i, ↑v (x i.1 * y i.2) = (⨆ i, ↑v (x i)) * ⨆ i, ↑v (y i)

Tactic:
·

Goal state after:
case e_a
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
v : ↑nonarchAbsVal
⊢ ⨆ i, ↑v (x i.1 * y i.2) = (⨆ i, ↑v (x i)) * ⨆ i, ↑v (y i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case b0
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)
⊢ 0 ≤ ⨆ s, v (coeff (↑s) p)

pp: case h₁
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) ≤ ⨆ s, v (coeff (↑s) p)

pp: case h₂
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)
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ (⨆ i, v (x i)) ^ N

Tactic:
·

Goal state after:
case b0
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)
⊢ 0 ≤ ⨆ s, v (coeff (↑s) p)
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.Height.MvPolynomial

Goal state before:
pp: case h₁
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) ≤ ⨆ s, v (coeff (↑s) p)

pp: case h₂
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)
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ (⨆ i, v (x i)) ^ N

Tactic:
·

Goal state after:
case h₁
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) ≤ ⨆ s, v (coeff (↑s) p)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
⊢ mulHeight (-0) = mulHeight 0

pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
hx : x ≠ 0
⊢ mulHeight (-x) = mulHeight x

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
⊢ mulHeight (-0) = mulHeight 0
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case h₂
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)
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ (⨆ i, v (x i)) ^ N

Tactic:
·

Goal state after:
case h₂
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)
⊢ ∏ x_1 ∈ s.support, v (x x_1) ^ s x_1 ≤ (⨆ i, v (x i)) ^ N
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : IsEmpty ι
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : Nonempty ι
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : IsEmpty ι
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
y : ι → K
hι : Nonempty ι
⊢ mulHeight (0 * y) ≤ mulHeight 0 * mulHeight y

pp: case inr.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
·

Goal state after:
case inr.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
y : ι → K
hι : Nonempty ι
⊢ mulHeight (0 * y) ≤ mulHeight 0 * mulHeight y
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inr.inr.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hι : Nonempty ι
hx : x ≠ 0
⊢ mulHeight (x * 0) ≤ mulHeight x * mulHeight 0

pp: case inr.inr.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
hι : Nonempty ι
hx : x ≠ 0
hy : y ≠ 0
⊢ mulHeight (x * y) ≤ mulHeight x * mulHeight y

Tactic:
·

Goal state after:
case inr.inr.inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hι : Nonempty ι
hx : x ≠ 0
⊢ mulHeight (x * 0) ≤ mulHeight x * mulHeight 0
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inl
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝ : IsEmpty ι'
⊢ (if archAbsVal.card = 0 then 1 else 0) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1

pp: case inr
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝ : Nonempty ι'
⊢ (if archAbsVal.card = 0 then 1 else 0) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1

Tactic:
·

Goal state after:
case inl
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝ : IsEmpty ι'
⊢ (if archAbsVal.card = 0 then 1 else 0) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case pos
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝¹ : IsEmpty ι'
h✝ : archAbsVal.card = 0
⊢ 1 * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1

pp: case neg
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝¹ : IsEmpty ι'
h✝ : ¬archAbsVal.card = 0
⊢ 0 * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1

Tactic:
·

Goal state after:
case pos
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝¹ : IsEmpty ι'
h✝ : archAbsVal.card = 0
⊢ 1 * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case neg
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝¹ : IsEmpty ι'
h✝ : ¬archAbsVal.card = 0
⊢ 0 * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1

Tactic:
·

Goal state after:
case neg
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝¹ : IsEmpty ι'
h✝ : ¬archAbsVal.card = 0
⊢ 0 * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝ : Nonempty ι'
⊢ (if archAbsVal.card = 0 then 1 else 0) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1

Tactic:
·

Goal state after:
case inr
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
ι' : Type u_6
inst✝ : AdmissibleAbsValues K
h✝ : Nonempty ι'
⊢ (if archAbsVal.card = 0 then 1 else 0) * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, 1 ≤ 1
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x y : ι → K
⊢ logHeight (x * y) ≤ logHeight x + logHeight y

Tactic:
simp only [logHeight_eq_log_mulHeight]
  pull (disch := positivity) log
  exact log_le_log (by positivity) <| mulHeight_mul_le ..

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

Goal state before:
pp: case inl
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
j : ι'
hs₀ : IsEmpty ↥(p j).support
⊢ HasFiniteMulSupport fun v ↦ max (⨆ s, ↑v (coeff (↑s) (p j))) 1

pp: case inr
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
j : ι'
hs₀ : Nonempty ↥(p j).support
⊢ HasFiniteMulSupport fun v ↦ max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
·

Goal state after:
case inl
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
h : Nonempty ι'
p : ι' → MvPolynomial ι K
j : ι'
hs₀ : IsEmpty ↥(p j).support
⊢ HasFiniteMulSupport fun v ↦ max (⨆ s, ↑v (coeff (↑s) (p j))) 1
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 / ↑(i + 1) ^ s - 1 / (↑(i + 1) + 1) ^ s) * ↑(i + 1) +
      (1 / ↑(N + 1) ^ s - 1 / (↑(N + 1) + 1) ^ s) * ↑(N + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s + 1 / (↑N + 1) ^ s - ↑(N + 1) / (↑(N + 1) + 1) ^ s

Tactic:
hN,

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
⊢ ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s + (1 / ↑(N + 1) ^ s - 1 / (↑(N + 1) + 1) ^ s) * ↑(N + 1) =
    ∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s + 1 / (↑N + 1) ^ s - ↑(N + 1) / (↑(N + 1) + 1) ^ s
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case c0
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
⊢ 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (constantCoeff (p i))

pp: case b0
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
⊢ 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod

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
⊢ (Multiset.map (fun v ↦ ⨆ i, v (constantCoeff (p i))) archAbsVal).prod ≤
    (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod

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
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (constantCoeff (p i)) ≤
    ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
·

Goal state after:
case c0
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
⊢ 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (constantCoeff (p 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)) ≤ ∑ i ∈ s, log (mulHeight₁ (x i))

Tactic:
← log_prod (fun _ _ ↦ by positivity)

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) ≤ ↑(#s) * ∏ i ∈ s, max (v (x i)) 1

pp: case refine_2
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
⊢ 1 ≤ ↑(#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) ≤ ↑(#s) * ∏ i ∈ s, max (v (x i)) 1
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case b0
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
⊢ 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod

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
⊢ (Multiset.map (fun v ↦ ⨆ i, v (constantCoeff (p i))) archAbsVal).prod ≤
    (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod

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
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (constantCoeff (p i)) ≤
    ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
·

Goal state after:
case b0
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
⊢ 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case refine_2
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
⊢ 1 ≤ ↑(#s) * ∏ i ∈ s, max (v (x i)) 1

Tactic:
·

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

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
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (constantCoeff (p i)) ≤
    ∏ᶠ (v : ↑nonarchAbsVal), ⨆ 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
⊢ (Multiset.map (fun v ↦ ⨆ i, v (constantCoeff (p i))) archAbsVal).prod ≤
    (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
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
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (constantCoeff (p i)) ≤
    ∏ᶠ (v : ↑nonarchAbsVal), ⨆ 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
⊢ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (constantCoeff (p i)) ≤
    ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1