mathlib-initiative/mathlib-tactics huggingface dataset:
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 ι'
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 ≤
    (Multiset.map (fun i ↦ (⨆ j, (p j).coeff.sum fun x c ↦ i c) * (⨆ i_1, i (x i_1)) ^ N) archAbsVal).prod

Tactic:
]

Goal state after:
case h₁
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 ≤
    (Multiset.map (fun i ↦ (⨆ j, (p j).coeff.sum fun x c ↦ i c) * (⨆ i_1, i (x i_1)) ^ N) archAbsVal).prod
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s - 1 ≠ 0
⊢ s - 1 ≠ 0

Tactic:
]

Goal state after:
case refine_2
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s - 1 ≠ 0
⊢ s - 1 ≠ 0
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
t : ℂ
ht : t ∈ {1}ᶜ
ht' : t = 1
⊢ f t - f 1 = 0

Tactic:
]

Goal state after:
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
t : ℂ
ht : t ∈ {1}ᶜ
ht' : t = 1
⊢ f t - f 1 = 0
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (-1) ^ (m + k) * ((∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k))

Tactic:
]

Goal state after:
case refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (-1) ^ (m + k) * ((∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k))
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 ι'
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
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
j : ι'
⊢ ((p j).coeff.sum fun x c ↦ v c) * (⨆ i, v (x i)) ^ N ≤ (⨆ j, (p j).coeff.sum fun x c ↦ v c) * (⨆ i, v (x i)) ^ N

Tactic:
]

Goal state after:
case h₁
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
v : AbsoluteValue K ℝ
x✝ : v ∈ archAbsVal
j : ι'
⊢ ((p j).coeff.sum fun x c ↦ v c) * (⨆ i, v (x i)) ^ N ≤ (⨆ j, (p j).coeff.sum fun x c ↦ v c) * (⨆ i, v (x i)) ^ N
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: case refine_2.e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ (∏ k ∈ range k, (μ ^ (k + 1) - 1)) * ∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1) =
    (∏ a ∈ range k, Z (a + 1) * (μ - 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)

Tactic:
]

Goal state after:
case refine_2.e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ ℤ[μ], μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k ↦ Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ ℤ[μ] ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ (∏ k ∈ range k, (μ ^ (k + 1) - 1)) * ∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1) =
    (∏ a ∈ range k, Z (a + 1) * (μ - 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
]

Goal state after:
h : Tendsto (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ Tendsto (fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
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 ι'
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), ⨆ i, ↑v ((eval x) (p i)) ≤
    ∏ᶠ (i : ↑nonarchAbsVal), (⨆ j, max (⨆ s, ↑i (coeff (↑s) (p j))) 1) * (⨆ i_1, ↑i (x i_1)) ^ N

Tactic:
]

Goal state after:
case h₂
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), ⨆ i, ↑v ((eval x) (p i)) ≤
    ∏ᶠ (i : ↑nonarchAbsVal), (⨆ j, max (⨆ s, ↑i (coeff (↑s) (p j))) 1) * (⨆ i_1, ↑i (x i_1)) ^ N
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))
⊢ Tendsto (fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))

Tactic:
]

Goal state after:
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))
⊢ Tendsto (fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
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'
⊢ ∑ i, ψ (1 - (Equiv.subLeft 1) i) * χ ((Equiv.subLeft 1) i) = ∑ x, ψ x * χ (1 - x)

Tactic:
]

Goal state after:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : Fintype R
inst✝ : CommRing R'
χ ψ : MulChar R R'
⊢ ∑ i, ψ (1 - (Equiv.subLeft 1) i) * χ ((Equiv.subLeft 1) i) = ∑ x, ψ x * χ (1 - x)
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
⊢ ∑ x, χ x * ψ (1 - x) = ∑ x, χ x + ∑ x, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
]

Goal state after:
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
⊢ ∑ x, χ x * ψ (1 - x) = ∑ x, χ x + ∑ x, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)
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))
this : {z | 0 < z.re} ∈ 𝓝 1
⊢ ∀ᶠ (x : ℂ) in 𝓝 1, x ∈ {1}ᶜ → ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) x = 1 / (x - 1) - 1 / x.Gammaℝ / (x - 1)

Tactic:
]

Goal state after:
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))
this : {z | 0 < z.re} ∈ 𝓝 1
⊢ ∀ᶠ (x : ℂ) in 𝓝 1, x ∈ {1}ᶜ → ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) x = 1 / (x - 1) - 1 / x.Gammaℝ / (x - 1)
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
⊢ ∏ m ∈ (multisetInfinitePlace K).toFinset, f m ^ Multiset.count m (multisetInfinitePlace K) = ∏ v, f ↑v ^ v.mult

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : CommMonoid M
f : AbsoluteValue K ℝ → M
⊢ ∏ m ∈ (multisetInfinitePlace K).toFinset, f m ^ Multiset.count m (multisetInfinitePlace K) = ∏ v, f ↑v ^ v.mult
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 ^ InfinitePlace.mult ⟨w, ?m.91⟩ = f ↑⟨w, ⋯⟩ ^ InfinitePlace.mult ⟨w, ⋯⟩

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
⊢ ∃ φ, place φ = w

Tactic:
]

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:
rw [count_multisetInfinitePlace_eq_mult ⟨w, _⟩]

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
⊢ ∑ m ∈ archAbsVal.toFinset, count m archAbsVal • f m = ∑ v, v.mult • f ↑v

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
M : Type u_2
inst✝ : AddCommMonoid M
f : AbsoluteValue K ℝ → M
⊢ ∑ m ∈ archAbsVal.toFinset, count m archAbsVal • f m = ∑ v, v.mult • f ↑v
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
⊢ ∑ x, χ x + ∑ x, ψ (1 - x) - ∑ x, 1 + ∑ x, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x, χ x + ∑ x, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
]

