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

Goal state before:
pp: case inl.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : a✝ ∈ 𝒢
hb : -b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
·

Goal state after:
case inl.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : a✝ ∈ 𝒢
hb : -b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inr.inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : -a✝ ∈ 𝒢
hb : b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
·

Goal state after:
case inr.inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : -a✝ ∈ 𝒢
hb : b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inr.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : -a✝ ∈ 𝒢
hb : -b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
·

Goal state after:
case inr.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
a✝ b✝ : GL n R
ha : -a✝ ∈ 𝒢
hb : -b✝ ∈ 𝒢
⊢ a✝ * b✝ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
x✝ : GL n R
ha : x✝ ∈ 𝒢
⊢ x✝⁻¹ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
·

Goal state after:
case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
x✝ : GL n R
ha : x✝ ∈ 𝒢
⊢ x✝⁻¹ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
x✝ : GL n R
ha : -x✝ ∈ 𝒢
⊢ x✝⁻¹ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}

Tactic:
·

Goal state after:
case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
x✝ : GL n R
ha : -x✝ ∈ 𝒢
⊢ x✝⁻¹ ∈ {g | g ∈ 𝒢 ∨ -g ∈ 𝒢}
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case pos
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∈ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

pp: case neg
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∉ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

Tactic:
·

Goal state after:
case pos
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∈ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case neg
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∉ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

Tactic:
·

Goal state after:
case neg
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
hG : -1 ∉ 𝒢
⊢ 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

Tactic:
·

Goal state after:
case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

Tactic:
·

Goal state after:
case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case pos
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : Even (Fintype.card n)
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

pp: case neg
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : ¬Even (Fintype.card n)
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

Tactic:
·

Goal state after:
case pos
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : Even (Fintype.card n)
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case neg
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : ¬Even (Fintype.card n)
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

Tactic:
·

Goal state after:
case neg
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
hn : ¬Even (Fintype.card n)
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1

pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1

Tactic:
·

Goal state after:
case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1

Tactic:
·

Goal state after:
case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
hn : Even (Fintype.card n)
x✝ : 𝒢.HasDetOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
⊢ ∃ a, a • w = ![1, 0]

pp: case neg
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : ¬w 1 = 0
⊢ ∃ a, a • w = ![(w 1)⁻¹ * w 0, 1]

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
⊢ ∃ a, a • w = ![1, 0]
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : ¬w 1 = 0
⊢ ∃ a, a • w = ![(w 1)⁻¹ * w 0, 1]

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : ¬w 1 = 0
⊢ ∃ a, a • w = ![(w 1)⁻¹ * w 0, 1]
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ∞ = ↑c

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ¬↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑((↑g 0 0 * c + ↑g 0 1) / (↑g 1 0 * c + ↑g 1 1)) = ↑c

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ∞ = ↑c
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ¬↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑((↑g 0 0 * c + ↑g 0 1) / (↑g 1 0 * c + ↑g 1 1)) = ↑c

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ¬↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑((↑g 0 0 * c + ↑g 0 1) / (↑g 1 0 * c + ↑g 1 1)) = ↑c
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
hc : ↑g 1 0 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑c = g.parabolicFixedPoint

pp: case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
hc : ¬↑g 1 0 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑c = g.parabolicFixedPoint

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
hc : ↑g 1 0 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑c = g.parabolicFixedPoint
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
hc : ¬↑g 1 0 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑c = g.parabolicFixedPoint

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
hc : ¬↑g 1 0 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑c = g.parabolicFixedPoint
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

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

pp: case right
g : GL (Fin 2) ℚ
⊢ (Subgroup.map (mapGL ℝ) ⊤).relIndex
      (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤) ≠
    0

Tactic:
·

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

Goal state before:
pp: case e'_1.e'_2
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ f (γ • z) * denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ (-k) =
    ((↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k)⁻¹ * f (γ • z)

pp: case convert_4
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k ≠ 0

Tactic:
·

Goal state after:
case e'_1.e'_2
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ f (γ • z) * denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ (-k) =
    ((↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k)⁻¹ * f (γ • z)
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: case convert_4
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k ≠ 0

Tactic:
·

Goal state after:
case convert_4
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k ≠ 0
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

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

Tactic:
·

Goal state after:
case right
g : GL (Fin 2) ℚ
⊢ (Subgroup.map (mapGL ℝ) ⊤).relIndex
      (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤) ≠
    0
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:
·

Goal state after:
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
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
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:
·

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.Cusps

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

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

Tactic:
·

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

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

Tactic:
·

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

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

pp: case insert.inr
ι : 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
⊢ (∏ i ∈ insert i t, f i) ∣[∑ i ∈ insert i t, k i] g =
    |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#(insert i t)) - 1) • ∏ i ∈ insert i t, f i ∣[k i] g

Tactic:
·

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

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

pp: case mpr
c : OnePoint ℝ
⊢ c ∈ Set.range (OnePoint.map Rat.cast) → IsCusp c (mapGL ℝ).range

Tactic:
·

Goal state after:
case mp
c : OnePoint ℝ
⊢ IsCusp c (mapGL ℝ).range → c ∈ Set.range (OnePoint.map Rat.cast)
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:
zpow_add',

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 * |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#t) - 1)

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.Cusps

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

Tactic:
·

Goal state after:
case mpr
c : OnePoint ℝ
⊢ c ∈ Set.range (OnePoint.map Rat.cast) → IsCusp c (mapGL ℝ).range
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

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

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

Tactic:
·

Goal state after:
case mp
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ c.IsBoundedAt f k → ∃ γ, (mapGL ℝ) γ • ∞ = c ∧ IsBoundedAtImInfty (f ∣[k] γ)
Module: Mathlib.NumberTheory.ModularForms.Cusps

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

pp: case mpr.refine_2
a : SL(2, ℤ)
⊢ (mapGL ℝ) (a * ModularGroup.T * a⁻¹) • OnePoint.map Rat.cast ((mapGL ℚ) a • ∞) =
    OnePoint.map Rat.cast ((mapGL ℚ) a • ∞)

Tactic:
·

Goal state after:
case mpr.refine_1
a : SL(2, ℤ)
⊢ ((mapGL ℝ) (a * ModularGroup.T * a⁻¹)).IsParabolic
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

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

Tactic:
·

Goal state after:
case mpr
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ (∃ γ, (mapGL ℝ) γ • ∞ = c ∧ IsBoundedAtImInfty (f ∣[k] γ)) → c.IsBoundedAt f k
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

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

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

Tactic:
·

Goal state after:
case mp
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ c.IsZeroAt f k → ∃ γ, (mapGL ℝ) γ • ∞ = c ∧ IsZeroAtImInfty (f ∣[k] γ)
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

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

Tactic:
·

Goal state after:
case mpr
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ (∃ γ, (mapGL ℝ) γ • ∞ = c ∧ IsZeroAtImInfty (f ∣[k] γ)) → c.IsZeroAt f k
Module: Mathlib.NumberTheory.ModularForms.Cusps

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

Tactic:
·

Goal state after:
case mpr.refine_2
a : SL(2, ℤ)
⊢ (mapGL ℝ) (a * ModularGroup.T * a⁻¹) • OnePoint.map Rat.cast ((mapGL ℚ) a • ∞) =
    OnePoint.map Rat.cast ((mapGL ℚ) a • ∞)
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:
·

Goal state after:
case mp
c : OnePoint ℝ
⊢ c ∈ Set.range (OnePoint.map Rat.cast) → ∃ g, c = (mapGL ℝ) g • ∞
Module: Mathlib.NumberTheory.ModularForms.Cusps

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

Tactic:
·

Goal state after:
case mpr
c : OnePoint ℝ
⊢ (∃ g, c = (mapGL ℝ) g • ∞) → c ∈ Set.range (OnePoint.map Rat.cast)
Module: Mathlib.NumberTheory.ModularForms.Cusps

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

pp: case neg
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : ¬𝒢.strictPeriods = 𝒢.periods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods = 𝒢.periods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
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
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : ¬𝒢.strictPeriods = 𝒢.periods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case neg.inl
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h✝ : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem : upperRightHom u ∈ 𝒢 ∨ -upperRightHom u ∈ 𝒢
hu_notMem : upperRightHom u ∉ 𝒢
h : upperRightHom b ∈ 𝒢
⊢ upperRightHom b * upperRightHom u ∈ 𝒢 ∨ upperRightHom b ∈ 𝒢

pp: case neg.inr
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h✝ : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem : upperRightHom u ∈ 𝒢 ∨ -upperRightHom u ∈ 𝒢
hu_notMem : upperRightHom u ∉ 𝒢
h : -upperRightHom b ∈ 𝒢
⊢ upperRightHom b * upperRightHom u ∈ 𝒢 ∨ upperRightHom b ∈ 𝒢

Tactic:
·

Goal state after:
case neg.inl
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h✝ : 𝒢.strictPeriods < 𝒢.periods
u b : R
hu_mem : upperRightHom u ∈ 𝒢 ∨ -upperRightHom u ∈ 𝒢
hu_notMem : upperRightHom u ∉ 𝒢
h : upperRightHom b ∈ 𝒢
⊢ upperRightHom b * upperRightHom u ∈ 𝒢 ∨ upperRightHom b ∈ 𝒢