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 : 𝒢.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 : ↥ℋ
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
hf : Ne (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
contrapose : ∀ (hf : ModularForm.norm ℋ f = 0), Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
⊢ ModularForm.norm ℋ f ≠ 0

Tactic:
contrapose hf
-- 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
hf : ModularForm.norm ℋ f = 0
rw :
  ∀
    (hf :
      ∃ (i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ),
        Membership.mem (γ := Finset (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) Finset.univ i ∧ quotientFunc f i = 0),
    Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
rw₁ :
  ∀ (hf : Eq (α := (a : ℍ) → ℂ) (∏ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q) 0) (i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ),
    Membership.mem (γ := Finset (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) Finset.univ i → MDiff (quotientFunc f i)
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0

Tactic:
rw [← DFunLike.coe_injective.eq_iff, coe_norm, coe_zero, prod_eq_zero_iff] at hf

Premises used: UpperHalfPlane.prod_eq_zero_iff, Function.Injective.eq_iff, DFunLike.coe_injective, ModularForm.coe_norm, ModularForm.coe_zero
-- 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
hf :
  ∃ (i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ), Membership.mem (γ := Finset (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) Finset.univ i ∧ quotientFunc f i = 0
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0

Tactic:
simpa [QuotientGroup.exists_mk] using hf

Premises used: QuotientGroup.exists_mk
-- 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
hf : Eq (α := (a : ℍ) → ℂ) (∏ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q) 0
⊢ ∀ (i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ),
    Membership.mem (γ := Finset (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) Finset.univ i → MDiff (quotientFunc f i)

Tactic:
Quotient.forall.mpr fun r _ ↦ (translate f r.val⁻¹).holo'

Premises used: Iff.mpr, Quotient.forall, ModularForm.translate, Inv.inv, ModularForm.holo', Subtype.val
-- 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
hf : Eq (α := (a : ℍ) → ℂ) (∏ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q) 0
⊢ ∀ (i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ),
    Membership.mem (γ := Finset (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) Finset.univ i → MDiff (quotientFunc f i)

Tactic:
exact Quotient.forall.mpr fun r _ ↦ (translate f r.val⁻¹).holo'

Premises used: Iff.mpr, Quotient.forall
-- 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
⊢ ModularForm.norm ℋ f = 0 ↔ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0

Tactic:
⟨fun hn ↦ ?_, fun hf ↦ ?_⟩

Premises used: Iff.intro
-- 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
refine_1 : ∀ (hn : ModularForm.norm ℋ f = 0), Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
refine_2 : ∀ (hf : Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0), ModularForm.norm ℋ f = 0
⊢ ModularForm.norm ℋ f = 0 ↔ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0

Tactic:
refine ⟨fun hn ↦ ?_, fun hf ↦ ?_⟩
-- 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
hn : ModularForm.norm ℋ f = 0
refine_1 : ∀ (hn : Ne (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0), ModularForm.norm ℋ f ≠ 0
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0

Tactic:
contrapose! hn
-- 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
hn : Ne (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
⊢ ModularForm.norm ℋ f ≠ 0

Tactic:
norm_ne_zero ℋ hn

Premises used: ModularForm.norm_ne_zero
-- 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
hn : Ne (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
⊢ ModularForm.norm ℋ f ≠ 0

Tactic:
exact norm_ne_zero ℋ hn

Premises used: ModularForm.norm_ne_zero
-- 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
hf : Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
refine_2 : ∀ (τ : ℍ), Eq (α := ℂ) ((ModularForm.norm ℋ f : (a : ℍ) → ℂ) τ : ℂ) ((0 : (a : ℍ) → ℂ) τ : ℂ)
⊢ ModularForm.norm ℋ f = 0

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
hf : Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
τ : ℍ
⊢ 1 ∈ ℋ ∧
    Eq (α := ℂ)
      (@SlashAction.map _ (GL (Fin 2) ℝ) _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k 1⁻¹
          (⇑f : (a : ℍ) → ℂ) τ :
        ℂ)
      (0 : ℂ)

Tactic:
simpa using congr_fun hf τ

Premises used: congr_fun
-- 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
hf : Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
τ : ℍ
⊢ Eq (α := ℂ) ((ModularForm.norm ℋ f : (a : ℍ) → ℂ) τ : ℂ) ((0 : (a : ℍ) → ℂ) τ : ℂ)

Tactic:
simpa [Finset.prod_eq_zero_iff, QuotientGroup.exists_mk]
      using ⟨1, by simpa using congr_fun hf τ⟩

Premises used: Finset.prod_eq_zero_iff, QuotientGroup.exists_mk
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
this :
  Eq (α :=
    ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
      (k *
        (↑(Nat.card
              (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
                Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
                (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
          ℤ)))
    (ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) f) 0
⊢ f = 0

Tactic:
simpa [ModularForm.norm_eq_zero_iff]

Premises used: ModularForm.norm_eq_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
suffices :
  Eq (α :=
    ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
      (k *
        (↑(Nat.card
              (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
                Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
                (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
          ℤ)))
    (ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) f) 0
⊢ f = 0

Tactic:
suffices ModularForm.norm 𝒮ℒ f = 0 by simpa [ModularForm.norm_eq_zero_iff]
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
h :
  ∀ (x : ℍ),
    Eq (α := ℂ)
      ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) f : (a : ℍ) → ℂ) x : ℂ)
      ((0 : (a : ℍ) → ℂ) x : ℂ)
⊢ Eq (α :=
    ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
      (k *
        (↑(Nat.card
              (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
                Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
                (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
          ℤ)))
    (ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) f) 0

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
x : ℍ
h : Eq (α := ℂ) (0 x : ℂ) ((0 : (a : ℍ) → ℂ) x : ℂ)
h₁ : Eq (α := ℂ) (0 : ℂ) ((0 : (a : ℍ) → ℂ) x : ℂ)
h₂ h₃ : Eq (α := ℂ) 0 0
⊢ Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) f : (a : ℍ) → ℂ) x : ℂ)
    ((0 : (a : ℍ) → ℂ) x : ℂ)

Tactic:
rw [ModularFormClass.levelOne_neg_weight_eq_zero
    (mul_neg_of_neg_of_pos hk <| mod_cast Nat.pos_of_ne_zero 𝒢.relIndex_ne_zero)
    (ModularForm.norm 𝒮ℒ f), Pi.zero_apply, zero_apply]

Premises used: mul_neg_of_neg_of_pos, MonoidHom.range, Real, ModularFormClass.levelOne_neg_weight_eq_zero, ModularForm.norm, ModularForm.zero_apply, Pi.zero_apply, Matrix.SpecialLinearGroup.mapGL
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 0
rw :
  ModularFormClass (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0)
    (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0
⊢ ModularFormClass
    (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
      (HMul.hMul (α := ℤ) 0
        (↑(Nat.card
              (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
                Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
                (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
          ℤ)))
    (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 0
⊢ ModularFormClass (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0)
    (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this : ModularFormClass
  (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (HMul.hMul (α := ℤ) 0
      (↑(Nat.card
            (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
              Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
              (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
        ℤ)))
  (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0 :=
  ⋯
obtain :
  ∀ (c : ℂ)
    (hc :
      (⇑(ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
              (f - const ((f : (a : ℍ) → ℂ) I))) :
          (a : ℍ) → ℂ) =
        Function.const ℍ c),
    ∃ (c : ℂ), (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
⊢ ∃ (c : ℂ), (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c

Tactic:
obtain ⟨c, hc⟩ := ModularFormClass.levelOne_weight_zero_const
    (ModularForm.norm 𝒮ℒ (f - .const (f I)))

Premises used: MonoidHom.range, Real, HSub.hSub, ModularForm.norm, ModularFormClass.levelOne_weight_zero_const, Matrix.SpecialLinearGroup.mapGL
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this : ModularFormClass
  (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (HMul.hMul (α := ℤ) 0
      (↑(Nat.card
            (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
              Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
              (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
        ℤ)))
  (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0 :=
  ⋯
c : ℂ
hc :
  (⇑(ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
          (f - const ((f : (a : ℍ) → ℂ) I))) :
      (a : ℍ) → ℂ) =
    Function.const ℍ c
⊢ @SlashAction.map ℤ (GL (Fin 2) ℝ) _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) 1)⁻¹
      (HSub.hSub (α := (a : ℍ) → ℂ) (β := (a : ℍ) → ℂ) ((⇑f : (a : ℍ) → ℂ) : (a : ℍ) → ℂ)
        (Function.const ℍ ((f : (a : ℍ) → ℂ) I) : ℍ → ℂ))
      I =
    0

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this : ModularFormClass
  (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (HMul.hMul (α := ℤ) 0
      (↑(Nat.card
            (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
              Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
              (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
        ℤ)))
  (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0 :=
  ⋯
c : ℂ
hc :
  (⇑(ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
          (f - const ((f : (a : ℍ) → ℂ) I))) :
      (a : ℍ) → ℂ) =
    Function.const ℍ c
⊢ Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (f - const ((f : (a : ℍ) → ℂ) I)) :
          (a : ℍ) → ℂ)
        I :
      ℂ)
    (0 : ℂ)

Tactic:
simpa [Finset.prod_eq_zero_iff, QuotientGroup.exists_mk] using ⟨1, by simp⟩

Premises used: Finset.prod_eq_zero_iff, QuotientGroup.exists_mk
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this : ModularFormClass
  (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (HMul.hMul (α := ℤ) 0
      (↑(Nat.card
            (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
              Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
              (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
        ℤ)))
  (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0 :=
  ⋯
c : ℂ
hc :
  (⇑(ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
          (f - const ((f : (a : ℍ) → ℂ) I))) :
      (a : ℍ) → ℂ) =
    Function.const ℍ c
⊢ Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (f - const ((f : (a : ℍ) → ℂ) I)) :
          (a : ℍ) → ℂ)
        I :
      ℂ)
    (0 : ℂ)

Tactic:
have : ModularForm.norm 𝒮ℒ (f - .const (f I)) I = 0 := by
    simpa [Finset.prod_eq_zero_iff, QuotientGroup.exists_mk] using ⟨1, by simp⟩
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this_1 : ModularFormClass
  (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (HMul.hMul (α := ℤ) 0
      (↑(Nat.card
            (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
              Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
              (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
        ℤ)))
  (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0 :=
  ⋯
c : ℂ
hc :
  (⇑(ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
          (f - const ((f : (a : ℍ) → ℂ) I))) :
      (a : ℍ) → ℂ) =
    Function.const ℍ c
this :
  Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (f - const ((f : (a : ℍ) → ℂ) I)) :
          (a : ℍ) → ℂ)
        I :
      ℂ)
    (0 : ℂ)
⊢ c = 0

Tactic:
simpa [hc]
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this_1 : ModularFormClass
  (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (HMul.hMul (α := ℤ) 0
      (↑(Nat.card
            (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
              Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
              (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
        ℤ)))
  (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0 :=
  ⋯
c : ℂ
hc :
  (⇑(ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
          (f - const ((f : (a : ℍ) → ℂ) I))) :
      (a : ℍ) → ℂ) =
    Function.const ℍ c
this :
  Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (f - const ((f : (a : ℍ) → ℂ) I)) :
          (a : ℍ) → ℂ)
        I :
      ℂ)
    (0 : ℂ)
⊢ Eq (α := (a : ℍ) → ℂ)
    (⇑(ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
          (f - const ((f : (a : ℍ) → ℂ) I))) :
      (a : ℍ) → ℂ)
    (Function.const ℍ 0)

Tactic:
obtain rfl : c = 0 := by simpa [hc]

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this_1 : ModularFormClass
  (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (HMul.hMul (α := ℤ) 0
      (↑(Nat.card
            (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
              Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
              (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
        ℤ)))
  (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0 :=
  ⋯
this :
  Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (f - const ((f : (a : ℍ) → ℂ) I)) :
          (a : ℍ) → ℂ)
        I :
      ℂ)
    (0 : ℂ)
hc :
  Eq (α := (a : ℍ) → ℂ)
    (⇑(ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
          (f - const ((f : (a : ℍ) → ℂ) I))) :
      (a : ℍ) → ℂ)
    (Function.const ℍ 0)
⊢ f = const ((f : (a : ℍ) → ℂ) I)

Tactic:
simp only [Function.const_zero, coe_eq_zero_iff, norm_eq_zero_iff, sub_eq_zero] at hc

Premises used: ModularForm.norm_eq_zero_iff, sub_eq_zero, ModularForm.coe_eq_zero_iff, Function.const_zero
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this_1 : ModularFormClass
  (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (HMul.hMul (α := ℤ) 0
      (↑(Nat.card
            (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
              Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
              (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
        ℤ)))
  (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0 :=
  ⋯
this :
  Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (f - const ((f : (a : ℍ) → ℂ) I)) :
          (a : ℍ) → ℂ)
        I :
      ℂ)
    (0 : ℂ)
hc : f = const ((f : (a : ℍ) → ℂ) I)
rw :
  Eq (α := (a : ℍ) → ℂ) ((⇑(const ((f : (a : ℍ) → ℂ) I)) : (a : ℍ) → ℂ) : (a : ℍ) → ℂ)
    (Function.const ℍ ((const ((f : (a : ℍ) → ℂ) I) : (a : ℍ) → ℂ) I) : ℍ → ℂ)
rw₁ :
  Eq (α := (a : ℍ) → ℂ) (Function.const ℍ ((f : (a : ℍ) → ℂ) I) : ℍ → ℂ)
    (Function.const ℍ (Function.const ℍ ((f : (a : ℍ) → ℂ) I) I) : ℍ → ℂ)
rw₂ rw₃ :
  Eq (α := (a : ℍ) → ℂ) (Function.const ℍ ((f : (a : ℍ) → ℂ) I) : ℍ → ℂ)
    (Function.const ℍ ((f : (a : ℍ) → ℂ) I) : ℍ → ℂ)
⊢ Eq (α := (a : ℍ) → ℂ) ((⇑f : (a : ℍ) → ℂ) : (a : ℍ) → ℂ) (Function.const ℍ ((f : (a : ℍ) → ℂ) I) : ℍ → ℂ)

Tactic:
rw [hc, ModularForm.coe_const, Function.const_apply]

Premises used: Function.const_apply, ModularForm.coe_const
-- Module: Mathlib.NumberTheory.ModularForms.NormTrace
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this_1 : ModularFormClass
  (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (HMul.hMul (α := ℤ) 0
      (↑(Nat.card
            (HasQuotient.Quotient ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (B :=
              Subgroup ↥(MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)))
              (𝒢.subgroupOf (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))))) :
        ℤ)))
  (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0 :=
  ⋯
this :
  Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
            (f - const ((f : (a : ℍ) → ℂ) I)) :
          (a : ℍ) → ℂ)
        I :
      ℂ)
    (0 : ℂ)
hc : f = const ((f : (a : ℍ) → ℂ) I)
⊢ ∃ (c : ℂ), (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c

Tactic:
exact ⟨f I, by rw [hc, ModularForm.coe_const, Function.const_apply]⟩