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

Goal state before:
pp: case refine_2
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))
⊢ (fun n ↦ ‖↑↑n ^ (-s)‖ * ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun x ↦ 1

pp: case refine_3
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))
⊢ (fun t ↦ deriv (fun t ↦ ‖↑t ^ (-s)‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖) =O[atTop] fun t ↦ t ^ (-(s.re + 1) + r)

pp: case refine_4
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))
⊢ IntegrableAtFilter (fun t ↦ t ^ (-(s.re + 1) + r)) atTop volume

Tactic:
· refine (IsBigO.mul_atTop_rpow_natCast_of_isBigO_rpow _ _ _ ?_ hO h₂).congr_right (by simp)
    exact (norm_ofReal_cpow_eventually_eq_atTop _).isBigO.natCast_atTop

Goal state after:
case refine_3
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))
⊢ (fun t ↦ deriv (fun t ↦ ‖↑t ^ (-s)‖) t * ∑ k ∈ Icc 1 ⌊t⌋₊, ‖f k‖) =O[atTop] fun t ↦ t ^ (-(s.re + 1) + r)

case refine_4
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))
⊢ IntegrableAtFilter (fun t ↦ t ^ (-(s.re + 1) + r)) atTop volume
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0 ∨ abscissaOfAbsConv f = ⊤

Tactic:
simp only [h, or_false]

Goal state after:
case neg
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0 ↔ f = 0
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
x₀ : ℝ
hx₀ : ∀ (b : ℝ), x₀ ≤ b → LSeries f ↑b = LSeries g ↑b
yf : EReal
hyf₁ : abscissaOfAbsConv f < yf
hyf₂ : yf < ⊤
yg : EReal
hyg₁ : abscissaOfAbsConv g < yg
hyg₂ : yg < ⊤
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → LSeries (f - g) ↑b = 0 b

Tactic:
lift yf to ℝ using ⟨hyf₂.ne, ((OrderBot.bot_le _).trans_lt hyf₁).ne'⟩

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

Goal state before:
pp: ⊢ Set.InjOn LSeries {f | f 0 = 0 ∧ abscissaOfAbsConv f < ⊤}

Tactic:
by
  intro f hf g hg h
  push _ ∈ _ at hf hg
  replace h := (LSeries_eq_iff_of_abscissaOfAbsConv_lt_top hf.2 hg.2).mp h
  ext1 n
  cases n with
  | zero => exact hf.1.trans hg.1.symm
  | succ n => exact h _ n.zero_ne_add_one.symm

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

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

Tactic:
hb,

Goal state after:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
hb : b = 0
⊢ J(a | 0) ≠ 0
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Tactic:
hb,

Goal state after:
case inl
a : ℤ
b : ℕ
h : J(a | 0) = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case succ.inl
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
⊢ J(a | b ^ (e + 1)) = J(a | b) ^ (e + 1)

Tactic:
hb,

Goal state after:
case succ.inl
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
⊢ J(a | 0 ^ (e + 1)) = J(a | 0) ^ (e + 1)
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: 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) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
x : R
hx✝ : x ∈ I ^ n
hx : ϖ ^ n ∣ x
⊢ ∃ a, g a = ⟨x, hx✝⟩

Tactic:
refine hx.imp ?_

Goal state after:
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) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
x : R
hx✝ : x ∈ I ^ n
hx : ϖ ^ n ∣ x
⊢ ∀ (a : R), x = ϖ ^ n * a → g a = ⟨x, hx✝⟩
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
⊢ lucasLehmerResidue p = 0 ↔ sMod p (p - 2) = 0

Tactic:
dsimp [lucasLehmerResidue]

Goal state after:
p : ℕ
w : 1 < p
⊢ sZMod p (p - 2) = 0 ↔ sMod p (p - 2) = 0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A

Tactic:
have HA : (⟨A, hA⟩ : Gamma0 N) ∈ Gamma1' N := by
      simp only [Gamma1_to_Gamma0_mem]
      exact ha

