mathlib-initiative/mathlib-tactics huggingface dataset:
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 : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        ↑g 1 0 = 0 →
          0 ≤ ↑g 1 1 → (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
⊢ 0 ≤ ↑(-g) 1 1

Tactic:
simpa using

Goal state after:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        ↑g 1 0 = 0 →
          0 ≤ ↑g 1 1 → (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 1 1 ≤ 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
h1 : HasFPowerSeriesAt (cuspFunction h ⇑f) (FormalMultilinearSeries.ofScalars ℂ c) 0
⊢ HasFPowerSeriesAt (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
h1 : HasFPowerSeriesAt (cuspFunction h ⇑f) (FormalMultilinearSeries.ofScalars ℂ c) 0
⊢ HasFPowerSeriesAt (cuspFunction h ⇑f)
    (FormalMultilinearSeries.ofScalars ℂ fun m ↦ (↑m.factorial)⁻¹ * iteratedDeriv m (cuspFunction h ⇑f) 0) 0
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
h1 : HasFPowerSeriesAt (cuspFunction h ⇑f) (FormalMultilinearSeries.ofScalars ℂ c) 0
h2 : HasFPowerSeriesAt (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0
⊢ HasFPowerSeriesOnBall (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0 1

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
h1 : HasFPowerSeriesAt (cuspFunction h ⇑f) (FormalMultilinearSeries.ofScalars ℂ c) 0
h2 : HasFPowerSeriesAt (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0
⊢ HasFPowerSeriesOnBall (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0 1
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
m : ℕ
h1 : HasFPowerSeriesAt (cuspFunction h ⇑f) (FormalMultilinearSeries.ofScalars ℂ c) 0
h2 : HasFPowerSeriesAt (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0
⊢ c m = (PowerSeries.coeff m) (qExpansion h ⇑f)

Tactic:
simpa using

Goal state after:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h ⇑f) 0
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
m : ℕ
h1 : HasFPowerSeriesAt (cuspFunction h ⇑f) (FormalMultilinearSeries.ofScalars ℂ c) 0
h2 : HasFPowerSeriesAt (cuspFunction h ⇑f) (qExpansionFormalMultilinearSeries h f) 0
⊢ c m = (PowerSeries.coeff m) (qExpansion h ⇑f)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd : 0 ≤ ↑g 1 1
⊢ ↑g 1 1 = 1 ∨ ↑g 1 1 = -1

Tactic:
simpa using

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd : 0 ≤ ↑g 1 1
⊢ ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
⊢ ‖↑z + ↑(↑g 1 1)‖ ≤ 1

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
⊢ ‖↑z + ↑(↑g 1 1)‖ ≤ 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
⊢ ↑g 0 1 = -1

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
⊢ ↑g 0 1 = -1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
⊢ ‖↑z‖ ≤ 1

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
⊢ ‖↑z‖ ≤ 1
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
n : ℕ+
⊢ ∑' (c : ↥(↑n).divisorsAntidiagonal), ↑(↑c).2 ^ k * r ^ ((↑c).1 * (↑c).2) =
    (∑ x ∈ (↑n).divisors, ↑(↑n / x) ^ k) * r ^ ↑n

Tactic:
simpa using

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
inst✝¹ : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k m : ℕ
inst✝ : NeZero m
⊢ ‖r ^ m‖ < 1

Tactic:
simpa using

Goal state after:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace 𝕜
inst✝¹ : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k m : ℕ
inst✝ : NeZero m
⊢ ‖r‖ ^ m < 1
Module: Mathlib.Order.Filter.AtTopBot.Interval

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Tendsto (fun p ↦ Icc p.1 p.2) (atBot ×ˢ atTop) atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ ∀ (b : Finset α), ∀ i ∈ b, ∀ᶠ (x : α × α) in atBot ×ˢ atTop, x.1 ≤ i ∧ i ≤ x.2
Module: Mathlib.Order.Filter.AtTopBot.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NoBotOrder α
⊢ Tendsto (fun p ↦ Ioc p.1 p.2) (atBot ×ˢ atTop) atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NoBotOrder α
⊢ ∀ (b : Finset α), ∀ i ∈ b, ∀ᶠ (x : α × α) in atBot ×ˢ atTop, x.1 < i ∧ i ≤ x.2
Module: Mathlib.Order.Filter.AtTopBot.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NoTopOrder α
⊢ Tendsto (fun p ↦ Ico p.1 p.2) (atBot ×ˢ atTop) atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NoTopOrder α
⊢ ∀ (b : Finset α), ∀ i ∈ b, ∀ᶠ (x : α × α) in atBot ×ˢ atTop, x.1 ≤ i ∧ i < x.2
Module: Mathlib.Order.Filter.AtTopBot.Interval

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoBotOrder α
inst✝ : NoTopOrder α
⊢ Tendsto (fun p ↦ Ioo p.1 p.2) (atBot ×ˢ atTop) atTop

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : NoBotOrder α
inst✝ : NoTopOrder α
⊢ ∀ (b : Finset α), ∀ i ∈ b, ∀ᶠ (x : α × α) in atBot ×ˢ atTop, x.1 < i ∧ i < x.2
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: α : Type u_1
f : ℤ → α
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousMul α
a : α
hf2 : Tendsto (fun N ↦ (f ↑N)⁻¹) atTop (𝓝 1)
hf : Tendsto ((fun s ↦ ∏ b ∈ s, f b) ∘ fun N ↦ Icc (-↑N) ↑N) atTop (𝓝 a)
⊢ Tendsto (((fun s ↦ ∏ b ∈ s, f b) ∘ fun N ↦ Ico (-N) N) ∘ Nat.cast / (fun s ↦ ∏ b ∈ s, f b) ∘ fun N ↦ Icc (-↑N) ↑N)
    atTop (𝓝 1)

Tactic:
simpa using

Goal state after:
α : Type u_1
f : ℤ → α
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousMul α
a : α
hf2 : Tendsto (fun N ↦ (f ↑N)⁻¹) atTop (𝓝 1)
hf : Tendsto ((fun s ↦ ∏ b ∈ s, f b) ∘ fun N ↦ Icc (-↑N) ↑N) atTop (𝓝 a)
⊢ Tendsto (fun i ↦ (f ↑i)⁻¹) atTop (𝓝 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A B : SL(2, ℤ)
z : ℍ
⊢ ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)

Tactic:
simpa using

Goal state after:
A B : SL(2, ℤ)
z : ℍ
⊢ ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z = ↑(↑A 1 0) + ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A : SL(2, ℤ)
⊢ D2 A ∣[2] A⁻¹ = -D2 A⁻¹

Tactic:
simpa using

Goal state after:
A : SL(2, ℤ)
⊢ D2 A ∣[2] A⁻¹ + D2 A⁻¹ = 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
⊢ normSq (↑z + 1) ≤ 1

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
⊢ normSq (↑z + 1) ≤ 1
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: n : ℕ
z : ℂ
hz : z ∈ ℍₒ
h : 1 = cexp (2 * ↑π * I * (↑n + 1) * z)
⊢ False

Tactic:
simpa using

Goal state after:
n : ℕ
z : ℂ
hz : z ∈ ℍₒ
h : 1 = cexp (2 * ↑π * I * (↑n + 1) * z)
⊢ False
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: n : ℕ
z : ℂ
hz : z ∈ ℍₒ
h : 1 = cexp (2 * ↑π * I * (↑n + 1) * z)
⊢ 0 < ((n + 1) • z).im

Tactic:
simpa using

Goal state after:
n : ℕ
z : ℂ
hz : z ∈ ℍₒ
h : 1 = cexp (2 * ↑π * I * (↑n + 1) * z)
⊢ 0 < z.im
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: q : ℂ
hq : ‖q‖ < 1
⊢ Summable fun i ↦ ‖-q ^ (i + 1)‖

Tactic:
simpa using

Goal state after:
q : ℂ
hq : ‖q‖ < 1
⊢ Summable fun i ↦ ‖q‖ ^ (i + 1)
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: case h.inl
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K = ∅
⊢ HasProdUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K

Tactic:
simpa using

Goal state after:
case h.inl
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K = ∅
⊢ TendstoUniformlyOn (fun x1 x2 ↦ ∏ i ∈ x1, (1 + -x2 ^ (i + 1))) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) Filter.atTop ∅
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left✝ : sSup ((fun q ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
⊢ ‖?m.238‖ < 1

Tactic:
simpa using

Goal state after:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left✝ : sSup ((fun q ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
⊢ ‖?m.238‖ < 1
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: case h.inr
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left✝ : sSup ((fun q ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
n : ℕ
x : ℂ
hx : x ∈ K
⊢ ‖-x ^ (n + 1)‖ ≤ ‖q₀‖ ^ (n + 1)

Tactic:
simpa using

Goal state after:
case h.inr
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left✝ : sSup ((fun q ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
n : ℕ
x : ℂ
hx : x ∈ K
⊢ ‖x‖ ^ (n + 1) ≤ ‖q₀‖ ^ (n + 1)
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: x✝ : Finset ℕ
⊢ DifferentiableOn ℂ (fun x2 ↦ ∏ i ∈ x✝, (fun n q ↦ 1 - q ^ (n + 1)) i x2) (Metric.ball 0 1)

Tactic:
simpa using

Goal state after:
x✝ : Finset ℕ
⊢ DifferentiableOn ℂ (fun x2 ↦ ∏ x ∈ x✝, (1 - x2 ^ (x + 1))) (Metric.ball 0 1)
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: k : ℕ
x✝ : ℂ
hq : x✝ ∈ Metric.ball 0 1
⊢ ‖x✝‖ < 1

Tactic:
simpa using

Goal state after:
k : ℕ
x✝ : ℂ
hq : x✝ ∈ Metric.ball 0 1
⊢ ‖x✝‖ < 1
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: z : ℍ
⊢ Summable fun n ↦ ‖-eta_q n ↑z‖

Tactic:
simpa using

Goal state after:
z : ℍ
⊢ ‖𝕢 1 ↑z‖ < 1
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: z : ℂ
hz : z ∈ ℍₒ
⊢ 𝕢 1 z ∈ Metric.ball 0 1

Tactic:
simpa using

Goal state after:
z : ℂ
hz : z ∈ ℍₒ
⊢ ‖𝕢 1 z‖ < 1
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: h : ℝ
z : ℂ
⊢ logDeriv (𝕢 h) z = 2 * ↑π * I / ↑h

Tactic:
by
  have : 𝕢 h = cexp ∘ ((2 * π * I / h) * ·) := by
    ext
    grind [Periodic.qParam]
  rw [this, logDeriv_comp (by fun_prop) (by fun_prop), deriv_const_mul_id]
  simp [logDeriv_exp]

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

Goal state before:
pp: z : ℍ
⊢ (fun m ↦ ((↑(m 0) * ↑z + ↑(m 1)) ^ 2 * (↑(m 0) * ↑z + ↑(m 1) + 1))⁻¹) =O[cofinite] fun n ↦ (‖n‖ ^ 3)⁻¹

Tactic:
simpa using

Goal state after:
z : ℍ
⊢ (fun m ↦ (↑(m 0) * ↑z + ↑(m 1) + 1)⁻¹ * (↑(m 0) * ↑z + ↑(m 1))⁻¹ * (↑(m 0) * ↑z + ↑(m 1))⁻¹) =O[cofinite] fun n ↦
    ‖n‖⁻¹ * ‖n‖⁻¹ * ‖n‖⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
⊢ ↑b * ↑z + ↑n + 1 ≠ 0

Tactic:
simpa using

Goal state after:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : ¬b = 0
⊢ ¬↑b * ↑z + (↑n + 1) = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

Tactic:
simpa using

Goal state after:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun b ↦ ∑' (n : ℤ), G2Term z ![b, n]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mem.inr
γ g : SL(2, ℤ)
h2 : g = T
⊢ G2 ∣[2] g = G2 - D2 g

Tactic:
simpa using

Goal state after:
case mem.inr
γ g : SL(2, ℤ)
h2 : g = T
⊢ G2 ∣[2] T = G2
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ ↑ofComplex) {z | 0 < z.im}
c : ℂ := (2 * ↑π * I)⁻¹
⊢ DifferentiableOn ℂ (fun z ↦ c * deriv (F ∘ ↑ofComplex) z) upperHalfPlaneSet

Tactic:
simpa using

Goal state after:
F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ ↑ofComplex) {z | 0 < z.im}
c : ℂ := (2 * ↑π * I)⁻¹
⊢ DifferentiableOn ℂ (fun y ↦ I * ((↑π)⁻¹ * 2⁻¹) * deriv (F ∘ ↑ofComplex) y) upperHalfPlaneSet
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 +ᵥ ρ
⊢ -1 ≤ ↑(↑g 0 0) ∧ ↑g 0 0 ≤ 0

Tactic:
simpa using

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 +ᵥ ρ
⊢ -1 ≤ ↑(↑g 0 0) ∧ ↑g 0 0 ≤ 0
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
⊢ HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z

Tactic:
simpa using

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
⊢ HasDerivAt (fun w ↦ (denom g w ^ k)⁻¹) (-(↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1))) ↑z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ}, z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ g⁻¹ • g • z ∈ 𝒟

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ}, z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ z ∈ 𝒟
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ}, z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ (g • z).im ≤ (g⁻¹ • g • z).im

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ}, z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g) • z).im ≤ z.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ (g • z).im = z.im

Tactic:
simpa using

Goal state after:
case inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g) • z).im = z.im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ -g • z ∈ 𝒟

Tactic:
simpa using

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g) • z ∈ 𝒟
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ z.im ≤ (-g • z).im

Tactic:
simpa using

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ z.im ≤ (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g) • z).im
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ 0 ≤ ↑(-g) 1 0

Tactic:
simpa using

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ ↑g 1 0 ≤ 0
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
hdet : (↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))).det = 1
z : ℍ
this :
  D (F ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z =
    (↑1)⁻¹ * (D F ∣[k + 2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z -
      ↑k * (2 * ↑π * I)⁻¹ *
          (↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) 1 0) /
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
        (F ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z
⊢ D (F ∣[k] γ) z =
    (D F ∣[k + 2] γ - fun z ↦
        ↑k * (2 * ↑π * I)⁻¹ *
            (↑(↑γ 1 0) /
              denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
          (F ∣[k] γ) z)
      z

Tactic:
simpa using

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
hdet : (↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))).det = 1
z : ℍ
this :
  D (F ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z =
    (↑1)⁻¹ * (D F ∣[k + 2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z -
      ↑k * (2 * ↑π * I)⁻¹ *
          (↑(↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) 1 0) /
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
        (F ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z
⊢ D (F ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z =
    (D F ∣[k + 2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z +
      ↑k * (I * ((↑π)⁻¹ * 2⁻¹)) *
          (↑(↑γ 1 0) /
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
        (F ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
⊢ Δ z ≠ 0

Tactic:
simpa using

Goal state after:
z : ℍ
⊢ ¬η ↑z = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

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

Tactic:
simpa using

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
h : Set.EqOn (η ∘ fun z ↦ -1 / z) (z • (sqrt * η)) upperHalfPlaneSet
⊢ η I = z * I.sqrt * η I

Tactic:
simpa using

Goal state after:
z : ℂ
hz : z ≠ 0
h : Set.EqOn (η ∘ fun z ↦ -1 / z) (z • (sqrt * η)) upperHalfPlaneSet
⊢ η I = z * I.sqrt * η I
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ Set.EqOn (η ∘ fun x ↦ -1 / x) (I.sqrt⁻¹ • (sqrt * η)) upperHalfPlaneSet

Tactic:
by
  obtain ⟨z, hz, h⟩ := eta_comp_eqOn_const_mul_csqrt_eta
  have h3 : η I = z * sqrt I * η I := by simpa [← mul_assoc] using h (show I ∈ _ by simp)
  grind [sqrt, eta_ne_zero (show 0 < I.im by simp)]

Goal state after: