awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
A : Type u_2
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
inst_6 : IsPrincipalIdealRing A
q : K
coe :
  ∀ (g : SL(2, A)) (hg0 : (↑g : Matrix (Fin 2) (Fin 2) A) 0 0 = IsFractionRing.num A q)
    (hg1 : (↑g : Matrix (Fin 2) (Fin 2) A) 1 0 = (↑(IsFractionRing.den A q) : A)),
    ∃ (g : SL(2, A)),
      HSMul.hSMul (α := GL (Fin 2) K) (β := OnePoint K) ((mapGL K : (a : SL(2, A)) → GL (Fin 2) K) g : GL (Fin 2) K) ∞ =
        (↑q : OnePoint K)
⊢ ∃ (g : SL(2, A)),
    HSMul.hSMul (α := GL (Fin 2) K) (β := OnePoint K) ((mapGL K : (a : SL(2, A)) → GL (Fin 2) K) g : GL (Fin 2) K) ∞ =
      (↑q : OnePoint K)

Tactic:
obtain ⟨g, hg0, hg1⟩ := (IsFractionRing.num_den_reduced A q).isCoprime.exists_SL2_col 0

Premises used: IsRelPrime.isCoprime, IsCoprime.exists_SL2_col, IsFractionRing.num_den_reduced, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
A : Type u_2
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
inst_6 : IsPrincipalIdealRing A
q : K
g : SL(2, A)
hg0 : (↑g : Matrix (Fin 2) (Fin 2) A) 0 0 = IsFractionRing.num A q
hg1 : (↑g : Matrix (Fin 2) (Fin 2) A) 1 0 = (↑(IsFractionRing.den A q) : A)
⊢ HSMul.hSMul (α := GL (Fin 2) K) (β := OnePoint K) ((mapGL K : (a : SL(2, A)) → GL (Fin 2) K) g : GL (Fin 2) K) ∞ =
    (↑q : OnePoint K)

Tactic:
simp [hg0, hg1, smul_infty_eq_ite]

Premises used: OnePoint.smul_infty_eq_ite
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
A : Type u_2
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
inst_6 : IsPrincipalIdealRing A
q : K
g : SL(2, A)
hg0 : (↑g : Matrix (Fin 2) (Fin 2) A) 0 0 = IsFractionRing.num A q
hg1 : (↑g : Matrix (Fin 2) (Fin 2) A) 1 0 = (↑(IsFractionRing.den A q) : A)
⊢ ∃ (g : SL(2, A)),
    HSMul.hSMul (α := GL (Fin 2) K) (β := OnePoint K) ((mapGL K : (a : SL(2, A)) → GL (Fin 2) K) g : GL (Fin 2) K) ∞ =
      (↑q : OnePoint K)

Tactic:
exact ⟨g, by simp [hg0, hg1, smul_infty_eq_ite]⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
K : Type u_1
inst : Field K
inst_1 : DecidableEq K
A : Type u_2
inst_2 : CommRing A
inst_3 : IsDomain A
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
inst_6 : IsPrincipalIdealRing A
c : OnePoint K
infty :
  ∃ (g : SL(2, A)),
    HSMul.hSMul (α := GL (Fin 2) K) (β := OnePoint K) ((mapGL K : (a : SL(2, A)) → GL (Fin 2) K) g : GL (Fin 2) K) ∞ = ∞
coe :
  ∀ (q : K),
    ∃ (g : SL(2, A)),
      HSMul.hSMul (α := GL (Fin 2) K) (β := OnePoint K) ((mapGL K : (a : SL(2, A)) → GL (Fin 2) K) g : GL (Fin 2) K) ∞ =
        (↑q : OnePoint K)
⊢ ∃ (g : SL(2, A)),
    HSMul.hSMul (α := GL (Fin 2) K) (β := OnePoint K) ((mapGL K : (a : SL(2, A)) → GL (Fin 2) K) g : GL (Fin 2) K) ∞ = c

Tactic:
cases c with
  | infty => exact ⟨1, by simp⟩
  | coe q =>
    obtain ⟨g, hg0, hg1⟩ := (IsFractionRing.num_den_reduced A q).isCoprime.exists_SL2_col 0
    exact ⟨g, by simp [hg0, hg1, smul_infty_eq_ite]⟩

Premises used: OnePoint.infty
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
𝒢 : Subgroup (GL (Fin 2) K)
inst_3 : 𝒢.HasDetPlusMinusOne
g : GL (Fin 2) K
hg : g ∈ 𝒢
hg10 : (↑g : Matrix (Fin 2) (Fin 2) K) 1 0 = 0
⊢ g.IsParabolic ↔
    (∃ (x : K), x ≠ 0 ∧ g = (upperRightHom : (a : K) → GL (Fin 2) K) x) ∨
      ∃ (x : K), x ≠ 0 ∧ g = -(upperRightHom : (a : K) → GL (Fin 2) K) x

Tactic:
isParabolic_iff_of_upperTriangular_of_det (HasDetPlusMinusOne.det_eq hg) hg10

Premises used: Matrix.GeneralLinearGroup.isParabolic_iff_of_upperTriangular_of_det, Subgroup.HasDetPlusMinusOne.det_eq
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
obtain :
  ∀ (p : GL (Fin 2) ℝ) (hp𝒢 : p ∈ 𝒢) (hpp : p.IsParabolic) (hpc : p • c = c),
    IsCusp (g • c)
      (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢)
⊢ IsCusp (g • c)
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢)

Tactic:
obtain ⟨p, hp𝒢, hpp, hpc⟩ := hc
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ IsCusp (g • c)
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢)

Tactic:
⟨_, 𝒢.smul_mem_pointwise_smul _ _ hp𝒢, ?_, ?_⟩

Premises used: IsCusp, And.intro, Exists.intro, Subgroup.smul_mem_pointwise_smul
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
refine_1 :
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) p).IsParabolic
refine_2 :
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) p •
      g • c =
    g • c
⊢ IsCusp (g • c)
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢)

Tactic:
refine ⟨_, 𝒢.smul_mem_pointwise_smul _ _ hp𝒢, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) p).IsParabolic

Tactic:
simpa [ConjAct.toConjAct_smul] using hpp

Premises used: ConjAct.toConjAct_smul
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
g p : GL (Fin 2) ℝ
hp𝒢 : p ∈ 𝒢
hpp : p.IsParabolic
hpc : p • c = c
⊢ HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) p •
      g • c =
    g • c

Tactic:
simp [ConjAct.toConjAct_smul, mul_smul, hpc]

Premises used: ConjAct.toConjAct_smul, SemigroupAction.mul_smul
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
⊢ IsCusp (g • c)
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢)

Tactic:
hc.smul g

Premises used: IsCusp.smul
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
h :
  𝒢 =
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢
⊢ IsCusp (g • c) 𝒢

Tactic:
convert! hc.smul g

Premises used: IsCusp.smul
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
h :
  ∀ (x : GL (Fin 2) ℝ),
    x ∈ 𝒢 ↔
      x ∈
        HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
          ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢
⊢ 𝒢 =
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢

Tactic:
ext x
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
x : GL (Fin 2) ℝ
h :
  x ∈ 𝒢 ↔
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        (((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g)⁻¹ : ConjAct (GL (Fin 2) ℝ)) x ∈
      𝒢
h₁ :
  x ∈ 𝒢 ↔
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) x ∈
      𝒢
h₂ : x ∈ 𝒢 ↔ g⁻¹ * x * g⁻¹⁻¹ ∈ 𝒢
h₃ : x ∈ 𝒢 ↔ g⁻¹ * x * g ∈ 𝒢
h₄ : x ∈ 𝒢 ↔ g⁻¹ * x ∈ 𝒢
h₅ h₆ : x ∈ 𝒢 ↔ x ∈ 𝒢
⊢ x ∈ 𝒢 ↔
    x ∈
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢

Tactic:
rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, ← ConjAct.toConjAct_inv,
    ConjAct.toConjAct_smul, inv_inv, Subgroup.mul_mem_cancel_right _ hg,
    Subgroup.mul_mem_cancel_left _ (inv_mem hg)]

Premises used: ConjAct.toConjAct_inv, Subgroup.mul_mem_cancel_left, ConjAct.toConjAct_smul, Subgroup.mul_mem_cancel_right, InvMemClass.inv_mem, inv_inv, Subgroup.mem_pointwise_smul_iff_inv_smul_mem
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
⊢ IsCusp c 𝒢' ↔ IsCusp c 𝒢

Tactic:
⟨fun ⟨g, hg, hgp, hgc⟩ ↦ ⟨g, h𝒢 hg, hgp, hgc⟩, fun ⟨g, hg, hgp, hgc⟩ ↦ ?_⟩

Premises used: IsCusp, And.intro, _private.0.isCusp_iff_of_relIndex_ne_zero.match_1, Iff.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
refine : IsCusp c 𝒢 → ∀ (g : GL (Fin 2) ℝ) (hg : g ∈ 𝒢) (hgp : g.IsParabolic) (hgc : g • c = c), IsCusp c 𝒢'
⊢ IsCusp c 𝒢' ↔ IsCusp c 𝒢

Tactic:
refine ⟨fun ⟨g, hg, hgp, hgc⟩ ↦ ⟨g, h𝒢 hg, hgp, hgc⟩, fun ⟨g, hg, hgp, hgc⟩ ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
h : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
obtain : ∀ (n : ℕ) (hn : 0 < n) (hgn : g ^ n ∈ 𝒢' ⊓ 𝒢), IsCusp c 𝒢'
⊢ IsCusp c 𝒢'

Tactic:
obtain ⟨n, hn, -, hgn⟩ := Subgroup.exists_pow_mem_of_relIndex_ne_zero h𝒢' hg

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

Tactic:
⟨g ^ n, (Subgroup.mem_inf.mpr hgn).1, hgp.pow hn.ne', ?_⟩

Premises used: Iff.mpr, Matrix.GeneralLinearGroup.IsParabolic.pow, IsCusp, LT.lt.ne', HPow.hPow, And.left, And.intro, Exists.intro, Subgroup.mem_inf
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
h : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : 0 < n
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
refine : g ^ n • c = c
⊢ IsCusp c 𝒢'

Tactic:
refine ⟨g ^ n, (Subgroup.mem_inf.mpr hgn).1, hgp.pow hn.ne', ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
h : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : 0 < n
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ n ≠ 0

Tactic:
rw [Nat.pos_iff_ne_zero] at hn

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
h : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : 0 < n
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
hn₁ : n ≠ 0
⊢ g ^ n ∈ 𝒢' ⊓ 𝒢

Tactic:
rw [Nat.pos_iff_ne_zero] at hn

Premises used: Nat.pos_iff_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
h : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : n ≠ 0
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
rwa : c = (g ^ n).parabolicFixedPoint
rwa₁ : c = g.parabolicFixedPoint
rwa₂ rwa₃ rwa₄ rwa₅ : g • c = c
⊢ g ^ n • c = c

Tactic:
rwa [(hgp.pow hn).smul_eq_self_iff, hgp.parabolicFixedPoint_pow hn, ← hgp.smul_eq_self_iff]

Premises used: Matrix.GeneralLinearGroup.IsParabolic.parabolicFixedPoint_pow, Matrix.GeneralLinearGroup.IsParabolic.pow, Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
h𝒢' : (𝒢 ⊓ 𝒢').relIndex 𝒢' ≠ 0
h𝒢'₁ : (𝒢 ⊓ 𝒢').relIndex 𝒢 ≠ 0
⊢ IsCusp c 𝒢 ↔ IsCusp c 𝒢'

Tactic:
rw [← isCusp_iff_of_relIndex_ne_zero inf_le_left, isCusp_iff_of_relIndex_ne_zero inf_le_right]

Premises used: inf_le_right, isCusp_iff_of_relIndex_ne_zero, inf_le_left
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢' ≠ 0

Tactic:
simpa [Subgroup.inf_relIndex_right] using h𝒢.1

Premises used: Subgroup.inf_relIndex_right, And.left
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢.Commensurable 𝒢'
c : OnePoint ℝ
⊢ (𝒢 ⊓ 𝒢').relIndex 𝒢 ≠ 0

Tactic:
simpa [Subgroup.inf_relIndex_left] using h𝒢.2

Premises used: Subgroup.inf_relIndex_left, And.right
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
hGH : 𝒢 ≤ ℋ
hc : IsCusp c 𝒢
⊢ IsCusp c ℋ

Tactic:
match hc with | ⟨h, hh, hp, hc⟩ => ⟨h, hGH hh, hp, hc⟩

Premises used: IsCusp, And.intro, _private.0.isCusp_iff_of_relIndex_ne_zero.match_1, Exists.intro
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
⊢ 𝒢.relIndex ℋ ≠ 0

Tactic:
have hGH : 𝒢.relIndex ℋ ≠ 0 := 𝒢.relIndex_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
hGH : 𝒢.relIndex ℋ ≠ 0
⊢ (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0

Tactic:
rw [← Subgroup.inf_relIndex_right] at hGH

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

Tactic:
rw [← isCusp_iff_of_relIndex_ne_zero inf_le_right hGH] at hc

Premises used: inf_le_right, isCusp_iff_of_relIndex_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
hGH : (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0
hc₁ : IsCusp c (𝒢 ⊓ ℋ)
⊢ (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0

Tactic:
rw [← isCusp_iff_of_relIndex_ne_zero inf_le_right hGH] at hc

Premises used: inf_le_right, isCusp_iff_of_relIndex_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c (𝒢 ⊓ ℋ)
hGH : (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0
⊢ IsCusp c 𝒢

Tactic:
hc.mono inf_le_left

Premises used: IsCusp.mono, inf_le_left
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c (𝒢 ⊓ ℋ)
hGH : (𝒢 ⊓ ℋ).relIndex ℋ ≠ 0
⊢ IsCusp c 𝒢

Tactic:
exact hc.mono inf_le_left

Premises used: IsCusp.mono, inf_le_left
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
suffices :
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) h : ConjAct (GL (Fin 2) ℝ))
        𝒢).IsFiniteRelIndex
    ℋ
⊢ IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) h : ConjAct (GL (Fin 2) ℝ)) 𝒢)

Tactic:
suffices (ConjAct.toConjAct h • 𝒢).IsFiniteRelIndex ℋ from hc.of_isFiniteRelIndex
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
relIndex_ne_zero :
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
          ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) h : ConjAct (GL (Fin 2) ℝ)) 𝒢).relIndex
      ℋ ≠
    0
⊢ (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) h : ConjAct (GL (Fin 2) ℝ))
        𝒢).IsFiniteRelIndex
    ℋ

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
relIndex_ne_zero : 𝒢.relIndex ℋ ≠ 0
⊢ (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
          ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) h : ConjAct (GL (Fin 2) ℝ)) 𝒢).relIndex
      ℋ ≠
    0

Tactic:
rw [← ℋ.conjAct_pointwise_smul_eq_self (ℋ.le_normalizer hh), 𝒢.relIndex_pointwise_smul]

Premises used: Subgroup.le_normalizer, Subgroup.conjAct_pointwise_smul_eq_self, Subgroup.relIndex_pointwise_smul
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ 𝒢.relIndex ℋ ≠ 0

Tactic:
𝒢.relIndex_ne_zero

Premises used: Subgroup.relIndex_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
c : OnePoint ℝ
inst : 𝒢.IsFiniteRelIndex ℋ
hc : IsCusp c ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
⊢ 𝒢.relIndex ℋ ≠ 0

Tactic:
exact 𝒢.relIndex_ne_zero

Premises used: Subgroup.relIndex_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
mp :
  IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) →
    Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c
mpr :
  Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c →
    IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ)) ↔
    Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
g : SL(2, ℤ)
hgp : GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g)
hgc : HSMul.hSMul (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) c = c
⊢ Eq (α := OnePoint ℝ) (OnePoint.map Rat.cast (parabolicFixedPoint ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) g)))
    (parabolicFixedPoint ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g))

Tactic:
simp [GeneralLinearGroup.parabolicFixedPoint, apply_ite]

Premises used: apply_ite, Matrix.GeneralLinearGroup.parabolicFixedPoint
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℝ
g : SL(2, ℤ)
hgp : GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g)
hgc : HSMul.hSMul (α := GL (Fin 2) ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g : GL (Fin 2) ℝ) c = c
⊢ Membership.mem (γ := Set (OnePoint ℝ)) (Set.range (OnePoint.map Rat.cast)) c

Tactic:
simpa only [hgp.smul_eq_self_iff.mp hgc] using ⟨(mapGL ℚ g).parabolicFixedPoint,
      by simp [GeneralLinearGroup.parabolicFixedPoint, apply_ite]⟩

Premises used: Iff.mp, Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
c : OnePoint ℚ
mpr :
  ∀ (a : SL(2, ℤ)),
    IsCusp
      (OnePoint.map Rat.cast
        (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ)
          ∞))
      (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))
⊢ IsCusp (OnePoint.map Rat.cast c) (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))

Tactic:
obtain ⟨a, rfl⟩ := c.exists_mem_SL2 ℤ

Premises used: Int, OnePoint.exists_mem_SL2, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
a : SL(2, ℤ)
⊢ IsCusp
    (OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ)
        ∞))
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))

Tactic:
⟨_, ⟨a * ModularGroup.T * a⁻¹, rfl⟩, ?_, ?_⟩

Premises used: HMul.hMul, ModularGroup.T, IsCusp, Inv.inv, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
a : SL(2, ℤ)
mpr : GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (a * ModularGroup.T * a⁻¹))
mpr₁ :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (a * ModularGroup.T * a⁻¹) : GL (Fin 2) ℝ)
      (OnePoint.map Rat.cast
        (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ)
          ∞)) =
    OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ) ∞)
⊢ IsCusp
    (OnePoint.map Rat.cast
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ)
        ∞))
    (MonoidHom.range (G := SL(2, ℤ)) (mapGL ℝ))

Tactic:
refine ⟨_, ⟨a * ModularGroup.T * a⁻¹, rfl⟩, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
a : SL(2, ℤ)
this : GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) ModularGroup.T)
⊢ GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (a * ModularGroup.T * a⁻¹))

Tactic:
simpa
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
a : SL(2, ℤ)
mpr : GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) ModularGroup.T)
⊢ GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (a * ModularGroup.T * a⁻¹))

Tactic:
suffices (mapGL ℝ ModularGroup.T).IsParabolic by simpa
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
a_1 : SL(2, ℤ)
h :
  Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) ℝ))
    (Set.range (ι := ℝ) (⇑(Matrix.scalar (Fin 2)) : (a : ℝ) → Matrix (Fin 2) (Fin 2) ℝ))
    (↑((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) ModularGroup.T) : Matrix (Fin 2) (Fin 2) ℝ)
a : ℝ
ha :
  Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
    ((Matrix.scalar (Fin 2) : (a : ℝ) → Matrix (Fin 2) (Fin 2) ℝ) a : Matrix (Fin 2) (Fin 2) ℝ)
    ((↑((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) ModularGroup.T) : Matrix (Fin 2) (Fin 2) ℝ) :
      Matrix (Fin 2) (Fin 2) ℝ)
⊢ Eq (α := ℝ) 0 1

Tactic:
simpa [ModularGroup.T] using congr_fun₂ ha 0 1

Premises used: ModularGroup.T, congr_fun₂, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
a : SL(2, ℤ)
mpr :
  Eq (α := ℝ)
    (Matrix.discr (n := Fin 2) (↑((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) ModularGroup.T) : Matrix (Fin 2) (Fin 2) ℝ))
    0
⊢ GeneralLinearGroup.IsParabolic (R := ℝ) ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) ModularGroup.T)

Tactic:
refine ⟨fun ⟨a, ha⟩ ↦ zero_ne_one' ℝ (by simpa [ModularGroup.T] using congr_fun₂ ha 0 1), ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
a : SL(2, ℤ)
mpr : HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) 1 1) 2 - 4 = 0
⊢ Eq (α := ℝ)
    (Matrix.discr (n := Fin 2) (↑((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) ModularGroup.T) : Matrix (Fin 2) (Fin 2) ℝ))
    0

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

Premises used: ModularGroup.T, Matrix.trace_fin_two, Matrix.det_fin_two, Matrix.discr_fin_two
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
a : SL(2, ℤ)
⊢ HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℝ) 1 1) 2 - 4 = 0

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.Cusps
Goal:
a : SL(2, ℤ)
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) (a * ModularGroup.T * a⁻¹) : GL (Fin 2) ℝ)
      (OnePoint.map (⇑(algebraMap ℚ ℝ) : (a : ℚ) → ℝ)
        (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ)
          ∞)) =
    OnePoint.map (⇑(algebraMap ℚ ℝ) : (a : ℚ) → ℝ)
      (HSMul.hSMul (α := GL (Fin 2) ℚ) (β := OnePoint ℚ) ((mapGL ℚ : (a : SL(2, ℤ)) → GL (Fin 2) ℚ) a : GL (Fin 2) ℚ) ∞)

Tactic:
simp [OnePoint.map_smul, mul_smul, smul_infty_eq_self_iff, ModularGroup.T]

Premises used: OnePoint.smul_infty_eq_self_iff, OnePoint.map_smul, ModularGroup.T, SemigroupAction.mul_smul