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

Goal state before:
pp: case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (n : ℕ), term (fun n ↦ ↑(residueClass a n)) (↑x) n =
    ↑(∑' (a_1 : ℕ), (term (fun n ↦ ↑(residueClass a n)) (↑x) a_1).re)

Tactic:
push_cast

Goal state after:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (n : ℕ), term (fun n ↦ ↑(residueClass a n)) (↑x) n =
    ∑' (a_1 : ℕ), ↑(term (fun n ↦ ↑(residueClass a n)) (↑x) a_1).re
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∃ a, ∀ (b : ℝ), a ≤ b → LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → LSeries (f - g) ↑b = 0 b

Tactic:
obtain ⟨x₀, hx₀⟩ := h

Goal state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ (b : ℝ), x₀ ≤ b → LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → LSeries (f - g) ↑b = 0 b
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a ↑q
this✝ : NeZero q
this : IsUnit ↑a
p : ℕ
hpn : p > n
hpp : Prime p
heq : ↑p = ↑a
⊢ ∃ p > n, Prime p ∧ ↑p ≡ a [ZMOD ↑q]

Tactic:
refine ⟨p, hpn, hpp, ?_⟩

Goal state after:
n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a ↑q
this✝ : NeZero q
this : IsUnit ↑a
p : ℕ
hpn : p > n
hpp : Prime p
heq : ↑p = ↑a
⊢ ↑p ≡ a [ZMOD ↑q]
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:
by
  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]
  have h₂ : s ≠ 0 := ne_zero_of_re_pos (hr.trans_lt hs)
  have h₃ (t : ℝ) (ht : t ∈ Set.Ici 1) : DifferentiableAt ℝ (fun x : ℝ ↦ (x : ℂ) ^ (-s)) t :=
    differentiableAt_id.ofReal_cpow_const (zero_lt_one.trans_le ht).ne' (neg_ne_zero.mpr h₂)
  have h₄ : ∀ n, ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k := fun n ↦ by
    rw [← insert_Icc_add_one_left_eq_Icc n.zero_le, sum_insert (by aesop), hf, zero_add, zero_add]
  simp_rw [← h₄] at hO
  rw [← integral_const_mul]
  refine tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).mpr hS.hasSum.tendsto_sum_nat) ?_
  simp_rw [Nat.range_succ_eq_Icc_zero, LSeries.term_def₀ hf, mul_comm (f _)]
  convert!
    tendsto_sum_mul_atTop_nhds_one_sub_integral₀ (f := fun x ↦ (x : ℂ) ^ (-s)) (l := 0) ?_ hf h₃ ?_
      ?_ ?_ (integrableAtFilter_rpow_atTop_iff.mpr h₁)
  · rw [zero_sub, ← integral_neg]
    refine setIntegral_congr_fun measurableSet_Ioi fun t ht ↦ ?_
    rw [deriv_ofReal_cpow_const (zero_lt_one.trans ht).ne', h₄]
    · ring_nf
    · exact neg_ne_zero.mpr <| ne_zero_of_re_pos (hr.trans_lt hs)
  · refine (Iff.mpr integrableOn_Ici_iff_integrableOn_Ioi <|
      integrableOn_Ioi_deriv_ofReal_cpow zero_lt_one
        (by simpa using! hr.trans_lt hs)).locallyIntegrableOn
  · have hlim : Tendsto (fun n : ℕ ↦ (n : ℝ) ^ (-(s.re - r))) atTop (𝓝 0) :=
      (tendsto_rpow_neg_atTop (by rwa [sub_pos])).comp tendsto_natCast_atTop_atTop
    refine (IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow (-s.re) _ _ ?_ hO ?_).trans_tendsto hlim
    · exact isBigO_norm_left.mp <| (norm_ofReal_cpow_eventually_eq_atTop _).isBigO.natCast_atTop
    · linarith
  · refine .mul_atTop_rpow_of_isBigO_rpow (-(s + 1).re) r _ ?_ ?_ (by rw [← neg_re, neg_add'])
    · simpa [-neg_add_rev, neg_add'] using! isBigO_deriv_ofReal_cpow_const_atTop _
    · exact (hO.comp_tendsto tendsto_nat_floor_atTop).trans <|
        isEquivalent_nat_floor.isBigO.rpow hr (eventually_ge_atTop 0)

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

Goal state before:
pp: a : ℤ
b : ℕ
h : a.gcd ↑b = 1
⊢ J(a ^ 2 | b) = 1

Tactic:
rw [pow_left, sq_one h]

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
hx : x * ϖ ^ n ∈ I * I ^ n
⊢ x ∈ I

Tactic:
rw [← pow_succ', hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx
      obtain ⟨y, hy⟩ := hx
      rw [mul_comm, pow_succ, mul_assoc, mul_right_inj' (pow_ne_zero _ _)] at hy
      · rw [hI, Ideal.mem_span_singleton]
        exact ⟨y, hy⟩
      · contrapose h'
        rw [hI, h', Ideal.span_singleton_eq_bot]

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

Goal state before:
pp: a : ℤ
n : ℕ
h : J(a | n) = -1
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
a : ℤ
h : J(a | 0) = -1
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
ha2 : a % 2 = 0
hb2 : b % 2 = 1
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a / 2 | b) else J(a / 2 | b)) = J(a | b)

Tactic:
obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha2

Goal state after:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(2 * a / 2 | b) else J(2 * a / 2 | b)) = J(2 * a | b)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

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

Tactic:
induction n with
  | zero =>
    simp only [pow_zero, Ideal.one_eq_top]
    exact Finite.of_fintype (↥𝒪[K] ⧸ ⊤)
  | succ n ih =>
    have : 𝓂[K] ^ (n + 1) ≤ 𝓂[K] ^ n := Ideal.pow_le_pow_right (by simp)
    replace ih := Finite.of_equiv _ (DoubleQuot.quotQuotEquivQuotOfLE this).symm.toEquiv
    suffices Finite (Ideal.map (Ideal.Quotient.mk (𝓂[K] ^ (n + 1))) (𝓂[K] ^ n)) from
      .of_ideal_quotient (.map (Ideal.Quotient.mk _) (𝓂[K] ^ n))
    exact @Finite.of_equiv _ _ h
      ((Ideal.quotEquivPowQuotPowSuccEquiv (IsPrincipalIdealRing.principal 𝓂[K])
        (IsDiscreteValuationRing.not_a_field _) n).trans
        (Ideal.powQuotPowSuccEquivMapMkPowSuccPow _ n))

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
h : Prime (mersenne p)
⊢ p ≠ 1

Tactic:
rintro rfl

Goal state after:
h : Prime (mersenne 1)
⊢ False
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i ^ 2 - 2) = ↑(s i) ^ 2 - 2

Tactic:
push_cast

Goal state after:
q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1)) = ↑1

Tactic:
push_cast

Goal state after:
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ↑(ωUnit (p' + 2)) ^ 2 ^ (p' + 1 + 1) = 1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
⊢ t ≠ 0

Tactic:
rintro rfl

Goal state after:
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
hv : 0 • ↑⟨w, hw⟩ ≠ 0
⊢ False
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case infty
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : ↑g 1 0 = 0
⊢ 0 ≤ (↑g).discr

Tactic:
have : g.val.discr = (g 0 0 - g 1 1) ^ 2 := by
      simp only [discr_fin_two, trace_fin_two, det_fin_two]
      grind

Goal state after:
case infty
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : ↑g 1 0 = 0
this : (↑g).discr = (↑g 0 0 - ↑g 1 1) ^ 2
⊢ 0 ≤ (↑g).discr
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
⊢ (∏ i, f i) ∣[k * ↑(Fintype.card ι)] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (Fintype.card ι - 1) • ∏ i, f i ∣[k] g

Tactic:
by
  have : 0 < Fintype.card ι := Fintype.card_pos
  simpa [← zpow_natCast, this] using ModularForm.prod_slash (s := (.univ : Finset ι))

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : a ≈ b
⊢ ⟦⟨(mapGL ℝ) a⁻¹ • ∞, ⋯⟩⟧ = ⟦⟨(mapGL ℝ) b⁻¹ • ∞, ⋯⟩⟧

Tactic:
rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hab

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : a⁻¹ * b ∈ Subgroup.comap (mapGL ℝ) 𝒢
⊢ ⟦⟨(mapGL ℝ) a⁻¹ • ∞, ⋯⟩⟧ = ⟦⟨(mapGL ℝ) b⁻¹ • ∞, ⋯⟩⟧
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h𝒢 : -1 ∈ 𝒢
⊢ 𝒢.strictPeriods = 𝒢.periods

Tactic:
simp [Subgroup.periods, adjoinNegOne_eq_self_iff.mpr h𝒢]

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

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
hf : Continuous f
hf' : Continuous f'
⊢ Continuous (petersson k f f')

Tactic:
by
  unfold petersson
  fun_prop (disch := simp [im_ne_zero _])

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

Goal state before:
pp: case inr
E✝ : Type u_1
inst✝ : SeminormedAddCommGroup E✝
f : ℍ → E✝
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
D : ℝ
hD : D > 0
y : ℝ
hy : ∀ (b : ℝ), y ≤ b → ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ D * a.im ^ t
hfm : ContinuousOn (fun τ ↦ ‖f τ‖ / τ.im ^ t) (truncatedFundamentalDomain y)
E : ℝ
hE : ∀ τ ∈ truncatedFundamentalDomain y, ‖f τ‖ / τ.im ^ t ≤ E
τ : ℍ
hτ : τ ∈ 𝒟
hτ' : τ.im ≤ y
⊢ ‖f τ‖ / τ.im ^ t ≤ max D E

Tactic:
exact (hE τ ⟨hτ, hτ'⟩).trans (le_max_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
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
⊢ ↑(-2 * π * t / h) + ↑(u * (2 * π / h)) * Complex.I = 2 * ↑π * Complex.I * (↑u + ↑t * ↑I) / ↑h

Tactic:
push_cast

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
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
⊢ -2 * ↑π * ↑t / ↑h + ↑u * (2 * ↑π / ↑h) * Complex.I = 2 * ↑π * Complex.I * (↑u + ↑t * Complex.I) / ↑h
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case e_f
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
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h ↑τ
⊢ ↑(2 * π / h) * f τ = 2 * ↑π * f τ / ↑h

Tactic:
push_cast

Goal state after:
case e_f
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
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h ↑τ
⊢ 2 * ↑π / ↑h * f τ = 2 * ↑π * f τ / ↑h
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : ModularFormClass F Γ k
inst✝ : CuspFormClass F' Γ k
⊢ ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C

Tactic:
simpa [petersson_norm_symm] using petersson_bounded_left k Γ f' f

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
a : ℂ
⊢ qExpansion h (a • f) = a • qExpansion h f

Tactic:
ext m

Goal state after:
h : ℝ
f : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
a : ℂ
m : ℕ
⊢ (PowerSeries.coeff m) (qExpansion h (a • f)) = (PowerSeries.coeff m) (a • qExpansion h f)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
⊢ qExpansion h (f + g) = qExpansion h f + qExpansion h g

Tactic:
ext m

Goal state after:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
m : ℕ
⊢ (PowerSeries.coeff m) (qExpansion h (f + g)) = (PowerSeries.coeff m) (qExpansion h f + qExpansion h g)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
⊢ qExpansion h 1 = 1

Tactic:
ext m

Goal state after:
h : ℝ
m : ℕ
⊢ (PowerSeries.coeff m) (qExpansion h 1) = (PowerSeries.coeff m) 1
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
m : ℕ
⊢ (PowerSeries.coeff m) (qExpansion h 1) = (PowerSeries.coeff m) 1

Tactic:
have h1 : cuspFunction h 1 = 1 := by
    ext q
    rcases eq_or_ne q 0 with rfl | hq
    · simpa [cuspFunction, Periodic.cuspFunction] using! tendsto_const_nhds.limUnder_eq
    · simp [cuspFunction, Periodic.cuspFunction_eq_of_nonzero h _ hq]

Goal state after:
h : ℝ
m : ℕ
h1 : cuspFunction h 1 = 1
⊢ (PowerSeries.coeff m) (qExpansion h 1) = (PowerSeries.coeff m) 1
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
a✝ : (Matrix.SpecialLinearGroup.mapGL ℝ) γ • ∞ = c
⊢ valueAtInfty ⇑f = 0

Tactic:
← qExpansion_coeff_zero one_pos
      (ModularFormClass.analyticAt_cuspFunction_zero f one_pos one_mem_strictPeriods_SL)
      (periodic_comp_ofComplex f one_mem_strictPeriods_SL)

Goal state after:
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
γ : SL(2, ℤ)
a✝ : (Matrix.SpecialLinearGroup.mapGL ℝ) γ • ∞ = c
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ ∑' (m : Fin 2 → ℤ), G2Term z m = ∑' (b : ℤ) (c : ℤ), G2Term z ![b, c]

pp: case h
z : ℍ
⊢ Summable (Function.uncurry fun m n ↦ G2Term z ![m, n])

pp: case h₁
z : ℍ
⊢ ∀ (b : ℤ), Summable fun n ↦ G2Term z ![b, n]

pp: case h₂
z : ℍ
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]

Tactic:
tsum_G2Term_eq_tsum

Goal state after:
z : ℍ
⊢ ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n] = ∑' (b : ℤ) (c : ℤ), G2Term z ![b, c]

case h
z : ℍ
⊢ Summable (Function.uncurry fun m n ↦ G2Term z ![m, n])

case h₁
z : ℍ
⊢ ∀ (b : ℤ), Summable fun n ↦ G2Term z ![b, n]

case h₂
z : ℍ
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n] = ∑' (m : Fin 2 → ℤ), G2Term z m

Tactic:
tsum_G2Term_eq_tsum

Goal state after:
z : ℍ
⊢ ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n] = ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
⊢ -(↑z)⁻¹ ∈ upperHalfPlaneSet

Tactic:
by grind [im_pnat_div_pos 1 z]

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

Goal state before:
pp: k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : f =O[atTop] fun n ↦ ↑n ^ l
h0 : (fun n ↦ (2 * ↑π * I * ↑n / ↑p) ^ k) =O[atTop] fun n ↦ ↑n ^ k
⊢ (fun n ↦ f n * (2 * ↑π * I * ↑n / ↑p) ^ k) =O[atTop] fun n ↦ ↑(n ^ (l + k))

Tactic:
push_cast

Goal state after:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : f =O[atTop] fun n ↦ ↑n ^ l
h0 : (fun n ↦ (2 * ↑π * I * ↑n / ↑p) ^ k) =O[atTop] fun n ↦ ↑n ^ k
⊢ (fun n ↦ f n * (2 * ↑π * I * ↑n / ↑p) ^ k) =O[atTop] fun n ↦ ↑n ^ (l + k)
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    rw [UpperHalfPlane.mdifferentiable_iff]
    refine .congr (fun z hz ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hz).pow
      24 |>.differentiableWithinAt) fun z hz ↦ ?_
    simp [ModularForm.discriminant, ofComplex_apply_of_im_pos hz]

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

Goal state before:
pp: p p4 p6 : PowerSeries ℂ
c4 c6 : ℂ
hp4_0 : PowerSeries.constantCoeff p4 = 1
hp6_0 : PowerSeries.constantCoeff p6 = 1
hp4_1 : (PowerSeries.coeff 1) p4 = 240
hp6_1 : (PowerSeries.coeff 1) p6 = -504
hqc4 : c4 • p4 = p ^ 2
hqc6 : c6 • p6 = p ^ 3
D : PowerSeries ℂ := (c4 • p4) ^ 3 - (c6 • p6) ^ 2
⊢ (PowerSeries.coeff 0) D = c4 ^ 3 - c6 ^ 2

Tactic:
simp [D, hp4_0, hp6_0]

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
x : ℂ
hx : x ∈ ℍₒ
⊢ ↑π * (↑π * x).cot = ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * x) ^ n

Tactic:
simpa using pi_mul_cot_pi_q_exp ⟨x, hx⟩

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

Goal state before:
pp: case e'_6
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ 1 - 24 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n -
      ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i =
    ∑' (b : ℕ), -24 * (↑((σ 1) (b + 1)) * cexp (2 * ↑π * I * ↑z) ^ (b + 1))

Tactic:
tsum_pnat_eq_tsum_succ (f := fun n ↦ σ 1 n * 𝕢 z ^ n),

Goal state after:
case e'_6
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ 1 - 24 * ∑' (n : ℕ), ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1) -
      ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i =
    ∑' (b : ℕ), -24 * (↑((σ 1) (b + 1)) * cexp (2 * ↑π * I * ↑z) ^ (b + 1))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), ((↑↑b * ↑z + ↑n) ^ k)⁻¹ =
      (-(2 * ↑π * I)) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
m n : ℕ+
⊢ ↑↑n ^ (k - 1) * cexp (↑↑n * (2 * ↑π * I * (↑↑m * ↑z))) = ↑↑n ^ (k - 1) * cexp (↑(↑m * ↑n) * (2 * ↑π * I * ↑z))

Tactic:
push_cast

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), ((↑↑b * ↑z + ↑n) ^ k)⁻¹ =
      (-(2 * ↑π * I)) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
m n : ℕ+
⊢ ↑↑n ^ (k - 1) * cexp (↑↑n * (2 * ↑π * I * (↑↑m * ↑z))) = ↑↑n ^ (k - 1) * cexp (↑↑m * ↑↑n * (2 * ↑π * I * ↑z))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ ↑π * I * ↑n ^ 2 * τ = ↑(π * ↑n ^ 2) * (τ * I)

Tactic:
push_cast

Goal state after:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ ↑π * I * ↑n ^ 2 * τ = ↑π * ↑n ^ 2 * (τ * I)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

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

Tactic:
by
  apply HasSum.tsum_eq
  simpa [HasSum, ← Nat.map_cast_int_atTop, ← PNat.tendsto_comp_val_iff]
    using tendsto_tsum_one_div_linear_sub_succ_eq z

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

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : ModularFormClass F 𝒢 k
c✝ : OnePoint ℝ
h : IsCusp c✝ ℋ
γ : GL (Fin 2) ℝ
⊢ γ • OnePoint.infty = c✝ → IsBoundedAtImInfty ((SlashInvariantForm.trace ℋ f).toFun ∣[k] γ)

