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

Goal state before:
pp: β : Type u_1
G : Type u_2
H : Type u_3
α : Type u_4
inst✝³ : Monoid G
inst✝² : AddMonoid α
inst✝¹ : Monoid H
inst✝ : SlashAction β G α
h : H →* G
k : β
a : α
⊢ a ∣[k] h 1 = a

Tactic:
by

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

Goal state before:
pp: β : Type u_1
G : Type u_2
H : Type u_3
α : Type u_4
inst✝³ : Monoid G
inst✝² : AddMonoid α
inst✝¹ : Monoid H
inst✝ : SlashAction β G α
h : H →* G
k : β
g gg : H
a : α
⊢ a ∣[k] h (g * gg) = (a ∣[k] h g) ∣[k] h gg

Tactic:
by

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

Goal state before:
pp: β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Group G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
⊢ a = 0 → a ∣[k] g = 0

Tactic:
by

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

Goal state before:
pp: β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Group G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
⊢ a ∣[k] g = 0 ↔ a = 0

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
⊢ ∃ N, N ≠ 0 ∧ ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
⊢ ∃ N,
    N ≠ 0 ∧
      toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ Subgroup.map (mapGL ℝ) Γ(M)

Tactic:
by

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

Goal state before:
pp: k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ (σ (A * B)) (f ((A * B) • τ)) * ↑|↑(Matrix.GeneralLinearGroup.det (A * B))| ^ (k - 1) * denom (A * B) ↑τ ^ (-k) =
    (σ B) ((σ A) (f (A • B • τ))) *
        (↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1)) *
      ((σ B) (denom A ↑(B • τ) ^ (-k)) * denom B ↑τ ^ (-k))

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
this : (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g)).index ≠ 0

Tactic:
by

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

Goal state before:
pp: k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ (σ B) ((σ A) (f (A • B • τ))) *
        (↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1)) *
      ((σ B) (denom A ↑(B • τ) ^ (-k)) * denom B ↑τ ^ (-k)) =
    (σ B) ((σ A) (f (A • B • τ)) * ↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * denom A ↑(B • τ) ^ (-k)) *
        ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1) *
      denom B ↑τ ^ (-k)

Tactic:
by

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

Goal state before:
pp: k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
⊢ f ∣[k] (A * B) = (f ∣[k] A) ∣[k] B

Tactic:
by

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

Goal state before:
pp: k : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
⊢ (f + g) ∣[k] A = f ∣[k] A + g ∣[k] A

Tactic:
by

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

Goal state before:
pp: k : ℤ
f : ℍ → ℂ
⊢ ∀ (x : ℍ), (f ∣[k] 1) x = f x

Tactic:
by

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

Goal state before:
pp: k : ℤ
A : GL (Fin 2) ℝ
x✝ : ℍ
⊢ (0 ∣[k] A) x✝ = 0 x✝

Tactic:
by

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

Goal state before:
pp: k : ℤ
A : GL (Fin 2) ℝ
f : ℍ → ℂ
c : ℂ
⊢ (c • f) ∣[k] A = (σ A) c • f ∣[k] A

Tactic:
by

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

Goal state before:
pp: k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
⊢ f ∣[k] γ = fun τ ↦
    f (γ • τ) * denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ ^ (-k)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
τ : ℍ
⊢ (f ∣[k] γ) τ =
    f (γ • τ) * denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ ^ (-k)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : SL(2, ℤ)
f : ℍ → ℂ
c : α
⊢ (c • f) ∣[k] A = c • f ∣[k] A

Tactic:
by

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

Goal state before:
pp: A : SL(2, ℤ)
x : ℂ
⊢ Function.const ℍ x ∣[0] A = Function.const ℍ x

Tactic:
by

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

Goal state before:
pp: A : SL(2, ℤ)
⊢ 1 ∣[0] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A) = 1

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℚ
⊢ (conjGL ⊤ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g)).FiniteIndex

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : DecidableEq K
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsPrincipalIdealRing A
⊢ (mapGL K) 1 • ∞ = ∞

Tactic:
by

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

Goal state before:
pp: k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ (f ∣[k] γ) z = f z ↔ f (γ • z) = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : DecidableEq K
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsPrincipalIdealRing A
q : K
g : SL(2, A)
hg0 : ↑g 0 0 = IsFractionRing.num A q
hg1 : ↑g 1 0 = ↑(IsFractionRing.den A q)
⊢ (mapGL K) g • ∞ = ↑q

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • (mapGL ℝ).range).IsArithmetic

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : DecidableEq K
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsPrincipalIdealRing A
c : OnePoint K
⊢ ∃ g, (mapGL K) g • ∞ = c

Tactic:
by

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

Goal state before:
pp: k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑|↑(Matrix.GeneralLinearGroup.det A)|
⊢ d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
⊢ IsCusp (g • c) (ConjAct.toConjAct g • 𝒢)

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
⊢ IsCusp (g • c) 𝒢

Tactic:
by

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

Goal state before:
pp: k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
⊢ (f * g) ∣[k1 + k2] A = |↑(Matrix.GeneralLinearGroup.det A)| • (f ∣[k1] A * g ∣[k2] A)

Tactic:
by

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

Goal state before:
pp: k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
⊢ (f * g) ∣[k1 + k2] A = f ∣[k1] A * g ∣[k2] A

Tactic:
by

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

Goal state before:
pp: 𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
⊢ IsCusp c 𝒢' ↔ IsCusp c 𝒢

Tactic:
by

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

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : IsCongruenceSubgroup Γ
g : GL (Fin 2) ℚ
⊢ IsCongruenceSubgroup (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))

Tactic:
by

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

Goal state before:
pp: k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
⊢ (f / g) ∣[k1 - k2] A = f ∣[k1] A / g ∣[k2] A

Tactic:
by

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

Goal state before:
pp: 𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ IsCusp c 𝒢 ↔ IsCusp c 𝒢'

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : IsZeroAtImInfty f
⊢ IsZeroAtImInfty (f ∣[k] g)

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : (fun x ↦ ‖f x‖) =O[atImInfty] 1
this : (fun x ↦ ‖↑(GeneralLinearGroup.det g) ^ (k - 1)‖ * ‖↑g 1 1 ^ (-k)‖ * ‖f (g • x)‖) =O[atImInfty] 1
⊢ (fun x ↦ ‖(f ∣[k] g) x‖) =O[atImInfty] 1

Tactic:
by

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

Goal state before:
pp: g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : IsBoundedAtImInfty f
⊢ IsBoundedAtImInfty (f ∣[k] g)

Tactic:
by

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

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
⊢ IsCusp c 𝒢

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (g • c).IsBoundedAt f k ↔ c.IsBoundedAt (f ∣[k] g) k

Tactic:
by

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

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ IsCusp c (ConjAct.toConjAct h • 𝒢)

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (g • c).IsZeroAt f k ↔ c.IsZeroAt (f ∣[k] g) k

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
f' : ℍ → ℂ
hf : c.IsBoundedAt f k
hf' : c.IsBoundedAt f' k
g : GL (Fin 2) ℝ
hg : g • ∞ = c
⊢ IsBoundedAtImInfty ((f + f') ∣[k] g)

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
f' : ℍ → ℂ
hf : c.IsZeroAt f k
hf' : c.IsZeroAt f' k
g : GL (Fin 2) ℝ
hg : g • ∞ = c
⊢ IsZeroAtImInfty ((f + f') ∣[k] g)

Tactic:
by

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
h : ∞.IsBoundedAt f k
⊢ 1 • ∞ = ∞

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
g : SL(2, ℤ)
hgp : ((mapGL ℝ) g).IsParabolic
hgc : (mapGL ℝ) g • c = c
⊢ OnePoint.map Rat.cast ((mapGL ℚ) g).parabolicFixedPoint = ((mapGL ℝ) g).parabolicFixedPoint

Tactic:
by

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
h : ∞.IsBoundedAt f k
⊢ IsBoundedAtImInfty f

Tactic:
by

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
h : ∞.IsZeroAt f k
⊢ 1 • ∞ = ∞

Tactic:
by

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
h : ∞.IsZeroAt f k
⊢ IsZeroAtImInfty f

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
hg : g • ∞ = c
⊢ IsBoundedAtImInfty (f ∣[k] g) → c.IsBoundedAt f k

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
hg : g • ∞ = c
⊢ IsZeroAtImInfty (f ∣[k] g) → c.IsZeroAt f k

Tactic:
by

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

Goal state before:
pp: a : SL(2, ℤ)
this : ((mapGL ℝ) ModularGroup.T).IsParabolic
⊢ ((mapGL ℝ) (a * ModularGroup.T * a⁻¹)).IsParabolic

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ c.IsBoundedAt f k ↔ ∃ γ, (mapGL ℝ) γ • ∞ = c ∧ IsBoundedAtImInfty (f ∣[k] γ)

Tactic:
by

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

Goal state before:
pp: a✝ : SL(2, ℤ)
x✝ : ↑((mapGL ℝ) ModularGroup.T) ∈ Set.range ⇑(Matrix.scalar (Fin 2))
a : ℝ
ha : (Matrix.scalar (Fin 2)) a = ↑((mapGL ℝ) ModularGroup.T)
⊢ 0 = 1

Tactic:
by

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

Goal state before:
pp: case mpr.refine_1
a : SL(2, ℤ)
⊢ (↑((mapGL ℝ) ModularGroup.T)).discr = 0

Tactic:
simp [discr_fin_two, trace_fin_two, det_fin_two, ModularGroup.T]

Goal state after:
case mpr.refine_1
a : SL(2, ℤ)
⊢ (1 + 1) ^ 2 - 4 = 0
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ c.IsZeroAt f k ↔ ∃ γ, (mapGL ℝ) γ • ∞ = c ∧ IsZeroAtImInfty (f ∣[k] γ)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc✝ : IsCusp c (mapGL ℝ).range
hc : c.IsBoundedAt f k
x✝ : SL(2, ℤ)
hγ : (mapGL ℝ) x✝ • ∞ = c
⊢ IsBoundedAtImInfty (f ∣[k] x✝)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ k * ↑(#s) = ∑ i ∈ s, k

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ c.IsBoundedAt f k ↔ ∀ (γ : SL(2, ℤ)), (mapGL ℝ) γ • ∞ = c → IsBoundedAtImInfty (f ∣[k] γ)

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc✝ : IsCusp c (mapGL ℝ).range
hc : c.IsZeroAt f k
x✝ : SL(2, ℤ)
hγ : (mapGL ℝ) x✝ • ∞ = c
⊢ IsZeroAtImInfty (f ∣[k] x✝)

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ c.IsZeroAt f k ↔ ∀ (γ : SL(2, ℤ)), (mapGL ℝ) γ • ∞ = c → IsZeroAtImInfty (f ∣[k] γ)

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
⊢ IsCusp c (mapGL ℝ).range ↔ c ∈ Set.range (OnePoint.map Rat.cast)

Tactic:
by

Goal state after:
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

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

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

Tactic:
by

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : SlashInvariantForm Γ k
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : Γ.HasDetOne
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
⊢ f (γ • z) = f z * denom γ ↑z ^ k

Tactic:
by

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : Γ.HasDetOne
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
⊢ f (γ • z) = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z

Tactic:
by

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

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
inst✝ : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k
f : F
γ : SL(2, ℤ)
hγ : γ ∈ Γ
z : ℍ
⊢ (Matrix.SpecialLinearGroup.mapGL ℝ) γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ

Tactic:
by

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : FunLike F ℍ ℂ
f g : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (⇑f + ⇑g) ∣[k] γ = ⇑f + ⇑g

Tactic:
by

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✝² : Γ.HasDetOne
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (c • ⇑f) ∣[k] γ = c • ⇑f

Tactic:
by

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : SMul α ℝ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (c • ⇑f) ∣[k] γ = c • ⇑f

Tactic:
by

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

Goal state before:
pp: c : OnePoint ℝ
⊢ IsCusp c (mapGL ℝ).range ↔ ∃ g, c = (mapGL ℝ) g • ∞

Tactic:
by

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : FunLike F ℍ ℂ
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (-⇑f) ∣[k] γ = -⇑f

Tactic:
by

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✝ : Γ.HasDetOne
x : ℂ
g : GL (Fin 2) ℝ
hg : g ∈ Γ
⊢ Function.const ℍ x ∣[0] g = Function.const ℍ x

Tactic:
by

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✝ : Γ.HasDetPlusMinusOne
x : ℝ
g : GL (Fin 2) ℝ
hg : g ∈ Γ
τ : ℍ
⊢ (Function.const ℍ ↑x ∣[0] g) τ = Function.const ℍ (↑x) τ

Tactic:
by

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✝ : Γ.HasDetPlusMinusOne
k₁ k₂ : ℤ
f : SlashInvariantForm Γ k₁
g : SlashInvariantForm Γ k₂
A : GL (Fin 2) ℝ
hA : A ∈ Γ
⊢ (⇑f * ⇑g) ∣[k₁ + k₂] A = ⇑f * ⇑g

Tactic:
by

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

Goal state before:
pp: F : Type u_1
Γ✝ : Subgroup (GL (Fin 2) ℝ)
k✝ : ℤ
inst✝¹ : FunLike F ℍ ℂ
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
f : (i : ι) → SlashInvariantForm Γ (k i)
A : GL (Fin 2) ℝ
hA : A ∈ Γ
⊢ (∏ i ∈ s, ⇑(f i)) ∣[m] A = ∏ i ∈ s, ⇑(f i)

Tactic:
by

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
g : SL(2, ℤ)
⊢ OnePoint.map Rat.cast ((mapGL ℚ) g⁻¹ • ∞) = (mapGL ℝ) g⁻¹ • ∞

Tactic:
by

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

Goal state before:
pp: F : Type u_1
Γ✝ : Subgroup (GL (Fin 2) ℝ)
k✝ : ℤ
inst✝¹ : FunLike F ℍ ℂ
ι : Type
s : Finset ι
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
f : ι → SlashInvariantForm Γ k
⊢ ↑s.card * k = ∑ i ∈ s, k

Tactic:
by

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:
by

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : a ≈ b
⊢ ⟦⟨(mapGL ℝ) a⁻¹ • ∞, ⋯⟩⟧ = ⟦⟨(mapGL ℝ) b⁻¹ • ∞, ⋯⟩⟧

Tactic:
by

Goal state after:
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
this : GeneralLinearGroup.upperRightHom h • τ = h +ᵥ τ
⊢ f (h +ᵥ τ) = (⇑f ∣[k] GeneralLinearGroup.upperRightHom h) τ

Tactic:
by

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ Function.Surjective (cosetToCuspOrbit 𝒢)

Tactic:
by

Goal state after:
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 τ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
x : R
⊢ x ∈ 𝒢.strictPeriods ↔ upperRightHom x ∈ 𝒢

Tactic:
by

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:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods ≤ 𝒢.periods

Tactic:
by

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:
by

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
z : ℍ
⊢ (f ∣[k] ModularGroup.S) z = f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * ↑z ^ (-k)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2

Tactic:
by

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

Goal state before:
pp: f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ f ∣[k] 1 = f

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods.Commensurable 𝒢.periods

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h𝒢 : -1 ∈ 𝒢
⊢ 𝒢.strictPeriods = 𝒢.periods

Tactic:
by

Goal state after: