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

Goal state before:
pp: b : ℕ
b_ge_two : 2 ≤ b
p : ℕ
p_prime : Prime p
p_gt_two : 2 < p
not_dvd : ¬p ∣ b * (b ^ 2 - 1)
A : ℕ := (b ^ p - 1) / (b - 1)
B : ℕ := (b ^ p + 1) / (b + 1)
hA : p < A
hi_A : 1 < A
hi_B : 1 < B
hi_b : 0 < b
hi_bsquared : 0 < b ^ 2 - 1
hi_bpowtwop : 1 ≤ b ^ (2 * p)
hi_bpowpsubone : 1 ≤ b ^ (p - 1)
p_odd : Odd p
AB_not_prime : ¬Prime (A * B)
AB_id : A * B = (b ^ (2 * p) - 1) / (b ^ 2 - 1)
hd : b ^ 2 - 1 ∣ b ^ (2 * p) - 1
ha₁ : (b ^ 2 - 1) * (A * B - 1) = b * (b ^ (p - 1) - 1) * (b ^ p + b)
ha₂ : 2 ∣ b ^ p + b
ha₃ : p ∣ b ^ (p - 1) - 1
ha₄ : b ^ 2 - 1 ∣ b ^ (p - 1) - 1
⊢ ¬p ∣ b ^ 2 - 1

Tactic:
rw [mul_comm] at not_dvd
        exact mt (fun h : p ∣ b ^ 2 - 1 => dvd_mul_of_dvd_left h _) not_dvd

Goal state after:
Module: Mathlib.NumberTheory.FrobeniusNumber

Goal state before:
pp: 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})

Tactic:
exact Submodule.span_mono (by simp) (hn m le (setGcd_dvd_of_mem hm))

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

Goal state before:
pp: case calc_3
n : ℕ
⊢ ∑ d ∈ Finset.Icc 1 n, (↑d)⁻¹ = ↑(harmonic n)

Tactic:
· simp only [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_natCast]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Three

Goal state before:
pp: K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 = -(↑(η ^ 2 * S.u₁ * S.u₂⁻¹) * (λ ^ (S.multiplicity - 1) * S.X) ^ 3)

Tactic:
eq_neg_iff_add_eq_zero,

Goal state after:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ S.Y ^ 3 + ↑S.u₄ * S.Z ^ 3 + ↑(η ^ 2 * S.u₁ * S.u₂⁻¹) * (λ ^ (S.multiplicity - 1) * S.X) ^ 3 = 0
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
a : ℝ
ha : a = 0
⊢ a ∉ Multiset.map (fun v ↦ max (v x) 1) archAbsVal

Tactic:
rw [ha]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x : K
H : (Multiset.map (fun v ↦ max (v x) 1) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), max (↑v x) 1 ≠ 0
a : ℝ
ha : a = 0
⊢ 0 ∉ Multiset.map (fun v ↦ max (v x) 1) archAbsVal
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: n : ℕ
s : ℝ
⊢ 0 ≤ term n s

Tactic:
rw [term, intervalIntegral.integral_of_le (by simp)]

Goal state after:
n : ℕ
s : ℝ
⊢ 0 ≤ ∫ (x : ℝ) in Ioc (↑n) (↑n + 1), (x - ↑n) / x ^ (s + 1) ∂volume
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: ⊢ Tendsto (fun N ↦ termSum 1 N) atTop (𝓝 (1 - γ))

Tactic:
simp_rw [termSum_one, sub_eq_neg_add]

Goal state after:
⊢ Tendsto (fun N ↦ -↑(harmonic (N + 1)) + log (↑N + 1) + 1) atTop (𝓝 (-γ + 1))
Module: Mathlib.NumberTheory.Height.Basic