Goal state after:
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
⊢ ∑ x, χ x + ∑ x, ψ (1 - x) - ∑ x, 1 + ∑ x, (χ x - 1) * (ψ (1 - x) - 1) =
    ∑ x, χ x + ∑ x, ψ x - ↑(Fintype.card F) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.card = archAbsVal.card

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case h₂.refine_1
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
j : ι'
⊢ (⨆ s, ↑v (coeff (↑s) (p j))) * (⨆ i, ↑v (x i)) ^ N ≤ (⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) * (⨆ i, ↑v (x i)) ^ N

Tactic:
]

Goal state after:
case h₂.refine_1
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
j : ι'
⊢ (⨆ s, ↑v (coeff (↑s) (p j))) * (⨆ i, ↑v (x i)) ^ N ≤ (⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1) * (⨆ i, ↑v (x i)) ^ N
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))
this : {z | 0 < z.re} ∈ 𝓝 1
a : ℂ
ha : 0 < a.re
a✝ : a ∈ {1}ᶜ
⊢ (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1) = (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1)

Tactic:
]

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
⊢ ∑ x, χ x + ∑ i, ψ i - ∑ x, 1 + (∑ x, (χ x - 1) * (ψ (1 - x) - 1) - 0) =
    ∑ x, χ x + ∑ x, ψ x - ∑ x, 1 + (∑ x, (χ x - 1) * (ψ (1 - x) - 1) - ∑ x ∈ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1))

Tactic:
]

Goal state after:
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
⊢ ∑ x, χ x + ∑ i, ψ i - ∑ x, 1 + (∑ x, (χ x - 1) * (ψ (1 - x) - 1) - 0) =
    ∑ x, χ x + ∑ x, ψ x - ∑ x, 1 + (∑ x, (χ x - 1) * (ψ (1 - x) - 1) - ∑ x ∈ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1))
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} ≠ ⊥
⊢ ∏ᶠ (i : FinitePlace K),
      ↑(absNorm (i.maximalIdeal.asIdeal ^ multiplicity i.maximalIdeal.asIdeal (⨆ i, span {x i}))) * ⨆ i_1, i ↑(x i_1) =
    1

pp: case hf
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} ≠ ⊥
⊢ Function.HasFiniteMulSupport fun x_1 ↦
    ↑(absNorm (x_1.maximalIdeal.asIdeal ^ multiplicity x_1.maximalIdeal.asIdeal (⨆ i, span {x i})))

Tactic:
]

Goal state after:
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} ≠ ⊥
⊢ ∏ᶠ (i : FinitePlace K),
      ↑(absNorm (i.maximalIdeal.asIdeal ^ multiplicity i.maximalIdeal.asIdeal (⨆ i, span {x i}))) * ⨆ i_1, i ↑(x i_1) =
    1

case hf
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} ≠ ⊥
⊢ Function.HasFiniteMulSupport fun x_1 ↦
    ↑(absNorm (x_1.maximalIdeal.asIdeal ^ multiplicity x_1.maximalIdeal.asIdeal (⨆ i, span {x i})))
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case e_a.e_a
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
⊢ 0 = 0

Tactic:
]

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) = ↑(Fintype.card F) - 2

Tactic:
]

Goal state after:
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) = ↑(Fintype.card F) - 2
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 : F
hx : x ∈ univ \ {0, 1}
⊢ 1 = 1

pp: case hc
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
hx : x ∈ univ \ {0, 1}
⊢ IsUnit (x * (1 - x))

Tactic:
]

Goal state after:
case hc
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
hx : x ∈ univ \ {0, 1}
⊢ IsUnit (x * (1 - x))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
]

Goal state after:
this : completedRiemannZeta 1 + 1 = completedRiemannZeta₀ 1
⊢ completedRiemannZeta₀ 1 = (↑γ - log (4 * ↑π)) / 2 + 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
]

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

Goal state before:
pp: case refine_2
⊢ rexp 1 < 4 * π

Tactic:
]

Goal state after:
case refine_2
⊢ rexp 1 < 4 * π
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
⊢ ↑(Fintype.card F) - 2 = ↑(Fintype.card F) - 2

Tactic:
]

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

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

Tactic:
]

Goal state after:
⊢ (↑γ - log (4 * ↑π)) / 2 = (↑γ - 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
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)
⊢ ⨆ i, (↑(absNorm v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal (span {x i})))⁻¹ = ⨆ i, v ↑(x i)

Tactic:
]

Goal state after:
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)
⊢ ⨆ i, (↑(absNorm v.maximalIdeal.asIdeal ^ multiplicity v.maximalIdeal.asIdeal (span {x i})))⁻¹ = ⨆ i, v ↑(x i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
]

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 < z.re

Tactic:
]

Goal state after:
s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
⊢ 1 < z.re
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)
i : ι
⊢ v ↑(x i) * ↑(absNorm v.maximalIdeal.asIdeal) ^ multiplicity v.maximalIdeal.asIdeal (span {x i}) = 1

Tactic:
]

Goal state after:
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)
i : ι
⊢ v ↑(x i) * ↑(absNorm v.maximalIdeal.asIdeal) ^ multiplicity v.maximalIdeal.asIdeal (span {x i}) = 1