awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)
hc_eq : c = 1728
rw :
  c * discriminant z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
rw₁ :
  (c • CuspForm.discriminant : (a : ℍ) → ℂ) z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
rw₂ :
  (g : (a : ℍ) → ℂ) z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
⊢ 1728 * discriminant z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
have rw₃ : (E₄CubeSubE₆SqForm : (a : ℍ) → ℂ) z =
  HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
Tactic: rw [← hc_eq, show c * discriminant z = (c • CuspForm.discriminant) z from rfl, hc,
      congr_fun hgE z, E₄CubeSubE₆SqForm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)
hc_eq : c = 1728
rw :
  c * discriminant z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
rw₁ :
  (c • CuspForm.discriminant : (a : ℍ) → ℂ) z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
rw₂ :
  (g : (a : ℍ) → ℂ) z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
rw₃ :
  (E₄CubeSubE₆SqForm : (a : ℍ) → ℂ) z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
⊢ 1728 * discriminant z =
    HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
have rw₄ : HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2 =
  HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
Tactic: rw [← hc_eq, show c * discriminant z = (c • CuspForm.discriminant) z from rfl, hc,
      congr_fun hgE z, E₄CubeSubE₆SqForm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (hypothesis)
Goal:
z : ℍ
g : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12
hg :
  (CuspForm.toModularFormₗ :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12)
      g =
    E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : Eq (α := (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) (⇑E₄CubeSubE₆SqForm : (a : ℍ) → ℂ)
hc_eq : c = 1728
⊢ discriminant z =
    (HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 -
        HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2) /
      1728
have h1728 : 1728 * discriminant z =
  HPow.hPow (α := ℂ) (β := ℕ) ((E₄ : (a : ℍ) → ℂ) z : ℂ) 3 - HPow.hPow (α := ℂ) (β := ℕ) ((E₆ : (a : ℍ) → ℂ) z : ℂ) 2
Tactic: have h1728 : (1728 : ℂ) * discriminant z = E₄ z ^ 3 - E₆ z ^ 2 := by
    rw [← hc_eq, show c * discriminant z = (c • CuspForm.discriminant) z from rfl, hc,
      congr_fun hgE z, E₄CubeSubE₆SqForm_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
⊢ (DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))) 12 :
        (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
      (modularForm CuspForm.discriminant) =
    (1 / 1728) •
      HSub.hSub (α :=
        DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
        (β :=
        DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
        ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))) 12 :
              (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
                DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
            (E₄.pow 3) :
          DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
        ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))) 12 :
              (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
                DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
            (E₆.pow 2) :
          DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
have rw : Eq (α := DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
  ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))) 12 :
        (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
      (modularForm CuspForm.discriminant) :
    DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
  ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))) 12 :
        (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
          DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
      ((1 / 1728) •
        HSub.hSub (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12) (β :=
          ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12)
          (E₄.pow 3 :
            ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
              (HMul.hMul (α := ℤ) (↑3 : ℤ) 4))
          (E₆.pow 2 :
            ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
              (HMul.hMul (α := ℤ) (↑2 : ℤ) 6))) :
    DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
Tactic: rw [← map_sub (DirectSum.of (ModularForm 𝒮ℒ) 12), ← DirectSum.of_smul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
⊢ Eq (α :=
    DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
    ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))) 12 :
          (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
            DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
        (modularForm CuspForm.discriminant) :
      DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
    ((DirectSum.of (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))) 12 :
          (a : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12) →
            DirectSum ℤ fun (i : ℤ) ↦ ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range i)
        ((1 / 1728) •
          HSub.hSub (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12) (β :=
            ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12)
            (E₄.pow 3 :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
                (HMul.hMul (α := ℤ) (↑3 : ℤ) 4))
            (E₆.pow 2 :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
                (HMul.hMul (α := ℤ) (↑2 : ℤ) 6))) :
      DirectSum ℤ fun (i : ℤ) ↦ ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) i)
have h : modularForm CuspForm.discriminant =
  (1 / 1728) •
    HSub.hSub (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12) (β :=
      ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12)
      (E₄.pow 3 :
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
          (HMul.hMul (α := ℤ) (↑3 : ℤ) 4))
      (E₆.pow 2 :
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
          (HMul.hMul (α := ℤ) (↑2 : ℤ) 6))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (goal)
Goal:
⊢ modularForm CuspForm.discriminant =
    (1 / 1728) •
      HSub.hSub (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12) (β :=
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12)
        (E₄.pow 3 :
          ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (HMul.hMul (α := ℤ) (↑3 : ℤ) 4))
        (E₆.pow 2 :
          ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (HMul.hMul (α := ℤ) (↑2 : ℤ) 6))
have h : ∀ (z : ℍ),
  Eq (α := ℂ) ((modularForm CuspForm.discriminant : (a : ℍ) → ℂ) z : ℂ)
    (((1 / 1728) •
            HSub.hSub (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12) (β :=
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 12)
              (E₄.pow 3 :
                ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
                  (HMul.hMul (α := ℤ) (↑3 : ℤ) 4))
              (E₆.pow 2 :
                ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
                  (HMul.hMul (α := ℤ) (↑2 : ℤ) 6)) :
          (a : ℍ) → ℂ)
        z :
      ℂ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (hypothesis)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h ≈ h'
⊢ ∃ g ∈ 𝒢, (↑h' : GL (Fin 2) ℝ) = (↑h : GL (Fin 2) ℝ) * g
have hhh'₁ : h⁻¹ * h' ∈ 𝒢.subgroupOf ℋ
Tactic: rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hhh'
Cleared hypotheses: hhh'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F 𝒢 k
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
τ : ℍ
h h' : ↥ℋ
hhh' : h ≈ h'
⊢ Eq (α := ℂ)
    ((fun (g : ↥ℋ) ↦
        (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k (↑g : GL (Fin 2) ℝ)⁻¹
            (⇑f : (a : ℍ) → ℂ) τ :
          ℂ))
      h)
    ((fun (g : ↥ℋ) ↦
        (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k (↑g : GL (Fin 2) ℝ)⁻¹
            (⇑f : (a : ℍ) → ℂ) τ :
          ℂ))
      h')
have obtain : ∀ (j : GL (Fin 2) ℝ) (hj : j ∈ 𝒢) (hj' : (↑h' : GL (Fin 2) ℝ) = (↑h : GL (Fin 2) ℝ) * j),
  Eq (α := ℂ)
    ((fun (g : ↥ℋ) ↦
        (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k (↑g : GL (Fin 2) ℝ)⁻¹
            (⇑f : (a : ℍ) → ℂ) τ :
          ℂ))
      h)
    ((fun (g : ↥ℋ) ↦
        (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k (↑g : GL (Fin 2) ℝ)⁻¹
            (⇑f : (a : ℍ) → ℂ) τ :
          ℂ))
      h')
Tactic: obtain ⟨j, hj, hj'⟩ : ∃ g ∈ 𝒢, h' = h * g := by
      rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hhh'
      exact ⟨h⁻¹ * h', hhh', mod_cast (mul_inv_cancel_left h h').symm⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F 𝒢 k
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k h (quotientFunc f q) =
    quotientFunc f ((Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ ℋ) h hh)⁻¹ • q)
have h₁ : ∀ (r : ↥ℋ),
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k h (quotientFunc f ⟦r⟧) =
    quotientFunc f ((Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ ℋ) h hh)⁻¹ • ⟦r⟧)
Tactic: induction q using Quotient.inductionOn with
  | h r => simp [SlashAction.slash_mul]
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : 𝒢.IsFiniteRelIndex ℋ
inst_2 : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty) ℋ
⊢ IsBoundedAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (SlashInvariantForm.trace ℋ f).toFun)
have rw : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
  (fun (a : ℍ) ↦
    ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
      @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
  1
Tactic: rw [SlashInvariantForm.trace, IsBoundedAtImInfty, Filter.BoundedAtFilter,
      SlashAction.sum_slash, Finset.sum_fn]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : 𝒢.IsFiniteRelIndex ℋ
inst_2 : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty) ℋ
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (fun (a : ℍ) ↦
      ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
        @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
    1
have refine : ∀ (x : ↥ℋ) (r : GL (Fin 2) ℝ) (hr : r ∈ ℋ),
  Membership.mem (γ := Finset (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) Finset.univ
      ⟦Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ ℋ) r hr⟧ →
    IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty)
      (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            (↑(Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ ℋ) r hr) : GL (Fin 2) ℝ)⁻¹⁻¹ :
          ConjAct (GL (Fin 2) ℝ))
        𝒢)
Tactic: refine .sum (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ (translate f _).bdd_at_cusps' ?_ γ rfl)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : 𝒢.IsFiniteRelIndex ℋ
inst_2 : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty) ℋ
⊢ IsZeroAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (ModularForm.trace ℋ f).toFun)
have simp_rw : Filter.Tendsto (β := ℂ)
  (fun (a : ℍ) ↦
    ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
      @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
  atImInfty (𝓝 0)
Tactic: simp_rw [ModularForm.toFun_eq_coe, ModularForm.coe_trace, IsZeroAtImInfty, Filter.ZeroAtFilter,
      SlashAction.sum_slash, Finset.sum_fn]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : 𝒢.IsFiniteRelIndex ℋ
inst_2 : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Filter.Tendsto (β := ℂ)
    (fun (a : ℍ) ↦
      ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
        @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
    atImInfty (𝓝 0)
have rw : Filter.Tendsto (β := ℂ)
  (fun (a : ℍ) ↦
    ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
      @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
  atImInfty (𝓝 (∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 0))
Tactic: rw [show (0 : ℂ) = ∑ c : ℋ ⧸ 𝒢.subgroupOf ℋ, 0 by simp]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : 𝒢.IsFiniteRelIndex ℋ
inst_2 : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Filter.Tendsto (β := ℂ)
    (fun (a : ℍ) ↦
      ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
        @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
    atImInfty (𝓝 (∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 0))
have refine : ∀ (x : ↥ℋ) (r : GL (Fin 2) ℝ) (hr : r ∈ ℋ),
  Membership.mem (γ := Finset (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) Finset.univ
      ⟦Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ ℋ) r hr⟧ →
    Filter.Tendsto
      (@SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ
        (quotientFunc f ⟦Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ ℋ) r hr⟧))
      atImInfty (𝓝 0)
Tactic: refine tendsto_finsetSum _ (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : 𝒢.IsFiniteRelIndex ℋ
inst_2 : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
x : ↥ℋ
r : GL (Fin 2) ℝ
hr : r ∈ ℋ
h_1 :
  Membership.mem (γ := Finset (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) Finset.univ ⟦Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ ℋ) r hr⟧
⊢ Filter.Tendsto
    (@SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ
      (quotientFunc f ⟦Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ ℋ) r hr⟧))
    atImInfty (𝓝 0)
have refine : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty)
  (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
    ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
        (↑(Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ ℋ) r hr) : GL (Fin 2) ℝ)⁻¹⁻¹ :
      ConjAct (GL (Fin 2) ℝ))
    𝒢)
Tactic: refine (translate f _).zero_at_cusps' ?_ γ rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : 𝒢.IsFiniteRelIndex ℋ
inst_2 : ℋ.HasDetPlusMinusOne
inst_3 : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _
      (k * (↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) : ℤ)) γ (∏ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q))
    1
have rw : Asymptotics.IsBigO (F := ℝ) atImInfty
  (HSMul.hSMul (β := ℍ → ℂ)
    (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) γ) : ℝ)|
      (HSub.hSub (α := ℤ) (↑(Finset.card (α := ↥ℋ ⧸ 𝒢.subgroupOf ℋ) Finset.univ) : ℤ) 1))
    (∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
      @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (quotientFunc f i)))
  1
Tactic: rw [Nat.card_eq_fintype_card, ← Finset.card_univ, ModularForm.prod_slash]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : 𝒢.IsFiniteRelIndex ℋ
inst_2 : ℋ.HasDetPlusMinusOne
inst_3 : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Asymptotics.IsBigO (F := ℝ) atImInfty
    (HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) γ) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(Finset.card (α := ↥ℋ ⧸ 𝒢.subgroupOf ℋ) Finset.univ) : ℤ) 1))
      (∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (quotientFunc f i)))
    1
have h₁ : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
  (∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
    @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (quotientFunc f i))
  1
Tactic: apply Asymptotics.IsBigO.const_smul_left
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : 𝒢.IsFiniteRelIndex ℋ
inst_2 : ℋ.HasDetPlusMinusOne
inst_3 : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Eq (α := ℍ → ℝ) 1 fun (x : ℍ) ↦ ∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 1
have h₁ : ∀ (x : ℍ), Eq (α := ℝ) (1 x) (∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : 𝒢.IsFiniteRelIndex ℋ
inst_2 : ℋ.HasDetPlusMinusOne
inst_3 : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
      @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (quotientFunc f i))
    1
have h₁ : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
  (fun (a : ℍ) ↦
    ∏ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
      @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (quotientFunc f c) a)
  fun (x : ℍ) ↦ ∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 1
Tactic: rw [show (1 : ℍ → ℝ) = (fun x ↦ ∏ (i : 𝒬), 1) by ext; simp, Finset.prod_fn]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : 𝒢.IsFiniteRelIndex ℋ
inst_2 : ℋ.HasDetPlusMinusOne
inst_3 : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (fun (a : ℍ) ↦
      ∏ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (quotientFunc f c) a)
    fun (x : ℍ) ↦ ∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 1
have h₁ : ∀ (x : ↥ℋ) (r : GL (Fin 2) ℝ) (hr : r ∈ ℋ),
  Membership.mem (γ := Finset (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) Finset.univ
      ⟦Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ ℋ) r hr⟧ →
    IsCusp (HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty)
      (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
        ((ConjAct.toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ))
            (↑(Subtype.mk (p := fun (x : GL (Fin 2) ℝ) ↦ x ∈ ℋ) r hr) : GL (Fin 2) ℝ)⁻¹⁻¹ :
          ConjAct (GL (Fin 2) ℝ))
        𝒢)
Tactic: refine .finsetProd (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ (translate f _).bdd_at_cusps' ?_ γ rfl)