mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
⊢ (Algebra.trace K L) x * (algebraMap A K) y ∈ ↑p

Tactic:
obtain ⟨z, hz, hz'⟩ := hx _ (Ideal.mem_map_of_mem _ hy)

Goal state after:
A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
⊢ (Algebra.trace K L) x * (algebraMap A K) y ∈ ↑p
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: case inr.inr.refine_3
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ 2 ∣ S'.a + ↑η ^ 2 * S'.b
x✝ : λ ∣ ↑η ^ 2 * S'.b
x : 𝓞 K
hx : ↑η ^ 2 * S'.b = λ * x
⊢ S'.b = S'.b * (↑η ^ 2 * ↑η)

Tactic:
← pow_succ,

Goal state after:
case inr.inr.refine_3
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S' : Solution' hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
h : λ ^ 2 ∣ S'.a + ↑η ^ 2 * S'.b
x✝ : λ ∣ ↑η ^ 2 * S'.b
x : 𝓞 K
hx : ↑η ^ 2 * S'.b = λ * x
⊢ S'.b = S'.b * ↑η ^ (2 + 1)
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
hh : λ ^ (3 * S.multiplicity - 2) * λ * λ * S.x * S.y * S.z = λ ^ (3 * S.multiplicity) * ↑S.u * S.w ^ 3
this : 2 ≤ S.multiplicity
⊢ S.x * S.y * S.z = ↑S.u * S.w ^ 3

Tactic:
← pow_succ,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hh : λ ^ (3 * S.multiplicity - 2 + 1) * λ * S.x * S.y * S.z = λ ^ (3 * S.multiplicity) * ↑S.u * S.w ^ 3
this : 2 ≤ S.multiplicity
⊢ S.x * S.y * S.z = ↑S.u * S.w ^ 3
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
hh : λ ^ (3 * S.multiplicity - 2 + 1) * λ * S.x * S.y * S.z = λ ^ (3 * S.multiplicity) * ↑S.u * S.w ^ 3
this : 2 ≤ S.multiplicity
⊢ S.x * S.y * S.z = ↑S.u * S.w ^ 3

Tactic:
← pow_succ,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hh : λ ^ (3 * S.multiplicity - 2 + 1 + 1) * S.x * S.y * S.z = λ ^ (3 * S.multiplicity) * ↑S.u * S.w ^ 3
this : 2 ≤ S.multiplicity
⊢ S.x * S.y * S.z = ↑S.u * S.w ^ 3
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.a + S.b) * ((S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)) = ↑S.u * (λ ^ (3 * S.multiplicity) * S.w ^ 3)

Tactic:
mul_comm 3,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ (S.a + S.b) * ((S.a + ↑η * S.b) * (S.a + ↑η ^ 2 * S.b)) = ↑S.u * (λ ^ (S.multiplicity * 3) * S.w ^ 3)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
⊢ logHeight₁ 0 = 0

Tactic:
by
  simp [logHeight₁_eq_log_mulHeight₁]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
⊢ logHeight₁ 1 = 0

Tactic:
by
  simp [logHeight₁_eq_log_mulHeight₁]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
e : ι ≃ ι'
x : ι' → K
H : ∀ (v : AbsoluteValue K ℝ), ⨆ i, v (x (e i)) = ⨆ i, v (x i)
hx : x ≠ 0
i : ι'
hi : x i ≠ 0
⊢ (x ∘ ⇑e) (e.symm i) ≠ 0 (e.symm i)

Tactic:
simp [hi]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : AdmissibleAbsValues K
ι : Type u_2
ι' : Type u_3
inst✝¹ : Finite ι
inst✝ : Finite ι'
f : ι → ι'
x : ι' → K
⊢ logHeight (x ∘ f) ≤ logHeight x

Tactic:
by
  simpa [logHeight_eq_log_mulHeight] using log_le_log (mulHeight_pos _) <| mulHeight_comp_le ..

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

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

Tactic:
rcases eq_or_ne x 0 with rfl | hx
  · simp
  obtain ⟨i, hi⟩ := Function.ne_iff.mp hx
  have : Nonempty ι := .intro i
  rw [← mulHeight_smul_eq_mulHeight x (inv_ne_zero hi)]
  convert! mulHeight_one
  ext1 j
  simpa [Subsingleton.elim j i] using inv_mul_cancel₀ hi

Goal state after:
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 hζ
hS' : S'.multiplicity = S.Solution'_descent.multiplicity
⊢ ∃ S₁, S₁.multiplicity < S.multiplicity

Tactic:
exact ⟨S', hS' ▸ Solution'_descent_multiplicity_lt S⟩

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

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ v ((eval x) p) ≤ (p.coeff.sum fun x c ↦ v c) * (⨆ i, v (x i)) ^ N

Tactic:
rw [eval_eq, sum_def, Finset.sum_mul]

Goal state after:
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
⊢ v (∑ d ∈ p.support, coeff d p * ∏ i ∈ d.support, x i ^ d i) ≤ ∑ i ∈ p.support, v (coeff i p) * (⨆ i, v (x i)) ^ N
Module: Mathlib.NumberTheory.NumberField.ProductFormula

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    1

Tactic:
let t₂ :=
    (fun v : HeightOneSpectrum (𝓞 K) ↦ (absNorm (v.maxPowDividing (span {x})) : ℝ)).mulSupport

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
h_x_nezero : x ≠ 0
h_span_nezero : span {x} ≠ 0
t₀ : Set (HeightOneSpectrum (𝓞 K)) := {v | x ∈ v.asIdeal}
h_fin₀ : t₀.Finite
t₁ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ‖(embedding v) ↑x‖
t₂ : Set (HeightOneSpectrum (𝓞 K)) := mulSupport fun v ↦ ↑(absNorm (v.maxPowDividing (span {x})))
⊢ (∏ᶠ (i : HeightOneSpectrum (𝓞 K)), ‖(embedding i) ↑x‖) *
      ↑(absNorm (∏ᶠ (v : HeightOneSpectrum (𝓞 K)), v.maxPowDividing (span {x}))) =
    1
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
simp_rw [mul_sub, mul_one]

Goal state after:
case hf
s : ℝ
hs : 1 < s
⊢ Tendsto (fun x ↦ 1 / (s - 1) - 1 / (s - 1) * (1 / (↑x + 1) ^ (s - 1))) atTop (𝓝 (1 / (s - 1) - 1 / (s - 1) * 0))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
rw [riemannZeta_one, ofReal_div, ofReal_sub, ofReal_log (by positivity : (0 : ℝ) ≤ 4 * π)]

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

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

Tactic:
rw [← completedRiemannZeta₀_one_sub]

Goal state after:
⊢ completedRiemannZeta₀ (1 - 0) = (↑γ - log (4 * ↑π)) / 2 + 1
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
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
⊢ ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t

Tactic:
intro t ht

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
t : F
ht : t ∈ univ \ {0}
⊢ (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case right
⊢ Tendsto riemannZeta₀ (𝓝[≠] 1) (𝓝 (riemannZeta₀ 1))

Tactic:
convert tendsto_nhdsWithin_congr ?_ tendsto_riemannZeta_sub_one_div

Goal state after:
case e'_5
⊢ riemannZeta₀ 1 = ↑γ

case right.convert_2
⊢ ∀ x ∈ {1}ᶜ, riemannZeta x - 1 / (x - 1) = riemannZeta₀ x
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
hf : f ≠ 0
⊢ f ≠ 0 ∧ (aeval h.root) f = 0

Tactic:
by simp [hf]

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

Goal state before:
pp: case succ
F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n✝ n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
ih : gaussSum χ ψ ^ n * gaussSum χ ψ = gaussSum (χ ^ n) ψ * gaussSum χ ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
⊢ gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)

Tactic:
← pow_succ,

Goal state after:
case succ
F : Type u_1
R : Type u_2
inst✝³ : Fintype F
inst✝² : Field F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
ψ : AddChar F R
n✝ n : ℕ
hn : Nat.succ 0 ≤ n
hn₂ : n + 1 < orderOf χ
gauss_rw : gaussSum (χ ^ n) ψ * gaussSum χ ψ = jacobiSum χ (χ ^ n) * gaussSum (χ ^ (n + 1)) ψ
ih : gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ n) ψ * gaussSum χ ψ * ∏ j ∈ Ico 1 n, jacobiSum χ (χ ^ j)
⊢ gaussSum χ ψ ^ (n + 1) = gaussSum (χ ^ (n + 1)) ψ * ∏ j ∈ Ico 1 (n + 1), jacobiSum χ (χ ^ j)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case e_f
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ LSeries.term (fun x ↦ 𝕖 (j * ↑x)) s n = cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑n) / ↑n ^ s

Tactic:
rw [LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs), ofReal_div, ofReal_natCast,
    ofReal_natCast, mul_assoc, div_mul_eq_mul_div, stdAddChar_apply]

Goal state after:
case e_f
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ↑(toCircle (j * ↑n)) / ↑n ^ s = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N)) / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s

Tactic:
rcases χ.even_or_odd with hχ | hχ

Goal state after:
case inl
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Even
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s

case inr
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
s : ℂ
h : s ≠ 0 ∨ N ≠ 1
hχ : χ.Odd
⊢ LFunction χ s = completedLFunction χ s / χ.gammaFactor s
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ContinuousOn (fun s ↦ -(deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s))
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

Tactic:
have h := differentiable_LFunctionTrivChar₁ n

Goal state after:
n : ℕ
inst✝ : NeZero n
h : Differentiable ℂ (LFunctionTrivChar₁ n)
⊢ ContinuousOn (fun s ↦ -(deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s))
    {s | s = 1 ∨ LFunctionTrivChar n s ≠ 0}
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ 1 • ∫ (x : ℝ) in 0..1, 1 • ↑(bernoulliFun k x) = 0

Tactic:
one_smul,

Goal state after:
k : ℕ
hk : k ≠ 0
⊢ ∫ (x : ℝ) in 0..1, ↑(bernoulliFun k x) = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case inl
⊢ -1 / 2 = -↑(1 / 2)

Tactic:
Rat.cast_div,

Goal state after:
case inl
⊢ -1 / 2 = -(↑1 / ↑2)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ 0 < B.F ↑(-2)

Tactic:
refine ArithmeticFunction.LSeries_positive_of_differentiable_of_eqOn (zetaMul_nonneg hχ)
    (χ.isMultiplicative_zetaMul.map_one ▸ zero_lt_one) B.F_differentiable ?_
    (fun _ ↦ B.F_eq_LSeries) _

Goal state after:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ LSeries.abscissaOfAbsConv ⇑χ.zetaMul ≤ ↑1
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case inl
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
k : ℕ
H : n + 1 < k
⊢ Tendsto (fun x ↦ F x k) atTop (nhds 0)

Tactic:
have H₀ : (0 : ℝ) ≤ k / (n + 1) := by positivity

Goal state after:
case inl
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ ↑k / (↑n + 1)
⊢ Tendsto (fun x ↦ F x k) atTop (nhds 0)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(bernoulli 2) / ↑2!

Tactic:
bernoulli_eq_bernoulli'_of_ne_one (by decide : 2 ≠ 1),

Goal state after:
case e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(bernoulli' 2) / ↑2!
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ (fun n ↦ 1 / ↑n ^ (2 * 1 + 1) * Real.sin (2 * π * ↑n * (1 / 4))) = fun n ↦ 1 / ↑n ^ 3 * Real.sin (π * ↑n / 2)

pp: ⊢ (-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32

pp: ⊢ 1 / 4 ∈ Icc 0 1

Tactic:
· ext1 n
    ring_nf

Goal state after:
⊢ (-1) ^ (1 + 1) * (2 * π) ^ (2 * 1 + 1) / 2 / ↑(2 * 1 + 1)! *
      Polynomial.eval (1 / 4) (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * 1 + 1))) =
    π ^ 3 / 32

⊢ 1 / 4 ∈ Icc 0 1
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Tactic:
← LSeries_congr fun _ ↦ if_neg _,

Goal state after:
f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ LSeries (fun {n} ↦ if ?m.225 then ?m.227 else f n) s =
    s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ {n : ℕ} → Prop

f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ {n : ℕ} → Decidable ?m.225

f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ {n : ℕ} → ℂ

f : ℕ → ℂ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable (fun n ↦ if n = 0 then 0 else f n) s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
this : ∀ (n : ℕ), (∑ k ∈ Icc 1 n, if k = 0 then 0 else f k) = ∑ k ∈ Icc 1 n, f k
⊢ ∀ {n : ℕ}, n ≠ 0 → ¬?m.225
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, Nat.Prime a_1 ∧ a_1 ∣ b ∧ ↑a_1 ∣ a) ↔ ∃ p, Nat.Prime p ∧ ↑p ∣ a ∧ p ∣ b

Tactic:
_root_.and_comm

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
p : ℕ
hp : p ≠ 0
n✝ : ℕ
⊢ 0 ≤ (sMod p n✝ ^ 2 - 2) % (2 ^ p - 1)

Tactic:
· apply Int.emod_nonneg
    exact mersenne_int_ne_zero p hp

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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)

Tactic:
have h₁ {C ε : ℝ} : Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε) := by
    rw [show 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε) by congr; ring]
    exact tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x y z : X q
⊢ x * y * z = x * (y * z)

Tactic:
by ext <;> dsimp <;> ring

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x✝¹ x✝ : X q
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
by ext <;> dsimp <;> ring

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
this : p.leadingCoeff = 1 ∨ p.leadingCoeff = -1
⊢ IsIntegral ℤ z

Tactic:
have : (C (1 / p.leadingCoeff) * p).Monic := by aesop (add safe (by simp [Monic.def]))

Goal state after:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
this✝ : p.leadingCoeff = 1 ∨ p.leadingCoeff = -1
this : (C (1 / p.leadingCoeff) * p).Monic
⊢ IsIntegral ℤ z
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: β : Type u_1
G : Type u_2
α : Type u_3
ι : Type u_4
inst✝² : Monoid G
inst✝¹ : AddCommGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : ι → α
s : Finset ι
⊢ (∑ i ∈ s, a i) ∣[k] g = ∑ i ∈ s, a i ∣[k] g

Tactic:
induction s using Finset.induction_on with

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : IsZeroAtImInfty f
⊢ IsZeroAtImInfty (f ∣[k] g)

Tactic:
rw [IsZeroAtImInfty, ZeroAtFilter, tendsto_zero_iff_norm_tendsto_zero] at hf ⊢

Goal state after:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : Tendsto (fun x ↦ ‖f x‖) atImInfty (nhds 0)
⊢ Tendsto (fun x ↦ ‖(f ∣[k] g) x‖) atImInfty (nhds 0)
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ (∏ i ∈ s, f i) ∣[∑ i ∈ s, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#s) - 1) • ∏ i ∈ s, f i ∣[k i] g

Tactic:
induction s using Finset.induction_on with

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

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g).det < 0
⊢ g = J * (J * g)

Tactic:
simp [← mul_assoc, ← sq]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f (1 • z) = denom (-1) ↑z ^ k * f z
⊢ f z = 0 z

Tactic:
one_smul,

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f z = denom (-1) ↑z ^ k * f z
⊢ f z = 0 z
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
τ : ℍ
⊢ HasSum (fun m ↦ (PowerSeries.coeff m) (qExpansion h f) • 𝕢 h ↑τ ^ m) (f τ)

Tactic:
by
  have : ‖𝕢 h τ‖ < 1 := Periodic.norm_qParam_lt_one hh τ.im_pos
  simpa [eq_cuspFunction τ hh.ne' hfper] using
    hasSum_qExpansion_of_norm_lt hh hfper hfhol hfbdd this

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |↑(Matrix.GeneralLinearGroup.det g)|
hD : ↑D ≠ 0
j : ℂ := denom g ↑τ
⊢ ↑D ^ (k - 2) * ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * ↑(g • τ).im ^ k) =
    ↑D ^ (k - 2) * (σ g) (petersson k f f' (g • τ))

Tactic:
by simp [petersson, σ_conj]

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

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ IsBoundedAtImInfty (⇑f ∣[k] g)

Tactic:
← OnePoint.isBoundedAt_infty_iff,

Goal state after:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ ∞.IsBoundedAt (⇑f ∣[k] g) ?m.26

k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ ℤ