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

Goal state before:
pp: n : ℕ
h : 3 ^ 2 ^ (2 ^ n - 1) = -1
⊢ Prime n.fermatNumber

Tactic:
by
  have := Fact.mk (two_lt_fermatNumber n)
  unfold fermatNumber at h this
  have key : 2 ^ n = 2 ^ n - 1 + 1 := (Nat.sub_add_cancel Nat.one_le_two_pow).symm
  apply lucas_primality (p := 2 ^ (2 ^ n) + 1) (a := 3)
  · rw [Nat.add_sub_cancel, key, pow_succ, pow_mul, ← pow_succ, ← key, h, neg_one_sq]
  · intro p hp1 hp2
    rw [Nat.add_sub_cancel, (Nat.prime_dvd_prime_iff_eq hp1 prime_two).mp (hp1.dvd_of_dvd_pow hp2),
        key, pow_succ, Nat.mul_div_cancel _ two_pos, ← pow_succ, ← key, h]
    exact neg_one_ne_one

Goal state after:
Module: Mathlib.NumberTheory.Fermat

Goal state before:
pp: a n p : ℕ
hp : Prime p
hp2 : p ≠ 2
hpdvd : p ∣ a ^ 2 ^ n + 1
this✝ : Fact (2 < p)
this : Fact (Prime p)
ha1 : 1 = 0
h : ↑a = 0
⊢ False

Tactic:
exact one_ne_zero ha1

Goal state after:
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:
Nat.sub_add_cancel hp

Goal state after:
b p : ℕ
hb : 0 < b
hp : 1 ≤ p
hi_bsquared : 1 ≤ b ^ 2
⊢ (b ^ p - b) * (b ^ p + b) = (b ^ p - b) * (b ^ p + b)
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: case refine_2
m✝ n✝¹ : ℕ
s✝ t✝ : Set ℕ
n✝ : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : ↑t ⊆ ↑s
hn : ∀ m ≥ n, setGcd ↑s ∣ m → m ∈ Ideal.span ↑t
m : ℕ
hm : m ∈ s
⊢ m ∈ Submodule.span ℕ ↑(t ∪ {m ∈ Finset.range n | m ∈ s})

Tactic:
obtain le | gt := le_or_gt n m

Goal state after:
case refine_2.inl
m✝ n✝¹ : ℕ
s✝ t✝ : Set ℕ
n✝ : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : ↑t ⊆ ↑s
hn : ∀ m ≥ n, setGcd ↑s ∣ m → m ∈ Ideal.span ↑t
m : ℕ
hm : m ∈ s
le : n ≤ m
⊢ m ∈ Submodule.span ℕ ↑(t ∪ {m ∈ Finset.range n | m ∈ s})

case refine_2.inr
m✝ n✝¹ : ℕ
s✝ t✝ : Set ℕ
n✝ : ℕ
s : Submodule ℕ ℕ
t : Finset ℕ
n : ℕ
hts : ↑t ⊆ ↑s
hn : ∀ m ≥ n, setGcd ↑s ∣ m → m ∈ Ideal.span ↑t
m : ℕ
hm : m ∈ s
gt : m < n
⊢ m ∈ Submodule.span ℕ ↑(t ∪ {m ∈ Finset.range n | m ∈ s})
Module: Mathlib.NumberTheory.Harmonic.Bounds

Goal state before:
pp: case e'_3.e'_6
n : ℕ
hn0 : ¬n = 0
hn : 1 ≤ n
⊢ ↑n = ↑(n + 1) - 1

Tactic:
simp only [Nat.cast_add, Nat.cast_one, add_sub_cancel_right]

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

Goal state before:
pp: case hx
y : ℝ
hy : 1 ≤ y
⊢ 0 < ↑⌊y⌋₊

Tactic:
exact_mod_cast Nat.floor_pos.mpr hy

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
inst✝ : Finite ι
x : ι → K
e : ↑(support x) ⊕ ↑(support x)ᶜ ≃ ι := Equiv.Set.sumCompl (support x)
val : ↑(support x)
⊢ x (e (Sum.inl val)) = Sum.elim (fun i ↦ x ↑i) 0 (Sum.inl val)

Tactic:
simp [e]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
n : ℕ
x : Fin n → K
e : Fin n ⊕ Fin 1 ≃ Fin n.succ := (Equiv.sumComm (Fin n) (Fin 1)).trans (finSumFinEquiv.trans (finCongr ⋯))
j : Fin n ⊕ Fin 1
val✝ : Fin n
⊢ (vecCons 0 x ∘ ⇑e) (Sum.inl val✝) = Sum.elim x 0 (Sum.inl val✝)

Tactic:
simp [e]

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
ι : Type u_2
ι' : Type u_3
inst✝³ : Fintype ι
inst✝² : Finite ι'
inst✝¹ : AdmissibleAbsValues K
inst✝ : Nonempty ι
A : ι' × ι → K
x : ι → K
⊢ (mulHeight fun j ↦ ∑ i, A (j, i) * x i) ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x

Tactic:
by
  have H₀ : 1 ≤ Nat.card ι ^ totalWeight K * mulHeight A * mulHeight x := by
    rw [show (1 : ℝ) = 1 * 1 * 1 by ring]
    gcongr
    · exact_mod_cast Nat.one_le_pow _ _ Nat.card_pos
    · exact one_le_mulHeight _
    · exact one_le_mulHeight _
  rcases isEmpty_or_nonempty ι' with hι' | hι'
  · simpa only [mulHeight_eq_one_of_subsingleton, mul_one] using H₀
  rcases eq_or_ne (fun j ↦ ∑ i, A (j, i) * x i) 0 with h | h
  · simpa only [h, mulHeight_zero] using H₀
  rcases eq_or_ne A 0 with rfl | hA
  · simpa using H₀
  rcases eq_or_ne x 0 with rfl | hx
  · simpa using H₀
  rw [mulHeight_eq h, mulHeight_eq hA, mulHeight_eq hx, mul_mul_mul_comm, ← mul_assoc, ← mul_assoc,
    mul_assoc (_ * _ * _)]
  gcongr
  · exact finprod_nonneg fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _
  · refine mul_nonneg (mul_nonneg (by simp) ?_) ?_ <;>
      exact prod_map_nonneg fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _
  · -- archimedean part: reduce to "local" statement `linearMap_apply_bound`
    rw [mul_assoc, ← prod_map_mul, ← prod_replicate, totalWeight, ← map_const', ← prod_map_mul]
    refine prod_map_le_prod_map₀ _ _ (fun v _ ↦ Real.iSup_nonneg_of_nonnegHomClass v _) fun v _ ↦ ?_
    rw [mul_comm (iSup _), ← mul_assoc]
    exact v.iSup_abv_linearMap_apply_le A x
  · -- nonarchimedean part: reduce to "local" statement `linearMap_apply_bound_of_isNonarchimedean`
    rw [← finprod_mul_distrib (by fun_prop) (by fun_prop)]
    refine finprod_le_finprod (by fun_prop)
      (fun v ↦ Real.iSup_nonneg_of_nonnegHomClass v.val _) (by fun_prop) fun v ↦ ?_
    exact (isNonarchimedean _ v.prop).iSup_abv_linearMap_apply_le A x

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 ι'
x : ι → K
hx : x ≠ 0
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (mulHeight fun a ↦ x a.1 * y a.2) =
    ((Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) * mulHeight y

Tactic:
mulHeight_eq hy,

Goal state after:
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
y : ι' → K
hy : y ≠ 0
hxy : (fun a ↦ x a.1 * y a.2) ≠ 0
⊢ (mulHeight fun a ↦ x a.1 * y a.2) =
    ((Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) *
      ((Multiset.map (fun v ↦ ⨆ i, v (y i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (y i))
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
a b : 𝓞 K
h : ↑n * a = ↑m * b
⊢ (Submodule.toAddSubgroup (span {↑m})).relIndex (Submodule.toAddSubgroup (span {↑m, a})) =
    (Submodule.toAddSubgroup (span {↑n})).relIndex (Submodule.toAddSubgroup (span {↑n, b}))

Tactic:
refine (relIndex_span_span_nat_mul m hn a).trans ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
m n : ℕ
hm : m ≠ 0
hn : n ≠ 0
a b : 𝓞 K
h : ↑n * a = ↑m * b
⊢ (Submodule.toAddSubgroup (span {↑n * ↑m})).relIndex (Submodule.toAddSubgroup (span {↑(n * m), ↑n * a})) =
    (Submodule.toAddSubgroup (span {↑n})).relIndex (Submodule.toAddSubgroup (span {↑n, b}))
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
⊢ ⨆ i, v ↑(x i) = 1

Tactic:
have hv : IsNonarchimedean (v ·) := FinitePlace.add_le v

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
x : ι → ℤ
v : FinitePlace ℚ
hx : Finset.univ.gcd x = 1
hv : IsNonarchimedean fun x ↦ v x
⊢ ⨆ i, v ↑(x i) = 1
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : R[X]
⊢ h.map (g %ₘ f) = h.map g

Tactic:
rw [← RingHom.sub_mem_ker_iff, mem_ker_map, modByMonic_eq_sub_mul_div, sub_right_comm,
    sub_self, zero_sub, dvd_neg]

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
g : R[X]
⊢ f ∣ f * (g /ₘ f)
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
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
⊢ span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R (adjoin.powerBasis' hx').gen)} =
    span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)}

Tactic:
rw [Algebra.adjoin.powerBasis'_minpoly_gen hx']

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

Goal state before:
pp: case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / (2 * 2 * ↑k * Complex.Gamma (2 * ↑k)) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * ↑k) / (2 * ↑k * 2 * Complex.Gamma (2 * ↑k))

Tactic:
mul_right_comm (2 : ℂ) (k : ℂ)

Goal state after:
case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / (2 * 2 * ↑k * Complex.Gamma (2 * ↑k)) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * ↑k) / (2 * 2 * ↑k * Complex.Gamma (2 * ↑k))
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
have i : ∫ x in (0 : ℝ)..m⁻¹, f (k + 1) x = 0 := by
      simp only [f]
      rw [intervalIntegral.integral_sub, intervalIntegral.integral_comp_mul_left _ m0', mul_zero,
        mul_inv_cancel₀ m0', integral_bernoulliFun_eq_zero (by lia), smul_zero, sub_eq_zero,
        intervalIntegral.integral_const_mul, eq_comm (a := 0), mul_eq_zero]
      · right
        rw [intervalIntegral.integral_finsetSum]
        · simp only [intervalIntegral.integral_comp_add_right, zero_add, ← one_div, ← add_div,
            add_comm (1 : ℝ), ← Nat.cast_add_one]
          rw [intervalIntegral.sum_integral_adjacent_intervals]
          · simp [div_self m0', integral_bernoulliFun_eq_zero]
          · intros; exact Continuous.intervalIntegrable (by fun_prop) _ _
        · intros; exact Continuous.intervalIntegrable (by fun_prop) _ _
      · exact Continuous.intervalIntegrable (by fun_prop) _ _
      · exact Continuous.intervalIntegrable (by fun_prop) _ _

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

Goal state before:
pp: case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ ↑(Real.sin ((↑k + 1 / 2) * π)) * (-↑1) ^ (k + 1) = -↑1

Tactic:
add_mul,

Goal state after:
case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ ↑(Real.sin (↑k * π + 1 / 2 * π)) * (-↑1) ^ (k + 1) = -↑1
Module: Mathlib.NumberTheory.LSeries.Linearity

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
⊢ term (-f) s = -term f s

Tactic:
by
  ext ⟨- | n⟩ <;>
  simp [neg_div]

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

Goal state before:
pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ χ.zetaMul n

Tactic:
simpa only [χ.isMultiplicative_zetaMul.multiplicative_factorization _ hn] using!
      Finset.prod_nonneg
        fun p hp ↦ zetaMul_prime_pow_nonneg hχ (Nat.prime_of_mem_primeFactors hp) _

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

Goal state before:
pp: case e_a.e_f
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
x : ℝ
hx : x ≥ y
m : ℕ
⊢ (if m = n + 1 then 0 else (↑n + 1) ^ ↑x * term f (↑x) m) = F x m

Tactic:
rcases eq_or_ne m (n + 1) with rfl | hm

Goal state after:
case e_a.e_f.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
x : ℝ
hx : x ≥ y
⊢ (if n + 1 = n + 1 then 0 else (↑n + 1) ^ ↑x * term f (↑x) (n + 1)) = F x (n + 1)

case e_a.e_f.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
x : ℝ
hx : x ≥ y
m : ℕ
hm : m ≠ n + 1
⊢ (if m = n + 1 then 0 else (↑n + 1) ^ ↑x * term f (↑x) m) = F x m
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑x) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x))

Tactic:
by
  -- first show it suffices to prove result for `Ico 0 1`
  suffices ∀ {y : ℝ}, y ∈ Ico (0 : ℝ) 1 →
      HasSum (fun (n : ℤ) ↦ 1 / (n : ℂ) ^ k * fourier n y)
        (-(2 * (π : ℂ) * I) ^ k / k ! * bernoulliFun k y) by
    rw [← Ico_insert_right (zero_le_one' ℝ), mem_insert_iff, or_comm] at hx
    rcases hx with (hx | rfl)
    · exact this hx
    · convert! this (left_mem_Ico.mpr zero_lt_one) using 1
      · rw [AddCircle.coe_period, QuotientAddGroup.mk_zero]
      · rw [bernoulliFun_endpoints_eq_of_ne_one (by lia : k ≠ 1)]
  intro y hy
  let B : C(𝕌, ℂ) :=
    ContinuousMap.mk ((↑) ∘ periodizedBernoulli k)
      (continuous_ofReal.comp (periodizedBernoulli.continuous (by lia)))
  have step1 : ∀ n : ℤ, fourierCoeff B n = -k ! / (2 * π * I * n) ^ k := by
    rw [ContinuousMap.coe_mk]; exact fourierCoeff_bernoulli_eq (by lia : k ≠ 0)
  have step2 :=
    has_pointwise_sum_fourier_series_of_summable
      ((summable_bernoulli_fourier hk).congr fun n => (step1 n).symm) y
  simp_rw [step1] at step2
  convert! step2.mul_left (-(2 * ↑π * I) ^ k / (k ! : ℂ)) using 2 with n
  · rw [smul_eq_mul, ← mul_assoc, mul_div, mul_neg, div_mul_cancel₀, neg_neg, mul_pow _ (n : ℂ),
      ← div_div, div_self]
    · rw [Ne, pow_eq_zero_iff', not_and_or]
      exact Or.inl two_pi_I_ne_zero
    · exact Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)
  · rw [ContinuousMap.coe_mk, Function.comp_apply, ofReal_inj, periodizedBernoulli,
      AddCircle.liftIco_coe_apply (show y ∈ Ico 0 (0 + 1) by rwa [zero_add])]

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
⊢ ‖L (fun n ↦ 1 ↑n) (1 + ↑x) ^ 3 * L (fun n ↦ χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n ↦ (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1

Tactic:
have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y
  have H₀ := summable_neg_log_one_sub_mul_prime_cpow (N := N) 1 h₀
  have H₁ := summable_neg_log_one_sub_mul_prime_cpow χ h₁
  have H₂ := summable_neg_log_one_sub_mul_prime_cpow (χ ^ 2) h₂
  have hsum₀ := (hasSum_re H₀.hasSum).summable.mul_left 3
  have hsum₁ := (hasSum_re H₁.hasSum).summable.mul_left 4
  have hsum₂ := (hasSum_re H₂.hasSum).summable
  rw [← LSeries_eulerProduct_exp_log _ h₀, ← LSeries_eulerProduct_exp_log χ h₁,
    ← LSeries_eulerProduct_exp_log _ h₂]
  simp only [← exp_nat_mul, Nat.cast_ofNat, ← exp_add, norm_exp, add_re, mul_re,
    re_ofNat, im_ofNat, zero_mul, sub_zero, Real.one_le_exp_iff]
  rw [re_tsum H₀, re_tsum H₁, re_tsum H₂, ← tsum_mul_left, ← tsum_mul_left,
    ← hsum₀.tsum_add hsum₁, ← (hsum₀.add hsum₁).tsum_add hsum₂]
  simpa only [neg_add_rev, neg_re, mul_neg, χ.pow_apply' two_ne_zero, ge_iff_le, add_re, one_re,
    ofReal_re, ofReal_add, ofReal_one] using
      tsum_nonneg fun (p : Nat.Primes) ↦ χ.re_log_comb_nonneg p.prop.two_le h₀ y

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

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

Tactic:
have h₁ : (-s - 1).re + r < -1 := by
    rwa [sub_re, one_re, neg_re, neg_sub_left, neg_add_lt_iff_lt_add, add_neg_cancel_comm]

Goal state after:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
h₁ : (-s - 1).re + r < -1
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))
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:
rw [EventuallyEq, eventually_atTop] at h ⊢
  obtain ⟨x₀, hx₀⟩ := h
  obtain ⟨yf, hyf₁, hyf₂⟩ := exists_between hf
  obtain ⟨yg, hyg₁, hyg₂⟩ := exists_between hg
  lift yf to ℝ using ⟨hyf₂.ne, ((OrderBot.bot_le _).trans_lt hyf₁).ne'⟩
  lift yg to ℝ using ⟨hyg₂.ne, ((OrderBot.bot_le _).trans_lt hyg₁).ne'⟩
  refine ⟨max x₀ (max yf yg), fun x hx ↦ ?_⟩
  have Hf : LSeriesSummable f x := by
    refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyf₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)
    exact (le_max_left _ yg).trans <| (le_max_right x₀ _).trans hx
  have Hg : LSeriesSummable g x := by
    refine LSeriesSummable_of_abscissaOfAbsConv_lt_re <|
      (ofReal_re x).symm ▸ hyg₁.trans_le (EReal.coe_le_coe_iff.mpr ?_)
    exact (le_max_right yf _).trans <| (le_max_right x₀ _).trans hx
  rw [LSeries_sub Hf Hg, hx₀ x <| (le_max_left ..).trans hx, sub_self, Pi.zero_apply]

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ -(s + 1).re + r ≤ (-s - 1).re + r

Tactic:
by rw [← neg_re, neg_add']

Goal state after:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : ¬DenselyOrdered (ValueGroupWithZero R)
⊢ IsDiscrete R

Tactic:
· rw [isNontrivial_iff_nontrivial_units] at h
      rw [← LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered] at H
      rw [nonempty_orderIso_withZeroMul_int_iff] at H
      exact H.left

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

Goal state before:
pp: case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h✝ : NeZero b
⊢ J(a | b) ≠ 0

Tactic:
contrapose! h; exact eq_zero_iff_not_coprime.1 h

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

Goal state before:
pp: a : ℤ
l : List ℕ
hl : ∀ n ∈ l, n ≠ 0
⊢ J(a | l.prod) = (List.map (fun n ↦ J(a | n)) l).prod

Tactic:
by
  induction l with
  | nil => simp only [List.prod_nil, one_right, List.map_nil]
  | cons n l' ih =>
    have hn := hl n List.mem_cons_self
    -- `n ≠ 0`
    have hl' := List.prod_ne_zero fun hf => hl 0 (List.mem_cons_of_mem _ hf) rfl
    -- `l'.prod ≠ 0`
    have h := fun m hm => hl m (List.mem_cons_of_mem _ hm)
    -- `∀ (m : ℕ), m ∈ l' → m ≠ 0`
    rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]

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 - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1

Tactic:
integral_Ioi_cpow_of_lt (by rwa [neg_re, neg_lt_neg_iff]) zero_lt_one,

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
⊢ (↑s - 1) * (-↑1 ^ (-↑s + 1) / (-↑s + 1)) = 1
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_2
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)
t : ℝ
ht : t ∈ Set.Ioc 1 T
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ‖S t - l * ↑t‖ * t ^ (-1 - 1)

Tactic:
· gcongr
      exact ht.1.le

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁸ : Ring R✝
inst✝⁷ : ValuativeRel R✝
inst✝⁶ : TopologicalSpace R✝
inst✝⁵ : IsValuativeTopology R✝
R : Type u_2
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
inst✝² : UniformSpace R
inst✝¹ : IsUniformAddGroup R
inst✝ : IsValuativeTopology R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
convert! mem_nhds_zero_iff (R := R)

Goal state after:
R✝ : Type u_1
inst✝⁸ : Ring R✝
inst✝⁷ : ValuativeRel R✝
inst✝⁶ : TopologicalSpace R✝
inst✝⁵ : IsValuativeTopology R✝
R : Type u_2
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
inst✝² : UniformSpace R
inst✝¹ : IsUniformAddGroup R
inst✝ : IsValuativeTopology R
a✝ : Set R
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)