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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
a b : { v // v ≠ 0 }
t : K
h : t = 0
⊢ ↑a ≠ t • ↑b

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
a b : { v // v ≠ 0 }
t : K
h : t = 0
⊢ ¬↑a = 0
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 : eval 1 (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) = eval 1 (∑ i ∈ range (n + 1), X ^ i)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
μ : R
hμ : IsPrimitiveRoot μ (n + 1)
this : eval 1 (∏ k ∈ range n, (X - C (μ ^ (k + 1) * 1))) = eval 1 (∑ i ∈ range (n + 1), X ^ i)
⊢ ∏ k ∈ range n, (1 - μ ^ (k + 1)) = ↑n + 1
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
⊢ 1 < (↑s).re

Tactic:
simpa using

Goal state after:
this : Tendsto (fun s ↦ ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
s : ℝ
hs : s ∈ Ioi 1
⊢ 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:
simpa using

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) (𝓝 (1 - termTSum 1))
Module: Mathlib.RingTheory.RootsOfUnity.Lemmas

Goal state before:
pp: case refine_1
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)
⊢ ((-1) ^ (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1) ∈ ℤ[μ]

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)
⊢ ↑(m + k + 1) = (((-1) ^ (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k

Tactic:
· apply Subalgebra.mul_mem
    · apply Subalgebra.mul_mem
      · exact Subalgebra.pow_mem _ (Subalgebra.neg_mem _ <| Subalgebra.one_mem _) _
      · exact Subalgebra.prod_mem _ fun _ _ ↦ (Zdef _).1
    · refine Subalgebra.prod_mem _ fun _ _ ↦ ?_
      apply Subalgebra.sub_mem
      · exact Subalgebra.pow_mem _ (self_mem_adjoin_singleton ℤ μ) _
      · exact Subalgebra.one_mem _

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)
⊢ ↑(m + k + 1) = (((-1) ^ (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k
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 * (x - 1) - f 1 * (x - 1)) (𝓝[≠] 1) (𝓝 (1 - 1 - f 1 * (1 - 1)))

Tactic:
apply Tendsto.sub

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

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

Goal state before:
pp: F : Type u_1
inst✝² : Norm F
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (fun s ↦ riemannZeta s - 1 / (s - 1)) =O[𝓝 1] fun x ↦ 1

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝² : Norm F
inst✝¹ : One F
inst✝ : NormOneClass F
⊢ (fun s ↦ riemannZeta s - 1 / (s - 1)) =O[𝓝 1] fun x ↦ 1
Module: Mathlib.NumberTheory.Height.NumberField

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

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (AbsoluteValue K ℝ)
v : InfinitePlace K
this : DecidableEq (InfinitePlace K)
⊢ (∑ x, if x = v then x.mult else 0) = v.mult
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : Inhabited (InfinitePlace K)
⊢ 0 < totalWeight K

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : Inhabited (InfinitePlace K)
⊢ 0 < ∑ x, x.mult
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case hc
F : Type u_1
R : Type u_2
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : CommRing R
x : F
hx : x ≠ 0 ∧ x ≠ 1
⊢ IsUnit (x * (1 - x))

Tactic:
simpa using

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 ≠ 0 ∧ x ≠ 1
⊢ ¬x = 0 ∧ ¬x = 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
simpa using

Goal state after:
case inr
s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
hgz : ∀ (z : ℂ), 1 < z.re → (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z)) = riemannZeta z
heq : EqOn (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) riemannZeta {1}ᶜ
⊢ riemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (riemannZeta s)
Module: Mathlib.NumberTheory.Height.MvPolynomial

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

Tactic:
simpa using

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : IsAlgebraic ℤ x
m : ℕ
r : 𝓞 K
hm : m ≠ 0
hmr : m • x = ↑r
n : ℕ := (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hndef : n = (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hn : n ≠ 0
this : n • r ∈ span {↑m}
⊢ ∃ a, ↑m * a = ↑n * r

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : IsAlgebraic ℤ x
m : ℕ
r : 𝓞 K
hm : m ≠ 0
hmr : m • x = ↑r
n : ℕ := (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hndef : n = (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, r}))
hn : n ≠ 0
this : n • r ∈ span {↑m}
⊢ ∃ a, a * ↑m = r * ↑n
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
⊢ 1 ≤ ↑(absNorm (span {↑n})) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i)

Tactic:
← absNorm_mul_finprod_finitePlace_eq_one (show ![a, n] ≠ 0 by simp [hn])

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : ¬n = 0
a : 𝓞 K
Hw : 0 < absNorm (span {↑n})
⊢ ↑(absNorm (span (Set.range ![a, ↑n]))) * ∏ᶠ (v : FinitePlace K), ⨆ i, v ↑(![a, ↑n] i) ≤
    ↑(absNorm (span {↑n})) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
hv : ∀ (i : Fin 2), ↑(![a, ↑n] i) = ![↑a, ↑n] i
⊢ ↑n ^ (totalWeight K - 1) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i) = 1

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
hv : ∀ (i : Fin 2), ↑(![a, ↑n] i) = ![↑a, ↑n] i
⊢ ↑n ^ (totalWeight K - 1) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i) = 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ Tendsto riemannZeta₁ (𝓝 1) (𝓝 1)

Tactic:
simpa using

Goal state after:
⊢ Tendsto riemannZeta₁ (𝓝 1) (𝓝 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : DifferentiableAt ℝ (fun s ↦ Real.log (riemannZeta₁ ↑s).re) 1
⊢ (fun s ↦ Real.log (riemannZeta₁ ↑s).re) =O[𝓝 1] fun x ↦ x - 1

Tactic:
simpa using

Goal state after:
this : DifferentiableAt ℝ (fun s ↦ Real.log (riemannZeta₁ ↑s).re) 1
⊢ (fun s ↦ Real.log (riemannZeta₁ ↑s).re) =O[𝓝 1] fun x ↦ x - 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : DifferentiableAt ℂ (fun s ↦ deriv riemannZeta₁ s / riemannZeta₁ s) 1
⊢ (fun s ↦ deriv riemannZeta₁ s / riemannZeta₁ s - ↑γ) =O[𝓝 1] fun x ↦ x - 1

Tactic:
simpa using

Goal state after:
this : DifferentiableAt ℂ (fun s ↦ deriv riemannZeta₁ s / riemannZeta₁ s) 1
⊢ (fun s ↦ deriv riemannZeta₁ s / riemannZeta₁ s - ↑γ) =O[𝓝 1] fun x ↦ x - 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : (fun s ↦ (riemannZeta₁ s)⁻¹ - 1) =O[𝓝 1] fun x ↦ x - 1
⊢ (fun s ↦ (s - 1) * ((riemannZeta₁ s)⁻¹ - 1)) =O[𝓝 1] fun s ↦ (s - 1) ^ 2

Tactic:
simpa using

Goal state after:
this : (fun s ↦ (riemannZeta₁ s)⁻¹ - 1) =O[𝓝 1] fun x ↦ x - 1
⊢ (fun s ↦ (s - 1) * ((riemannZeta₁ s)⁻¹ - 1)) =O[𝓝 1] fun s ↦ (s - 1) * (s - 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ (fun s ↦ (riemannZeta₁ s)⁻¹ - 1) =O[𝓝 1] fun x ↦ x - 1

Tactic:
simpa using

Goal state after:
⊢ (fun s ↦ (riemannZeta₁ s)⁻¹ - 1) =O[𝓝 1] fun x ↦ x - 1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: this : (fun x ↦ x - 1) =o[𝓝 1] fun x ↦ 1
⊢ (fun s ↦ (s - 1) ^ 2) =o[𝓝[≠] 1] fun x ↦ x - 1

Tactic:
simpa using

Goal state after:
this : (fun x ↦ x - 1) =o[𝓝 1] fun x ↦ 1
⊢ (fun s ↦ (s - 1) * (s - 1)) =o[𝓝[≠] 1] fun x ↦ x - 1
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
p : R[X]
⊢ h.map p = 0 ↔ f ∣ p

Tactic:
simpa using

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
p : R[X]
⊢ h.map p = 0 ↔ f ∣ p
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
a : AdjoinRoot f
⊢ h.adjoinRootAlgEquiv a = h.map ⋯.choose

Tactic:
by
  rw (occs := [1]) [← (AdjoinRoot.mk_surjective a).choose_spec, adjoinRootAlgEquiv_apply_mk]

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

Goal state before:
pp: case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ψ = 1
⊢ ∃ z ∈ ℤ[μ], jacobiSum 1 1 = -1 + z * (μ - 1) ^ 2

Tactic:
jacobiSum_one_one

Goal state after:
case pos
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : χ = 1
hψ₀ : ψ = 1
⊢ ∃ z ∈ ℤ[μ], ↑(Fintype.card F) - 2 = -1 + z * (μ - 1) ^ 2
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
⊢ (∏ v, (⨆ i, v ((Int.cast ∘ x) i)) ^ v.mult) * ∏ᶠ (v : FinitePlace ℚ), ⨆ i, v ((Int.cast ∘ x) i) = ⨆ i, ↑|x i|

Tactic:
infinitePlace_apply

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
hx : Finset.univ.gcd x = 1
hx₀ : Int.cast ∘ x ≠ 0
⊢ (∏ x_1, (⨆ i, ↑|(Int.cast ∘ x) i|) ^ x_1.mult) * ∏ᶠ (v : FinitePlace ℚ), ⨆ i, v ((Int.cast ∘ x) i) = ⨆ i, ↑|x i|
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: q : ℚ
⊢ Finset.univ.gcd ![q.num, ↑q.den] = 1

Tactic:
simpa using

Goal state after:
q : ℚ
⊢ q.num.gcd ↑q.den = 1
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 : IsAdjoinRootMonic S f
n : ℕ
a✝ : Nontrivial R
hdeg : f.degree ≤ ↑n
⊢ f.natDegree ≤ n

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
a✝ : Nontrivial R
hdeg : f.degree ≤ ↑n
⊢ f.degree ≤ ↑n
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 : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
⊢ h.modByMonicHom h.root = X

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
⊢ h.modByMonicHom h.root = X
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : R[α] = ⊤
x✝ : R[X]
⊢ x✝ ∈ RingHom.ker (aeval α) ↔ x✝ ∈ Ideal.span {minpoly R α}

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : IsTorsionFree R S
inst✝ : IsIntegrallyClosed R
α : S
hα : IsIntegral R α
hα₂ : R[α] = ⊤
x✝ : R[X]
⊢ (aeval α) x✝ = 0 ↔ minpoly R α ∣ x✝
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
C₁ : ℝ
hC₁ : ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C₁ + logHeight ![a, b] + logHeight ![c, d]
C₂ : ℝ
hC₂ :
  ∀ {a b c d : K},
    ![a, b] ≠ 0 → ![c, d] ≠ 0 → C₂ + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]
a✝ b✝ c✝ d✝ : K
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ |logHeight ![a✝ * c✝, a✝ * d✝ + b✝ * c✝, b✝ * d✝] - (logHeight ![a✝, b✝] + logHeight ![c✝, d✝])| ≤ max C₁ (-C₂)

Tactic:
specialize hC₂ hab hcd

Goal state after:
K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
C₁ : ℝ
hC₁ : ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C₁ + logHeight ![a, b] + logHeight ![c, d]
C₂ : ℝ
a✝ b✝ c✝ d✝ : K
hC₂ : C₂ + logHeight ![a✝, b✝] + logHeight ![c✝, d✝] ≤ logHeight ![a✝ * c✝, a✝ * d✝ + b✝ * c✝, b✝ * d✝]
hab : ![a✝, b✝] ≠ 0
hcd : ![c✝, d✝] ≠ 0
⊢ |logHeight ![a✝ * c✝, a✝ * d✝ + b✝ * c✝, b✝ * d✝] - (logHeight ![a✝, b✝] + logHeight ![c✝, d✝])| ≤ max C₁ (-C₂)
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case refine_3.refine_2
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
t : ℂ
ht : 1 < t.re
⊢ LFunction ((changeLevel hMN) χ) t = (fun s ↦ LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))) t

Tactic:
simpa using

Goal state after:
case refine_3.refine_2
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : s ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
t : ℂ
ht : 1 < t.re
⊢ LSeries (fun x ↦ ((changeLevel hMN) χ) ↑x) t = LSeries (fun x ↦ χ ↑x) t * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-t))
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case neg
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
h : ¬j = 0
⊢ IsPreconnected U

Tactic:
simpa using

Goal state after:
case neg
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
h : ¬j = 0
⊢ IsPreconnected Set.univ
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
p : ℕ
hp : p ∈ n.primeFactors
⊢ 1 - (↑p)⁻¹ ≠ 0

Tactic:
simpa using

Goal state after:
n : ℕ
inst✝ : NeZero n
p : ℕ
hp : p ∈ n.primeFactors
⊢ ¬p = 1
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ContinuousWithinAt (LFunctionTrivChar₁ n) {1}ᶜ 1

Tactic:
simpa using

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ Tendsto (fun s ↦ (s - 1) * LFunctionTrivChar n s) (𝓝[≠] 1) (𝓝 (∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
⊢ bernoulliFun k (1 - x) = (-1) ^ k * bernoulliFun k x

Tactic:
simpa using

Goal state after:
k : ℕ
x : ℝ
⊢ (Polynomial.aeval (1 - x)) (Polynomial.bernoulli k) = (-1) ^ k * (Polynomial.aeval x) (Polynomial.bernoulli k)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case succ
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
i : c = 0
⊢ ∀ (x : ℝ), f (k + 1) x = 0

Tactic:
simpa using

Goal state after:
case succ
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
i : c = 0
⊢ ∀ (x : ℝ), f (k + 1) x = 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case neg
k : ℕ
k1 : ¬k = 1
m : bernoulliFun k 1 = 2 ^ k / 2 * (0 + bernoulliFun k (2⁻¹ + 0 / 2) + bernoulliFun k (2⁻¹ + 1 / 2))
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)

Tactic:
← one_div,

Goal state after:
case neg
k : ℕ
k1 : ¬k = 1
m : bernoulliFun k 1 = 2 ^ k / 2 * (0 + bernoulliFun k (1 / 2 + 0 / 2) + bernoulliFun k (1 / 2 + 1 / 2))
⊢ bernoulliFun k 2⁻¹ = (2 / 2 ^ k - 1) * ↑(bernoulli k)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 0 n = 0

Tactic:
simpa using

Goal state after:
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff 0 n = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaEven (↑x) (-(2 * ↑k.succ)) = 0

Tactic:
simpa using

Goal state after:
x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaEven (↑x) (-(2 * (↑k + 1))) = 0
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeriesSummable (f + g) s

Tactic:
simpa using

Goal state after:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ Summable (term (f + g) s)
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeries (f + g) s = LSeries f s + LSeries g s

Tactic:
simpa using

Goal state after:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ ∑' (n : ℕ), (term f s n + term g s n) = ∑' (n : ℕ), term f s n + ∑' (n : ℕ), term g s n
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeriesSummable (f - g) s

Tactic:
simpa using

Goal state after:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ Summable (term (f - g) s)
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ LSeries (f - g) s = LSeries f s - LSeries g s

Tactic:
simpa using

Goal state after:
f g : ℕ → ℂ
s : ℂ
hf : LSeriesSummable f s
hg : LSeriesSummable g s
⊢ ∑' (n : ℕ), (term f s n - term g s n) = ∑' (n : ℕ), term f s n - ∑' (n : ℕ), term g s n
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f : ℕ → ℂ
c s : ℂ
hc : c ≠ 0
hf : LSeriesSummable (c • f) s
⊢ LSeriesSummable f s

Tactic:
simpa using

Goal state after:
f : ℕ → ℂ
c s : ℂ
hc : c ≠ 0
hf : LSeriesSummable (c • f) s
⊢ LSeriesSummable f s
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
a : ι → ℂ
hf : ∀ i ∈ S, LSeriesHasSum (f i) s (a i)
⊢ LSeriesHasSum (∑ i ∈ S, f i) s (∑ i ∈ S, a i)

Tactic:
simpa using

Goal state after:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
a : ι → ℂ
hf : ∀ i ∈ S, LSeriesHasSum (f i) s (a i)
⊢ HasSum (fun a ↦ ∑ c ∈ S, term (f c) s a) (∑ i ∈ S, a i)
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
hf : ∀ i ∈ S, LSeriesSummable (f i) s
⊢ LSeriesSummable (∑ i ∈ S, f i) s

Tactic:
simpa using

Goal state after:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
hf : ∀ i ∈ S, LSeriesSummable (f i) s
⊢ Summable (term (∑ i ∈ S, f i) s)
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
hf : ∀ i ∈ S, LSeriesSummable (f i) s
⊢ LSeries (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries (f i) s

Tactic:
simpa using

Goal state after:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
hf : ∀ i ∈ S, LSeriesSummable (f i) s
⊢ ∑' (n : ℕ), ∑ i ∈ S, term (f i) s n = ∑ i ∈ S, ∑' (n : ℕ), term (f i) s n
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ ‖(toArithmeticFunction fun x ↦ χ ↑x) n‖ ≤ 1

Tactic:
simpa using

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ ‖χ ↑n‖ ≤ 1