awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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'
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')
⊢ 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⟩
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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'
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:
simp [hj', SlashAction.slash_mul, SlashInvariantFormClass.slash_action_eq f j⁻¹ (inv_mem hj)]

Premises used: InvMemClass.inv_mem, SlashAction.slash_mul, Inv.inv, SlashInvariantFormClass.slash_action_eq
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F 𝒢 k
h : ↥ℋ
⊢ quotientFunc f ⟦h⟧ =
    @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k (↑h : GL (Fin 2) ℝ)⁻¹
      (⇑f : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: SlashInvariantForm.quotientFunc, rfl
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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 ∈ ℋ
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:
simp [SlashAction.slash_mul]

Premises used: SlashAction.slash_mul
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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 ℋ
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⟧)
⊢ @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)

Tactic:
induction q using Quotient.inductionOn with
  | h r => simp [SlashAction.slash_mul]

Premises used: SlashAction.slash_mul
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F 𝒢 k
inst_2 : 𝒢.IsFiniteRelIndex ℋ
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Eq (α := ℍ → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k h
      (let this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ);
      ∑ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q))
    (let this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ);
    ∑ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q)

Tactic:
simpa [SlashAction.sum_slash, quotientFunc_smul f hh]
      using Equiv.sum_comp (MulAction.toPerm (_ : ℋ)) _

Premises used: SlashInvariantForm.quotientFunc_smul, Equiv.sum_comp, MulAction.toPerm, SlashAction.sum_slash
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : SlashInvariantFormClass F 𝒢 k
inst_2 : 𝒢.IsFiniteRelIndex ℋ
inst_3 : ℋ.HasDetPlusMinusOne
h : GL (Fin 2) ℝ
hh : h ∈ ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ Eq (α := ℍ → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _
      (k * (↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) : ℤ)) h
      (let this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ);
      ∏ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q))
    (let this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ);
    ∏ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q)

Tactic:
simpa [← Finset.card_univ, ModularForm.prod_slash,
      quotientFunc_smul f hh, Subgroup.HasDetPlusMinusOne.abs_det hh,
      -Matrix.GeneralLinearGroup.val_det_apply] using Equiv.prod_comp (MulAction.toPerm (_ : ℋ)) _

Premises used: Finset.card_univ, ModularForm.prod_slash, SlashInvariantForm.quotientFunc_smul, MulAction.toPerm, Equiv.prod_comp, Subgroup.HasDetPlusMinusOne.abs_det, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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) ℋ
rw :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (fun (a : ℍ) ↦
      ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
        @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
    1
⊢ IsBoundedAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (SlashInvariantForm.trace ℋ f).toFun)

Tactic:
rw [SlashInvariantForm.trace, IsBoundedAtImInfty, Filter.BoundedAtFilter,
      SlashAction.sum_slash, Finset.sum_fn]

Premises used: UpperHalfPlane.IsBoundedAtImInfty, Filter.BoundedAtFilter, SlashAction.sum_slash, SlashInvariantForm.trace, Finset.sum_fn
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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

Tactic:
.sum (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ (translate f _).bdd_at_cusps' ?_ γ rfl)

Premises used: Iff.mpr, Subgroup.subgroupOf, Quotient.forall, ModularForm.trace.match_1, Asymptotics.IsBigO, UpperHalfPlane.atImInfty, QuotientGroup.leftRel, ModularForm.translate, Asymptotics.IsBigO.sum, Quotient.mk, Subtype.mk, SlashAction.map, Inv.inv, SlashInvariantForm.quotientFunc, OfNat.ofNat, Subtype.val, ModularForm.bdd_at_cusps', rfl
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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) ℋ
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) ℝ))
          𝒢)
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (fun (a : ℍ) ↦
      ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
        @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
    1

Tactic:
refine .sum (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ (translate f _).bdd_at_cusps' ?_ γ rfl)
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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) ℋ
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⟧
⊢ 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:
simpa using h.of_isFiniteRelIndex_conj hr

Premises used: IsCusp.of_isFiniteRelIndex_conj
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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) ℋ
simp_rw :
  Filter.Tendsto (β := ℂ)
    (fun (a : ℍ) ↦
      ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
        @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
    atImInfty (𝓝 0)
⊢ IsZeroAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (ModularForm.trace ℋ f).toFun)

Tactic:
simp_rw [ModularForm.toFun_eq_coe, ModularForm.coe_trace, IsZeroAtImInfty, Filter.ZeroAtFilter,
      SlashAction.sum_slash, Finset.sum_fn]

Premises used: Filter.ZeroAtFilter, SlashAction.sum_slash, UpperHalfPlane.IsZeroAtImInfty, Finset.sum_fn, ModularForm.toFun_eq_coe, ModularForm.coe_trace
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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 ℋ)
⊢ Eq (α := ℂ) 0 (∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 0)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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 ℋ)
rw :
  Filter.Tendsto (β := ℂ)
    (fun (a : ℍ) ↦
      ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
        @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
    atImInfty (𝓝 (∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 0))
⊢ Filter.Tendsto (β := ℂ)
    (fun (a : ℍ) ↦
      ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
        @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
    atImInfty (𝓝 0)

Tactic:
rw [show (0 : ℂ) = ∑ c : ℋ ⧸ 𝒢.subgroupOf ℋ, 0 by simp]
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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))

Tactic:
tendsto_finsetSum _ (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ ?_)

Premises used: Iff.mpr, Subgroup.subgroupOf, Quotient.forall, ModularForm.trace.match_1, UpperHalfPlane.atImInfty, QuotientGroup.leftRel, nhds, Quotient.mk, SlashAction.map, Filter.Tendsto, SlashInvariantForm.quotientFunc, tendsto_finsetSum, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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 ℋ)
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)
⊢ Filter.Tendsto (β := ℂ)
    (fun (a : ℍ) ↦
      ∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
        @SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (quotientFunc f c) a)
    atImInfty (𝓝 (∑ c : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 0))

Tactic:
refine tendsto_finsetSum _ (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ ?_)

Premises used: Iff.mpr, Quotient.forall, tendsto_finsetSum
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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)

Tactic:
(translate f _).zero_at_cusps' ?_ γ rfl

Premises used: CuspForm.translate, Filter.ZeroAtFilter, CuspForm.zero_at_cusps', SlashInvariantForm.quotientFunc, UpperHalfPlane.IsZeroAtImInfty, rfl
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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⟧
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) ℝ))
      𝒢)
⊢ 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 (translate f _).zero_at_cusps' ?_ γ rfl

Premises used: CuspForm.translate, CuspForm.zero_at_cusps', rfl
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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⟧
⊢ 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:
simpa using h.of_isFiniteRelIndex_conj hr

Premises used: IsCusp.of_isFiniteRelIndex_conj
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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 ℋ)
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
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _
      (k * (↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) : ℤ)) γ (∏ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q))
    1

Tactic:
rw [Nat.card_eq_fintype_card, ← Finset.card_univ, ModularForm.prod_slash]

Premises used: Finset.card_univ, ModularForm.prod_slash, Nat.card_eq_fintype_card
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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 ℋ)
h₁ :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
      @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (quotientFunc f i))
    1
⊢ 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:
apply Asymptotics.IsBigO.const_smul_left

Premises used: Asymptotics.IsBigO.const_smul_left
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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 ℋ)
h₁ : ∀ (x : ℍ), Eq (α := ℝ) (1 x) (∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 1)
⊢ Eq (α := ℍ → ℝ) 1 fun (x : ℍ) ↦ ∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 1

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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 ℋ)
x : ℍ
⊢ Eq (α := ℝ) (1 x) (∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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 ℋ)
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
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atImInfty
    (∏ i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ,
      @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (quotientFunc f i))
    1

Tactic:
rw [show (1 : ℍ → ℝ) = (fun x ↦ ∏ (i : 𝒬), 1) by ext; simp, Finset.prod_fn]

Premises used: Finset.prod_fn
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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

Tactic:
.finsetProd (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ (translate f _).bdd_at_cusps' ?_ γ rfl)

Premises used: Iff.mpr, Subgroup.subgroupOf, Quotient.forall, Asymptotics.IsBigO, UpperHalfPlane.atImInfty, _private.0.ModularForm.norm.match_3, QuotientGroup.leftRel, ModularForm.translate, Quotient.mk, Subtype.mk, Asymptotics.IsBigO.finsetProd, SlashAction.map, Inv.inv, SlashInvariantForm.quotientFunc, OfNat.ofNat, Subtype.val, ModularForm.bdd_at_cusps', rfl
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
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 ℋ)
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) ℝ))
          𝒢)
⊢ 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:
refine .finsetProd (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ (translate f _).bdd_at_cusps' ?_ γ rfl)