mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : ModularForm Γ k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
bdd_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ } = g

Tactic:
;

Goal state after:
case mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : ModularForm Γ k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
bdd_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ } = g
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
bdd_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
bdd_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_cusps' := bdd_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ }
⊢ { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_cusps' := bdd_at_cusps'✝¹ } =
    { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ }

Tactic:
;

Goal state after:
case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
bdd_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
bdd_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_cusps' := bdd_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ }
⊢ { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_cusps' := bdd_at_cusps'✝¹ } =
    { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ }
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
bdd_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
bdd_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_cusps' := bdd_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ }
⊢ toSlashInvariantForm✝¹ = toSlashInvariantForm✝

Tactic:
;

Goal state after:
case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
bdd_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
bdd_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_cusps' := bdd_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ }
⊢ toSlashInvariantForm✝¹ = toSlashInvariantForm✝
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : CuspForm Γ k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
zero_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ } = g

Tactic:
;

Goal state after:
case mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : CuspForm Γ k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
zero_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ } = g
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
zero_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
zero_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_cusps' := zero_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ }
⊢ { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_cusps' := zero_at_cusps'✝¹ } =
    { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ }

Tactic:
;

Goal state after:
case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
zero_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
zero_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_cusps' := zero_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ }
⊢ { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_cusps' := zero_at_cusps'✝¹ } =
    { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ }
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
zero_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
zero_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_cusps' := zero_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ }
⊢ toSlashInvariantForm✝¹ = toSlashInvariantForm✝

Tactic:
;

Goal state after:
case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
zero_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
zero_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_cusps' := zero_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ }
⊢ toSlashInvariantForm✝¹ = toSlashInvariantForm✝
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
i : ι
hi : i ∈ s
⊢ MDiff ⇑(F i).toSlashInvariantForm

Tactic:
;

Goal state after:
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
i : ι
hi : i ∈ s
⊢ MDiff ⇑(F i).toSlashInvariantForm
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ ((g * γ) • ∞).IsZeroAt (⇑f) k

Tactic:
apply CuspFormClass.zero_at_cusps f

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ IsCusp ((g * γ) • ∞) Γ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
h : Int.cast ∘ p = 0
i : Fin 2
⊢ p i = 0 i

Tactic:
;

Goal state after:
g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
h : Int.cast ∘ p = 0
i : Fin 2
⊢ p i = 0 i
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hp : IsCoprime (↑g 1 0) (↑g 1 1)
nonZ1 : ↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2 ≠ 0
this : Int.cast ∘ ↑g 1 ≠ 0
nonZ2 : ↑(↑g 1 0) * ↑z + ↑(↑g 1 1) ≠ 0
⊢ ↑z * ↑(↑g 1 0) + ↑(↑g 1 1) = ↑(↑g 1 0) * ↑z + ↑(↑g 1 1)

Tactic:
;

Goal state after:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime (↑g 1 0) (↑g 1 1)
nonZ1 : ↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2 ≠ 0
this : Int.cast ∘ ↑g 1 ≠ 0
nonZ2 : ↑(↑g 1 0) * ↑z + ↑(↑g 1 1) ≠ 0
⊢ ↑z * ↑(↑g 1 0) + ↑(↑g 1 1) = ↑(↑g 1 0) * ↑z + ↑(↑g 1 1)
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
τ : ℍ
| Real.exp (-a * τ.im)

Tactic:
;

Goal state after:
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
τ : ℍ
| Real.exp (-a * τ.im)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 0 = 1
⊢ ↑g 0 0 * ↑g 1 1 = 1

Tactic:
;

Goal state after:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 0 = 1
⊢ ↑g 0 0 * ↑g 1 1 = 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
this : g = T ^ ↑g 0 1
z : ℍ
⊢ g • z = T ^ ↑g 0 1 • z

Tactic:
;

Goal state after:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
this : g = T ^ ↑g 0 1
z : ℍ
⊢ g • z = T ^ ↑g 0 1 • z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
i j : Fin 2
⊢ ↑g i j = ↑(T ^ ↑g 0 1) i j

Tactic:
;

Goal state after:
case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
i j : Fin 2
⊢ ↑g i j = ↑(T ^ ↑g 0 1) i j
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
z : ℍ
⊢ g • z = T ^ (-↑g 0 1) • z

Tactic:
;

Goal state after:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
z : ℍ
⊢ g • z = T ^ (-↑g 0 1) • z
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
| 0

Tactic:
;

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
| 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
i j : Fin 2
⊢ ↑g i j = ↑(-T ^ (-↑g 0 1)) i j

Tactic:
;

Goal state after:
case h
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
i j : Fin 2
⊢ ↑g i j = ↑(-T ^ (-↑g 0 1)) i j
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 τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ¬↑g 1 0 = 0
⊢ (↑(↑g 1 0) * τ.re + ↑(↑g 1 1)) * (↑(↑g 1 0) * τ.re + ↑(↑g 1 1)) + ↑(↑g 1 0) * τ.im * (↑(↑g 1 0) * τ.im) =
    (↑(↑g 1 0) * τ.re + ↑(↑g 1 1)) ^ 2 + ↑(↑g 1 0) ^ 2 * τ.im ^ 2

Tactic:
;

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 : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ¬↑g 1 0 = 0
⊢ (↑(↑g 1 0) * τ.re + ↑(↑g 1 1)) * (↑(↑g 1 0) * τ.re + ↑(↑g 1 1)) + ↑(↑g 1 0) * τ.im * (↑(↑g 1 0) * τ.im) =
    (↑(↑g 1 0) * τ.re + ↑(↑g 1 1)) ^ 2 + ↑(↑g 1 0) ^ 2 * τ.im ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : 1 = ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 1
⊢ ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1

Tactic:
;

Goal state after:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : 1 = ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 1
⊢ ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : c * ↑z + d ≠ 0
⊢ ↑z * c + d = c * ↑z + d

Tactic:
;

Goal state after:
k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
a b c d u v : ℂ
hc : c * ↑z + d ≠ 0
⊢ ↑z * c + d = c * ↑z + d
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ 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✝ : ModularFormClass F' Γ k
C : ℝ
τ : ℍ
| ‖petersson k (⇑f) (⇑f') τ‖

Tactic:
;

Goal state after:
k : ℤ
hk : 0 ≤ 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✝ : ModularFormClass F' Γ k
C : ℝ
τ : ℍ
| ‖petersson k (⇑f) (⇑f') τ‖
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
C : ℝ
τ : ℍ
| ‖petersson k (⇑f) (⇑f') τ‖

Tactic:
;

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
C : ℝ
τ : ℍ
| ‖petersson k (⇑f) (⇑f') τ‖
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
this : cuspFunction h 0 = 0
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) (qExpansion h 0) = (PowerSeries.coeff n✝) 0

Tactic:
;

Goal state after:
h : ℝ
this : cuspFunction h 0 = 0
n✝ : ℕ
⊢ (PowerSeries.coeff n✝) (qExpansion h 0) = (PowerSeries.coeff n✝) 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 ≤ 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 ≤ 1
⊢ (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 * 16 ≤ 16

Tactic:
;

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 ≤ 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 ≤ 1
⊢ (c * z.im) ^ 4 / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ^ 2 * 16 ≤ 16
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

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

Tactic:
simp only [div_eq_mul_one_div (_ * _ ^ _)]
  apply Summable.mul_tendsto_const (c := 1 / (1 - 0))
    (by simpa using! summable_norm_pow_mul_geometric_of_norm_lt_one k hr)
  simpa only [Nat.cofinite_eq_atTop] using!
   tendsto_const_nhds.div ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).const_sub 1) (by simp)

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

Goal state before:
pp: A B : SL(2, ℤ)
z : ℍ
hd : ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)
this : denom (toGL (φ A)) (num (toGL (φ B)) ↑z / denom (toGL (φ B)) ↑z) = denom (toGL (φ A)) ↑(B • z)
a✝ b✝ c✝ d✝ f✝ e✝ : ℂ
he✝ : e✝ ≠ 0
⊢ a✝ / b✝ = c✝ / d✝ * (e✝ ^ 2)⁻¹ + f✝ / e✝ ↔ a✝ * e✝ ^ 2 / b✝ = c✝ / d✝ + e✝ * f✝

Tactic:
;

Goal state after:
A B : SL(2, ℤ)
z : ℍ
hd : ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)
this : denom (toGL (φ A)) (num (toGL (φ B)) ↑z / denom (toGL (φ B)) ↑z) = denom (toGL (φ A)) ↑(B • z)
a✝ b✝ c✝ d✝ f✝ e✝ : ℂ
he✝ : e✝ ≠ 0
⊢ a✝ / b✝ = c✝ / d✝ * (e✝ ^ 2)⁻¹ + f✝ / e✝ ↔ a✝ * e✝ ^ 2 / b✝ = c✝ / d✝ + e✝ * f✝
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
hnorm : normSq (↑z + 1) ≤ 1
⊢ (z.re + 1) * (z.re + 1) + z.im * z.im = z.re * z.re + z.im * z.im + (2 * z.re + 1)

Tactic:
;

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
hnorm : normSq (↑z + 1) ≤ 1
⊢ (z.re + 1) * (z.re + 1) + z.im * z.im = z.re * z.re + z.im * z.im + (2 * z.re + 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 pow_le_pow_left₀ (norm_nonneg _) (HB x hx) (n + 1)

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

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

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

Goal state after:
r : ℂ
g : ℂ → ℂ
hg : Differentiable ℂ g
y : ℂ
⊢ (fun z ↦ -r * cexp z / (1 - r * cexp z)) (g y) * deriv g y = -r * deriv g y * cexp (g y) / (1 - r * cexp (g y))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

Tactic:
;

Goal state after:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
hn0 : ↑n ≠ 0
⊢ ¬n + 1 = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

Tactic:
have H := G2Term_summable z
    rw [← ((finTwoArrowEquiv _).trans (.prodComm ..)).symm.summable_iff] at H
    exact H.prod_factor

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

Goal state before:
pp: case mul
γ g h : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
hy✝ : h ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
ih : G2 ∣[2] h = G2 - D2 h
⊢ G2 ∣[2] (g * h) = G2 - (D2 g ∣[2] h + D2 h)

Tactic:
SlashAction.slash_mul,

Goal state after:
case mul
γ g h : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
hy✝ : h ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
ih : G2 ∣[2] h = G2 - D2 h
⊢ (G2 ∣[2] g) ∣[2] h = G2 - (D2 g ∣[2] h + D2 h)
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F : ℍ → ℂ
hF : MDiff F
x✝ : ℍ
⊢ (-F) x✝ = (-1 • F) x✝

Tactic:
;

Goal state after:
F : ℍ → ℂ
hF : MDiff F
x✝ : ℍ
⊢ (-F) x✝ = (-1 • F) x✝
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * (deriv (F ∘ ↑ofComplex) ↑z * (G ∘ ↑ofComplex) ↑z + (F ∘ ↑ofComplex) ↑z * deriv (G ∘ ↑ofComplex) ↑z) =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z * G z + F z * ((2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z)

Tactic:
simp [Function.comp_apply, ofComplex_apply]

Goal state after:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ -(I * ((↑π)⁻¹ * 2⁻¹) * (deriv (F ∘ ↑ofComplex) ↑z * G z + F z * deriv (G ∘ ↑ofComplex) ↑z)) =
    -(I * ((↑π)⁻¹ * 2⁻¹) * deriv (F ∘ ↑ofComplex) ↑z * G z) + -(F z * (I * ((↑π)⁻¹ * 2⁻¹) * deriv (G ∘ ↑ofComplex) ↑z))
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F : ℍ → ℂ
n : ℕ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * (↑n * (F ∘ ↑ofComplex) ↑z ^ (n - 1) * deriv (F ∘ ↑ofComplex) ↑z) =
    ↑n z * F z ^ (n - 1) * ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z)

Tactic:
simp [Function.comp_apply, ofComplex_apply]

Goal state after:
F : ℍ → ℂ
n : ℕ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
⊢ I * ((↑π)⁻¹ * 2⁻¹) * (↑n * F z ^ (n - 1) * deriv (F ∘ ↑ofComplex) ↑z) =
    ↑n * F z ^ (n - 1) * (I * ((↑π)⁻¹ * 2⁻¹) * deriv (F ∘ ↑ofComplex) ↑z)