Tactic:
rintro rfl

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsBoundedAtImInfty ((SlashInvariantForm.trace ℋ f).toFun ∣[k] γ)
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
c✝ : OnePoint ℝ
h : IsCusp c✝ ℋ
γ : GL (Fin 2) ℝ
⊢ γ • OnePoint.infty = c✝ → IsZeroAtImInfty ((ModularForm.trace ℋ f).toFun ∣[k] γ)

Tactic:
rintro rfl

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsZeroAtImInfty ((ModularForm.trace ℋ f).toFun ∣[k] γ)
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: ⊢ Tendsto (fun t ↦ ↑ofComplex (I * ↑t)) atTop atImInfty

Tactic:
rw [atImInfty, tendsto_comap_iff]

Goal state after:
⊢ Tendsto (UpperHalfPlane.im ∘ fun t ↦ ↑ofComplex (I * ↑t)) atTop atTop
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
c✝ : OnePoint ℝ
h : IsCusp c✝ ℋ
γ : GL (Fin 2) ℝ
⊢ γ • OnePoint.infty = c✝ →
    IsBoundedAtImInfty ((SlashInvariantForm.norm ℋ f).toFun ∣[k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ))] γ)

Tactic:
rintro rfl

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsBoundedAtImInfty ((SlashInvariantForm.norm ℋ f).toFun ∣[k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ))] γ)
Module: Mathlib.Topology.Algebra.RestrictedProduct.Units

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, ↑(B i)]_[𝓕]
hx : ∀ (i : ι), IsUnit (x i)
hxr : ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), IsUnit ⟨x i, h⟩
⊢ ∀ᶠ (i : ι) in 𝓕, ⋯.unit.inv ∈ ↑(B i)

Tactic:
by
    filter_upwards [hxr] with i ⟨h, hu⟩
    have hu : (hx i).unit.1 * hu.unit.inv = 1 := Subtype.val_inj.2 hu.mul_val_inv
    simp [← Units.eq_inv_of_mul_eq_one_left hu]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hn
p : ℕ
hp : 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
⊢ ¬↑p ∣ ↑k

Tactic:
Int.natCast_dvd_natCast

Goal state after:
case succ.hn
p : ℕ
hp : 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
⊢ ¬p ∣ k