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

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
⊢ mulHeight (Sum.elim 0 0) = mulHeight 0

pp: case inr
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
⊢ mulHeight (Sum.elim x 0) = mulHeight x

Tactic:
· simp

Goal state after:
case inr
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
⊢ mulHeight (Sum.elim x 0) = mulHeight x
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 ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : IsEmpty ι'
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)

pp: case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
· simp

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι'
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (↑(Nat.card ι) * ⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl
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
i✝ : ι
hi : x i✝ ≠ 0 i✝
this : Nonempty ι
hx' : Sum.elim x 0 ≠ 0
v : AbsoluteValue K ℝ
i : ι
⊢ v (Sum.elim x 0 (Sum.inl i)) ≤ ⨆ i, v (x i)

Tactic:
| inl i =>

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 ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝ : IsEmpty ι
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

pp: case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
· simp

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝ : Nonempty ι
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : IsEmpty ι'
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)

Tactic:
· simp

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Fintype ι
inst✝ : Finite ι'
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
A : ι' × ι → K
x : ι → K
h✝¹ : Nonempty ι
h✝ : Nonempty ι'
⊢ ⨆ j, v (∑ i, A (j, i) * x i) ≤ (⨆ ji, v (A ji)) * ⨆ i, v (x i)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
⊢ mulHeight 0 = 1

pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
hx : x ≠ 0
⊢ mulHeight x = 1

Tactic:
· simp

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_5
inst✝ : Subsingleton ι
x : ι → K
hx : x ≠ 0
⊢ mulHeight x = 1
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
⊢ mulHeight₁ (x / 0) = mulHeight ![x, 0]

pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
hy : y ≠ 0
⊢ mulHeight₁ (x / y) = mulHeight ![x, y]

Tactic:
· simp

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
hy : y ≠ 0
⊢ mulHeight₁ (x / y) = mulHeight ![x, y]
Module: Mathlib.NumberTheory.Height.Basic

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

Tactic:
rcases le_or_gt 0 n with h | h
  · lift n to ℕ using h
    rw [zpow_natCast, mulHeight₁_pow, Int.natAbs_natCast]
  · nth_rewrite 1 [show n = -n.natAbs by grind]
    rw [zpow_neg, mulHeight₁_inv, zpow_natCast, mulHeight₁_pow]

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

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
x : ι → K
hx : x ≠ 0
⊢ mulHeight (-x) = mulHeight x
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:
· simp

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

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

Goal state before:
pp: case inl
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
x : ι → R
⊢ max (v (∑ i ∈ ∅, x i)) 1 ≤ ∏ i ∈ ∅, max (v (x i)) 1

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

Tactic:
· simp

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
⊢ max (v (∑ i ∈ s, x i)) 1 ≤ ∏ i ∈ s, max (v (x i)) 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
x✝ : ↑nonarchAbsVal
⊢ 0 ≤ max (↑x✝ (∑ a ∈ s, x a)) 1

Tactic:
by grind

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
x : α → K
⊢ logHeight₁ (∑ a ∈ ∅, x a) ≤ ↑(totalWeight K) * log ↑(#∅) + ∑ a ∈ ∅, logHeight₁ (x a)

pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
⊢ logHeight₁ (∑ a ∈ s, x a) ≤ ↑(totalWeight K) * log ↑(#s) + ∑ a ∈ s, logHeight₁ (x a)

Tactic:
· simp

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
α : Type u_2
s : Finset α
x : α → K
hs : s.Nonempty
⊢ logHeight₁ (∑ a ∈ s, x a) ≤ ↑(totalWeight K) * log ↑(#s) + ∑ a ∈ s, logHeight₁ (x a)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
refine Tendsto.congr' ?_ (tendsto_const_nhds.mono_left nhdsWithin_le_nhds)

Goal state after:
case refine_2.refine_2.hf
f : ℂ → ℂ := fun s ↦ riemannZeta s - 1 / (s - 1)
⊢ (fun x ↦ 1) =ᶠ[𝓝[≠] 1] fun x ↦ (x - 1) * (1 / (x - 1))
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: case e'_3.a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
a✝ : x✝ ∈ Finset.univ
⊢ x✝.mult = x✝.mult • 1

Tactic:
· simp

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 + ∑ x, ψ ((Equiv.subLeft 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:
rw [(Equiv.subLeft 1).sum_comp ψ, Fintype.card_eq_sum_ones, Nat.cast_sum, Nat.cast_one,
    sum_sdiff_eq_sub (subset_univ _), ← sub_zero (_ - _ + _), add_sub_assoc]

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
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
⊢ r ∈ {↑m, r}

Tactic:
by grind

Goal state after:
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
a : 𝓞 K
ha' : ↑m * a = ↑n * r
ha : ↑n * x = ↑a
⊢ {↑n} ⊆ {↑n, a}

Tactic:
by grind

Goal state after:
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 < n ^ Module.finrank ℤ (𝓞 K)
⊢ 1 ≤ ↑(n ^ Module.finrank ℤ (𝓞 K)) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i)

Tactic:
← absNorm_span_natCast

Goal state after:
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)
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
p : Fin 3 → MvPolynomial (Fin 4) K := ![X 0, X 1 + X 2, X 3]
hom : ∀ (i : Fin 3), (p i).IsHomogeneous 1
C : ℝ
hC₀ : C > 0
hC : ∀ (x : Fin 4 → K), (mulHeight fun j ↦ (eval x) (p j)) ≤ C * mulHeight x
⊢ max C 1 > 0

Tactic:
by grind

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
⊢ ↑(n * q + 1) - 2 = -1 + ↑q * z₁ * (μ - 1) ^ 2

Tactic:
Nat.cast_add,

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
⊢ ↑(n * q) + ↑1 - 2 = -1 + ↑q * z₁ * (μ - 1) ^ 2
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
⊢ jacobiSum 1 χ = -1 + 0 * (μ - 1) ^ 2

Tactic:
jacobiSum_one_nontrivial hχ₀,

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
⊢ -1 = -1 + 0 * (μ - 1) ^ 2
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
h : IsAdjoinRoot S f
T : Type u_1
inst✝ : CommRing T
i : R →+* T
x : T
hx : eval₂ i x f = 0
z : R[X]
⊢ (h.lift i x hx) (h.map z) = eval₂ i x z

Tactic:
simp [lift, h.eval₂_repr_eq_eval₂_of_map_eq hx _ _ rfl]

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case hl.inl
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
x : S
a✝ : Nontrivial R
i : ℕ
h : IsAdjoinRootMonic S 1
hi : natDegree 1 ≤ i
⊢ ({ toFun := fun x ↦ h.repr x %ₘ 1, map_add' := ⋯ } x).coeff i = 0

pp: case hl.inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
hf : f ≠ 1
⊢ ({ toFun := fun x ↦ h.repr x %ₘ f, map_add' := ⋯ } x).coeff i = 0

Tactic:
· simp

Goal state after:
case hl.inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
x : S
a✝ : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
hf : f ≠ 1
⊢ ({ toFun := fun x ↦ h.repr x %ₘ f, map_add' := ⋯ } x).coeff i = 0
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case neg.refine_2
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
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
⊢ 0 + 0 - ↑(n * q + 1) + (∑ i ∈ univ \ {0, 1}, ⋯.choose) * (μ - 1) ^ 2 =
    -1 + (-↑q * z₁ + ∑ x ∈ univ \ {0, 1}, ⋯.choose) * (μ - 1) ^ 2

Tactic:
Nat.cast_add,

Goal state after:
case neg.refine_2
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
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
⊢ 0 + 0 - (↑(n * q) + ↑1) + (∑ i ∈ univ \ {0, 1}, ⋯.choose) * (μ - 1) ^ 2 =
    -1 + (-↑q * z₁ + ∑ x ∈ univ \ {0, 1}, ⋯.choose) * (μ - 1) ^ 2
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case refine_1
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s✝ : ℂ
hs✝ : s✝ ≠ 1
hpc : IsPreconnected {1}ᶜ
hne : 2 ∈ {1}ᶜ
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableWithinAt ℂ (LFunction ((changeLevel hMN) χ)) {1}ᶜ s

Tactic:
exact (differentiableAt_LFunction _ _ (.inl hs)).differentiableWithinAt

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

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

Tactic:
simp only [ε]

Goal state after:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
⊢ completedLFunction χ (1 - s) =
    (↑N ^ (s - 1) * χ (-1) / I ^ if χ.Even then 0 else 1) * ZMod.completedLFunction (𝓕 ⇑χ) s
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case neg
k : ℕ
h : ¬k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli k) + 0

Tactic:
bernoulli_eq_bernoulli'_of_ne_one h,

Goal state after:
case neg
k : ℕ
h : ¬k = 1
⊢ (algebraMap ℚ ℝ) (bernoulli' k) = ↑(bernoulli' k) + 0
Module: Mathlib.NumberTheory.LSeries.ZMod

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

Tactic:
by
  rw [LFunction]
  have (j : ZMod N) : Φ j * hurwitzZeta (toAddCircle j) (1 - s) = Φ j *
      ((2 * π) ^ (-s) * Gamma s * (cexp (-π * I * s / 2) *
      expZeta (toAddCircle j) s + cexp (π * I * s / 2) * expZeta (-toAddCircle j) s)) := by
    rcases eq_or_ne j 0 with rfl | hj
    · rcases hs' with hΦ | hs'
      · simp only [hΦ, zero_mul]
      · rw [hurwitzZeta_one_sub _ hs (Or.inr hs')]
    · rw [hurwitzZeta_one_sub _ hs (Or.inl <| toAddCircle_eq_zero.not.mpr hj)]
  simp only [this, mul_assoc _ _ (Gamma s)]
  -- get rid of Gamma terms and power of N
  generalize (2 * π) ^ (-s) * Gamma s = C
  simp_rw [← mul_assoc, mul_comm _ C, mul_assoc, ← mul_sum, ← mul_assoc, mul_comm _ C, mul_assoc,
    neg_sub]
  congr 2
  -- now gather sum terms
  rw [LFunction_dft _ hs', LFunction_dft _ (hs'.imp_left <| by simp only [neg_zero, imp_self])]
  conv_rhs => enter [2, 2]; rw [← (Equiv.neg _).sum_comp _ _ (by simp), Equiv.neg_apply]
  simp_rw [neg_neg, mul_sum, ← sum_add_distrib, ← mul_assoc, mul_comm _ (Φ _), mul_assoc,
    ← mul_add, map_neg, add_comm]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k✝ : ℕ
hk✝ : k✝ ≠ 0
n : ℤ
hn : n ≠ 0
k : ℕ
hk : 1 ≤ k
h'k : bernoulliFourierCoeff k n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ ¬k + 1 = 1

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (Ideal.map (↑(quotMapEquivQuotQuotMap hx hx').symm)
        (span
          (⇑(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)})) ''
            {Polynomial.map (Ideal.Quotient.mk I) Q}))) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
image_singleton,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (Ideal.map (↑(quotMapEquivQuotQuotMap hx hx').symm)
        (span
          {(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
              (Polynomial.map (Ideal.Quotient.mk I) Q)})) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (span
        (⇑↑(quotMapEquivQuotQuotMap hx hx').symm ''
          {(Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
              (Polynomial.map (Ideal.Quotient.mk I) Q)})) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})

Tactic:
image_singleton,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
Q : R[X]
hQ : Polynomial.map (Ideal.Quotient.mk I) Q ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ comap (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I))
      (span
        {↑(quotMapEquivQuotQuotMap hx hx').symm
            ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}))
              (Polynomial.map (Ideal.Quotient.mk I) Q))}) =
    span (↑(Ideal.map (algebraMap R S) I) ∪ {(aeval x) Q})
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))

Tactic:
have step1 : ∀ n : ℤ, fourierCoeff B n = -k ! / (2 * π * I * n) ^ k := by
    rw [ContinuousMap.coe_mk]; exact fourierCoeff_bernoulli_eq (by lia : k ≠ 0)

Goal state after:
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inr.refine_1
N : ℕ
inst✝ : NeZero N
B : BadChar N
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ B.F z

pp: case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : BadChar N
⊢ ContinuousAt B.F 1

Tactic:
· filter_upwards [self_mem_nhdsWithin] with t ht
    exact B.F_differentiableAt_of_ne ht

Goal state after:
case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : BadChar N
⊢ ContinuousAt B.F 1