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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : LSeries f = LSeries g
⊢ f = g

Tactic:
replace h := (LSeries_eq_iff_of_abscissaOfAbsConv_lt_top hf.2 hg.2).mp h

Goal state after:
f : ℕ → ℂ
hf : f 0 = 0 ∧ abscissaOfAbsConv f < ⊤
g : ℕ → ℂ
hg : g 0 = 0 ∧ abscissaOfAbsConv g < ⊤
h : ∀ (n : ℕ), n ≠ 0 → f n = g n
⊢ f = g
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
h : Fact (Nat.Prime p)
a : ℤ
ha0 : ↑a ≠ 0
hp : Odd p
⊢ ↑(legendreSym p a) = ↑((-1) ^ #({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val}))

Tactic:
rw [legendreSym.eq_pow, gauss_lemma_aux p ha0]

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

Goal state before:
pp: case zero
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
⊢ Finite (↥𝒪[K] ⧸ 𝓂[K] ^ 0)

Tactic:
simp only [pow_zero, Ideal.one_eq_top]

Goal state after:
case zero
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
h : Finite 𝓀[K]
⊢ Finite (↥𝒪[K] ⧸ ⊤)
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
⊢ Continuous[inst✝¹, _] ⇑v

Tactic:
by
  simp only [continuous_iff_continuousAt, ContinuousAt]
  rintro x
  by_cases hx : v x = 0
  · simpa [hx, ((valuation R).hasBasis_nhds _).tendsto_iff WithZeroTopology.hasBasis_nhds_zero]
      using fun i hi ↦ ⟨(Units.mk0 i hi).mapEquiv (ValueGroupWithZero.orderMonoidIso (valuation R)),
        fun y ↦ by simp [Valuation.map_sub_of_right_eq_zero _ hx]⟩
  · simpa [((valuation R).hasBasis_nhds _).tendsto_iff (hasBasis_nhds_of_ne_zero hx)]
      using ⟨(Units.mk0 (v x) hx).mapEquiv (ValueGroupWithZero.orderMonoidIso (valuation R)),
        fun _ ↦ by simpa [← (valuation R).restrict_def] using Valuation.map_eq_of_sub_lt _⟩

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

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

Tactic:
exact (integrableOn_Ioi_cpow_of_lt
          (by rwa [neg_re, ofReal_re, neg_lt_neg_iff]) zero_lt_one).const_mul _

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 ℂ
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 _ (FaithfulSMul.algebraMap_injective ↥K ℂ),

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
⊢ (algebraMap ↥K ℂ) ((aeval y) p) = 0
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inr.mp
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
⊢ g ^ (-1) < g ^ n → g ^ n < g ^ 1 → ⟨g ^ n, ⋯⟩ = 1

Tactic:
intro hn hn'

Goal state after:
case inr.mp
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
hn : g ^ (-1) < g ^ n
hn' : g ^ n < g ^ 1
⊢ ⟨g ^ n, ⋯⟩ = 1
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ x ∈ conjGL Γ (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↔ x ∈ toConjAct g⁻¹ • Γ

Tactic:
mem_conjGL,

Goal state after:
Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ (∃ y ∈ Γ,
      toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) y) =
        toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g) * toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) x) *
          (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g))⁻¹) ↔
    x ∈ toConjAct g⁻¹ • Γ
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
⊢ ∀ {g : GL n R}, g ∈ 𝒢.adjoinNegOne → GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

Tactic:
rintro g (hg | hg)

Goal state after:
case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
⊢ ∀ {g : GL n R}, g ∈ 𝒢.adjoinNegOne → GeneralLinearGroup.det g = 1

Tactic:
rintro g (hg | hg)

Goal state after:
case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1

case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : OnePoint K
⊢ (fun p ↦ Projectivization.lift (fun u ↦ if ↑u 1 = 0 then ∞ else ↑((↑u 1)⁻¹ * ↑u 0)) ⋯ p)
      ((fun p ↦ p.elim (mk K ![1, 0] ⋯) fun t ↦ mk K ![t, 1] ⋯) p) =
    p

Tactic:
by cases p <;> simp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2

Tactic:
obtain ⟨u, hu_mem, hu_notMem⟩ := (SetLike.lt_iff_le_and_exists.mp h).2

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u : R
hu_mem : u ∈ 𝒢.periods
hu_notMem : u ∉ 𝒢.strictPeriods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
this : upperRightHom 𝒢.widthInfty ∈ 𝒢.adjoinNegOne
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
rcases this with (h | h) <;>
    simpa [-upperRightHom_apply, ← AddChar.map_nsmul_eq_pow] using Subgroup.pow_mem _ h 2

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1»
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) ((fun i ↦ i) ⟨1, ⋯⟩) = c ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
change (z : ℂ).im⁻¹ * ((z : ℂ) * conj (f c)).im = c 1
      rw [f_def, map_add, map_mul, mul_add, mul_left_comm, mul_conj, conj_ofReal,
        conj_ofReal, ← ofReal_mul, add_im, ofReal_im, zero_add, inv_mul_eq_iff_eq_mul₀ hz]
      simp only [ofReal_im, ofReal_re, mul_im, zero_add, mul_zero]

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

Goal state before:
pp: case neg
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : w.im ≤ 0
⊢ (⇑f ∘ ↑ofComplex) (w + ↑h) = (⇑f ∘ ↑ofComplex) w

Tactic:
have : im (w + h) ≤ 0 := by simpa using hw

Goal state after:
case neg
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : SlashInvariantFormClass F Γ k
hΓ : h ∈ Γ.strictPeriods
w : ℂ
hw : w.im ≤ 0
this : (w + ↑h).im ≤ 0
⊢ (⇑f ∘ ↑ofComplex) (w + ↑h) = (⇑f ∘ ↑ofComplex) w
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case «0»
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ ↑r ∣ v ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp [← hv.2, Int.gcd_dvd_left, Int.gcd_dvd_right]

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

Goal state before:
pp: case «1»
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ ↑r ∣ v ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [← hv.2, Int.gcd_dvd_left, Int.gcd_dvd_right]

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
⊢ (2 * ↑π * Complex.I)⁻¹ *
      ∫ (θ : ℝ) in 0..h * (2 * π / h),
        deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1)) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }

Tactic:
conv => enter [1, 2, 2]; rw [show 0 = 0 * (2 * π / h) by simp]

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
⊢ (2 * ↑π * Complex.I)⁻¹ *
      ∫ (θ : ℝ) in 0 * (2 * π / h)..h * (2 * π / h),
        deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1)) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right.right
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
⊢ |((T⁻¹ * g) • z).re| < |(g • z).re|

Tactic:
rw [mul_smul, re_T_inv_smul]

Goal state after:
case right.right
z : ℍ
g₀ : SL(2, ℤ)
hg₀ : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g₀ • z).im
g : SL(2, ℤ)
hg : ↑g 1 = ↑g₀ 1
hg₀' : ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
hg' : 1 / 2 < (g • z).re
⊢ |(g • z).re - 1| < |(g • z).re|
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
⊢ ‖∫ (x : ℝ) in 0..h, 1 / ↑h * (1 / 𝕢 h (↑x + ↑(1 / ↑n) * I) ^ n * f { coe := ↑x + ↑(1 / ↑n) * I, coe_im_pos := ⋯ })‖ ≤
    1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖

Tactic:
simp only [ofReal_div, ofReal_one, ofReal_natCast]

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
⊢ ‖∫ (x : ℝ) in 0..h, 1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖ ≤
    1 / Real.exp (-2 * Real.pi / h) * C * ‖↑n ^ e‖
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : CompleteSpace 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
⊢ Summable fun n ↦ ‖↑n ^ k * r ^ n‖

Tactic:
by simpa using! summable_norm_pow_mul_geometric_of_norm_lt_one k hr

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
⊢ (symmetricIoo G).filter ≤ atTop

Tactic:
by
    rw [symmetricIoo, map_le_iff_le_comap, ← @tendsto_iff_comap]
    exact tendsto_Ioo_neg_atTop_atTop

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

Goal state before:
pp: z : ℍ
⊢ ∑'[symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2 -
      ∑'[symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) =
    ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]

Tactic:
← tsum_eq_of_summable_unconditional (L := symmetricIco ℤ),

Goal state after:
z : ℍ
⊢ ∑'[symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2 -
      ∑'[symmetricIco ℤ] (n : ℤ), ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) =
    ∑'[symmetricIco ℤ] (b : ℤ), ∑' (m : ℤ), G2Term z ![m, b]

z : ℍ
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: q : ℂ
hq : q ∈ Metric.ball 0 1
hq0 : ¬q = 0
⊢ ‖q‖ < 1

Tactic:
simpa [dist_zero_right] using hq

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

Goal state before:
pp: case hf2
k : ℕ
z : ℍ
⊢ ∀ (n k_1 : ℕ) (r : ℂ),
    k_1 ≤ k → r ∈ ℍₒ → DifferentiableAt ℂ (iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) r

Tactic:
· exact fun n l z hl hz ↦ differentiableAt_iteratedDerivWithin_cexp n l
      isOpen_upperHalfPlaneSet hz

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

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

Tactic:
norm_num [E_qExpansion_coeff _ ⟨3, rfl⟩, show bernoulli 6 = 1 / 42 by decide +kernel]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case pos
k : ℕ
hk_even : Even ↑k
h✝ : k ≡ 2 [MOD 12]
⊢ ↑(k / 12) < Cardinal.aleph0

Tactic:
exact_mod_cast Cardinal.natCast_lt_aleph0

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case neg
k : ℕ
hk_even : Even ↑k
h✝ : ¬k ≡ 2 [MOD 12]
⊢ ↑(k / 12 + 1) < Cardinal.aleph0

Tactic:
exact_mod_cast Cardinal.natCast_lt_aleph0

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta τ = 1 + 2 * ∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)

Tactic:
(hasSum_nat_jacobiTheta hτ).tsum_eq,

Goal state after:
τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta τ = 1 + 2 * ((jacobiTheta τ - 1) / 2)
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case refine_2
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
⊢ Summable fun i ↦ ‖(PowerSeries.coeff i) (qExpansion (h Γ) ⇑f)‖ / ↑i ^ s.re / (2 / h Γ) ^ s.re

Tactic:
apply Summable.div_const

Goal state after:
case refine_2
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
⊢ Summable fun i ↦ ‖(PowerSeries.coeff i) (qExpansion (h Γ) ⇑f)‖ / ↑i ^ s.re
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
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1)) =
    (Ideal.Quotient.mk (span {s})) (↑p * b * ∑ x ∈ range p, a ^ (p - 2) * ↑x) +
      (Ideal.Quotient.mk (span {s})) (↑p * a ^ (p - 1))

Tactic:
simp only [Finset.mul_sum, ← mul_assoc, ← pow_add]
      rw [Finset.sum_congr rfl]
      rintro (⟨⟩ | ⟨x⟩) hx
      · rw [Nat.cast_zero, mul_zero, mul_zero]
      · have : x.succ - 1 + (p - 1 - x.succ) = p - 2 := by
          rw [← Nat.add_sub_assoc (Nat.le_sub_one_of_lt (Finset.mem_range.mp hx))]
          exact congr_arg Nat.pred (Nat.add_sub_cancel_left _ _)
        rw [this]
        ring1

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
rcases emultiplicity_eq_coe.mp h.emultiplicity_eq_multiplicity with ⟨⟨k, hk⟩, hpn⟩

Goal state after:
case succ
p : ℕ
hp : Nat.Prime p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
⊢ Differentiable ℂ fun s ↦ Λ hk f s * (2 / s.Gammaℂ)

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
⊢ Differentiable ℂ fun s ↦ Λ hk f s * (2 * s.Gammaℂ⁻¹)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity 2 ↑(n + 1)

Tactic:
rcases emultiplicity_eq_coe.mp h.emultiplicity_eq_multiplicity with ⟨⟨k, hk⟩, hpn⟩

Goal state after:
case succ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
h : FiniteMultiplicity 2 (n + 1)
hpn : ¬2 ^ (multiplicity 2 (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = 2 ^ multiplicity 2 (n + 1) * k
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity 2 ↑(n + 1)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
⊢ Odd y

Tactic:
rw [← even_iff_two_dvd, Int.not_even_iff_odd] at hx

Goal state after:
x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : Odd x
hn : Even n
⊢ Odd y
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ 2 ^ 3 ∣ (x + 1) * (x - 1)

Tactic:
simp [← Nat.pow_two_sub_pow_two x 1]

Goal state after:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ 8 ∣ x ^ 2 - 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
this : mixedEmbedding.norm (c • 1) ≠ 0
⊢ logMap (c • x) = logMap x

Tactic:
← smul_one_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
c : ℝ
hc : c ≠ 0
this : mixedEmbedding.norm (c • 1) ≠ 0
⊢ logMap (c • 1 * x) = logMap x
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
w : InfinitePlace ↥K⁺
x : ↥K⁺
⊢ ((equivInfinitePlace K).symm w) ((algebraMap (↥K⁺) K) x) = w x

Tactic:
← comap_apply,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
w : InfinitePlace ↥K⁺
x : ↥K⁺
⊢ (((equivInfinitePlace K).symm w).comap (algebraMap (↥K⁺) K)) x = w x
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
⊢ Fintype.card (InfinitePlace ↥K⁺) - 1 = Fintype.card (InfinitePlace K) - 1

Tactic:
card_infinitePlace_eq_card_infinitePlace K

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ Fintype.card (InfinitePlace K) - 1 = Fintype.card (InfinitePlace K) - 1