awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
g : GL (Fin 2) ℚ
⊢ (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
          ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
            ConjAct (GL (Fin 2) ℝ))
          (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)).relIndex
      (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤) ≠
    0
have is_commensurable : Subgroup.index (G := SL(2, ℤ))
    (Subgroup.comap (mapGL ℝ)
      (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤))) ≠
  0
Tactic: rw [← Subgroup.relIndex_comap, Subgroup.relIndex_top_right]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
g : GL (Fin 2) ℚ
⊢ Subgroup.relIndex (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)
      (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤)) ≠
    0
have is_commensurable : Subgroup.index (G := SL(2, ℤ))
    (Subgroup.comap (mapGL ℝ)
      (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
        (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
              ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
          ConjAct (GL (Fin 2) ℝ))
        (Subgroup.map (G := SL(2, ℤ)) (mapGL ℝ) ⊤))) ≠
  0
Tactic: rw [← Subgroup.relIndex_pointwise_smul (toConjAct (g.map (Rat.castHom ℝ)))⁻¹,
      inv_smul_smul, ← Subgroup.relIndex_comap, Subgroup.relIndex_top_right]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
hΓ : IsCongruenceSubgroup Γ
g : GL (Fin 2) ℚ
⊢ IsCongruenceSubgroup
    (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))
have obtain : ∀ (M : ℕ) (hN : M ≠ 0) (hΓM : Γ(M) ≤ Γ),
  IsCongruenceSubgroup
    (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))
Tactic: obtain ⟨M, hN, hΓM⟩ := hΓ
Cleared hypotheses: hΓ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN : M ≠ 0
hΓM : Γ(M) ≤ Γ
⊢ IsCongruenceSubgroup
    (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))
have x : NeZero M
Tactic: haveI _ : NeZero M := ⟨hN⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN : M ≠ 0
hΓM : Γ(M) ≤ Γ
h : NeZero M
⊢ IsCongruenceSubgroup
    (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))
have obtain : ∀ (N : ℕ) (hN : N ≠ 0)
  (hN' :
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        (Subgroup.map (mapGL ℝ) Γ(N)) ≤
      Subgroup.map (mapGL ℝ) Γ(M)),
  IsCongruenceSubgroup
    (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))
Tactic: obtain ⟨N, hN, hN'⟩ := exists_Gamma_le_conj' g M
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (hypothesis)
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN_1 : M ≠ 0
hΓM : Γ(M) ≤ Γ
h : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(N)) ≤
    Subgroup.map (mapGL ℝ) Γ(M)
⊢ IsCongruenceSubgroup
    (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))
have hN'₁ : Subgroup.map (mapGL ℝ) Γ(N) ≤
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
    (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
          ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
      ConjAct (GL (Fin 2) ℝ))
    (Subgroup.map (mapGL ℝ) Γ(M))
Tactic: rw [Subgroup.pointwise_smul_subset_iff] at hN'
Cleared hypotheses: hN'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN_1 : M ≠ 0
hΓM : Γ(M) ≤ Γ
h : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(M))
⊢ IsCongruenceSubgroup
    (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))
have refine : ∀ (x : SL(2, ℤ)) (hx : x ∈ Γ(N)),
  x ∈ CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)
Tactic: refine ⟨N, ‹_›, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CongruenceSubgroups (goal)
Goal:
Γ : Subgroup SL(2, ℤ)
g : GL (Fin 2) ℚ
M : ℕ
hN_1 : M ≠ 0
hΓM : Γ(M) ≤ Γ
h : NeZero M
N : ℕ
hN : N ≠ 0
hN' :
  Subgroup.map (mapGL ℝ) Γ(N) ≤
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := Subgroup (GL (Fin 2) ℝ))
      (((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g))⁻¹ :
        ConjAct (GL (Fin 2) ℝ))
      (Subgroup.map (mapGL ℝ) Γ(M))
x : SL(2, ℤ)
hx : x ∈ Γ(N)
⊢ x ∈ CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)
have obtain : ∀ (y : SL(2, ℤ)) (hy : y ∈ (↑Γ(M) : Set SL(2, ℤ)))
  (hy' :
    (mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) y =
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ)) (β := GL (Fin 2) ℝ)
        ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g) :
          ConjAct (GL (Fin 2) ℝ))
        ((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) x : GL (Fin 2) ℝ)),
  x ∈ CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ) : (a : GL (Fin 2) ℚ) → GL (Fin 2) ℝ) g)
Tactic: obtain ⟨y, hy, hy'⟩ := Subgroup.mem_inv_pointwise_smul_iff.mp <| hN' ⟨x, hx, rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CuspFormSubmodule (hypothesis)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
⊢ IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
have hh : 0 < Γ.strictWidthInfty
Tactic: have hh : 0 < Γ.strictWidthInfty := Γ.strictWidthInfty_pos_iff.mpr Fact.out
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CuspFormSubmodule (hypothesis)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
hh : 0 < Γ.strictWidthInfty
⊢ IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
have hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
Tactic: have hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CuspFormSubmodule (hypothesis)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
⊢ IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
have hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) 0
Tactic: have hanal := ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CuspFormSubmodule (hypothesis)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) 0
⊢ IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
have hper : Function.Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑Γ.strictWidthInfty : ℂ)
Tactic: have hper := periodic_comp_ofComplex f hΓ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CuspFormSubmodule (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : DiscreteTopology ↥Γ
inst_2 : Γ.HasDetPlusMinusOne
inst_3 : Fact (IsCusp ∞ Γ)
inst_4 : ModularFormClass F Γ k
f : F
h : valueAtInfty (⇑f : (a : ℍ) → ℂ) = 0
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
hanal : AnalyticAt ℂ (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ)) 0
hper : Function.Periodic (β := ℂ) ((⇑f : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑Γ.strictWidthInfty : ℂ)
⊢ IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
have simp_rw : Tendsto (⇑f : (a : ℍ) → ℂ) atImInfty (𝓝 (cuspFunction Γ.strictWidthInfty (⇑f : (a : ℍ) → ℂ) 0))
Tactic: simp_rw [IsZeroAtImInfty, ZeroAtFilter, ← h, ← cuspFunction_apply_zero hh hanal hper]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CuspFormSubmodule (goal)
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
⊢ c.IsZeroAt (⇑f : (a : ℍ) → ℂ) k
have rw : ∀ (γ : SL(2, ℤ)),
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
      c →
    IsZeroAtImInfty (α := ℂ)
      (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
        (⇑f : (a : ℍ) → ℂ))
Tactic: rw [isZeroAt_iff_forall_SL2Z hc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CuspFormSubmodule (goal)
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h_1 :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
    c
⊢ IsZeroAtImInfty (α := ℂ)
    (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (⇑f : (a : ℍ) → ℂ))
have rw : IsZeroAtImInfty (α := ℂ) (⇑f : (a : ℍ) → ℂ)
Tactic: rw [show (⇑f ∣[k] γ) = ⇑f from f.slash_action_eq' _ ⟨γ, rfl⟩]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CuspFormSubmodule (goal)
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
⊢ f.IsCuspForm ↔
    Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
have refine : f.IsCuspForm →
  ∀ (g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k)
    (hg :
      (CuspForm.toModularFormₗ :
            (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
              ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
          g =
        f),
    Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
Tactic: refine ⟨fun ⟨g, hg⟩ ↦ ?_, fun h ↦ (isCuspForm_iff f).mpr (isZeroAt_of_coeffZero_eq_zero f h)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.CuspFormSubmodule (goal)
Goal:
k : ℤ
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
h : f.IsCuspForm
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
      g =
    f
⊢ Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
have rw : valueAtInfty
    (⇑((CuspForm.toModularFormₗ :
              (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) →
                ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)
            g :
          ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) :
      (a : ℍ) → ℂ) =
  0
Tactic: rw [← hg, qExpansion_coeff_zero one_pos
    (ModularFormClass.analyticAt_cuspFunction_zero _ one_pos one_mem_strictPeriods_SL)
    (periodic_comp_ofComplex _ one_mem_strictPeriods_SL)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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)),
    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)
have 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)
Tactic: obtain ⟨g, hg0, hg1⟩ := (IsFractionRing.num_den_reduced A q).isCoprime.exists_SL2_col 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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
⊢ ∃ (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
have 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) ∞ = ∞
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]⟩
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ∞ = ∞
⊢ ∃ (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
have 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)
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]⟩
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : 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) ℝ)) 𝒢)
have 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) ℝ)) 𝒢)
Tactic: obtain ⟨p, hp𝒢, hpp, hpc⟩ := hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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) ℝ)) 𝒢)
have 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
Tactic: refine ⟨_, 𝒢.smul_mem_pointwise_smul _ _ hp𝒢, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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
⊢ IsCusp (g • c)
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢)
have 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
Tactic: refine ⟨_, 𝒢.smul_mem_pointwise_smul _ _ hp𝒢, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
⊢ IsCusp (g • c) 𝒢
have h : 𝒢 =
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
    ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢
Tactic: convert! hc.smul g
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
⊢ 𝒢 =
    HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢
have 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) ℝ)) 𝒢
Tactic: ext x
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
Goal:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
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) ℝ)) 𝒢
have h : x ∈ 𝒢 ↔
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      (((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g)⁻¹ : ConjAct (GL (Fin 2) ℝ)) x ∈
    𝒢
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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 ∈
      𝒢
⊢ x ∈ 𝒢 ↔
    x ∈
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢
have h₁ : x ∈ 𝒢 ↔
  HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) x ∈
    𝒢
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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 ∈
      𝒢
⊢ x ∈ 𝒢 ↔
    x ∈
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢
have h₂ : x ∈ 𝒢 ↔ g⁻¹ * x * g⁻¹⁻¹ ∈ 𝒢
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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⁻¹⁻¹ ∈ 𝒢
⊢ x ∈ 𝒢 ↔
    x ∈
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢
have h₃ : x ∈ 𝒢 ↔ g⁻¹ * x * g ∈ 𝒢
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Cusps (goal)
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 ∈ 𝒢
⊢ x ∈ 𝒢 ↔
    x ∈
      HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g : ConjAct (GL (Fin 2) ℝ)) 𝒢
have h₄ : x ∈ 𝒢 ↔ g⁻¹ * x ∈ 𝒢
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)]