awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)

Tactic:
simp [ModularGroup.coe_T_zpow]

Premises used: ModularGroup.coe_T_zpow
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)

Tactic:
simp [ModularGroup.coe_T_zpow]

Premises used: ModularGroup.coe_T_zpow
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
m : ℤ
⊢ Eq (α := ℝ)
    ((RingHom.mapMatrix (algebraMap ℤ ℝ) : (a : Matrix (Fin 2) (Fin 2) ℤ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(ModularGroup.T ^ m) : Matrix (Fin 2) (Fin 2) ℤ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) ((fun (x : ℤ) ↦ HSMul.hSMul (β := ℝ) x 1) m)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)

Tactic:
simp [ModularGroup.coe_T_zpow]

Premises used: ModularGroup.coe_T_zpow
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
⊢ strictPeriods (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) = AddSubgroup.zmultiples 1

Tactic:
simpa [MonoidHom.range_eq_map] using strictPeriods_eq_zmultiples_one_of_T_mem (mem_top _)

Premises used: MonoidHom.range_eq_map, Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem, Subgroup.mem_top
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ LE.le (α := ℝ) 0
    (if h : DiscreteTopology ↥𝒢.strictPeriods then
      |⋯.choose (p := fun (a : ℝ) ↦ AddSubgroup.zmultiples a = 𝒢.strictPeriods)|
    else 0)

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ 0 ≤ 𝒢.widthInfty

Tactic:
𝒢.adjoinNegOne.strictWidthInfty_nonneg

Premises used: Subgroup.adjoinNegOne, Subgroup.strictWidthInfty_nonneg, Subgroup.widthInfty
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
⊢ 𝒢.strictPeriods = AddSubgroup.zmultiples 𝒢.strictWidthInfty

Tactic:
simp [Subgroup.strictWidthInfty, dif_pos,
    Exists.choose_spec <| 𝒢.strictPeriods.isAddCyclic_iff_exists_zmultiples_eq_top.mp
      <| AddSubgroup.discrete_iff_addCyclic.mpr inferInstance]

Premises used: Iff.mpr, Exists.choose_spec, inferInstance, dif_pos, AddSubgroup.discrete_iff_addCyclic, Subgroup.strictPeriods, AddSubgroup.isAddCyclic_iff_exists_zmultiples_eq_top, Iff.mp, Subgroup.strictWidthInfty
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
⊢ strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1

Tactic:
have hsp := strictPeriods_eq_zmultiples_one_of_T_mem hΓ
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1
rw : DiscreteTopology ↥(AddSubgroup.zmultiples 1)
⊢ DiscreteTopology ↥(strictPeriods (map (mapGL ℝ) Γ))

Tactic:
rw [hsp]
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1
⊢ DiscreteTopology ↥(AddSubgroup.zmultiples 1)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1
⊢ DiscreteTopology ↥(strictPeriods (map (mapGL ℝ) Γ))

Tactic:
have : DiscreteTopology (Γ : Subgroup (GL (Fin 2) ℝ)).strictPeriods := by
    -- In fact the image of `Γ` in `GL (Fin 2) ℝ` is itself discrete, but this is quicker:
    rw [hsp]
    infer_instance
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1
this : DiscreteTopology ↥(strictPeriods (map (mapGL ℝ) Γ))
⊢ 1 = strictWidthInfty (map (mapGL ℝ) Γ) ∨ -1 = strictWidthInfty (map (mapGL ℝ) Γ)

Tactic:
rw [strictPeriods_eq_zmultiples_strictWidthInfty, Eq.comm,
    AddSubgroup.zmultiples_eq_zmultiples_iff (not_isOfFinAddOrder_of_isAddTorsionFree one_ne_zero)]
    at hsp

Premises used: not_isOfFinAddOrder_of_isAddTorsionFree, Eq.comm, one_ne_zero, Subgroup.strictPeriods_eq_zmultiples_strictWidthInfty, AddSubgroup.zmultiples_eq_zmultiples_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : strictPeriods (map (mapGL ℝ) Γ) = AddSubgroup.zmultiples 1
this : DiscreteTopology ↥(strictPeriods (map (mapGL ℝ) Γ))
hsp₁ : 1 = strictWidthInfty (map (mapGL ℝ) Γ) ∨ -1 = strictWidthInfty (map (mapGL ℝ) Γ)
⊢ DiscreteTopology ↥(strictPeriods (map (mapGL ℝ) Γ))

Tactic:
rw [strictPeriods_eq_zmultiples_strictWidthInfty, Eq.comm,
    AddSubgroup.zmultiples_eq_zmultiples_iff (not_isOfFinAddOrder_of_isAddTorsionFree one_ne_zero)]
    at hsp

Premises used: not_isOfFinAddOrder_of_isAddTorsionFree, Eq.comm, one_ne_zero, Subgroup.strictPeriods_eq_zmultiples_strictWidthInfty, AddSubgroup.zmultiples_eq_zmultiples_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
hsp : 1 = strictWidthInfty (map (mapGL ℝ) Γ) ∨ -1 = strictWidthInfty (map (mapGL ℝ) Γ)
this : DiscreteTopology ↥(strictPeriods (map (mapGL ℝ) Γ))
⊢ strictWidthInfty (map (mapGL ℝ) Γ) = 1

Tactic:
grind [strictWidthInfty_nonneg]

Premises used: Subgroup.strictWidthInfty_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
⊢ strictWidthInfty (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) = 1

Tactic:
simpa [MonoidHom.range_eq_map] using strictWidthInfty_eq_one_of_T_mem (mem_top _)

Premises used: MonoidHom.range_eq_map, Subgroup.strictWidthInfty_eq_one_of_T_mem, Subgroup.mem_top
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
pos : ∀ (h : DiscreteTopology ↥𝒢.strictPeriods), 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods
neg : ∀ (h : ¬DiscreteTopology ↥𝒢.strictPeriods), 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods
⊢ 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods

Tactic:
by_cases h : DiscreteTopology 𝒢.strictPeriods

Premises used: DiscreteTopology, Membership.mem, Subtype, Subgroup.strictPeriods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : DiscreteTopology ↥𝒢.strictPeriods
⊢ 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods

Tactic:
simp [strictPeriods_eq_zmultiples_strictWidthInfty]

Premises used: Subgroup.strictPeriods_eq_zmultiples_strictWidthInfty
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : ¬DiscreteTopology ↥𝒢.strictPeriods
⊢ 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods

Tactic:
simp [strictWidthInfty, dif_neg h]

Premises used: dif_neg, Subgroup.strictWidthInfty
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.periods
⊢ 𝒢.periods = AddSubgroup.zmultiples 𝒢.widthInfty

Tactic:
have : DiscreteTopology 𝒢.adjoinNegOne.strictPeriods := ‹_›
  𝒢.adjoinNegOne.strictPeriods_eq_zmultiples_strictWidthInfty

Premises used: Subgroup.widthInfty, Subgroup.strictPeriods_eq_zmultiples_strictWidthInfty, Subgroup.periods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ 𝒢.widthInfty ∈ 𝒢.periods

Tactic:
𝒢.adjoinNegOne.strictWidthInfty_mem_strictPeriods

Premises used: Set.Mem, Subgroup.adjoinNegOne, Subgroup.strictWidthInfty_mem_strictPeriods, Subgroup.widthInfty
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
⊢ 𝒢.widthInfty ∈ 𝒢.periods

Tactic:
have := 𝒢.widthInfty_mem_periods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
this : 𝒢.widthInfty ∈ 𝒢.periods
⊢ Membership.mem (α := GL (Fin 2) ℝ) 𝒢.adjoinNegOne
    ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)

Tactic:
simp only [Subgroup.periods, mem_strictPeriods_iff] at this

Premises used: Subgroup.mem_strictPeriods_iff, Subgroup.periods
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
this :
  Membership.mem (α := GL (Fin 2) ℝ) 𝒢.adjoinNegOne
    ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)
inl :
  ∀ (h : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)),
    2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
inr :
  ∀ (h : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 (-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)),
    2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
rcases this with (h | h)
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
simpa [-upperRightHom_apply, ← AddChar.map_nsmul_eq_pow] using Subgroup.pow_mem _ h 2

Premises used: AddChar.map_nsmul_eq_pow, Matrix.GeneralLinearGroup.upperRightHom_apply, Subgroup.pow_mem, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 (-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) 𝒢.widthInfty : GL (Fin 2) ℝ)
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
simpa [-upperRightHom_apply, ← AddChar.map_nsmul_eq_pow] using Subgroup.pow_mem _ h 2

Premises used: AddChar.map_nsmul_eq_pow, Matrix.GeneralLinearGroup.upperRightHom_apply, Subgroup.pow_mem, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
mp : 0 < 𝒢.strictWidthInfty → IsCusp ∞ 𝒢
mpr : IsCusp ∞ 𝒢 → 0 < 𝒢.strictWidthInfty
⊢ 0 < 𝒢.strictWidthInfty ↔ IsCusp ∞ 𝒢

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
⊢ 0 < 𝒢.strictWidthInfty → IsCusp ∞ 𝒢

Tactic:
fun h ↦ ⟨_, mem_strictPeriods_iff.mpr 𝒢.strictWidthInfty_mem_strictPeriods, ?_, ?_⟩

Premises used: Iff.mpr, AddChar.toAddMonoidHom, Additive.toMul, IsCusp, Subgroup.strictWidthInfty_mem_strictPeriods, And.intro, Matrix.GeneralLinearGroup.upperRightHom, Exists.intro, Subgroup.mem_strictPeriods_iff, DFunLike.coe, Subgroup.strictWidthInfty
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
mp :
  ∀ (h : 0 < 𝒢.strictWidthInfty),
    GeneralLinearGroup.IsParabolic (R := ℝ)
      ((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
        ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty))
mp₁ :
  ∀ (h : 0 < 𝒢.strictWidthInfty),
    HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
            ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty) :
          GL (Fin 2) ℝ)
        ∞ =
      ∞
⊢ 0 < 𝒢.strictWidthInfty → IsCusp ∞ 𝒢

Tactic:
refine fun h ↦ ⟨_, mem_strictPeriods_iff.mpr 𝒢.strictWidthInfty_mem_strictPeriods, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ Eq (α := ℝ)
    ((↑((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
            ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty)) :
        Matrix (Fin 2) (Fin 2) ℝ)
      1 0)
    0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
mp :
  Eq (α := ℝ)
      ((↑((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
              ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        0 0)
      ((↑((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
              ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        1 1) ∧
    Ne (α := ℝ)
      ((↑((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
              ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        0 1)
      0
⊢ GeneralLinearGroup.IsParabolic (R := ℝ)
    ((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
      ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty))

Tactic:
rw [GeneralLinearGroup.isParabolic_iff_of_upperTriangular (by simp)]

Premises used: Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ Eq (α := ℝ)
      ((↑((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
              ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        0 0)
      ((↑((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
              ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        1 1) ∧
    Ne (α := ℝ)
      ((↑((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
              ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty)) :
          Matrix (Fin 2) (Fin 2) ℝ)
        0 1)
      0

Tactic:
simpa using h.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
h : 0 < 𝒢.strictWidthInfty
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Additive.toMul : (a : Additive (GL (Fin 2) ℝ)) → GL (Fin 2) ℝ)
          ((AddChar.toAddMonoidHom upperRightHom : (a : ℝ) → Additive (GL (Fin 2) ℝ)) 𝒢.strictWidthInfty) :
        GL (Fin 2) ℝ)
      ∞ =
    ∞

Tactic:
simp [smul_infty_eq_self_iff]

Premises used: OnePoint.smul_infty_eq_self_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : HSMul.hSMul (β := OnePoint ℝ) g ∞ = ∞
mpr : 𝒢.strictWidthInfty ≠ 0
⊢ 0 < 𝒢.strictWidthInfty

Tactic:
apply 𝒢.strictWidthInfty_nonneg.lt_of_ne'

Premises used: Subgroup.strictWidthInfty_nonneg, LE.le.lt_of_ne'
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : HSMul.hSMul (β := OnePoint ℝ) g ∞ = ∞
mpr : Ne (α := AddSubgroup ℝ) (AddSubgroup.zmultiples 𝒢.strictWidthInfty) ⊥
⊢ 𝒢.strictWidthInfty ≠ 0

Tactic:
rw [← AddSubgroup.zmultiples_ne_bot]

Premises used: AddSubgroup.zmultiples_ne_bot
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : HSMul.hSMul (β := OnePoint ℝ) g ∞ = ∞
mpr :
  ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)
⊢ Ne (α := AddSubgroup ℝ) (AddSubgroup.zmultiples 𝒢.strictWidthInfty) ⊥

Tactic:
simp only [AddSubgroup.ne_bot_iff_exists_ne_zero, Subtype.exists, Ne, AddSubgroup.mk_eq_zero,
      exists_prop, and_comm, ← strictPeriods_eq_zmultiples_strictWidthInfty, mem_strictPeriods_iff]

Premises used: AddSubgroup.ne_bot_iff_exists_ne_zero, Subtype.exists, Ne, and_comm, exists_prop, AddSubgroup.mk_eq_zero, Subgroup.mem_strictPeriods_iff, Subgroup.strictPeriods_eq_zmultiples_strictWidthInfty
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : HSMul.hSMul (β := OnePoint ℝ) g ∞ = ∞
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0

Tactic:
rw [smul_infty_eq_self_iff] at hgi

Premises used: OnePoint.smul_infty_eq_self_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ (∃ (x : ℝ), x ≠ 0 ∧ g = (upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) ∨
    ∃ (x : ℝ), x ≠ 0 ∧ g = -(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x

Tactic:
rw [Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular hgg hgi] at hgp

Premises used: Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp : g.IsParabolic
hgi : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hgp₁ :
  (∃ (x : ℝ), x ≠ 0 ∧ g = (upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) ∨
    ∃ (x : ℝ), x ≠ 0 ∧ g = -(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0

Tactic:
rw [Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular hgg hgi] at hgp

Premises used: Subgroup.HasDetPlusMinusOne.isParabolic_iff_of_upperTriangular
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) ℝ
hgg : g ∈ 𝒢
hgp :
  (∃ (x : ℝ), x ≠ 0 ∧ g = (upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) ∨
    ∃ (x : ℝ), x ≠ 0 ∧ g = -(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x
hgi : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
mpr :
  ∀ (x : ℝ) (hx : x ≠ 0)
    (hgg : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ))
    (hgi : Eq (α := ℝ) ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 0),
    ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)
mpr₁ :
  ∀ (x : ℝ) (hx : x ≠ 0)
    (hgg : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 (-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ))
    (hgi : Eq (α := ℝ) ((↑(-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 0),
    ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)
⊢ ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)

Tactic:
rcases hgp with ⟨x, hx, rfl⟩ | ⟨x, hx, rfl⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
x : ℝ
hx : x ≠ 0
hgg : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
hgi : Eq (α := ℝ) ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 0
⊢ ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)

Tactic:
⟨x, hx, hgg⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
x : ℝ
hx : x ≠ 0
hgg : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
hgi : Eq (α := ℝ) ((↑((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 0
⊢ ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)

Tactic:
exact ⟨x, hx, hgg⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
x : ℝ
hx : x ≠ 0
hgg : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 (-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
hgi : Eq (α := ℝ) ((↑(-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 0
⊢ ¬HSMul.hSMul (α := ℕ) 2 x = 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
x : ℝ
hx : x ≠ 0
hgg : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 (-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
hgi : Eq (α := ℝ) ((↑(-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 0
⊢ Membership.mem (α := GL (Fin 2) ℝ) 𝒢
    ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) (HSMul.hSMul (α := ℕ) 2 x) : GL (Fin 2) ℝ)

Tactic:
simpa only [AddChar.map_nsmul_eq_pow, neg_sq] using pow_mem hgg 2

Premises used: AddChar.map_nsmul_eq_pow, neg_sq, pow_mem, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : DiscreteTopology ↥𝒢.strictPeriods
inst_1 : 𝒢.HasDetPlusMinusOne
x : ℝ
hx : x ≠ 0
hgg : Membership.mem (α := GL (Fin 2) ℝ) 𝒢 (-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)
hgi : Eq (α := ℝ) ((↑(-(upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) x) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 0
⊢ ∃ (a : ℝ), ¬a = 0 ∧ Membership.mem (α := GL (Fin 2) ℝ) 𝒢 ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) a : GL (Fin 2) ℝ)

Tactic:
exact ⟨2 • x, by grind,
        by simpa only [AddChar.map_nsmul_eq_pow, neg_sq] using pow_mem hgg 2⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
rw : IsCusp ∞ 𝒢
⊢ 0 < 𝒢.strictWidthInfty

Tactic:
rw [strictWidthInfty_pos_iff]

Premises used: Subgroup.strictWidthInfty_pos_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
⊢ IsCusp ∞ 𝒢

Tactic:
simpa [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff]
    using ⟨_, OnePoint.map_infty _⟩

Premises used: Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
h𝒢 : h ∈ 𝒢.strictPeriods
⊢ IsCusp ∞ 𝒢

Tactic:
⟨upperRightHom h, 𝒢.mem_strictPeriods_iff.mp h𝒢, ?_, smul_infty_eq_self_iff.mpr rfl⟩

Premises used: Iff.mpr, OnePoint.smul_infty_eq_self_iff, IsCusp, And.intro, Matrix.GeneralLinearGroup.upperRightHom, Exists.intro, Iff.mp, Subgroup.mem_strictPeriods_iff, DFunLike.coe, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
h𝒢 : h ∈ 𝒢.strictPeriods
refine : GeneralLinearGroup.IsParabolic (R := ℝ) ((upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h)
⊢ IsCusp ∞ 𝒢

Tactic:
refine ⟨upperRightHom h, 𝒢.mem_strictPeriods_iff.mp h𝒢, ?_, smul_infty_eq_self_iff.mpr rfl⟩