Goal state after:
case mpr
N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
HA : ⟨A, hA⟩ ∈ Gamma1' N
⊢ ∃ x ∈ ⊤, ((Gamma0 N).subtype.comp (Gamma1' N).subtype) x = A
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ
HN : N ≠ 0 ∧ Γ(N) ≤ Γ
⊢ IsCongruenceSubgroup (g • Γ)

Tactic:
refine ⟨N, ?_⟩

Goal state after:
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ
HN : N ≠ 0 ∧ Γ(N) ≤ Γ
⊢ N ≠ 0 ∧ Γ(N) ≤ g • Γ
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' : toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ Subgroup.map (mapGL ℝ) Γ(1)
⊢ (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0

Tactic:
Gamma_one_top,

Goal state after:
g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' : toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ Subgroup.map (mapGL ℝ) ⊤
⊢ (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0
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:
← Quotient.eq_iff_equiv,

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

Goal state before:
pp: case right
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.periods.relIndex 𝒢.strictPeriods ≠ 0

Tactic:
simp [AddSubgroup.relIndex_eq_one.mpr 𝒢.strictPeriods_le_periods]

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
H1 : HasFPowerSeriesOnBall (update (cuspFunction h f) 0 (c 0)) (FormalMultilinearSeries.ofScalars ℂ c) 0 1
L1 : ContinuousAt (update (cuspFunction h f) 0 (c 0)) 0
L2 : ContinuousAt (cuspFunction h f) 0
⊢ update (cuspFunction h f) 0 (c 0) =ᶠ[𝓝[≠] 0] cuspFunction h f

Tactic:
by filter_upwards [self_mem_nhdsWithin] with a ha using update_of_ne ha ..

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
⊢ ∃ C, ∀ (τ : ℍ), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

Tactic:
by
  -- First find an `F` such that `∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t`.
  obtain ⟨F, hF𝒟⟩ : ∃ F, ∀ τ ∈ 𝒟, ‖f τ‖ ≤ F * τ.im ^ t :=
    exists_bound_fundamental_domain_of_isBigO hf_cont hf_infinity
  refine ⟨F, fun τ ↦ ?_⟩
  -- Given `τ`, choose a `g = [a, b; c, d] ∈ SL(2, ℤ)` that translates `τ` into `𝒟`.
  obtain ⟨g, hg⟩ := exists_smul_mem_fd τ
  specialize hF𝒟 (g • τ) hg
  rw [hf_inv g τ] at hF𝒟
  grw [hF𝒟]
  gcongr
  · rw [← div_le_iff₀ (by positivity)] at hF𝒟
    exact le_trans (by positivity) hF𝒟
  -- It remains to show `(g • τ).im ≤ max τ.im (1 / τ.im)`.
  -- We split into two cases depending whether `c = g 1 0` is zero.
  rw [im_smul_eq_div_normSq, denom_apply]
  by_cases hg : g 1 0 = 0
  · -- If `c = 0`, then `(g • τ).im = τ.im / d ^ 2` and `d ^ 2 ≥ 1`.
    -- (In fact `d = ±1`, but we do not need this stronger statement).
    have : g 1 1 ≠ 0 := fun hg' ↦ zero_ne_one <| by
      simpa only [Matrix.det_fin_two, hg, hg', mul_zero, mul_zero, sub_zero] using g.det_coe
    have : (1 : ℝ) ≤ g 1 1 ^ 2 := mod_cast (one_le_sq_iff_one_le_abs _).mpr (Int.one_le_abs this)
    refine le_trans ?_ <| le_max_left _ _
    rw [show Complex.normSq ((g 1 0) * τ + (g 1 1)) = (g 1 1) ^ 2 by simp [hg, sq]]
    simpa [field] using inv_le_one_of_one_le₀ this
  · -- If `c ≠ 0`, then `1 ≤ c ^ 2`, so
    -- `(g • τ).im = τ.im / (c ^ 2 * τ.im ^ 2 +  ...) ≤ 1 / τ.im`.
    refine le_trans ?_ <| le_max_right _ _
    rw [show 1 / τ.im = τ.im / τ.im ^ 2 by field_simp]
    gcongr
    rw [show Complex.normSq ((g 1 0) * τ + (g 1 1)) =
      ((g 1 0) * τ.re + (g 1 1)) ^ 2 + (g 1 0) ^ 2 * τ.im ^ 2 by simp [Complex.normSq_apply]; ring]
    have : (1 : ℝ) ≤ g 1 0 ^ 2 := mod_cast (one_le_sq_iff_one_le_abs _).mpr (Int.one_le_abs hg)
    nlinarith

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : ∀ (g : SL(2, ℤ)), (fun τ ↦ f (g • τ)) =O[atImInfty] fun z ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst✝ : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
τ : ℍ
g h : SL(2, ℤ)
hgh : g ≈ h
⊢ ∃ j ∈ Γ, h = g * j

Tactic:
← Quotient.eq_iff_equiv,

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : ∀ (g : SL(2, ℤ)), (fun τ ↦ f (g • τ)) =O[atImInfty] fun z ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst✝ : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
τ : ℍ
g h : SL(2, ℤ)
hgh : ⟦g⟧ = ⟦h⟧
⊢ ∃ j ∈ Γ, h = g * j
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
⊢ |(g • z).re - 1| < |(g • z).re|

Tactic:
cases abs_cases ((g • z).re - 1)

Goal state after:
case right.right.inl
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
h✝ : |(g • z).re - 1| = (g • z).re - 1 ∧ 0 ≤ (g • z).re - 1
⊢ |(g • z).re - 1| < |(g • z).re|

case right.right.inr
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
h✝ : |(g • z).re - 1| = -((g • z).re - 1) ∧ (g • z).re - 1 < 0
⊢ |(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
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ IsZeroAtImInfty fun τ ↦ ‖petersson k (⇑f) (⇑f') (g • τ)‖

Tactic:
rw [IsZeroAtImInfty, ZeroAtFilter, ← tendsto_zero_iff_norm_tendsto_zero]

Goal state after:
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✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ Tendsto (fun τ ↦ petersson k (⇑f) (⇑f') (g • τ)) atImInfty (𝓝 0)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inl
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:
hb,

Goal state after:
case inr.inl
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
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:
hb,

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
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ 2⁻¹ * (‖2‖ * ‖f x‖) = ‖f x‖

pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ -x ∉ {x}

pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}

Tactic:
Int.norm_eq_abs,

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ 2⁻¹ * (|↑2| * ‖f x‖) = ‖f x‖

F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ -x ∉ {x}

F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

Tactic:
simp [← tsum_symmetricIco_linear_sub_linear_add_one_eq_zero z b]

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
⊢ cexp (log z * 12) = z ^ 12

Tactic:
show (log z * 12) = (12 : ℕ) * log z by ring,

Goal state after:
z : ℂ
hz : z ≠ 0
⊢ cexp (↑12 * log z) = z ^ 12
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
⊢ (↑z).sqrt ≠ 0

Tactic:
by simp [sqrt, ne_zero z]

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

Goal state before:
pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ ∀
    (w :
      ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k),
    ∃ c, c • Submodule.Quotient.mk (E hk) = w

Tactic:
· refine (Submodule.Quotient.forall _).mpr fun f ↦ ⟨(qExpansion 1 f).coeff 0, ?_⟩
    rw [← Submodule.Quotient.mk_smul, Submodule.Quotient.eq, mem_cuspFormSubmodule_iff,
      isCuspForm_iff_coeffZero_eq_zero, FunLike.coe_sub, ModularForm.qExpansion_sub,
      FunLike.coe_smul, ModularForm.qExpansion_smul, map_sub,
      PowerSeries.coeff_smul, E_qExpansion_coeff_zero hk hk2, smul_eq_mul, mul_one, sub_self]
    all_goals simp

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

Goal state before:
pp: case inl
k : ℤ
hk_neg : k < 0
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

pp: case inr
k : ℤ
hk_nonneg : 0 ≤ k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
· rw [levelOne_neg_weight_rank_zero hk_neg]
    exact Cardinal.aleph0_pos

Goal state after:
case inr
k : ℤ
hk_nonneg : 0 ≤ k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
hsucc : k / 12 = (k - 12) / 12 + 1
⊢ ↑((k - 12) / 12) < (qExpansion 1 ⇑(mcast ⋯ (CuspForm.discriminantEquiv (f.toCuspForm h0)) ⋯)).order

Tactic:
rw [qExpansion_eq_qExpansion_discriminant_mul f h0, PowerSeries.order_mul,
      discriminant_qExpansion_order, add_comm, hsucc, Nat.cast_add, Nat.cast_one] at h

Goal state after:
case h.inr
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
h : ↑((k - 12) / 12) + 1 < (qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm h0))).order + 1
hk12 : 12 ≤ k
hsucc : k / 12 = (k - 12) / 12 + 1
⊢ ↑((k - 12) / 12) < (qExpansion 1 ⇑(mcast ⋯ (CuspForm.discriminantEquiv (f.toCuspForm h0)) ⋯)).order
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (b : ℕ) (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑c) z =
    ∑' (b : ℕ) (c : { x // x ∈ gammaSet 1 1 0 }), (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

pp: case h₁
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun z_1 ↦ (↑z_1.1 ^ k)⁻¹ * eisSummand (↑k) (↑z_1.2) z

pp: case h₂
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
b : ℕ
⊢ Summable fun c ↦ (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

Tactic:
case h₁ =>
    exact summable_mul_of_summable_norm (f := fun (n : ℕ) ↦ ((n : ℂ) ^ k)⁻¹)
      (g := fun (v : gammaSet 1 1 0) ↦ eisSummand k v z) (by simp [hk1])
      ((summable_norm_eisSummand hk2 z).subtype _)

Goal state after:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (b : ℕ) (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑c) z =
    ∑' (b : ℕ) (c : { x // x ∈ gammaSet 1 1 0 }), (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

case h₂
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
b : ℕ
⊢ Summable fun c ↦ (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ interior 𝒟 ⊆ 𝒟ᵒ

Tactic:
have ho1 := isOpenMap_re.image_interior_subset 𝒟

Goal state after:
ho1 : UpperHalfPlane.re '' interior 𝒟 ⊆ interior (UpperHalfPlane.re '' 𝒟)
⊢ interior 𝒟 ⊆ 𝒟ᵒ
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h ≈ h'
⊢ ∃ g ∈ 𝒢, ↑h' = ↑h * g

Tactic:
← Quotient.eq_iff_equiv,

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : ⟦h⟧ = ⟦h'⟧
⊢ ∃ g ∈ 𝒢, ↑h' = ↑h * g
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
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsZeroAtImInfty (⇑(ModularForm.trace ℋ f) ∣[k] γ)

Tactic:
ModularForm.coe_trace,

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 ((∑ q, quotientFunc f q) ∣[k] γ)
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
r C : ℝ
hCpos : C > 0
hCO : (fun τ ↦ f τ - valueAtInfty ⇑f) =O[atImInfty] fun τ ↦ rexp (-C * τ.im)
⊢ (fun t ↦ f (↑ofComplex (I * ↑t)) - valueAtInfty ⇑f) =O[atTop] fun t ↦ t ^ r

Tactic:
refine (hCO.comp_tendsto tendsto_ofComplex_I_mul_atTop_atImInfty).trans ?_

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
r C : ℝ
hCpos : C > 0
hCO : (fun τ ↦ f τ - valueAtInfty ⇑f) =O[atImInfty] fun τ ↦ rexp (-C * τ.im)
⊢ ((fun τ ↦ rexp (-C * τ.im)) ∘ fun t ↦ ↑ofComplex (I * ↑t)) =O[atTop] fun t ↦ t ^ r
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
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
x : ℕ
hx : x + 1 ∈ range p
⊢ a ^ (x + 1 - 1 + (p - 1 - (x + 1))) * ↑p * b * ↑(x + 1) = ↑p * b * a ^ (p - 2) * ↑(x + 1)

Tactic:
· 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: