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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
⊢ ↑((quadraticChar F) a) = a ^ (Fintype.card F / 2)

Tactic:
by_cases ha : a = 0
  · have : 0 < Fintype.card F / 2 := Nat.div_pos Fintype.one_lt_card two_pos
    simp only [ha, quadraticChar_apply, quadraticCharFun_zero, Int.cast_zero, zero_pow this.ne']
  · rw [quadraticChar_eq_pow_of_char_ne_two hF ha]
    by_cases ha' : a ^ (Fintype.card F / 2) = 1
    · simp only [ha', if_true, Int.cast_one]
    · have ha'' := Or.resolve_left (FiniteField.pow_dichotomy hF ha) ha'
      simp only [ha'', Int.cast_ite, Int.cast_one, Int.cast_neg, ite_eq_right_iff]
      exact Eq.symm

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
⊢ legendreSym p ↑q = 1 ↔ legendreSym q ↑p = 1

Tactic:
quadratic_reciprocity_one_mod_four hp1 hq1

Goal state after:
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp1 : p % 4 = 1
hq1 : q ≠ 2
h : p ≠ q
⊢ legendreSym p ↑q = 1 ↔ legendreSym p ↑q = 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: case pos
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : (k * m).ProbablePrime (k * j)
⊢ False

Tactic:
apply Nat.Prime.not_dvd_one hk

Goal state after:
case pos
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : (k * m).ProbablePrime (k * j)
⊢ k ∣ 1
Module: Mathlib.NumberTheory.FermatPsp

Goal state before:
pp: b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p - b) * (b ^ p + b) = (b ^ (p - 1 + 1) - b) * (b ^ p + b)

Tactic:
by rw [Nat.sub_add_cancel hp]

Goal state after:
Module: Mathlib.RingTheory.Ideal.NatInt

Goal state before:
pp: case refine_1.inr
s✝ : LTSeries (PrimeSpectrum ℕ)
hs : 2 < s✝.length
s : RelSeries {(a, b) | a < b} := RelSeries.take s✝ ⟨3, ⋯⟩
this : NeZero s.length
h1 : ⊥ < (s.toFun 1).asIdeal
p : ℕ
hp : Nat.Prime p
hsp : (s.toFun 1).asIdeal = span {p}
⊢ False

Tactic:
obtain hmax | ⟨q, hq, hsq⟩ :=
      (Ideal.isPrime_nat_iff.mp (s 2).2).resolve_left (h1.trans (s.step 1)).ne'

Goal state after:
case refine_1.inr.inl
s✝ : LTSeries (PrimeSpectrum ℕ)
hs : 2 < s✝.length
s : RelSeries {(a, b) | a < b} := RelSeries.take s✝ ⟨3, ⋯⟩
this : NeZero s.length
h1 : ⊥ < (s.toFun 1).asIdeal
p : ℕ
hp : Nat.Prime p
hsp : (s.toFun 1).asIdeal = span {p}
hmax : (s.toFun 2).asIdeal = maximalIdeal ℕ
⊢ False

case refine_1.inr.inr
s✝ : LTSeries (PrimeSpectrum ℕ)
hs : 2 < s✝.length
s : RelSeries {(a, b) | a < b} := RelSeries.take s✝ ⟨3, ⋯⟩
this : NeZero s.length
h1 : ⊥ < (s.toFun 1).asIdeal
p : ℕ
hp : Nat.Prime p
hsp : (s.toFun 1).asIdeal = span {p}
q : ℕ
hq : Nat.Prime q
hsq : (s.toFun 2).asIdeal = span {q}
⊢ False
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: n : ℕ
s : Set ℕ
⊢ FrobeniusNumber n s ↔ n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s

Tactic:
by
  simp_rw [FrobeniusNumber, IsGreatest, upperBounds, Set.mem_ofPred, not_imp_comm, not_le]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: case inr
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this : P.IsMaximal
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P

Tactic:
let := Localization.AtPrime.algebraOfLiesOver (P.under A) P

Goal state after:
case inr
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 B
inst✝ : P.IsPrime
hPbot : P ≠ ⊥
hp : Ideal.under A P ≠ ⊥
hp' : ¬Ideal.map (algebraMap A B) (Ideal.under A P) = ⊥
this✝ : P.IsMaximal
this : Algebra (Localization.AtPrime (Ideal.under A P)) (Localization.AtPrime P) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under A P) P
⊢ ¬P ∣ differentIdeal A B ↔ IsUnramifiedAt A P
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
⊢ IsCoprime S.Y S.Z

Tactic:
← IsCoprime.pow_iff (m := 3) (n := 3) (by decide) (by decide),

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ IsCoprime (S.Y ^ 3) (S.Z ^ 3)
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this✝ : Nonempty { j // x j ≠ 0 }
this : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
v : ↑nonarchAbsVal
⊢ ⨆ i, ↑v (x i) = ⨆ i, ↑v (x ↑i)

Tactic:
obtain ⟨i, hi⟩ : ∃ j, x j ≠ 0 := Function.ne_iff.mp hx

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this✝ : Nonempty { j // x j ≠ 0 }
this : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
v : ↑nonarchAbsVal
i : ι
hi : x i ≠ 0
⊢ ⨆ i, ↑v (x i) = ⨆ i, ↑v (x ↑i)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ HasSum (fun n ↦ term (n + 1) 1) (1 - γ)

Tactic:
rw [hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) 1)]
  change Tendsto (fun N ↦ termSum 1 N) atTop _
  simp_rw [termSum_one, sub_eq_neg_add]
  refine Tendsto.add ?_ tendsto_const_nhds
  have := (tendsto_eulerMascheroniSeq'.comp (tendsto_add_atTop_nat 1)).neg
  refine this.congr' (Eventually.of_forall (fun n ↦ ?_))
  simp_rw [Function.comp_apply, eulerMascheroniSeq', reduceCtorEq, if_false]
  push_cast
  abel

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

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
hx : x ≠ 0
H : x • ![x⁻¹, 1] = ![1, x]
⊢ mulHeight ![x⁻¹, 1] = mulHeight ![x, 1]

Tactic:
rw [← mulHeight_smul_eq_mulHeight _ hx, H, mulHeight_swap]

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

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
n : ℤ
h : 0 ≤ n
⊢ mulHeight₁ (x ^ n) = mulHeight₁ x ^ n.natAbs

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

Goal state before:
pp: case h₂.inr
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
this : Nonempty ι'
v : ↑nonarchAbsVal
j : ι'
h₀ : coeff 0 (p j) ≠ 0
⊢ ↑v (coeff 0 (p j)) ≤ max (⨆ s, ↑v (coeff (↑s) (p j))) 1

Tactic:
exact le_sup_of_le_left <| Finite.le_ciSup_of_le ⟨0, by simp [h₀]⟩ le_rfl

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

Goal state before:
pp: case h
⊢ Tendsto (fun x ↦ x * termTSum x) (𝓝[>] 1) (𝓝 (termTSum 1))

Tactic:
rw [← one_mul (termTSum 1)]

Goal state after:
case h
⊢ Tendsto (fun x ↦ x * termTSum x) (𝓝[>] 1) (𝓝 (1 * termTSum 1))
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ Tendsto (fun s ↦ riemannZeta ↑s - 1 / (↑s - 1)) (𝓝[>] 1) (𝓝 ↑γ)

Tactic:
by
  suffices Tendsto (fun s : ℝ ↦ (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1))
    (𝓝[>] 1) (𝓝 γ) by
    apply ((Complex.continuous_ofReal.tendsto _).comp this).congr'
    filter_upwards [self_mem_nhdsWithin] with s hs
    simp only [Function.comp_apply, Complex.ofReal_sub, Complex.ofReal_div,
      Complex.ofReal_one, sub_left_inj, Complex.ofReal_tsum]
    rw [zeta_eq_tsum_one_div_nat_add_one_cpow (by simpa using hs)]
    congr 1 with n
    rw [Complex.ofReal_cpow (by positivity)]
    norm_cast
  suffices aux2 : Tendsto (fun s : ℝ ↦ (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1))
    (𝓝[>] 1) (𝓝 (1 - termTSum 1)) by
    have := term_tsum_one.tsum_eq
    rw [← termTSum, eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at this
    simpa only [this] using aux2
  apply Tendsto.congr'
  · filter_upwards [self_mem_nhdsWithin] with s hs using (zeta_limit_aux1 hs).symm
  · apply tendsto_const_nhds.sub
    rw [← one_mul (termTSum 1)]
    apply (tendsto_id.mono_left nhdsWithin_le_nhds).mul
    have := continuousOn_termTSum.continuousWithinAt self_mem_Ici
    exact Tendsto.mono_left this (nhdsWithin_mono _ Ioi_subset_Ici_self)

Goal state after:
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
⊢ (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ =ᶠ[𝓝[≠] 1] fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)

Tactic:
EventuallyEq,

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, ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) x = 1 / (x - 1) - 1 / x.Gammaℝ / (x - 1)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

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

Tactic:
eq_sub_iff_add_eq

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

Goal state before:
pp: case pos
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
a b c d : K
hab : ![a, b] = 0
⊢ mulHeight ![a * c, a * d + b * c, b * d] ≤ max C 1 * mulHeight ![c, d]

Tactic:
show a = 0 from congrFun hab 0,

Goal state after:
case pos
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
a b c d : K
hab : ![a, b] = 0
⊢ mulHeight ![0 * c, 0 * d + b * c, b * d] ≤ max C 1 * mulHeight ![c, d]
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
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ (∑ a, (χ * φ) a * ψ a) * jacobiSum χ φ = (∑ i ∈ univ \ {0}, (χ * φ) i * ψ i) * jacobiSum χ φ

Tactic:
sum_eq_sum_sdiff_singleton_add (mem_univ (0 : F)),

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
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
⊢ (∑ x ∈ univ \ {0}, (χ * φ) x * ψ x + (χ * φ) 0 * ψ 0) * jacobiSum χ φ =
    (∑ i ∈ univ \ {0}, (χ * φ) i * ψ i) * jacobiSum χ φ
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 ^ (Module.finrank ℚ K - 1)
⊢ ↑n ≤ mulHeight₁ x

Tactic:
rw [← totalWeight_eq_finrank] at ha₂

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)
⊢ ↑n ≤ mulHeight₁ x
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
⊢ deriv riemannZeta s = -(s - 1)⁻¹ ^ 2 * riemannZeta₁ s + (s - 1)⁻¹ * deriv riemannZeta₁ s

Tactic:
by
  have := sub_ne_zero_of_ne hs
  convert EventuallyEq.deriv_eq (f := fun s ↦ (s - 1)⁻¹ * riemannZeta₁ s) ?_
  · rw [deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_inv'' (by fun_prop) (by exact this)]
    simp [field]
  · filter_upwards [compl_singleton_mem_nhds hs] using by grind [riemannZeta_eq_inv_sub_mul]

Goal state after:
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
x : S
i : Fin f.natDegree
⊢ (h.basis.repr x) i = (h.modByMonicHom x).coeff ↑i

Tactic:
by
  simp [IsAdjoinRootMonic.basis, toFinsupp_apply]

Goal state after:
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
inst✝ : Nontrivial S
x : R
i : ℕ
⊢ (x • Pi.single 0 1) i = Pi.single 0 x i

Tactic:
Pi.smul_apply,

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
inst✝ : Nontrivial S
x : R
i : ℕ
⊢ x • Pi.single 0 1 i = Pi.single 0 x i
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case inl
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Tactic:
have hχ : changeLevel hMN χ ≠ 1 := h ∘ (changeLevel_eq_one_iff hMN).mp

Goal state after:
case inl
M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ : (changeLevel hMN) χ ≠ 1
⊢ LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))
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
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
J' : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
hJ' : (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J'
⊢ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J') = J

Tactic:
← hJ',

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
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
this :
  Multiset.count J (normalizedFactors (Ideal.map (algebraMap R S) I)) =
    Multiset.count (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)))
J' : ↑{d | d ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
hJ' : (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J'
⊢ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm
        ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩)) =
    J
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
this : ∑ x, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
by
    simp only [completedLFunction_def_even hΦ, neg_sub, completedHurwitzZetaEven_one_sub, this]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
⊢ Differentiable ℂ B.F

Tactic:
intro s
  rcases ne_or_eq s 1 with hs | rfl
  · exact B.F_differentiableAt_of_ne hs
  -- now need to deal with `s = 1`
  refine (analyticAt_of_differentiable_on_punctured_nhds_of_continuousAt ?_ ?_).differentiableAt
  · filter_upwards [self_mem_nhdsWithin] with t ht
    exact B.F_differentiableAt_of_ne ht
  -- now reduced to showing *continuity* at s = 1
  let G := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1
  let H := Function.update (fun s ↦ (B.χ.LFunction s - B.χ.LFunction 1) / (s - 1)) 1
    (deriv B.χ.LFunction 1)
  have : B.F = G * H := by
    ext1 t
    rcases eq_or_ne t 1 with rfl | ht
    · simp only [F, G, H, Pi.mul_apply, one_mul, Function.update_self]
    · simp only [F, G, H, Function.update_of_ne ht, mul_comm _ (riemannZeta _), B.hχ, sub_zero,
      Pi.mul_apply, mul_assoc, mul_div_cancel₀ _ (sub_ne_zero.mpr ht)]
  rw [this]
  apply ContinuousAt.mul
  · simpa only [G, continuousAt_update_same] using riemannZeta_residue_one
  · exact (B.χ.differentiableAt_LFunction 1 (.inr B.χ_ne)).hasDerivAt.continuousAt_div

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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
n : ℕ
⊢ ↑q.totient * ↑(residueClass a n) = ∑ χ, χ a⁻¹ * χ ↑n * ↑(Λ n)

Tactic:
simp +contextual only [residueClass, Set.indicator_apply, Set.mem_ofPred_eq, apply_ite,
    ofReal_zero, mul_zero, ← Finset.sum_mul, sum_char_inv_mul_char_eq ℂ ha n, eq_comm (a := a),
    ite_mul, zero_mul, ↓reduceIte, ite_self]

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

Goal state before:
pp: case pos
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
n : ℕ
hn : n = 0
⊢ ↑(residueClass a n) / ↑n ^ ↑x = 0

Tactic:
simp only [hn, residueClass_apply_zero, ofReal_zero, zero_div]

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

Goal state before:
pp: f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] 0
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
⊢ (fun x ↦ ↑n ^ ↑x * LSeries f ↑x) =ᶠ[atTop] fun x ↦ 0

Tactic:
rw [eventuallyEq_iff_exists_mem] at H ⊢

Goal state after:
f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
H : ∃ s ∈ atTop, Set.EqOn (fun x ↦ LSeries f ↑x) 0 s
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
⊢ ∃ s ∈ atTop, Set.EqOn (fun x ↦ ↑n ^ ↑x * LSeries f ↑x) (fun x ↦ 0) s
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] fun x ↦ LSeries g ↑x
⊢ (fun x ↦ LSeries (f - g) ↑x) =ᶠ[atTop] 0

Tactic:
EventuallyEq,

Goal state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∀ᶠ (x : ℝ) in atTop, LSeries f ↑x = LSeries g ↑x
⊢ ∀ᶠ (x : ℝ) in atTop, LSeries (f - g) ↑x = 0 x
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ ε * ((s - 1) * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s)) = ε

Tactic:
rw [integral_Ioi_rpow_of_lt (by rwa [neg_lt_neg_iff]) zero_lt_one, Real.one_rpow]

Goal state after:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ ε * ((s - 1) * (-1 / (-s + 1))) = ε
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
x : K
⊢ x ∈ 𝒪[K] ↔ ‖x‖ ≤ 1

Tactic:
by
  simp [Valuation.mem_integer_iff, ← NNReal.coe_le_coe]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mp.mk
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : TotallyBounded Set.univ
p : ↥𝒪[K]
hp : Irreducible p
t : Set ↥𝒪[K]
ht : t.Finite
a✝ : IsLocalRing.ResidueField ↥𝒪[K]
x y : ↥𝒪[K]
hy : y ∈ t
hy' : dist y x < ‖p‖
⊢ y - x ∈ {y | v ((algebraMap (↥v.integer) K) y) ≤ v ((algebraMap (↥v.integer) K) p)}

Tactic:
simpa [dist_eq_norm] using! hy'.le

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
hb' : Odd (b % (4 * a.natAbs))
⊢ χ₄ ↑(b % 4) * J(↑a.natAbs | b % (4 * a.natAbs)) = χ₄ ↑(b % (4 * a.natAbs) % 4) * J(↑a.natAbs | b % (4 * a.natAbs))

Tactic:
mod_mod_of_dvd b (dvd_mul_right 4 _)

Goal state after:
case inr
a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
hb' : Odd (b % (4 * a.natAbs))
⊢ χ₄ ↑(b % 4) * J(↑a.natAbs | b % (4 * a.natAbs)) = χ₄ ↑(b % 4) * J(↑a.natAbs | b % (4 * a.natAbs))
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : 0 ≤ t
⊢ ‖S t - l * ↑t‖ * ‖t ^ (-s - 1)‖ = ‖S t - l * ↑t‖ * t ^ (-s - 1)

Tactic:
Real.norm_of_nonneg (Real.rpow_nonneg ht _)

Goal state after:
case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : 0 ≤ t
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) = ‖S t - l * ↑t‖ * t ^ (-s - 1)