mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : y < 1
⊢ y ≤ x

Tactic:
rcases eq_or_ne y 0 with rfl | hy0

Goal state after:
case mp.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
hy : 0 < 1
⊢ 0 ≤ x

case mp.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
e : ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ)
x : ValueGroupWithZero R := e.symm (exp (-1))
hx0 : x ≠ 0
hx1 : x < 1
y : ValueGroupWithZero R
hy : y < 1
hy0 : y ≠ 0
⊢ y ≤ x
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: 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)
⊢ 0 ≤ C

Tactic:
refine setIntegral_nonneg_ae measurableSet_Ioc (univ_mem' fun t ht ↦ ?_)

Goal state after:
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)
t : ℝ
ht : t ∈ Set.Ioc 1 T
⊢ 0 ≤ ‖S t - l * ↑t‖ * t ^ (-1 - 1)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: m n : ℕ
hm : Odd m
hn : Odd n
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)

Tactic:
rcases odd_mod_four_iff.mp (odd_iff.mp hm) with h | h

Goal state after:
case inl
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 1
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)

case inr
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 3
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
⊢ qrSign m n * x = y ↔ x = qrSign m n * y

Tactic:
refine
      ⟨fun h' =>
        let h := h'.symm
        ?_,
        fun h => ?_⟩

Goal state after:
case refine_1
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := Eq.symm h'
⊢ x = qrSign m n * y

case refine_2
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
⊢ qrSign m n * x = y
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ legendreSym (mersenne p) 3 = -1

Tactic:
by
  rw [(by rfl : (3 : ℤ) = (3 : ℕ)), legendreSym.quadratic_reciprocity_three_mod_four (by norm_num)
    (mersenne_mod_four (by lia)),
    legendreSym.mod]
  rw_mod_cast [mersenne_mod_three odd hp]
  simp

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

Goal state before:
pp: γ : SL(2, ℤ)
⊢ γ ∈ Γ(1)

Tactic:
by
  simp only [Gamma_one_top, Subgroup.mem_top]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
⊢ g • ∞ = ∞ ↔ ↑g 1 0 = 0

Tactic:
simp [smul_infty_eq_ite]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst✝ : NeZero 2
c : OnePoint K
⊢ g • c = c ↔ c = g.parabolicFixedPoint

Tactic:
rcases hg with ⟨hg, hdisc⟩

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
c : OnePoint K
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g).discr = 0
⊢ g • c = c ↔ c = g.parabolicFixedPoint
Module: Mathlib.NumberTheory.ModularForms.SlashActions

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

Tactic:
by
  have : k * (#s) = ∑ i ∈ s, k := by
    rw [Finset.sum_const, nsmul_eq_mul']
  rw [this]
  exact prod_slash_sum_weights

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj : j ∈ toConjAct g⁻¹ • Γ
⊢ (⇑f ∣[k] g) ∣[k] j = ⇑f ∣[k] g

Tactic:
rw [map_inv, Γ.mem_inv_pointwise_smul_iff, toConjAct_smul] at hj
    simpa [← SlashAction.slash_mul] using congr_arg (· ∣[k] g) (slash_action_eqn f _ hj)

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

Goal state before:
pp: N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ f (↑N * ↑n +ᵥ z) = f z

Tactic:
apply vAdd_apply_of_mem_strictPeriods
  simp [strictPeriods_Gamma, AddSubgroup.mem_zmultiples_iff, mul_comm]

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

Goal state before:
pp: N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ f (ModularGroup.T ^ (↑N * n) • z) = f z

Tactic:
rw [modular_T_zpow_smul z (N * n)]
  simpa only [Int.cast_mul, Int.cast_natCast] using vAdd_width_periodic N k n f z

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

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
| ‖↑1 ^ (k - 2) * (σ g) (petersson k (⇑f) (⇑f') (g • τ))‖

Tactic:
Complex.ofReal_one,

Goal state after:
F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
| ‖1 ^ (k - 2) * (σ g) (petersson k (⇑f) (⇑f') (g • τ))‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case ha
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < z.im

pp: case hb
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g')) ↑z)

pp: case hc
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)

Tactic:
· exact z.im_pos

Goal state after:
case hb
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g')) ↑z)

case hc
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: v : Fin 2 → ℤ
⊢ v ∈ gammaSet 1 1 0 ↔ IsCoprime (v 0) (v 1)

Tactic:
gammaSet_one_mem_iff,

Goal state after:
v : Fin 2 → ℤ
⊢ (v 0).gcd (v 1) = 1 ↔ IsCoprime (v 0) (v 1)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
⊢ (g • z).im = (g₀ • z).im

Tactic:
rw [ModularGroup.im_smul_eq_div_normSq, ModularGroup.im_smul_eq_div_normSq,
        denom_apply, denom_apply, hg]

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

Goal state before:
pp: h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (Periodic.cuspFunction h f) 0
hgcts : ContinuousAt (Periodic.cuspFunction h g) 0
⊢ Periodic.cuspFunction h (f * g) 0 = Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0

Tactic:
rw [Periodic.cuspFunction, update_self]

Goal state after:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (Periodic.cuspFunction h f) 0
hgcts : ContinuousAt (Periodic.cuspFunction h g) 0
⊢ (𝓝[≠] 0).limUnder ((f * g) ∘ Periodic.invQParam h) = Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this : (-g = T ∨ -g = -T) ∧ z.re = -1 / 2 ∨ (-g = T⁻¹ ∨ -g = -T⁻¹) ∧ z.re = 1 / 2 ∨ -g = 1 ∨ -g = -1
hd : ¬0 ≤ ↑g 1 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
convert! this using 2 <;> simp [neg_eq_iff_eq_neg, or_comm]

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
n : ℕ+
i : ℕ
hi : i ∈ (↑n).divisors
⊢ ↑(↑n / i) ^ k * r ^ (i * (↑n / i)) = ↑(↑n / i) ^ k * r ^ ↑n

Tactic:
Nat.mul_div_cancel' (dvd_of_mem_divisors hi)

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
n : ℕ+
i : ℕ
hi : i ∈ (↑n).divisors
⊢ ↑(↑n / i) ^ k * r ^ ↑n = ↑(↑n / i) ^ k * r ^ ↑n
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
r : 𝕜
hr : ‖r‖ < 1
h1 : ∀ (m : ℕ+), ‖r ^ ↑m‖ < 1
m : ℕ+
this : (r ^ ↑m) ^ 0 + ∑' (n : ℕ+), (r ^ ↑m) ^ ↑n = (1 - r ^ ↑m)⁻¹
⊢ ∑' (n : ℕ+), r ^ (↑n * ↑m) = (1 - r ^ ↑m)⁻¹ - 1

Tactic:
simp_rw [← this, pow_zero, add_sub_cancel_left, mul_comm, pow_mul]

Goal state after:
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 : HasSum f L (symmetricIcc ℤ)
⊢ Tendsto (fun x ↦ ‖f x‖) atTop (𝓝 0)

Tactic:
HasSum,

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun s ↦ ∑ b ∈ s, f b) (symmetricIcc ℤ).filter (𝓝 L)
⊢ Tendsto (fun x ↦ ‖f x‖) atTop (𝓝 0)
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)
⊢ Tendsto (fun x ↦ ‖f x‖) atTop (𝓝 0)

Tactic:
refine (mul_zero (_ : ℝ) ▸ this.const_mul 2⁻¹).congr' ?_

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)
⊢ (fun x ↦ 2⁻¹ * ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) =ᶠ[atTop] fun x ↦ ‖f x‖
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: r : ℂ
g : ℂ → ℂ
hg : Differentiable ℂ g
⊢ logDeriv ((fun z ↦ 1 - r * cexp z) ∘ g) = fun z ↦ -r * deriv g z * cexp (g z) / (1 - r * cexp (g z))

Tactic:
ext y
  rw [logDeriv_comp (by fun_prop) (hg y), logDeriv_one_sub_cexp]
  ring

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

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

Tactic:
H1

Goal state after:
case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 :
  G2 =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) +
      -D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)
⊢ G2 ∣[2] g⁻¹ =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) +
        -D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) -
      D2 g⁻¹
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝³ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝² : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
this✝¹ : S • ρ = T • ρ
this✝ : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
this : -1 ≤ ↑(↑g 0 0) ∧ ↑g 0 0 ≤ 0
⊢ ↑g 0 0 = 0 ∨ ↑g 0 0 = -1

