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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
⊢ ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod M))) ⟨z, hz_det⟩) = ↑1

Tactic:
]

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
⊢ ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod M))) ⟨z, hz_det⟩) = ↑1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
⊢ g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint

Tactic:
]

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
⊢ g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst✝ : CharZero K
n : ℕ
IH : g ^ n • g.parabolicFixedPoint = g.parabolicFixedPoint
⊢ g.parabolicFixedPoint = g.parabolicFixedPoint

Tactic:
]

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

Goal state before:
pp: case infty
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
⊢ ¬↑g 1 0 = 0

Tactic:
]

Goal state after:
case infty
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
⊢ ¬↑g 1 0 = 0
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case infty
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : ↑g 1 0 = 0
this : (↑g).discr = (↑g 0 0 - ↑g 1 1) ^ 2
⊢ 0 ≤ (↑g 0 0 - ↑g 1 1) ^ 2

Tactic:
]

Goal state after:
case infty
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
h : ↑g 1 0 = 0
this : (↑g).discr = (↑g 0 0 - ↑g 1 1) ^ 2
⊢ 0 ≤ (↑g 0 0 - ↑g 1 1) ^ 2
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case coe
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • ↑c = ↑c
this : (↑g).discr = (2 * ↑g 1 0 * c + (↑g 1 1 + -↑g 0 0)) ^ 2
⊢ 0 ≤ (2 * ↑g 1 0 * c + (↑g 1 1 + -↑g 0 0)) ^ 2

Tactic:
]

Goal state after:
case coe
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
h : g • ↑c = ↑c
this : (↑g).discr = (2 * ↑g 1 0 * c + (↑g 1 1 + -↑g 0 0)) ^ 2
⊢ 0 ≤ (2 * ↑g 1 0 * c + (↑g 1 1 + -↑g 0 0)) ^ 2
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case coe
K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : K
⊢ g • ↑c ≠ ↑c

Tactic:
refine fun h ↦ not_le_of_gt hg ?_
    have : g.val.discr = (2 * g 1 0 * c + (g 1 1 + -g 0 0)) ^ 2 := by
      replace h : g 1 0 * (c * c) + (g 1 1 + -g 0 0) * c + -g 0 1 = 0 := by
        simpa [← fixpointPolynomial_aeval_eq_zero_iff, fixpointPolynomial, sq, sub_eq_add_neg]
          using h
      simp only [← discrim_eq_sq_of_quadratic_eq_zero h, discr_fin_two, discrim, trace_fin_two,
        det_fin_two]
      grind
    rw [this]
    apply sq_nonneg

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

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

Tactic:
]

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)| ^ (k - 1) * ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1)) *
      ((σ B) (denom A ↑(B • τ)) ^ (-k) * denom B ↑τ ^ (-k)) =
    (σ A) ((σ B) (f (A • B • τ))) *
        (↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1)) *
      ((σ B) (denom A ↑(B • τ)) ^ (-k) * denom B ↑τ ^ (-k))

Tactic:
]

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
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g)⁻¹ • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex
      (mapGL ℝ).range ≠
    0

Tactic:
]

Goal state after:
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
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g)⁻¹ • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex
      (mapGL ℝ).range ≠
    0
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) * (σ B) (denom A ↑(B • τ)) ^ (-k) *
        ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1) *
      denom B ↑τ ^ (-k)

Tactic:
]

Goal state after:
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) * (σ B) (denom A ↑(B • τ)) ^ (-k) *
        ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1) *
      denom B ↑τ ^ (-k)
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
⊢ (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0

Tactic:
]

Goal state after:
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
⊢ (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

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

Tactic:
]

Goal state after:
g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤).Commensurable
    (Subgroup.map (mapGL ℝ) ⊤)
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case left
g : GL (Fin 2) ℚ
⊢ (Subgroup.comap (mapGL ℝ) (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤)).index ≠
    0

Tactic:
]

Goal state after:
case left
g : GL (Fin 2) ℚ
⊢ (Subgroup.comap (mapGL ℝ) (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤)).index ≠
    0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: case right
g : GL (Fin 2) ℚ
⊢ (Subgroup.comap (mapGL ℝ)
        ((toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) ⊤)).index ≠
    0

Tactic:
]

Goal state after:
case right
g : GL (Fin 2) ℚ
⊢ (Subgroup.comap (mapGL ℝ)
        ((toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) ⊤)).index ≠
    0
Module: Mathlib.NumberTheory.ModularForms.SlashActions

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

Tactic:
]

Goal state after:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑|↑(Matrix.GeneralLinearGroup.det A)|
this : d ≠ 0
⊢ d ^ (k1 + k2 - 1) = d ^ (1 + (k1 - 1) + (k2 - 1))
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case refine_1
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ (ConjAct.toConjAct g • p).IsParabolic

pp: case refine_2
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ (ConjAct.toConjAct g • p) • g • c = g • c

Tactic:
· simpa [ConjAct.toConjAct_smul] using hpp

Goal state after:
case refine_2
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ (ConjAct.toConjAct g • p) • g • c = g • c
Module: Mathlib.NumberTheory.ModularForms.SlashActions

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

Tactic:
]

Goal state after:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := ↑|↑(Matrix.GeneralLinearGroup.det A)|
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
⊢ (σ A) (f (A • x)) * (σ A) (g (A • x)) * (d * d ^ (k1 - 1) * d ^ (k2 - 1)) *
      (denom A ↑x ^ (-k1) * denom A ↑x ^ (-k2)) =
    d *
      ((σ A) (f (A • x)) * d ^ (k1 - 1) * denom A ↑x ^ (-k1) * ((σ A) (g (A • x)) * d ^ (k2 - 1) * denom A ↑x ^ (-k2)))
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN✝ : M ≠ 0
hΓM : Γ(M) ≤ Γ
x✝ : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) Γ(M)
⊢ IsCongruenceSubgroup (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))

Tactic:
]

Goal state after:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN✝ : M ≠ 0
hΓM : Γ(M) ≤ Γ
x✝ : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • Subgroup.map (mapGL ℝ) Γ(M)
⊢ IsCongruenceSubgroup (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))
Module: Mathlib.NumberTheory.ModularForms.Cusps

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

Tactic:
]

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

Goal state before:
pp: 𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
x✝ : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : n ≠ 0
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ g ^ n • c = c

Tactic:
]

Goal state after:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
x✝ : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : n ≠ 0
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ g ^ n • c = c
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
x✝ : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : n ≠ 0
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ g • c = c

Tactic:
]

Goal state after:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
x✝ : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : n ≠ 0
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ g • c = c
Module: Mathlib.NumberTheory.ModularForms.Cusps

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

pp: case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ ?m.30).relIndex ?m.30 ≠ 0

pp: 𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ Subgroup (GL (Fin 2) ℝ)

pp: case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ ?m.30).relIndex 𝒢 ≠ 0

Tactic:
]

Goal state after:
case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢' ≠ 0

case h𝒢'
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢 ≠ 0
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : Tendsto (fun x ↦ ‖f x‖) atImInfty (nhds 0)
⊢ Tendsto (fun x ↦ ‖(f ∣[k] g) x‖) atImInfty (nhds 0)

Tactic:
]

Goal state after:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : Tendsto (fun x ↦ ‖f x‖) atImInfty (nhds 0)
⊢ Tendsto (fun x ↦ ‖(f ∣[k] g) x‖) atImInfty (nhds 0)
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
⊢ (fun x ↦ ‖(f ∣[k] g) x‖) =O[atImInfty] 1

Tactic:
]

Goal state after:
g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : (fun x ↦ ‖f x‖) =O[atImInfty] 1
⊢ (fun x ↦ ‖(f ∣[k] g) x‖) =O[atImInfty] 1
Module: Mathlib.NumberTheory.ModularForms.Cusps

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

Tactic:
]

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
hGH : (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0
⊢ IsCusp c 𝒢
Module: Mathlib.NumberTheory.ModularForms.Cusps

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

Tactic:
]

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c (𝒢 ⊓ ℋ)
hGH : (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0
⊢ IsCusp c 𝒢
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (∀ (b : GL (Fin 2) ℝ),
      (Equiv.symm (Equiv.mulLeft g⁻¹)) b • ∞ = g • c → IsBoundedAtImInfty (f ∣[k] (Equiv.symm (Equiv.mulLeft g⁻¹)) b)) ↔
    ∀ (g_1 : GL (Fin 2) ℝ), g_1 • ∞ = c → IsBoundedAtImInfty ((f ∣[k] g) ∣[k] g_1)

Tactic:
]

Goal state after:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (∀ (b : GL (Fin 2) ℝ),
      (Equiv.symm (Equiv.mulLeft g⁻¹)) b • ∞ = g • c → IsBoundedAtImInfty (f ∣[k] (Equiv.symm (Equiv.mulLeft g⁻¹)) b)) ↔
    ∀ (g_1 : GL (Fin 2) ℝ), g_1 • ∞ = c → IsBoundedAtImInfty ((f ∣[k] g) ∣[k] g_1)
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 ∈ ℋ
⊢ 𝒢.relIndex ℋ ≠ 0

Tactic:
]

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst✝ : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ 𝒢.relIndex ℋ ≠ 0
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (∀ (b : GL (Fin 2) ℝ),
      (Equiv.symm (Equiv.mulLeft g⁻¹)) b • ∞ = g • c → IsZeroAtImInfty (f ∣[k] (Equiv.symm (Equiv.mulLeft g⁻¹)) b)) ↔
    ∀ (g_1 : GL (Fin 2) ℝ), g_1 • ∞ = c → IsZeroAtImInfty ((f ∣[k] g) ∣[k] g_1)

Tactic:
]

Goal state after:
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (∀ (b : GL (Fin 2) ℝ),
      (Equiv.symm (Equiv.mulLeft g⁻¹)) b • ∞ = g • c → IsZeroAtImInfty (f ∣[k] (Equiv.symm (Equiv.mulLeft g⁻¹)) b)) ↔
    ∀ (g_1 : GL (Fin 2) ℝ), g_1 • ∞ = c → IsZeroAtImInfty ((f ∣[k] g) ∣[k] g_1)
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: case insert.inr.e_a
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ |↑(Matrix.GeneralLinearGroup.det g)| * |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (1 + (↑(#t) - 1))

Tactic:
]

Goal state after:
case insert.inr.e_a
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ |↑(Matrix.GeneralLinearGroup.det g)| * |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (1 + (↑(#t) - 1))
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: case insert.inr.e_a
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ |↑(Matrix.GeneralLinearGroup.det g)| * |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) =
    |↑(Matrix.GeneralLinearGroup.det g)| * |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1)

pp: case insert.inr.e_a
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ |↑(Matrix.GeneralLinearGroup.det g)| ≠ 0 ∨ 1 + (↑(#t) - 1) ≠ 0 ∨ 1 = 0 ∧ ↑(#t) - 1 = 0

Tactic:
]

Goal state after:
case insert.inr.e_a
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
i : ι
t : Finset ι
hi : i ∉ t
IH : (∏ i ∈ t, f i) ∣[∑ i ∈ t, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1) • ∏ i ∈ t, f i ∣[k i] g
ht : t.Nonempty
⊢ |↑(Matrix.GeneralLinearGroup.det g)| ≠ 0 ∨ 1 + (↑(#t) - 1) ≠ 0 ∨ 1 = 0 ∧ ↑(#t) - 1 = 0
Module: Mathlib.NumberTheory.ModularForms.SlashActions

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

Tactic:
]

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

Goal state before:
pp: case mpr.refine_2
a : SL(2, ℤ)
⊢ (mapGL ℝ) (a * ModularGroup.T * a⁻¹) • OnePoint.map (⇑(algebraMap ℚ ℝ)) ((mapGL ℚ) a • ∞) =
    OnePoint.map (⇑(algebraMap ℚ ℝ)) ((mapGL ℚ) a • ∞)

Tactic:
]

Goal state after:
case mpr.refine_2
a : SL(2, ℤ)
⊢ (mapGL ℝ) (a * ModularGroup.T * a⁻¹) • OnePoint.map (⇑(algebraMap ℚ ℝ)) ((mapGL ℚ) a • ∞) =
    OnePoint.map (⇑(algebraMap ℚ ℝ)) ((mapGL ℚ) a • ∞)
Module: Mathlib.NumberTheory.ModularForms.SlashActions

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

Tactic:
]

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

Goal state before:
pp: c : OnePoint ℝ
⊢ c ∈ Set.range (OnePoint.map Rat.cast) ↔ ∃ g, c = (mapGL ℝ) g • ∞

Tactic:
]

Goal state after:
c : OnePoint ℝ
⊢ c ∈ Set.range (OnePoint.map Rat.cast) ↔ ∃ g, c = (mapGL ℝ) g • ∞
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 : ℍ
this : f (γ • z) = f z * denom γ ↑z ^ k
⊢ (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z

Tactic:
]

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 = ⇑f + ⇑g

Tactic:
]

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

Goal state before:
pp: case mp
g : SL(2, ℤ)
⊢ (mapGL ℝ) g • ∞ = (mapGL ℝ) g • ∞

Tactic:
]

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 • 1) • ⇑f) ∣[k] γ = (c • 1) • ⇑f

Tactic:
]

Goal state after:
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 • 1) • ⇑f) ∣[k] γ = (c • 1) • ⇑f
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp
c : OnePoint ℝ
⊢ c ∈ Set.range (OnePoint.map Rat.cast) → ∃ g, c = (mapGL ℝ) g • ∞

pp: case mpr
c : OnePoint ℝ
⊢ (∃ g, c = (mapGL ℝ) g • ∞) → c ∈ Set.range (OnePoint.map Rat.cast)

Tactic:
· rintro ⟨c, rfl⟩
    obtain ⟨g, rfl⟩ := c.exists_mem_SL2 ℤ
    refine ⟨g, ?_⟩
    rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
      ← (Rat.castHom ℝ).algebraMap_toAlgebra, g.map_mapGL]

Goal state after:
case mpr
c : OnePoint ℝ
⊢ (∃ g, c = (mapGL ℝ) g • ∞) → c ∈ Set.range (OnePoint.map Rat.cast)
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 • 1) • ⇑f = ↑(c • 1) • ⇑f

Tactic:
]

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

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ (mapGL ℝ) g • ∞ = (mapGL ℝ) g • ∞

Tactic:
]

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 = -⇑f

Tactic:
]

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

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

Tactic:
]

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 : g * j * g⁻¹ ∈ Γ
⊢ (⇑f ∣[k] g) ∣[k] j = ⇑f ∣[k] g

Tactic:
]

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj : g * j * g⁻¹ ∈ Γ
⊢ (⇑f ∣[k] g) ∣[k] j = ⇑f ∣[k] g
Module: Mathlib.NumberTheory.ModularForms.Cusps

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

Tactic:
]

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