awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hf : Ne (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
⊢ ModularForm.norm ℋ f ≠ 0
have contrapose : ∀ (hf : ModularForm.norm ℋ f = 0), Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
Tactic: contrapose hf
Cleared hypotheses: hf
-- 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
hf : ModularForm.norm ℋ f = 0
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
have rw : ∀
  (hf :
    ∃ (i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ),
      Membership.mem (γ := Finset (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) Finset.univ i ∧ quotientFunc f i = 0),
  Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
Tactic: rw [← DFunLike.coe_injective.eq_iff, coe_norm, coe_zero, prod_eq_zero_iff] at hf
Cleared hypotheses: hf
-- 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
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
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
have rw₁ : ∀ (hf : Eq (α := (a : ℍ) → ℂ) (∏ q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ, quotientFunc f q) 0) (i : ↥ℋ ⧸ 𝒢.subgroupOf ℋ),
  Membership.mem (γ := Finset (↥ℋ ⧸ 𝒢.subgroupOf ℋ)) Finset.univ i → MDiff (quotientFunc f i)
Tactic: rw [← DFunLike.coe_injective.eq_iff, coe_norm, coe_zero, prod_eq_zero_iff] at hf
Cleared hypotheses: hf
-- 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
⊢ ModularForm.norm ℋ f = 0 ↔ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
have refine_1 : ∀ (hn : ModularForm.norm ℋ f = 0), Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
Tactic: refine ⟨fun hn ↦ ?_, fun hf ↦ ?_⟩
-- 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
refine_1 : ∀ (hn : ModularForm.norm ℋ f = 0), Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
⊢ ModularForm.norm ℋ f = 0 ↔ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
have refine_2 : ∀ (hf : Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0), ModularForm.norm ℋ f = 0
Tactic: refine ⟨fun hn ↦ ?_, fun hf ↦ ?_⟩
-- 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
hn : ModularForm.norm ℋ f = 0
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
have refine_1 : ∀ (hn : Ne (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0), ModularForm.norm ℋ f ≠ 0
Tactic: contrapose! hn
Cleared hypotheses: hn
-- 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
hf : Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
⊢ ModularForm.norm ℋ f = 0
have refine_2 : ∀ (τ : ℍ), Eq (α := ℂ) ((ModularForm.norm ℋ f : (a : ℍ) → ℂ) τ : ℂ) ((0 : (a : ℍ) → ℂ) τ : ℂ)
Tactic: ext τ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
⊢ f = 0
have 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
Tactic: suffices ModularForm.norm 𝒮ℒ f = 0 by simpa [ModularForm.norm_eq_zero_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
⊢ 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
have h : ∀ (x : ℍ),
  Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) f : (a : ℍ) → ℂ) x : ℂ)
    ((0 : (a : ℍ) → ℂ) x : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
x : ℍ
⊢ Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) f : (a : ℍ) → ℂ) x : ℂ)
    ((0 : (a : ℍ) → ℂ) x : ℂ)
have h : Eq (α := ℂ) (0 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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
x : ℍ
h : Eq (α := ℂ) (0 x : ℂ) ((0 : (a : ℍ) → ℂ) x : ℂ)
⊢ Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) f : (a : ℍ) → ℂ) x : ℂ)
    ((0 : (a : ℍ) → ℂ) x : ℂ)
have h₁ : Eq (α := ℂ) (0 : ℂ) ((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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
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 : ℂ)
⊢ Eq (α := ℂ)
    ((ModularForm.norm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) f : (a : ℍ) → ℂ) x : ℂ)
    ((0 : (a : ℍ) → ℂ) x : ℂ)
have h₂ : Eq (α := ℂ) 0 0
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]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
Goal:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst : 𝒢.IsArithmetic
inst_1 : 𝒢.HasDetOne
f : ModularForm 𝒢 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
have rw : ModularFormClass (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0)
  (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
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 : ℂ), (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
have 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
Tactic: obtain ⟨c, hc⟩ := ModularFormClass.levelOne_weight_zero_const
    (ModularForm.norm 𝒮ℒ (f - .const (f I)))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (hypothesis)
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
⊢ ∃ (c : ℂ), (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
have this₁ : 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⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (hypothesis)
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 : ℂ), (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
have hc₁ : 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]
Cleared hypotheses: c, hc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (hypothesis)
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)
⊢ ∃ (c : ℂ), (⇑f : (a : ℍ) → ℂ) = Function.const ℍ c
have hc₁ : f = const ((f : (a : ℍ) → ℂ) I)
Tactic: simp only [Function.const_zero, coe_eq_zero_iff, norm_eq_zero_iff, sub_eq_zero] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
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)
⊢ Eq (α := (a : ℍ) → ℂ) ((⇑f : (a : ℍ) → ℂ) : (a : ℍ) → ℂ) (Function.const ℍ ((f : (a : ℍ) → ℂ) I) : ℍ → ℂ)
have rw : Eq (α := (a : ℍ) → ℂ) ((⇑(const ((f : (a : ℍ) → ℂ) I)) : (a : ℍ) → ℂ) : (a : ℍ) → ℂ)
  (Function.const ℍ ((const ((f : (a : ℍ) → ℂ) I) : (a : ℍ) → ℂ) I) : ℍ → ℂ)
Tactic: rw [hc, ModularForm.coe_const, Function.const_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
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) : ℍ → ℂ)
⊢ Eq (α := (a : ℍ) → ℂ) ((⇑f : (a : ℍ) → ℂ) : (a : ℍ) → ℂ) (Function.const ℍ ((f : (a : ℍ) → ℂ) I) : ℍ → ℂ)
have rw₁ : Eq (α := (a : ℍ) → ℂ) (Function.const ℍ ((f : (a : ℍ) → ℂ) I) : ℍ → ℂ)
  (Function.const ℍ (Function.const ℍ ((f : (a : ℍ) → ℂ) I) I) : ℍ → ℂ)
Tactic: rw [hc, ModularForm.coe_const, Function.const_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.NormTrace (goal)
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) : ℍ → ℂ)
⊢ Eq (α := (a : ℍ) → ℂ) ((⇑f : (a : ℍ) → ℂ) : (a : ℍ) → ℂ) (Function.const ℍ ((f : (a : ℍ) → ℂ) I) : ℍ → ℂ)
have rw₂ : Eq (α := (a : ℍ) → ℂ) (Function.const ℍ ((f : (a : ℍ) → ℂ) I) : ℍ → ℂ) (Function.const ℍ ((f : (a : ℍ) → ℂ) I) : ℍ → ℂ)
Tactic: rw [hc, ModularForm.coe_const, Function.const_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
k : ℤ
f f' : ℍ → ℂ
hf : Continuous f
hf' : Continuous f'
⊢ Continuous (Y := ℂ) fun (τ : ℍ) ↦
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (f τ) : ℂ) (f' τ) * (↑τ.im : ℂ) ^ k
have funProp : ∀ (a : ℂ), a ≠ 0 ∨ 0 ≤ k
Tactic: fun_prop (disch := simp [im_ne_zero _])
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
k : ℤ
f f' : ℍ → ℂ
hf : Continuous f
hf' : Continuous f'
funProp : ∀ (a : ℂ), a ≠ 0 ∨ 0 ≤ k
⊢ Continuous (Y := ℂ) fun (τ : ℍ) ↦
    HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (f τ) : ℂ) (f' τ) * (↑τ.im : ℂ) ^ k
have funProp₁ : ∀ (a : ℍ), (↑a.im : ℂ) ≠ 0 ∨ 0 ≤ k
Tactic: fun_prop (disch := simp [im_ne_zero _])
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (hypothesis)
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
⊢ petersson k (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f') τ =
    HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 2)) ((σ g : (a : ℂ) → ℂ) (petersson k f f' (g • τ)) : ℂ)
have hD : (↑D : ℂ) ≠ 0
Tactic: have hD : (D : ℂ) ≠ 0 := mod_cast abs_ne_zero.mpr g.det_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
⊢ petersson k (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f') τ =
    HMul.hMul (β := ℂ)
        (HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 2 + k))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ))
        ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
      ((↑τ.im : ℂ) ^ k * (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ) ^ (-k))
have simp : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| : ℂ) ^ (k - 1)) *
        (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (denom g (↑τ : ℂ)) : ℂ) k)⁻¹ *
      (HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ)
          ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| : ℂ) ^ (k - 1)) *
        (denom g (↑τ : ℂ) ^ k)⁻¹) *
    (↑τ.im : ℂ) ^ k =
  HMul.hMul (β := ℂ)
      (HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 1) * (↑D : ℂ) ^ (k - 1))
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ))
      ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
    ((↑τ.im : ℂ) ^ k * ((j ^ k)⁻¹ * (HPow.hPow (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) j : ℂ) k)⁻¹))
Tactic: simp [Complex.normSq_eq_conj_mul_self, (by abel : k - 2 + k = (k - 1) + (k - 1)), petersson,
      zpow_add₀ hD, mul_zpow, ModularForm.slash_def, -Matrix.GeneralLinearGroup.val_det_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
⊢ HMul.hMul (β := ℂ)
        (HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 2 + k))
          ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ))
        ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
      ((↑τ.im : ℂ) ^ k * (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ) ^ (-k)) =
    (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        ((↑D : ℂ) * (↑τ.im : ℂ) / (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ)) ^ k)
have rw : HMul.hMul (β := ℂ)
      (HMul.hMul (β := ℂ) ((↑D : ℂ) ^ (k - 2) * (↑D : ℂ) ^ k)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ))
      ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
    ((↑τ.im : ℂ) ^ k * ((↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ) ^ k)⁻¹) =
  (↑D : ℂ) ^ (k - 2) *
    (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
        ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
      ((↑D : ℂ) ^ k * (↑τ.im : ℂ) ^ k * ((↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ) ^ k)⁻¹))
Tactic: rw [div_zpow, mul_zpow, zpow_neg, div_eq_mul_inv, zpow_add₀ hD]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Petersson (goal)
Goal:
k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
hD : (↑D : ℂ) ≠ 0
j : ℂ := denom g (↑τ : ℂ)
⊢ (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        ((↑D : ℂ) * (↑τ.im : ℂ) / (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ)) ^ k) =
    (↑D : ℂ) ^ (k - 2) *
      (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
          ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
        (↑(g • τ).im : ℂ) ^ k)
have rw : (↑D : ℂ) ^ (k - 2) *
    (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
        ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
      ((↑D : ℂ) * (↑τ.im : ℂ) / (↑((Complex.normSq : (a : ℂ) → ℝ) j) : ℂ)) ^ k) =
  (↑D : ℂ) ^ (k - 2) *
    (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ) : ℂ)
        ((σ g : (a : ℂ) → ℂ) (f' (g • τ)) : ℂ) *
      (↑(HDiv.hDiv (β := ℝ) (|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * τ.im)
              ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑τ : ℂ)) : ℝ)) :
          ℂ) ^
        k)
Tactic: rw [im_smul_eq_div_normSq, Complex.ofReal_div, Complex.ofReal_mul]