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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
x : 𝓞 K
h : ∏ v, (⨆ i, v (![↑x, ↑n] i)) ^ v.mult ≤ B
v : InfinitePlace K
⊢ v ↑x ≤ B / ↑n ^ (totalWeight K - 1)

Tactic:
rw [le_div_iff₀' (by positivity)]
  calc
    _ ≤ n ^ (totalWeight K - 1) * ⨆ i, v (![(x : K), n] i) := by
      gcongr; exact Finite.le_ciSup_of_le 0 le_rfl
    _ ≤ (∏ v' ∈ univ.erase v, (⨆ i, v' (![↑x, ↑n] i)) ^ v'.mult) *
         (⨆ i, v (![↑x, ↑n] i)) ^ (v.mult - 1) * ⨆ i, v (![(x : K), n] i) := by
      rw [pow_totalWeight_sub_one_eq hn]
      gcongr
      · exact Real.iSup_nonneg_of_nonnegHomClass ..
      · exact prod_nonneg fun _ _ ↦ pow_nonneg (Real.iSup_nonneg_of_nonnegHomClass ..) _
      all_goals exact Finite.le_ciSup_of_le 1 <| by simp
    _ ≤ B := by
      rwa [mul_assoc, pow_sub_one_mul v.mult_ne_zero, prod_erase_mul _ _ (mem_univ v)]

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

Goal state before:
pp: 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 ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

Tactic:
obtain ⟨z₁, hz₁, Hz₁⟩ := hμ.self_sub_one_pow_dvd_order hn

Goal state after:
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
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 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✝³ : Ring T
inst✝² : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst✝¹ : Ring U
inst✝ : Algebra R U
e : T ≃ₐ[R] U
a : S
⊢ (h.algEquiv (h'.ofAlgEquiv e)) a = ((h.algEquiv h').trans e) a

Tactic:
simp [algEquiv_def, AlgEquiv.trans_apply, adjoinRootAlgEquiv_apply_eq_map, ofAlgEquiv_map_apply]

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

Goal state before:
pp: case neg
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 ∈ ℤ[μ], 0 + 0 - ↑(n * q + 1) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1) = -1 + z * (μ - 1) ^ 2

Tactic:
have : NeZero n := ⟨by lia⟩

Goal state after:
case neg
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
⊢ ∃ z ∈ ℤ[μ], 0 + 0 - ↑(n * q + 1) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1) = -1 + z * (μ - 1) ^ 2
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ ↑N ^ (-s) * Φ j * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s) = Φ j * ↑N ^ (-s) * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s)

Tactic:
mul_comm _ (Φ _)

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j * ↑N ^ (-s) * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s) = Φ j * ↑N ^ (-s) * (1 / (↑m + ↑(↑j.val / ↑N)) ^ s)
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 : ℕ
this : ↑(toCircle ↑(↑j.val * ↑n)) = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N))
⊢ ↑(toCircle (j * ↑n)) / ↑n ^ s = ↑(toCircle (↑j.val * ↑n)) / ↑n ^ s

Tactic:
natCast_zmod_val

Goal state after:
case e_f
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this : ↑(toCircle ↑(↑j.val * ↑n)) = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N))
⊢ ↑(toCircle (j * ↑n)) / ↑n ^ s = ↑(toCircle (j * ↑n)) / ↑n ^ 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
⊢ normalizedFactors (Ideal.map (algebraMap R S) I) =
    Multiset.map (fun f ↦ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
      (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach

Tactic:
by
  ext J
  -- WLOG, assume J is a normalized factor
  by_cases hJ : J ∈ normalizedFactors (I.map (algebraMap R S))
  swap
  · rw [Multiset.count_eq_zero.mpr hJ, eq_comm, Multiset.count_eq_zero, Multiset.mem_map]
    simp only [not_exists]
    rintro J' ⟨_, rfl⟩
    exact
      hJ ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J').prop
  -- Then we just have to compare the multiplicities, which we already proved are equal.
  have := emultiplicity_factors_map_eq_emultiplicity hI hI' hx hx' hJ
  rw [emultiplicity_eq_count_normalizedFactors, emultiplicity_eq_count_normalizedFactors,
    UniqueFactorizationMonoid.normalize_normalized_factor _ hJ,
    UniqueFactorizationMonoid.normalize_normalized_factor, Nat.cast_inj] at this
  · refine this.trans ?_
    -- Get rid of the `map` by applying the equiv to both sides.
    generalize hJ' :
      (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩ = J'
    have : ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm J' : Ideal S) =
        J := by
      rw [← hJ', Equiv.symm_apply_apply _ _, Subtype.coe_mk]
    subst this
    -- Get rid of the `attach` by applying the subtype `coe` to both sides.
    rw [Multiset.count_map_eq_count' fun f =>
        ((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f :
          Ideal S),
      Multiset.count_attach]
    · exact Subtype.coe_injective.comp (Equiv.injective _)
  · exact (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' _).prop
  · exact irreducible_of_normalized_factor _
        (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' _).prop
  · exact Polynomial.map_monic_ne_zero (minpoly.monic hx')
  · exact irreducible_of_normalized_factor _ hJ
  · rwa [← bot_eq_zero, Ne,
      map_eq_bot_iff_of_injective (FaithfulSMul.algebraMap_injective R S)]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: 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
⊢ ∫ (x : ℝ) in ↑0 / ↑m..↑m / ↑m, bernoulliFun (k + 1) x = 0

Tactic:
simp [div_self m0', integral_bernoulliFun_eq_zero]

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case h
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
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach =
    {⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩}

Tactic:
apply Multiset.map_injective Subtype.coe_injective

Goal state after:
case h
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
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ Multiset.map (fun a ↦ ↑a) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach =
    Multiset.map (fun a ↦ ↑a) {⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩}
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : ℂ
Φ : ZMod N → ℂ
s : ℂ
⊢ completedLFunction (fun j ↦ a * Φ j) s = a * completedLFunction Φ s

Tactic:
by
  simp only [completedLFunction, mul_add, mul_sum]
  congr with i <;> ring

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
fourier_zero,

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

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ bernoulliFourierCoeff k 0 = 0

Tactic:
simp_rw [bernoulliFourierCoeff, fourierCoeffOn_eq_integral, neg_zero, fourier_zero, sub_zero,
    div_one, one_smul, intervalIntegral.integral_ofReal, integral_bernoulliFun_eq_zero hk,
    ofReal_zero]

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

Goal state before:
pp: k : ℕ
⊢ -↑(bernoulli' (k + 1)) / (↑k + 1) = (-1) ^ k * (↑(-1) ^ (k + 1) * ↑(bernoulli' (k + 1))) / (↑k + 1)

Tactic:
Rat.cast_neg,

Goal state after:
k : ℕ
⊢ -↑(bernoulli' (k + 1)) / (↑k + 1) = (-1) ^ k * ((-↑1) ^ (k + 1) * ↑(bernoulli' (k + 1))) / (↑k + 1)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case e_a.e_f.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : s ≠ 0 ∨ Φ 0 = 0
⊢ Φ 0 * hurwitzZetaEven (toAddCircle 0) s = Φ 0 * (completedHurwitzZetaEven (toAddCircle 0) s / s.Gammaℝ)

Tactic:
rcases hs with hs | hΦ'
    · rw [hurwitzZetaEven_def_of_ne_or_ne (.inr hs)]
    · simp only [hΦ', map_zero, zero_mul]

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

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

Tactic:
let G := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1

Goal state after:
case inr.refine_2
N : ℕ
inst✝ : NeZero N
B : BadChar N
G : ℂ → ℂ := Function.update (fun s ↦ (s - 1) * riemannZeta s) 1 1
⊢ ContinuousAt B.F 1
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: p : Nat.Primes
k : ℕ
⊢ 2 * ((↑↑p)⁻¹ ^ (-1 / 2) * (↑↑p)⁻¹ ^ (k + 2)) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)

Tactic:
← Real.rpow_natCast,

Goal state after:
p : Nat.Primes
k : ℕ
⊢ 2 * ((↑↑p)⁻¹ ^ (-1 / 2) * (↑↑p)⁻¹ ^ ↑(k + 2)) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: p : Nat.Primes
k : ℕ
⊢ 2 * (↑↑p)⁻¹ ^ (-1 / 2 + (↑k + ↑2)) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)

Tactic:
Nat.cast_two,

Goal state after:
p : Nat.Primes
k : ℕ
⊢ 2 * (↑↑p)⁻¹ ^ (-1 / 2 + (↑k + 2)) = 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case convert_2
N : ℕ
inst✝ : NeZero N
⊢ Tendsto (fun w ↦ 1 + w) (𝓝[≠] 0) (𝓝[≠] 1)

Tactic:
simpa only [tendsto_iff_comap, Homeomorph.coe_addLeft, add_zero, map_le_iff_le_comap] using
          ((Homeomorph.addLeft (1 : ℂ)).map_punctured_nhds_eq 0).le

Goal state after:
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)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
H : n + 1 < k
⊢ ‖F y' k‖ ≤ ‖F y k‖

pp: case inr
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)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
H : k ≤ n + 1
⊢ ‖F y' k‖ ≤ ‖F y k‖

Tactic:
· simp only [Set.mem_ofPred_eq, H, Set.indicator_of_mem, norm_div, norm_cpow_real,
      Complex.norm_natCast, F]
    rw [← Nat.cast_one, ← Nat.cast_add, Complex.norm_natCast]
    have hkn : 1 ≤ (k / (n + 1 :) : ℝ) :=
      (one_le_div (by positivity)).mpr <| mod_cast Nat.le_of_succ_le H
    gcongr

Goal state after:
case inr
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)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
y' : ℝ
hy' : y ≤ y'
k : ℕ
H : k ≤ n + 1
⊢ ‖F y' k‖ ≤ ‖F y k‖
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case neg.refine_1
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
⊢ ∀ (n : ℕ), F n = 0

Tactic:
have ha : ¬ abscissaOfAbsConv F = ⊤ := abscissaOfAbsConv_congr hF ▸ h

Goal state after:
case neg.refine_1
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 = ⊤
⊢ ∀ (n : ℕ), F n = 0
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
⊢ False

Tactic:
let C := ∑' n, residueClass a n / n

Goal state after:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
⊢ False
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : k ≠ 0
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)

Tactic:
rw [mul_zero, Real.cos_zero, mul_one]

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
ε : ℝ
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
⊢ (-↑s).re < -1

Tactic:
rwa [neg_re, neg_lt_neg_iff]

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
ε : ℝ
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
⊢ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε

Tactic:
let Cs := ∫ t in Set.Ioc 1 T, ‖S t - l * t‖ * t ^ (-s - 1)

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ε : ε > 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)
⊢ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑2 | b) ^ e * (qrSign b a' * J(↑b | a')) =
    J(↑2 | b % (4 * a)) ^ e * (qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a'))

Tactic:
Nat.cast_two,

Goal state after:
case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(2 | b) ^ e * (qrSign b a' * J(↑b | a')) =
    J(2 | b % (4 * a)) ^ e * (qrSign (b % (4 * a)) a' * J(↑(b % (4 * a)) | a'))
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a | b) = fastJacobiSymAux (a % ↑b).natAbs b false ⋯

Tactic:
fastJacobiSymAux.eq_jacobiSym,

Goal state after:
case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a | b) = if false = true then -J(↑(a % ↑b).natAbs | b) else J(↑(a % ↑b).natAbs | b)

case neg.hb2
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b % 2 = 1

case neg.hb1
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b > 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
⊢ J(a | b) = fastJacobiSym a b

Tactic:
| ind b IH =>

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
x✝ : IsSimpleRing A
⊢ IsField ↥⊤

Tactic:
by
    rw [← Subring.center_eq_top A]; exact IsSimpleRing.isField_center A

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
⊢ CompactSpace ↥𝒪[K] ↔ CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨_, _, h⟩ ↦ ⟨?_⟩⟩

Goal state after:
case refine_1
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
h : CompactSpace ↥𝒪[K]
⊢ CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]

case refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
x✝ : CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]
left✝¹ : CompleteSpace ↥𝒪[K]
left✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
⊢ IsCompact Set.univ
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
⊢ {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.Finite ∧
    {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.ncard ≤ ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)

Tactic:
have h_card :
      Set.ncard {p : ℤ[X] | p.natDegree ≤ n ∧ ∀ i : Fin (n + 1), ‖p.coeff i‖ ≤ n.choose i * B} =
      ∏ i : Fin (n + 1), (2 * ⌊n.choose i * B⌋₊ + 1) := by
    simp_rw [norm_eq_abs, abs_le]
    rw [← boxPoly, ncard_boxPoly]
    simp only [ceil_neg, sub_neg_eq_add, ← two_mul]
    apply Finset.prod_congr rfl fun i _ ↦ ?_
    zify
    rw [toNat_of_nonneg (by positivity), ← natCast_floor_eq_floor (by positivity)]
    norm_cast

Goal state after:
n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
⊢ {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.Finite ∧
    {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B}.ncard ≤ ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

Tactic:
have : NeZero n := ⟨hn⟩

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
this : NeZero n
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:

Tactic:
(s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
      _ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
      _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
      _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by
        rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
      _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ 2 ∣ q + 1

Tactic:
← even_iff_two_dvd

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ Even (q + 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
⊢ ω ^ ((q + 1) / 2) * ωb ^ ((q + 1) / 4) = -ωb ^ ((q + 1) / 4)

Tactic:
rw [pow_ω odd leg3 leg2]

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
⊢ -1 * ωb ^ ((q + 1) / 4) = -ωb ^ ((q + 1) / 4)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬↑(sModNat (2 ^ p - 1) (p - 2)) = 0

Tactic:
← sModNatTR_eq_sModNat

Goal state after:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬↑(sModNatTR (2 ^ p - 1) (p - 2)) = 0
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: G : Type u_1
inst✝⁶ : CommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedMonoid G
inst✝³ : TopologicalSpace G
inst✝² : OrderTopology G
inst✝¹ : MulArchimedean G
inst✝ : DiscreteTopology G
a✝ : Nontrivial G
⊢ IsCyclic G

Tactic:
exact LinearOrderedCommGroup.isCyclic_iff_not_denselyOrdered.mpr fun h ↦
    have := h.subsingleton_of_discreteTopology; false_of_nontrivial_of_subsingleton G

Goal state after: