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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
⊢ f (h +ᵥ τ) = (⇑f ∣[k] GeneralLinearGroup.upperRightHom h) τ

Tactic:
]

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
⊢ f (h +ᵥ τ) = (⇑f ∣[k] GeneralLinearGroup.upperRightHom h) τ
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mk
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
b✝ : CuspOrbits 𝒢
c : OnePoint ℝ
hc✝ : IsCusp c 𝒢
hc : ∃ g, c = (mapGL ℝ) g • ∞
⊢ ∃ a, cosetToCuspOrbit 𝒢 a = Quot.mk ⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) ⟨c, hc✝⟩

Tactic:
]

Goal state after:
case mk
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
b✝ : CuspOrbits 𝒢
c : OnePoint ℝ
hc✝ : IsCusp c 𝒢
hc : ∃ g, c = (mapGL ℝ) g • ∞
⊢ ∃ a, cosetToCuspOrbit 𝒢 a = Quot.mk ⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) ⟨c, hc✝⟩
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:
]

Goal state after:
N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ f (↑(↑N * n) +ᵥ z) = f z
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
z : ℍ
⊢ f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } *
      denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)) ↑z ^ (-k) =
    f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * ↑z ^ (-k)

Tactic:
]

Goal state after:
f : ℍ → ℂ
k : ℤ
z : ℍ
⊢ f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } *
      denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)) ↑z ^ (-k) =
    f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * ↑z ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u : R
hu_mem : u ∈ 𝒢.periods
hu_notMem : u ∉ 𝒢.strictPeriods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨
    ∃ a ∈ 𝒢.periods, a ∉ 𝒢.strictPeriods ∧ ∀ b ∈ 𝒢.periods, b + a ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u : R
hu_mem : u ∈ 𝒢.periods
hu_notMem : u ∉ 𝒢.strictPeriods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨
    ∃ a ∈ 𝒢.periods, a ∉ 𝒢.strictPeriods ∧ ∀ b ∈ 𝒢.periods, b + a ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ A 0 0 * A 1 1 - A 0 1 * A 1 0 = b₀ * cd 0 + a * cd 1

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ A 0 0 * A 1 1 - A 0 1 * A 1 0 = b₀ * cd 0 + a * cd 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1

Tactic:
by ring

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

Goal state before:
pp: case mpr.inv
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
x : GL (Fin 2) ℝ
hx : x ∈ Subgroup.closure s
hf : f ∣[k] x = f
⊢ f ∣[k] (x * x⁻¹) = f ∣[k] x

Tactic:
]

Goal state after:
case mpr.inv
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
x : GL (Fin 2) ℝ
hx : x ∈ Subgroup.closure s
hf : f ∣[k] x = f
⊢ f ∣[k] (x * x⁻¹) = f ∣[k] x
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
this : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
x✝ : Fin 2 → ℝ
⊢ ↑(Function.eval 0 x✝) * ↑z + ↑(Function.eval 1 x✝) = ↑(x✝ 0) * ↑z + ↑(x✝ 1)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
this : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
x✝ : Fin 2 → ℤ
⊢ normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = (⇑normSq ∘ (fun p ↦ ↑(p 0) * ↑z + ↑(p 1)) ∘ fun p ↦ Int.cast ∘ p) x✝

Tactic:
]

Goal state after:
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
x✝ : Fin 2 → ℤ
⊢ normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = (⇑normSq ∘ (fun p ↦ ↑(p 0) * ↑z + ↑(p 1)) ∘ fun p ↦ Int.cast ∘ p) x✝
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
this : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
x✝ : Fin 2 → ℤ
⊢ normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1))

Tactic:
]

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

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : (map (mapGL ℝ) Γ).strictPeriods = AddSubgroup.zmultiples 1
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 1)

Tactic:
]

Goal state after:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : (map (mapGL ℝ) Γ).strictPeriods = AddSubgroup.zmultiples 1
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 1)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
⊢ Tendsto (⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p) cofinite atTop

Tactic:
]

Goal state after:
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
⊢ Tendsto (⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p) cofinite atTop
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : 1 = (map (mapGL ℝ) Γ).strictWidthInfty ∨ -1 = (map (mapGL ℝ) Γ).strictWidthInfty
this : DiscreteTopology ↥(map (mapGL ℝ) Γ).strictPeriods
⊢ (map (mapGL ℝ) Γ).strictWidthInfty = 1

Tactic:
]

Goal state after:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : 1 = (map (mapGL ℝ) Γ).strictWidthInfty ∨ -1 = (map (mapGL ℝ) Γ).strictWidthInfty
this : DiscreteTopology ↥(map (mapGL ℝ) Γ).strictPeriods
⊢ (map (mapGL ℝ) Γ).strictWidthInfty = 1
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp.refine_1
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 0 =
      ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 1 1 ∧
    ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 1 ≠ 0

Tactic:
]

Goal state after:
case mp.refine_1
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 0 =
      ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 1 1 ∧
    ↑(Additive.toMul (upperRightHom.toAddMonoidHom 𝒢.strictWidthInfty)) 0 1 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : g • ∞ = ∞
⊢ AddSubgroup.zmultiples 𝒢.strictWidthInfty ≠ ⊥

Tactic:
]

Goal state after:
case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : g • ∞ = ∞
⊢ AddSubgroup.zmultiples 𝒢.strictWidthInfty ≠ ⊥
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : ↑g 1 0 = 0
⊢ ∃ a, ¬a = 0 ∧ upperRightHom a ∈ 𝒢

Tactic:
]

Goal state after:
case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : ↑g 1 0 = 0
⊢ ∃ a, ¬a = 0 ∧ upperRightHom a ∈ 𝒢
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ • g (f c) = c

Tactic:
]

Goal state after:
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ • g (f c) = c
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : (∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x
hgi : ↑g 1 0 = 0
⊢ ∃ a, ¬a = 0 ∧ upperRightHom a ∈ 𝒢

Tactic:
]

Goal state after:
case mpr
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.strictPeriods
inst✝ : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : (∃ x, x ≠ 0 ∧ g = upperRightHom x) ∨ ∃ x, x ≠ 0 ∧ g = -upperRightHom x
hgi : ↑g 1 0 = 0
⊢ ∃ a, ¬a = 0 ∧ upperRightHom a ∈ 𝒢
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ IsCusp ∞ 𝒢

Tactic:
]

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ IsCusp ∞ 𝒢
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : DiscreteTopology ↥𝒢.periods
inst✝ : 𝒢.HasDetPlusMinusOne
this : DiscreteTopology ↥𝒢.adjoinNegOne.strictPeriods
⊢ IsCusp ∞ 𝒢 ↔ IsCusp ∞ 𝒢

Tactic:
]

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : DiscreteTopology ↥𝒢.periods
h : 𝒢.widthInfty ∈ 𝒢.strictPeriods
⊢ 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
]

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : DiscreteTopology ↥𝒢.periods
h : 𝒢.widthInfty ∈ 𝒢.strictPeriods
⊢ 𝒢.widthInfty ∈ 𝒢.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hf : DifferentiableOn ℂ (fun x ↦ f (↑ofComplex x)) {z | 0 < z.im}
z : ℂ
h : z ∈ {z | 0 < z.im}
⊢ (fun x ↦ (starRingEnd ℂ) (f (↑ofComplex (-(starRingEnd ℂ) ↑(↑ofComplex x))))) z =
    (fun x ↦ (starRingEnd ℂ) (f (↑ofComplex (-(starRingEnd ℂ) x)))) z

Tactic:
by simp [ofComplex_apply_of_im_pos h]

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

Goal state before:
pp: case mp
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
g : SL(2, ℤ)
hx : (mapGL ℝ) g = upperRightHom x
hg : ↑(↑g 0 1) = 0
⊢ ↑(↑g 0 1) ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)

Tactic:
]

Goal state after:
case mp
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
g : SL(2, ℤ)
hx : (mapGL ℝ) g = upperRightHom x
hg : ↑(↑g 0 1) = 0
⊢ ↑(↑g 0 1) ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ c 0 = c 0

Tactic:
]

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

Goal state before:
pp: case mp
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
g : SL(2, ℤ)
hx : (mapGL ℝ) g = upperRightHom x
hg : ↑(↑g 0 1) = 0
⊢ ↑(↑g 0 1) = 0

Tactic:
]

Goal state after:
case mp
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
g : SL(2, ℤ)
hx : (mapGL ℝ) g = upperRightHom x
hg : ↑(↑g 0 1) = 0
⊢ ↑(↑g 0 1) = 0
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g).det < 0
⊢ MDiff ((f ∣[k] J) ∣[k] (J * g))

Tactic:
]

Goal state after:
f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : (↑g).det < 0
⊢ MDiff ((f ∣[k] J) ∣[k] (J * g))
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f z = -1 * f z
⊢ f z = 0 z

Tactic:
]

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f z = -1 * f z
⊢ f z = 0 z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z * ↑(c 1)).im = (↑z).im * c 1

Tactic:
]

Goal state after:
case «1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z * ↑(c 1)).im = (↑z).im * c 1
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
hsp : ↑N = (Subgroup.map (mapGL ℝ) Γ(N)).strictWidthInfty ∨ -↑N = (Subgroup.map (mapGL ℝ) Γ(N)).strictWidthInfty
⊢ (Subgroup.map (mapGL ℝ) Γ(N)).strictWidthInfty = ↑N

Tactic:
]

Goal state after:
N : ℕ
inst✝ : NeZero N
hsp : ↑N = (Subgroup.map (mapGL ℝ) Γ(N)).strictWidthInfty ∨ -↑N = (Subgroup.map (mapGL ℝ) Γ(N)).strictWidthInfty
⊢ (Subgroup.map (mapGL ℝ) Γ(N)).strictWidthInfty = ↑N
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
⊢ ball 0 1 ∈ 𝓝 0

Tactic:
by simpa [ball_zero_eq] using Metric.ball_mem_nhds (0 : ℂ) zero_lt_one

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_4
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
hf : f.ker = ⊥
hf' : IsClosedEmbedding ⇑f
⊢ cofinite = cofinite

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case e'_5
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
hf : f.ker = ⊥
hf' : IsClosedEmbedding ⇑f
⊢ cocompact (Fin 2 → ℝ) = cocompact (Fin 2 → ℝ)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ¬cd 0 ^ 2 + cd 1 ^ 2 = 0

Tactic:
]

Goal state after:
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ¬cd 0 ^ 2 + cd 1 ^ 2 = 0
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |↑(Matrix.GeneralLinearGroup.det g)|
hD : ↑D ≠ 0
j : ℂ := denom g ↑τ
⊢ ↑D ^ (k - 2) * ↑D ^ k * (starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) *
      (↑τ.im ^ k * (↑(Complex.normSq j) ^ k)⁻¹) =
    ↑D ^ (k - 2) *
      ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * (↑D ^ k * ↑τ.im ^ k * (↑(Complex.normSq j) ^ k)⁻¹))

Tactic:
]

Goal state after:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |↑(Matrix.GeneralLinearGroup.det g)|
hD : ↑D ≠ 0
j : ℂ := denom g ↑τ
⊢ ↑D ^ (k - 2) * ↑D ^ k * (starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) *
      (↑τ.im ^ k * (↑(Complex.normSq j) ^ k)⁻¹) =
    ↑D ^ (k - 2) *
      ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * (↑D ^ k * ↑τ.im ^ k * (↑(Complex.normSq j) ^ k)⁻¹))
Module: Mathlib.NumberTheory.ModularForms.Basic

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

Tactic:
]

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

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
⊢ ‖(ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm
        (FormalMultilinearSeries.ofScalars ℂ (fun m ↦ (PowerSeries.coeff m) (qExpansion h ⇑f)) m)‖ =
    ‖(PowerSeries.coeff m) (qExpansion h ⇑f)‖

Tactic:
]

Goal state after:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
⊢ ‖(ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm
        (FormalMultilinearSeries.ofScalars ℂ (fun m ↦ (PowerSeries.coeff m) (qExpansion h ⇑f)) m)‖ =
    ‖(PowerSeries.coeff m) (qExpansion h ⇑f)‖
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |↑(Matrix.GeneralLinearGroup.det g)|
hD : ↑D ≠ 0
j : ℂ := denom g ↑τ
⊢ ↑D ^ (k - 2) * ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * (↑D * ↑τ.im / ↑(Complex.normSq j)) ^ k) =
    ↑D ^ (k - 2) *
      ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) *
        (↑|↑(Matrix.GeneralLinearGroup.det g)| * ↑τ.im / ↑(Complex.normSq (denom g ↑τ))) ^ k)

Tactic:
]

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

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
r : NNReal
hr : ↑r < 1
⊢ Summable fun n ↦ ‖(PowerSeries.coeff n) (qExpansion h ⇑f)‖ * ↑r ^ n

Tactic:
← r.abs_eq

Goal state after:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
r : NNReal
hr : ↑r < 1
⊢ Summable fun n ↦ ‖(PowerSeries.coeff n) (qExpansion h ⇑f)‖ * |↑r| ^ n
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
r : NNReal
hr : ↑r < 1
⊢ Summable fun n ↦ ‖(PowerSeries.coeff n) (qExpansion h ⇑f)‖ * |↑r| ^ n

Tactic:
]

Goal state after:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
hh : 0 < h
hfper : Periodic (⇑f ∘ ↑ofComplex) ↑h
hfhol : MDiff ⇑f
hfbdd : IsBoundedAtImInfty ⇑f
r : NNReal
hr : ↑r < 1
⊢ Summable fun n ↦ ‖(PowerSeries.coeff n) (qExpansion h ⇑f)‖ * |↑r| ^ n
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:
]

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
⊢ ((g * γ) • ∞).IsZeroAt (⇑f) k
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ (toGL ((map (Int.castRingHom ℝ)) g) • ∞).IsBoundedAt (⇑f) k

Tactic:
]

Goal state after:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ (toGL ((map (Int.castRingHom ℝ)) g) • ∞).IsBoundedAt (⇑f) k
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ ∃ g_1, toGL ((map (Int.castRingHom ℝ)) g) • ∞ = (mapGL ℝ) g_1 • ∞

Tactic:
]

Goal state after:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ ∃ g_1, toGL ((map (Int.castRingHom ℝ)) g) • ∞ = (mapGL ℝ) g_1 • ∞