Goal state before:
pp: case h₁
R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : CommSemiring S
inst✝² : LinearOrder S
inst✝¹ : IsOrderedRing S
inst✝ : CharZero S
v : AbsoluteValue R S
ι : Type u_3
s : Finset ι
hs : s.Nonempty
x : ι → R
⊢ 1 ≤ ↑(#s)

Tactic:
simp [hs]

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

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ archAbsVal.card = (Multiset.map (fun x ↦ 1) archAbsVal).sum

Tactic:
rw [← Multiset.sum_map_toList, ← Fin.sum_univ_fun_getElem, ← Multiset.length_toList,
      Fin.sum_const, Multiset.length_toList, smul_eq_mul, mul_one]

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

Goal state before:
pp: h₁ :
  HasDerivAt (id * completedRiemannZeta₀ - 1 - id / (1 - id))
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
      (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2)
    0
⊢ HasDerivAt (fun x ↦ (x * completedRiemannZeta₀ x - 1 - x / (1 - x)) / (2 * ↑π ^ (-x / 2) * Gamma (x / 2 + 1)))
    (-log (2 * ↑π) / 2) 0

Tactic:
have h₂ : HasDerivAt ((fun x : ℂ => 2) * fun (x : ℂ) => (π : ℂ) ^ (-x / 2)) _ 0 :=
    .mul (hasDerivAt_const 0 2) <|
    .cpow (hasDerivAt_const 0 _) (.div_const (.neg <| hasDerivAt_id 0) 2) (by simp [Real.pi_pos])

Goal state after:
h₁ :
  HasDerivAt (id * completedRiemannZeta₀ - 1 - id / (1 - id))
    (1 * completedRiemannZeta₀ 0 + id 0 * deriv completedRiemannZeta₀ 0 - 0 -
      (1 * (1 - id) 0 - id 0 * (0 - 1)) / (1 - id) 0 ^ 2)
    0
h₂ :
  HasDerivAt ((fun x ↦ 2) * fun x ↦ ↑π ^ (-x / 2))
    (0 * ↑π ^ (-0 / 2) + 2 * (-0 / 2 * ↑π ^ (-0 / 2 - 1) * 0 + ↑π ^ (-0 / 2) * log ↑π * (-1 / 2))) 0
⊢ HasDerivAt (fun x ↦ (x * completedRiemannZeta₀ x - 1 - x / (1 - x)) / (2 * ↑π ^ (-x / 2) * Gamma (x / 2 + 1)))
    (-log (2 * ↑π) / 2) 0
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ gaussSum χ' ψ.char * gaussSum χ'⁻¹ ψ.char⁻¹ * (gaussSum φ' ψ.char * gaussSum φ'⁻¹ ψ.char⁻¹) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ * ↑(Fintype.card F)

Tactic:
gaussSum_mul_gaussSum_eq_card Hχ ψ.prim,

Goal state after:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ ↑(Fintype.card F) * (gaussSum φ' ψ.char * gaussSum φ'⁻¹ ψ.char⁻¹) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ'⁻¹ * φ'⁻¹) ψ.char⁻¹ * ↑(Fintype.card F)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case neg.refine_1.refine_2
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
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
⊢ ∑ x ∈ univ \ {0, 1}, ⋯.choose ∈ ℤ[μ]

Tactic:
exact Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: case hl
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
a✝ : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
⊢ i ∉ ↑(h.modByMonicHom x).toFinsupp.coeff.support

Tactic:
simp only [Polynomial.toFinsupp_apply, Classical.not_not, Finsupp.mem_support_iff, Ne,
      modByMonicHom, LinearMap.coe_mk, Finset.mem_coe]

Goal state after:
case hl
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
a✝ : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
⊢ ({ toFun := fun x ↦ h.repr x %ₘ f, map_add' := ⋯ } x).coeff i = 0
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
⊢ 0 < f.natDegree

Tactic:
by
  rcases h.basis.index_nonempty with ⟨⟨i, hi⟩⟩
  exact Nat.zero_lt_of_lt hi

Goal state after:
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case e'_3
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
Q : R[X]
⊢ (quotAdjoinEquivQuotMap hx ⋯).symm ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q)) =
    (Ideal.Quotient.mk (Ideal.map (algebraMap R ↥R[x]) I)) ((aeval (adjoin.powerBasis' hx').gen) Q)

Tactic:
apply (quotAdjoinEquivQuotMap hx
    (FaithfulSMul.algebraMap_injective ((adjoin R {x})) S)).injective

Goal state after:
case e'_3
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
Q : R[X]
⊢ (quotAdjoinEquivQuotMap hx ⋯)
      ((quotAdjoinEquivQuotMap hx ⋯).symm ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval x) Q))) =
    (quotAdjoinEquivQuotMap hx ⋯)
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R ↥R[x]) I)) ((aeval (adjoin.powerBasis' hx').gen) Q))
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
T : Type u_1
inst✝² : CommRing T
inst✝¹ : Algebra R T
h' : IsAdjoinRoot T f
U : Type u_2
inst✝ : CommRing U
i : R →+* U
x : U
hx : eval₂ i x f = 0
z : S
⊢ (h'.lift i x hx) ((h.algEquiv h') (h.map (h.repr z))) = (h.lift i x hx) (h.map (h.repr z))

Tactic:
simp [-map_repr]

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

Goal state before:
pp: case e_f
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
⊢ ↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s) = ∑' (m : ℕ), LSeries.term (fun x ↦ Φ ↑x) s (j.val + N * m)

Tactic:
have : (j.val / N : ℝ) ∈ Set.Icc 0 1 := mem_Icc.mpr ⟨by positivity,
    (div_le_one (Nat.cast_pos.mpr <| NeZero.pos _)).mpr <| Nat.cast_le.mpr (val_lt j).le⟩

Goal state after:
case e_f
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
⊢ ↑N ^ (-s) * (Φ j * hurwitzZeta (toAddCircle j) s) = ∑' (m : ℕ), LSeries.term (fun x ↦ Φ ↑x) s (j.val + N * m)
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
⊢ LFunction (𝓕 Φ) s = ∑ j, Φ j * expZeta (toAddCircle (-j)) s

Tactic:
by
  have (j : ZMod N) : Φ j * LFunction (fun k ↦ 𝕖 (-j * k)) s =
      Φ j * expZeta (toAddCircle (-j)) s := by
    by_cases h : -j ≠ 0 ∨ s ≠ 1
    · rw [LFunction_stdAddChar_eq_expZeta _ _ h]
    · simp only [neg_ne_zero, not_or, not_not] at h
      rw [h.1, show Φ 0 = 0 by tauto, zero_mul, zero_mul]
  simp only [LFunction, ← this, mul_sum]
  rw [dft_def, sum_comm]
  simp only [sum_mul, mul_sum, smul_eq_mul, stdAddChar_apply, ← mul_assoc]
  congr 1 with j
  congr 1 with k
  rw [mul_assoc (Φ _), mul_comm (Φ _), neg_mul]

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

Goal state before:
pp: case inl
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n ≠ 0
⊢ hurwitzZeta (↑x) (-↑(2 * n)) =
    -1 / (↑(2 * n) + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1)))

pp: case inr
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n + 1 ≠ 0
⊢ hurwitzZeta (↑x) (-↑(2 * n + 1)) =
    -1 / (↑(2 * n + 1) + 1) *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1 + 1)))

Tactic:
· exact_mod_cast hurwitzZeta_neg_two_mul_nat (by lia : n ≠ 0) hx

Goal state after:
case inr
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n + 1 ≠ 0
⊢ hurwitzZeta (↑x) (-↑(2 * n + 1)) =
    -1 / (↑(2 * n + 1) + 1) *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * n + 1 + 1)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: ⊢ riemannZeta 2 = ↑π ^ 2 / 6

Tactic:
convert! congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_two.tsum_eq

Goal state after:
case e'_2
⊢ riemannZeta 2 = ↑(∑' (b : ℕ), 1 / ↑b ^ 2)

case e'_3
⊢ ↑π ^ 2 / 6 = ↑(π ^ 2 / 6)
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
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
suffices ∑ x, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s by
    simp only [completedLFunction_def_even hΦ, neg_sub, completedHurwitzZetaEven_one_sub, this]

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs : 1 < s.re
hs₀ : s ≠ 0
hs₁ : s ≠ 1
⊢ ∑ x, Φ x * completedCosZeta (toAddCircle x) s = completedLFunction (𝓕 Φ) s
Module: Mathlib.NumberTheory.LSeries.SumCoeff

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

Tactic:
mul_comm (f _)

Goal state after:
f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ‖↑x ^ (-s)‖) t
h₄ : (deriv fun t ↦ ‖↑t ^ (-s)‖) =ᶠ[atTop] fun t ↦ -s.re * t ^ (-(s.re + 1))
⊢ Summable fun x ↦ ↑x ^ (-s) * f x
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2

Tactic:
rw [eq_div_iff (two_ne_zero' ℝ)]

Goal state after:
k : ℕ
hk : k ≠ 0
⊢ 2 ^ (2 * k - 1) * 2 = 2 ^ (2 * k)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case inl
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
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : C + C' ≤ 0
this : 0 < (C + C') * (2 - 1)
⊢ False

Tactic:
rw [show (2 : ℝ) - 1 = 1 by norm_num, mul_one] at this

Goal state after:
case inl
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
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : C + C' ≤ 0
this : 0 < C + C'
⊢ False
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
⊢ Tendsto (fun n ↦ ∑ x ∈ Icc 0 n, f x * ↑x ^ (-s)) atTop
    (𝓝 (∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1)))))

Tactic:
mul_comm (f _)

Goal state after:
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
⊢ Tendsto (fun n ↦ ∑ x ∈ Icc 0 n, ↑x ^ (-s) * f x) atTop
    (𝓝 (∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1)))))
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) / t)

Tactic:
mul_div_cancel₀ _ ht.ne'

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 ^ (-s)
Module: Mathlib.Topology.Algebra.Module.Compact

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
⊢ (Fintype.linearCombination R Subtype.val).range = N

Tactic:
simp [hs]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
u : (↥𝒪[K])ˣ
⊢ ‖↑u‖ = 1

Tactic:
by
  simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : ValueGroupWithZero K
hr✝ : r ≠ 0
hrs : {x | (valuation K) x < r} ⊆ s
r' : K
hr' : ¬r' = 0
hr : (valuation K) r' < 1
hr1 : r < 1
⊢ ∃ r', r' ≠ 0 ∧ (valuation K) r' < 1 ∧ {x | (valuation K) x ≤ (valuation K) r'} ⊆ s

Tactic:
obtain ⟨r, rfl⟩ := ValuativeRel.valuation_surjective r

Goal state after:
case inl
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r' : K
hr' : ¬r' = 0
hr✝ : (valuation K) r' < 1
r : K
hr : (valuation K) r ≠ 0
hrs : {x | (valuation K) x < (valuation K) r} ⊆ s
hr1 : (valuation K) r < 1
⊢ ∃ r', r' ≠ 0 ∧ (valuation K) r' < 1 ∧ {x | (valuation K) x ≤ (valuation K) r'} ⊆ s
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz✝ : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ (aeval z) p = 0
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz✝)) }
y : ↥K := ⟨z, ⋯⟩
φ : ↥K →+* ℂ
H : ∀ (ψ : ↥K →+* ℂ), ψ ((aeval y) p) = (aeval (ψ y)) p
⊢ φ ((aeval y) p) = 0

Tactic:
map_eq_zero_iff _ φ.injective,

Goal state after:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz✝ : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ (aeval z) p = 0
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz✝)) }
y : ↥K := ⟨z, ⋯⟩
φ : ↥K →+* ℂ
H : ∀ (ψ : ↥K →+* ℂ), ψ ((aeval y) p) = (aeval (ψ y)) p
⊢ (aeval y) p = 0
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case refine_2
p' : ℕ
⊢ ¬2 ∣ 2 * 2 ^ (p' + 1) - 1

Tactic:
exact Nat.two_not_dvd_two_mul_sub_one Nat.one_le_two_pow

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

Goal state before:
pp: k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
⊢ f ∣[k] (A * B) = (f ∣[k] A) ∣[k] B

Tactic:
ext1 τ
  calc σ (A * B) (f ((A * B) • τ)) * |(A * B).det.val| ^ (k - 1) * denom (A * B) τ ^ (-k)
  _ = σ B (σ A (f (A • B • τ))) * (|A.det.val| ^ (k - 1) * |B.det.val| ^ (k - 1)) *
      (((σ B) (denom A ↑(B • τ) ^ (-k))) * denom B τ ^ (-k)) := by
    rw [σ_mul_comm, σ_mul, denom_cocycle_σ, mul_zpow, mul_smul, map_mul, Units.val_mul,
      abs_mul, ofReal_mul, mul_zpow, map_zpow₀]
  _ = σ B (σ A (f (A • B • τ)) * |A.det.val| ^ (k - 1) * (denom A ↑(B • τ) ^ (-k)))
        * |B.det.val| ^ (k - 1) * denom B τ ^ (-k) := by
     rw [map_mul, map_zpow₀, map_mul, map_zpow₀, σ_ofReal]
     ring
  _ = ((f ∣[k] A) ∣[k] B) τ := rfl

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

Goal state before:
pp: c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
⊢ IsCusp (g • c) 𝒢

Tactic:
convert! hc.smul g

Goal state after:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
⊢ 𝒢 = ConjAct.toConjAct g • 𝒢
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp
c : OnePoint ℝ
⊢ c ∈ Set.range (OnePoint.map Rat.cast) → ∃ g, c = (mapGL ℝ) g • ∞

Tactic:
rintro ⟨c, rfl⟩
    obtain ⟨g, rfl⟩ := c.exists_mem_SL2 ℤ
    refine ⟨g, ?_⟩
    rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
      ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]

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

Goal state before:
pp: case hasSum
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
y : ℂ
hy : y ∈ ball 0 ↑1
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ y) (update (cuspFunction h f) 0 (c 0) (0 + y))

Tactic:
NNReal.coe_one,

Goal state after:
case hasSum
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
y : ℂ
hy : y ∈ ball 0 1
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ y) (update (cuspFunction h f) 0 (c 0) (0 + y))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
⊢ ↑(T ^ n • z) = ↑z + ↑n

Tactic:
by
  rw [UpperHalfPlane.coe_specialLinearGroup_apply]
  simp [coe_T_zpow, -map_zpow]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
⊢ (T ^ n • z).re = z.re + ↑n

Tactic:
by
  rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, coe_re]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
h : normSq ↑z < 1
⊢ z.im < (S • z).im

Tactic:
rw [ModularGroup.im_smul_eq_div_normSq]

Goal state after:
z : ℍ
h : normSq ↑z < 1
⊢ z.im < z.im / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) S)) ↑z)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ (-1)
hre : (g • z).re = ↑b + z.re
hb : b = -1
⊢ z.re = 1 / 2

Tactic:
rw [hb, Int.cast_neg, Int.cast_one] at hre

Goal state after:
case inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ (-1)
hre : (g • z).re = -1 + z.re
hb : b = -1
⊢ z.re = 1 / 2