Tactic:
rw [← Int.cast_one, ← Int.cast_neg, Int.cast_le] at this

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝³ : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝² : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
this✝¹ : S • ρ = T • ρ
this✝ : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
this : -1 ≤ ↑g 0 0 ∧ ↑g 0 0 ≤ 0
⊢ ↑g 0 0 = 0 ∨ ↑g 0 0 = -1
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case hg
z : ℍ
⊢ DifferentiableAt ℂ (fun x ↦ -x⁻¹) ↑z

Tactic:
· fun_prop (disch := exact z.ne_zero)

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

Goal state before:
pp: ⊢ Δ ∣[12] ModularGroup.T = Δ

Tactic:
by
  ext z
  rw [SL_slash_apply, denom, modular_T_smul, ModularGroup.T]
  simp [discriminant_eq_q_prod, eta_q, Periodic.qParam, ← exp_periodic (2 * π * I * z)]
  ring_nf

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
have : iteratedDerivWithin k (fun z ↦ ((π * I) -
    (2 * π * I) * ∑' n : ℕ, cexp (2 * π * I * z) ^ n)) ℍₒ z =
    -(2 * π * I) * ∑' n : ℕ, iteratedDerivWithin k (fun s : ℂ ↦ cexp (2 * π * I * s) ^ n) ℍₒ z := by
    rw [iteratedDerivWithin_const_sub hk, iteratedDerivWithin_fun_neg,
      iteratedDerivWithin_const_mul (by simpa using z.2) (isOpen_upperHalfPlaneSet.uniqueDiffOn)]
    · simp only [iteratedDerivWithin_tsum_cexp_eq, neg_mul]
    · exact (contDiffOn_tsum_cexp k).contDiffWithinAt (by simpa using z.2)
  have h : -(2 * π * I * (2 * π * I) ^ k) * ∑' (n : ℕ), n ^ k * cexp (2 * π * I * z) ^ n =
        -(2 * π * I) * ∑' n : ℕ, (2 * π * I * n) ^ k * cexp (2 * π * I * z) ^ n := by
    simp_rw [← tsum_mul_left]
    congr
    ext y
    ring
  simp only [this, neg_mul, pow_succ', h, neg_inj, mul_eq_mul_left_iff, mul_eq_zero,
    OfNat.ofNat_ne_zero, ofReal_eq_zero, Real.pi_ne_zero, or_self, I_ne_zero, or_false]
  congr
  ext n
  have := exp_nsmul' (p := 1) (a := 2 * π * I) (n := n)
  simp_rw [div_one] at this
  simpa [this, UpperHalfPlane.coe] using
    iteratedDerivWithin_cexp_aux k n 1 isOpen_upperHalfPlaneSet z.2

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

Goal state before:
pp: case h.inl.«0»
k : ℕ
ihn :
  ∀ m < 0,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even 0
hk : 0 < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑0) =
    ↑(if 0 ≡ 2 [MOD 12] then 0 / 12 else 0 / 12 + 1)

Tactic:
simpa using! levelOne_weight_zero_rank_one

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
⊢ T • z ≠ z

Tactic:
apply_fun UpperHalfPlane.re

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzI : z ≠ I
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
⊢ (T • z).re ≠ z.re
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e_a
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
⊢ ∑' (c : ℤ), eisSummand ↑k ![(0, c).1, (0, c).2] z = 2 * riemannZeta ↑k

pp: case e_a.e_a
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
⊢ ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
· simp [eisSummand, two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even (by grind) hk2]

Goal state after:
case e_a.e_a
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
⊢ ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n
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
this :
  ∑' (m : ℕ+) (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑m * ↑z)) ^ ↑n =
    ∑' (m : ℕ+) (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * ↑z) ^ (↑m * ↑n)
⊢ ∑' (n : ℕ+) (c : ℤ), eisSummand ↑k ![(↑↑n, c).1, (↑↑n, c).2] z =
    (-2 * ↑π * I) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
simp [eisSummand, H, tsum_mul_left,
        ← tsum_prod_pow_eq_tsum_sigma (k - 1) (norm_exp_two_pi_I_lt_one z), this]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mpr
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y

Tactic:
have hz' : 0 < z.im := by
      apply hz.lt_of_ne
      contrapose! h3
      simpa [← sq_lt_one_iff₀ (norm_nonneg _), ← Complex.normSq_eq_norm_sq, Complex.normSq,
        ← h3, ← sq] using h2.trans_lt (by norm_num)

Goal state after:
case mpr
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
hz' : 0 < z.im
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
⊢ (PowerSeries.coeff m) (qExpansion 1 ⇑(E hk)) = if m = 0 then 1 else -(2 * ↑k / ↑(bernoulli k)) * ↑((σ (k - 1)) m)

Tactic:
by
  set β : ℂ := -(2 * k / bernoulli k : ℂ)
  set c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑(σ (k - 1) m)
  suffices ∀ τ : ℍ, HasSum (fun m ↦ c m • 𝕢 (1 : ℝ) τ ^ m) (E hk τ) from
    (ModularFormClass.qExpansion_coeff_unique one_pos one_mem_strictPeriods_SL this m).symm
  intro τ
  have hS : Summable fun n : ℕ ↦ (σ (k - 1) (n + 1) : ℂ) * cexp (2 * π * I * τ) ^ (n + 1) :=
    (summable_nat_add_iff 1).mpr (summable_sigma_mul_cexp_pow (by omega) τ)
  rw [← hasSum_nat_add_iff' 1]
  simp only [Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte, smul_eq_mul, Finset.range_one,
    ite_mul, one_mul, Finset.sum_singleton, pow_zero, c]
  have hval : E hk τ - 1 = β * ∑' n : ℕ, (σ (k - 1) (n + 1)) * cexp (2 * π * I * τ) ^ (n + 1) := by
    have := q_expansion_bernoulli hk hk2 τ
    simp_rw [zpow_natCast] at this
    rw [this, ← tsum_pnat_eq_tsum_succ (f := fun n ↦ (σ (k - 1) n : ℂ) * cexp (2 * π * I * τ) ^ n)]
    ring
  rw [hval]
  convert! (hS.mul_left β).hasSum using 1
  · grind [Periodic.qParam, ofReal_one, div_one]
  · rw [tsum_mul_left]

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

Goal state before:
pp: ⊢ id =ᶠ[atTop] UpperHalfPlane.im ∘ fun t ↦ ↑ofComplex (I * ↑t)

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Goal state after:
t : ℝ
ht : 0 < t
⊢ id t = (UpperHalfPlane.im ∘ fun t ↦ ↑ofComplex (I * ↑t)) t
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 τ ↦ rexp (-C * τ.im)) ∘ fun t ↦ ↑ofComplex (I * ↑t)) =ᶠ[atTop] fun x ↦ rexp (-C * x)

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

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)
t : ℝ
ht : 0 < t
⊢ ((fun τ ↦ rexp (-C * τ.im)) ∘ fun t ↦ ↑ofComplex (I * ↑t)) t = rexp (-C * t)
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: case refine_1
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hn : ModularForm.norm ℋ f = 0
⊢ ⇑f = 0

Tactic:
contrapose! hn

Goal state after:
case refine_1
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hn : ⇑f ≠ 0
⊢ ModularForm.norm ℋ f ≠ 0
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ p ^ 2 ∣ (x + p) ^ n - x ^ (n - 1) * p * ↑n - x ^ n

Tactic:
rcases n with - | n
  · simp only [pow_zero, Nat.cast_zero, sub_zero, sub_self, dvd_zero, mul_zero]
  · simp only [add_pow, sum_range_succ, add_tsub_cancel_left, pow_one, Nat.choose_succ_self_right,
      Nat.cast_succ, tsub_self, pow_zero, mul_one, Nat.choose_self, Nat.cast_zero, zero_add,
      Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
    suffices p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i) by
      convert! this; abel
    apply Finset.dvd_sum
    intro y hy
    calc
      p ^ 2 ∣ p ^ (n + 1 - y) :=
        pow_dvd_pow p (le_tsub_of_add_le_left (by linarith [Finset.mem_range.mp hy]))
      _ ∣ x ^ y * p ^ (n + 1 - y) * ↑((n + 1).choose y) :=
        dvd_mul_of_dvd_left (dvd_mul_left _ _) _

Goal state after: