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

Goal state before:
pp: case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ -(1 / (2 * ↑π * I * ↑n)) = -1 / (2 * ↑π * I * ↑n)

Tactic:
neg_div

Goal state after:
case inr.refine_1
k : ℕ
hk : k ≠ 0
n : ℤ
hn : n ≠ 0
⊢ -(1 / (2 * ↑π * I * ↑n)) = -(1 / (2 * ↑π * I * ↑n))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * ↑π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    ↑((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!)

Tactic:
· norm_cast

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

Goal state before:
pp: case e'_3
⊢ ↑π ^ 2 / 6 = ↑(π ^ 2 / 6)

Tactic:
· norm_cast

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

Goal state before:
pp: case e'_3
⊢ ↑π ^ 4 / 90 = ↑(π ^ 4 / 90)

Tactic:
· norm_cast

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

Goal state before:
pp: case inl
⊢ riemannZeta 0 = -↑(bernoulli' (0 + 1)) / (0 + 1)

Tactic:
riemannZeta_zero,

Goal state after:
case inl
⊢ -1 / 2 = -↑(bernoulli' (0 + 1)) / (0 + 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

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

Tactic:
neg_div

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

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

Tactic:
sub_eq_add_neg,

Goal state after:
f g : ℕ → ℂ
s : ℂ
⊢ term (f + -g) s = term f s + -term g s
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑↑zeta) s * LSeries (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s

Tactic:
have hs' : s ≠ 1 := fun h ↦ by simp only [h, one_re, lt_self_iff_false] at hs

Goal state after:
N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
hs' : s ≠ 1
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑↑zeta) s * LSeries (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ (2 * ↑π * I) ^ k ≠ 0

Tactic:
rw [Ne, pow_eq_zero_iff', not_and_or]
      exact Or.inl two_pi_I_ne_zero

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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ -(↑q.totient)⁻¹ *
      (deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
        ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s) =
    -(↑q.totient)⁻¹ * ∑ χ, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) - (↑q.totient)⁻¹ * (1 / (s - 1))

Tactic:
sub_eq_add_neg,

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ -(↑q.totient)⁻¹ *
      (deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s +
        ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s) =
    -(↑q.totient)⁻¹ * ∑ χ, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) + -((↑q.totient)⁻¹ * (1 / (s - 1)))
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : χ ^ 2 ≠ 1 ∨ I * ↑s.im ≠ 0
hs' : s = 1 + I * ↑s.im
⊢ LFunction χ s ≠ 0

Tactic:
replace h : χ ^ 2 ≠ 1 ∨ s.im ≠ 0 :=
      h.imp_right (fun H ↦ by exact_mod_cast right_ne_zero_of_mul H)

Goal state after:
case neg
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
hs' : s = 1 + I * ↑s.im
h : χ ^ 2 ≠ 1 ∨ s.im ≠ 0
⊢ LFunction χ s ≠ 0
Module: Mathlib.NumberTheory.LSeries.ZetaZeros

Goal state before:
pp: ⊢ IsDiscrete riemannZetaZeros

Tactic:
by
  simpa using (mem_codiscrete'.mp compl_riemannZetaZeros_mem_codiscrete).2

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
b : ℕ
hb : b ∈ Ico 1 (p / 2).succ
⊢ (↑b / a).valMinAbs.natAbs ≠ 0

Tactic:
simp only [div_eq_mul_inv, hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hb, not_false_iff,
        valMinAbs_eq_zero, inv_eq_zero, Int.natAbs_eq_zero, Ne, _root_.mul_eq_zero, or_self_iff]

Goal state after:
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
t : ℝ
ht : 0 < t
⊢ t ^ (-s) = t * t ^ (-s - 1)

Tactic:
Real.rpow_sub ht,

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
t : ℝ
ht : 0 < t
⊢ t ^ (-s) = t * (t ^ (-s) / t ^ 1)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
⊢ ∀ x ∈ List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯,
    x ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯

Tactic:
by
        intro _ ha'
        rcases List.mem_pmap.mp ha' with ⟨p, hp, rfl⟩
        have : Fact p.Prime := ⟨prime_of_mem_primeFactorsList hp⟩
        exact quadraticChar_isQuadratic (ZMod p) a

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

Goal state before:
pp: case inr
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 3
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)

Tactic:
· rw [χ₄_nat_three_mod_four h, ← χ₄_eq_neg_one_pow (odd_iff.mp hn), jacobiSym.at_neg_one hn]

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

Goal state before:
pp: case hx
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 : ℝ → ℂ := ⋯
C : ℝ := ⋯
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 : ℝ
ht : t ∈ Set.Ioc 1 T
⊢ 1 ≤ t

Tactic:
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
x : R
hx : v x = 0
i : ValueGroupWithZero R
hi : ¬i = 0
y : R
⊢ v.restrict (y - x) < ↑((Units.mapEquiv ↑(ValueGroupWithZero.orderMonoidIso v)) (Units.mk0 i hi)) → v y < i

Tactic:
simp [Valuation.map_sub_of_right_eq_zero _ hx]

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

Goal state before:
pp: case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ (Set.Icc x y).Finite

Tactic:
refine ((this x).union H.inv).subset (le_of_eq ?_)

Goal state after:
case inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
h : x ≤ 1
pf✝² : MonoidHomClass (K →*₀ Γ₀) K Γ₀
pf✝¹ : MonoidWithZeroHomClass (Valuation K Γ₀) K Γ₀
pf✝ : MonoidHomClass (K →*₀ Γ₀) K Γ₀
hy : 1 ≤ y
H : (Set.Icc y⁻¹ 1).Finite
⊢ Set.Icc x y = Set.Icc x 1 ∪ (Set.Icc y⁻¹ 1)⁻¹
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' i : ℕ
⊢ sZMod (p' + 2) i = ↑(s i)

Tactic:
by
  induction i with
  | zero => dsimp [s, sZMod]; simp
  | succ i ih => push_cast [s, sZMod, ih]; rfl

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
⊢ ∃ n, 0 < n ∧ z ^ n = 1

Tactic:
by
/- We want to use `NumberField.Embeddings.pow_eq_one_of_norm_le_one` but it can only be applied to
elements of number fields. We thus first construct the number field `K` obtained by adjoining `z`
to `ℚ`.
-/
  let K := ℚ⟮z⟯
  let : NumberField K := {
    to_charZero := ℚ⟮z⟯.charZero,
    to_finiteDimensional := adjoin.finiteDimensional
      (isIntegral_of_mahlerMeasure_eq_one h hz).tower_top }
-- `y` is `z` as an element of `K`
  let y : K := ⟨z, mem_adjoin_simple_self ℚ z⟩
  suffices ∃ (n : ℕ) (_ : 0 < n), y ^ n = 1 by
    obtain ⟨n, hn₀, hn₁⟩ := this
    exact ⟨n, hn₀, congrArg (algebraMap K ℂ) hn₁⟩
  refine NumberField.Embeddings.pow_eq_one_of_norm_le_one (x := y) K ℂ (Subtype.coe_ne_coe.mp hz₀)
    (coe_isIntegral_iff.mp <| isIntegral_of_mahlerMeasure_eq_one h hz)
    fun φ ↦ norm_root_le_one_of_mahlerMeasure_eq_one h ?_
  rw [mem_aroots] at hz ⊢
  refine ⟨hz.1, ?_⟩
  have H (ψ : K →+* ℂ) : ψ ((aeval y) p) = (aeval (ψ y)) p := by
    conv_rhs => rw [← map_id (p := p)]
    exact p.map_aeval_eq_aeval_map (by ext; simp) y
  rw [← H, map_eq_zero_iff _ φ.injective,
    ← map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective ↥K ℂ), H]
  exact hz.2

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
k : ℤ
w : ω ^ 2 ^ (p' + 1) = ↑k * 0 * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = -1

Tactic:
simpa using w

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

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

Tactic:
by_cases hG : -1 ∈ 𝒢

Goal state after:
case pos
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∈ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

case neg
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∉ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods.Commensurable 𝒢.periods

Tactic:
by
  constructor
  · rcases 𝒢.relIndex_strictPeriods with h | h <;> simp [h]
  · simp [AddSubgroup.relIndex_eq_one.mpr 𝒢.strictPeriods_le_periods]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (((↑z).im⁻¹ • g) ∘ₗ f) c = LinearMap.id c

Tactic:
rw [LinearMap.comp_apply, LinearMap.smul_apply, LinearMap.id_apply]

Goal state after:
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ • g (f c) = c
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst✝ : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
⊢ qExpansion h ⇑(f.pow n) = qExpansion h ⇑f ^ n

Tactic:
induction n with
  | zero => simp only [coe_pow, pow_zero, qExpansion_one]
  | succ n ih =>
    rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Interval

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Tendsto (fun p ↦ Icc p.1 p.2) (atBot ×ˢ atTop) atTop

Tactic:
simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
    using fun b i _ ↦ (eventually_le_atBot i).prod_mk (eventually_ge_atTop i)

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ (symmetricIoc G).filter ≤ atTop

Tactic:
rw [symmetricIoc, map_le_iff_le_comap, ← @tendsto_iff_comap]

Goal state after:
G✝ : Type u_1
inst✝⁹ : Neg G✝
inst✝⁸ : Preorder G✝
inst✝⁷ : LocallyFiniteOrder G✝
inst✝⁶ : atTop.NeBot
G : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : PartialOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : LocallyFiniteOrder G
inst✝¹ : NoTopOrder G
inst✝ : NoBotOrder G
⊢ Tendsto (fun N ↦ Ioc (-N) N) atTop atTop
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: z : ℍ
HG : logDeriv (fun x ↦ ∏' (i : ℕ), (1 - eta_q i x)) ↑z = ∑' (i : ℕ), logDeriv (fun x ↦ 1 - eta_q i x) ↑z
⊢ 2 * ↑π * I / ↑24 + 2 * ↑π * I * ∑' (n : ℕ), (↑n + 1) * -eta_q n ↑z / (1 - eta_q n ↑z) =
    ↑π * I / 12 *
      ((↑π ^ 2 / 6)⁻¹ * 2⁻¹ * (2 * (↑π ^ 2 / 6)) -
        (↑π ^ 2 / 6)⁻¹ * 2⁻¹ *
          (8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n ^ 1 * cexp (2 * ↑π * I * ↑z) ^ ↑n / (1 - cexp (2 * ↑π * I * ↑z) ^ ↑n)))

Tactic:
sub_eq_add_neg,

Goal state after:
z : ℍ
HG : logDeriv (fun x ↦ ∏' (i : ℕ), (1 - eta_q i x)) ↑z = ∑' (i : ℕ), logDeriv (fun x ↦ 1 - eta_q i x) ↑z
⊢ 2 * ↑π * I / ↑24 + 2 * ↑π * I * ∑' (n : ℕ), (↑n + 1) * -eta_q n ↑z / (1 - eta_q n ↑z) =
    ↑π * I / 12 *
      ((↑π ^ 2 / 6)⁻¹ * 2⁻¹ * (2 * (↑π ^ 2 / 6)) +
        -((↑π ^ 2 / 6)⁻¹ * 2⁻¹ *
            (8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n ^ 1 * cexp (2 * ↑π * I * ↑z) ^ ↑n / (1 - cexp (2 * ↑π * I * ↑z) ^ ↑n))))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ Summable (G2Term z)

Tactic:
have H : Summable fun m ↦ G2Term z m - δ m := by
    simp_rw [G2Term, add_sub_cancel_right]
    apply summable_of_isBigO_rpow_norm (a := 3) (by linarith)
    simpa [pow_three, pow_two, ← mul_assoc] using ((isBigO_linear_add_const_vec z 0 1).mul
      (isBigO_linear_add_const_vec z 0 0)).mul (isBigO_linear_add_const_vec z 0 0)
  exact H.congr_cofinite <| δ_eventually_cofinite.mp <| .of_forall <| by simp +contextual

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mul
γ g h : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
hy✝ : h ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
ih : G2 ∣[2] h = G2 - D2 h
⊢ (G2 - D2 g) ∣[2] h = G2 - (D2 g ∣[2] h + D2 h)

Tactic:
sub_eq_add_neg,

Goal state after:
case mul
γ g h : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
hy✝ : h ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
ih : G2 ∣[2] h = G2 - D2 h
⊢ (G2 + -D2 g) ∣[2] h = G2 - (D2 g ∣[2] h + D2 h)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 : G2 ∣[2] (g * g⁻¹) = (G2 - D2 g) ∣[2] g⁻¹
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹

Tactic:
sub_eq_add_neg,

Goal state after:
case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 : G2 ∣[2] (g * g⁻¹) = (G2 + -D2 g) ∣[2] g⁻¹
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ HasSum (fun x ↦ e2Summand x z)
    (2 * riemannZeta 2 - 8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n) (symmetricIco ℤ)

Tactic:
by
  apply (hasSum_e2Summand_symmetricIcc z).hasSum_symmetricIco_of_hasSum_symmetricIcc
  simpa using! (tendsto_e2Summand_atTop_nhds_zero z).neg.comp tendsto_natCast_atTop_atTop

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ ((-1) ^ (m + 1 + 1) * 2 ^ (2 * (m + 1) - 1) * ↑π ^ (2 * (m + 1)) * ↑(bernoulli (2 * (m + 1))) /
            ↑(2 * (m + 1) * (2 * m + 1)!))⁻¹ *
        (-2 * ↑π * I) ^ (2 * (m + 1)) /
      ↑(2 * (m + 1) - 1)! =
    -(2 * (2 * ↑(m + 1)) / ↑(bernoulli (2 * (m + 1))))

Tactic:
show 2 * (m + 1) - 1 = 2 * m + 1 by grind,

Goal state after:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ ((-1) ^ (m + 1 + 1) * 2 ^ (2 * m + 1) * ↑π ^ (2 * (m + 1)) * ↑(bernoulli (2 * (m + 1))) /
            ↑(2 * (m + 1) * (2 * m + 1)!))⁻¹ *
        (-2 * ↑π * I) ^ (2 * (m + 1)) /
      ↑(2 * m + 1)! =
    -(2 * (2 * ↑(m + 1)) / ↑(bernoulli (2 * (m + 1))))
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: ⊢ (PowerSeries.coeff 1) (qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ - qExpansion 1 ⇑E₆ * qExpansion 1 ⇑E₆) =
    1728

Tactic:
norm_num [PowerSeries.coeff_mul, Finset.Nat.antidiagonal_succ, E₄_qExpansion_coeff_one,
    E₆_qExpansion_coeff_one, E_qExpansion_coeff_zero _ ⟨2, rfl⟩,
    E_qExpansion_coeff_zero _ ⟨3, rfl⟩]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ Function.Surjective ⇑(extensionEmbeddingOfIsReal hv)

Tactic:
rw [← RingHom.fieldRange_eq_top_iff, ← Real.subfield_eq_of_closed]

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ IsClosed ↑(extensionEmbeddingOfIsReal hv).fieldRange
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) ↑p ^ 2 * (Ideal.Quotient.mk (span {s})) b *
        (Ideal.Quotient.mk (span {s})) (a ^ (p - 2)) *
      (Ideal.Quotient.mk (span {s})) ↑((p - 1) / 2) =
    0

Tactic:
rw [mul_assoc, mul_assoc]

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) ↑p ^ 2 *
      ((Ideal.Quotient.mk (span {s})) b *
        ((Ideal.Quotient.mk (span {s})) (a ^ (p - 2)) * (Ideal.Quotient.mk (span {s})) ↑((p - 1) / 2))) =
    0
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (∑ i ∈ range p, x ^ i * y ^ (p - 1 - i)) = 1

Tactic:
rw [← Nat.cast_one]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)) = 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - -y
hx : ¬↑p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (↑p) (x ^ n - -y ^ n) = emultiplicity (↑p) (x - -y) + emultiplicity p n

Tactic:
← Odd.neg_pow hn

Goal state after:
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - -y
hx : ¬↑p ∣ x
n : ℕ
hn : Odd n
⊢ emultiplicity (↑p) (x ^ n - (-y) ^ n) = emultiplicity (↑p) (x - -y) + emultiplicity p n
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ ∀ (x y : (𝓞 K)ˣ),
    ⟨x * y * ((unitsComplexConj K) (x * y))⁻¹, ⋯⟩ =
      ⟨x * ((unitsComplexConj K) x)⁻¹, ⋯⟩ * ⟨y * ((unitsComplexConj K) y)⁻¹, ⋯⟩

Tactic:
by
    intro _ _
    rw [MulMemClass.mk_mul_mk, Subtype.mk_eq_mk]
    apply coe_injective
    simp only [map_mul, mul_inv_rev, Units.val_mul, map_units_inv]
    ring

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : ↑↑ζ * ↑(preimageOfMemIntegerSet a) = ↑(preimageOfMemIntegerSet a)
⊢ ↑(preimageOfMemIntegerSet a) ≠ 0

Tactic:
exact nonZeroDivisors.coe_ne_zero _

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ≤ torsion K
⊢ Subgroup.closure (Set.range (realFundSystem K)) ⊔ torsion K =
    Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (Subgroup.closure (Set.range (fundSystem ↥K⁺))) ⊔
      (Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ⊔ torsion K)

Tactic:
RingHom.toMonoidHom_eq_coe,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ≤ torsion K
⊢ Subgroup.closure (Set.range (realFundSystem K)) ⊔ torsion K =
    Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (Subgroup.closure (Set.range (fundSystem ↥K⁺))) ⊔
      (Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ⊔ torsion K)
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsRamified K w
⊢ Module.finrank v.Completion w.Completion = 2

Tactic:
by
  have H := NumberField.InfinitePlace.isRamified_iff.mp h
  rw [NumberField.InfinitePlace.LiesOver.comap_eq w v] at H
  have := LiesOver.extensionEmbedding_liesOver_of_isReal w H.2
  rw [Algebra.finrank_eq_of_equiv_equiv (ringEquivRealOfIsReal H.2)
      (ringEquivComplexOfIsComplex H.1) (by ext; simp),
    Complex.finrank_real_complex]

Goal state after: