awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : ModularForm Γ k
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
bdd_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : ModularForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' })
    ((fun (f : ModularForm Γ k) ↦ f.toFun) g)
⊢ { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' : ModularForm Γ k } =
    g
have mk : ∀ (toSlashInvariantForm_1 : SlashInvariantForm Γ k) (holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ))
  (bdd_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm_1.toFun k)
  (h :
    Eq (α := (a : ℍ) → ℂ)
      ((fun (f : ModularForm Γ k) ↦ f.toFun)
        { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' })
      ((fun (f : ModularForm Γ k) ↦ f.toFun)
        { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := @bdd_at_cusps'_1 })),
  { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' : ModularForm Γ k } =
    { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := @bdd_at_cusps'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
bdd_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm.toFun k
toSlashInvariantForm_1 : SlashInvariantForm Γ k
holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ)
bdd_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsBoundedAt toSlashInvariantForm_1.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : ModularForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' })
    ((fun (f : ModularForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := @bdd_at_cusps'_1 })
⊢ { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := @bdd_at_cusps' : ModularForm Γ k } =
    { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := @bdd_at_cusps'_1 }
have mk : toSlashInvariantForm = toSlashInvariantForm_1
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : CuspForm Γ k
h : Eq (α := (a : ℍ) → ℂ) ((fun (f : CuspForm Γ k) ↦ f.toFun) f) ((fun (f : CuspForm Γ k) ↦ f.toFun) g)
⊢ f = g
have mk : ∀ (toSlashInvariantForm : SlashInvariantForm Γ k) (holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ))
  (zero_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm.toFun k)
  (h :
    Eq (α := (a : ℍ) → ℂ)
      ((fun (f : CuspForm Γ k) ↦ f.toFun)
        { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' })
      ((fun (f : CuspForm Γ k) ↦ f.toFun) g)),
  { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' : CuspForm Γ k } = g
Tactic: cases f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : CuspForm Γ k
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
zero_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : CuspForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' })
    ((fun (f : CuspForm Γ k) ↦ f.toFun) g)
⊢ { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' : CuspForm Γ k } = g
have mk : ∀ (toSlashInvariantForm_1 : SlashInvariantForm Γ k) (holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ))
  (zero_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm_1.toFun k)
  (h :
    Eq (α := (a : ℍ) → ℂ)
      ((fun (f : CuspForm Γ k) ↦ f.toFun)
        { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' })
      ((fun (f : CuspForm Γ k) ↦ f.toFun)
        { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := @zero_at_cusps'_1 })),
  { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' : CuspForm Γ k } =
    { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := @zero_at_cusps'_1 }
Tactic: cases g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm : SlashInvariantForm Γ k
holo' : MDiff (⇑toSlashInvariantForm : (a : ℍ) → ℂ)
zero_at_cusps' : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm.toFun k
toSlashInvariantForm_1 : SlashInvariantForm Γ k
holo'_1 : MDiff (⇑toSlashInvariantForm_1 : (a : ℍ) → ℂ)
zero_at_cusps'_1 : ∀ {c : OnePoint ℝ} (hc : IsCusp c Γ), c.IsZeroAt toSlashInvariantForm_1.toFun k
h :
  Eq (α := (a : ℍ) → ℂ)
    ((fun (f : CuspForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' })
    ((fun (f : CuspForm Γ k) ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := @zero_at_cusps'_1 })
⊢ { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', zero_at_cusps' := @zero_at_cusps' : CuspForm Γ k } =
    { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, zero_at_cusps' := @zero_at_cusps'_1 }
have mk : toSlashInvariantForm = toSlashInvariantForm_1
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
c : OnePoint ℝ
hc : IsCusp c Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c
⊢ IsBoundedAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (toFun (Γ := Γ) (k := k) 0))
have simp : IsBoundedAtImInfty (α := ℂ) 0
Tactic: simp only [SlashInvariantForm.toFun_eq_coe, coe_zero, SlashAction.zero_slash]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : ModularForm Γ k
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0 ↔ f = 0
have rw : Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑0 : (a : ℍ) → ℂ) ↔ f = 0
Tactic: rw [← coe_zero, DFunLike.coe_fn_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : ModularForm Γ k
rw : Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑0 : (a : ℍ) → ℂ) ↔ f = 0
rw₁ : Subgroup (GL (Fin 2) ℝ)
rw₂ : ℤ
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0 ↔ f = 0
have rw₃ : f = 0 ↔ f = 0
Tactic: rw [← coe_zero, DFunLike.coe_fn_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
⊢ f = 0
have h : ∀ (z : ℍ), Eq (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((0 : (a : ℍ) → ℂ) z : ℂ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (hypothesis)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((0 : (a : ℍ) → ℂ) z : ℂ)
have hf : (f : (a : ℍ) → ℂ) (HSMul.hSMul (α := GL (Fin 2) ℝ) (-1) z) =
  HMul.hMul (β := ℂ) (denom (-1) (↑z : ℂ) ^ k) ((f : (a : ℍ) → ℂ) z : ℂ)
Tactic: have hf := slash_action_eqn'' f h_neg_one z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (hypothesis)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf :
  (f : (a : ℍ) → ℂ) (HSMul.hSMul (α := GL (Fin 2) ℝ) (-1) z) =
    HMul.hMul (β := ℂ) (denom (-1) (↑z : ℂ) ^ k) ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((0 : (a : ℍ) → ℂ) z : ℂ)
have hf₁ : (f : (a : ℍ) → ℂ) z = HMul.hMul (α := ℂ) (β := ℂ) (-1 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
Tactic: rw [neg_smul, one_smul, denom_neg, denom_one, hk.neg_one_zpow] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (hypothesis)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : (f : (a : ℍ) → ℂ) z = HMul.hMul (α := ℂ) (β := ℂ) (-1 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((0 : (a : ℍ) → ℂ) z : ℂ)
have h2 : HMul.hMul (α := ℂ) (β := ℂ) (2 : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) = 0
Tactic: have h2 : (2 : ℂ) * f z = 0 := by linear_combination hf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
inst_2 : Γ.HasDetOne
c : α
f : ModularForm Γ k
c_1 : OnePoint ℝ
hc : IsCusp c_1 Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c_1
⊢ IsBoundedAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g
      (c • f.toSlashInvariantForm).toFun)
have simp_rw : Asymptotics.IsBigO (F := ℝ) atImInfty
  (HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ g : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) c 1) : ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
  1
Tactic: simp_rw [IsBoundedAtImInfty, Filter.BoundedAtFilter, SlashInvariantForm.toFun_eq_coe,
        SlashInvariantForm.coe_smul, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f, smul_slash]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℝ
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℝ ℂ
c : α
f : CuspForm Γ k
c_1 : OnePoint ℝ
hc : IsCusp c_1 Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c_1
⊢ IsZeroAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g
      (c • f.toSlashInvariantForm).toFun)
have simp_rw : Filter.Tendsto
  (HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ g : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) c 1) : ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
  atImInfty (𝓝 0)
Tactic: simp_rw [IsZeroAtImInfty, Filter.ZeroAtFilter, SlashInvariantForm.toFun_eq_coe,
        SlashInvariantForm.coe_smulℝ, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f, smul_slash]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
inst_2 : Γ.HasDetOne
c : α
f : CuspForm Γ k
c_1 : OnePoint ℝ
hc : IsCusp c_1 Γ
g : GL (Fin 2) ℝ
hg : HSMul.hSMul (β := OnePoint ℝ) g OnePoint.infty = c_1
⊢ IsZeroAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g
      (c • f.toSlashInvariantForm).toFun)
have simp_rw : Filter.Tendsto
  (HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ g : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) c 1) : ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (⇑f : (a : ℍ) → ℂ)))
  atImInfty (𝓝 0)
Tactic: simp_rw [IsZeroAtImInfty, Filter.ZeroAtFilter, SlashInvariantForm.toFun_eq_coe,
        SlashInvariantForm.coe_smul, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f,
        smul_slash]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
a b : GradedMonoid (ModularForm Γ)
h : a.fst (β := ModularForm Γ) = b.fst (β := ModularForm Γ)
h2 : mcast h (a.snd (β := ModularForm Γ)) ⋯ = b.snd (β := ModularForm Γ)
⊢ a = b
have obtain : ∀ (i : ℤ) (a : ModularForm Γ i)
  (h : (Sigma.mk (β := ModularForm Γ) i a).fst (β := ModularForm Γ) = b.fst (β := ModularForm Γ))
  (h2 : mcast h ((Sigma.mk (β := ModularForm Γ) i a).snd (β := ModularForm Γ)) sorry = b.snd (β := ModularForm Γ)),
  Sigma.mk (β := ModularForm Γ) i a = b
Tactic: obtain ⟨i, a⟩ := a
Cleared hypotheses: a, h, h2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
b : GradedMonoid (ModularForm Γ)
i : ℤ
a : ModularForm Γ i
h : (Sigma.mk (β := ModularForm Γ) i a).fst (β := ModularForm Γ) = b.fst (β := ModularForm Γ)
h2 : mcast h ((Sigma.mk (β := ModularForm Γ) i a).snd (β := ModularForm Γ)) ⋯ = b.snd (β := ModularForm Γ)
⊢ Sigma.mk (β := ModularForm Γ) i a = b
have refl : ∀ (a : ModularForm Γ b.1)
  (h2 : mcast sorry ((Sigma.mk (β := ModularForm Γ) b.1 a).snd (β := ModularForm Γ)) sorry = b.snd (β := ModularForm Γ)),
  Sigma.mk (β := ModularForm Γ) b.1 a = b
Tactic: cases h
Cleared hypotheses: i, a, h, h2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
⊢ (⇑(f.pow n) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n
have zero : (⇑(f.pow 0) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (β := ℕ) (⇑f : (a : ℍ) → ℂ) 0
Tactic: induction n with
  | zero => simp [pow]
  | succ n ih => simp_all only [pow, coe_mcast, coe_mul, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
zero : (⇑(f.pow 0) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (β := ℕ) (⇑f : (a : ℍ) → ℂ) 0
⊢ (⇑(f.pow n) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n
have succ : ∀ (n : ℕ) (ih : (⇑(f.pow n) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n),
  (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (n + 1)
Tactic: induction n with
  | zero => simp [pow]
  | succ n ih => simp_all only [pow, coe_mcast, coe_mul, pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
⊢ Sigma.mk (β := ModularForm Γ) (HSMul.hSMul (α := ℕ) 0 k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) 0 f) =
    Sigma.mk (β := ModularForm Γ) ((↑0 : ℤ) * k) (f.pow 0)
have zero : 1 = Sigma.mk (β := ModularForm Γ) ((↑0 : ℤ) * k) (f.pow 0)
Tactic: refine (GradedMonoid.GMonoid.gnpow_zero' ⟨k, f⟩).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
ih :
  Sigma.mk (β := ModularForm Γ) (n • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n f) =
    Sigma.mk (β := ModularForm Γ) ((↑n : ℤ) * k) (f.pow n)
⊢ Sigma.mk (β := ModularForm Γ) ((n + 1) • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) (n + 1) f) =
    Sigma.mk (β := ModularForm Γ) ((↑(n + 1) : ℤ) * k) (f.pow (n + 1))
have succ : Sigma.mk (β := ModularForm Γ) (n • (Sigma.mk (β := ModularForm Γ) k f).fst (β := ModularForm Γ))
      (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n
        ((Sigma.mk (β := ModularForm Γ) k f).snd (β := ModularForm Γ))) *
    Sigma.mk (β := ModularForm Γ) k f =
  Sigma.mk (β := ModularForm Γ) ((↑(n + 1) : ℤ) * k) (f.pow (n + 1))
Tactic: refine (GradedMonoid.GMonoid.gnpow_succ' n ⟨k, f⟩).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
ih :
  Sigma.mk (β := ModularForm Γ) (n • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n f) =
    Sigma.mk (β := ModularForm Γ) ((↑n : ℤ) * k) (f.pow n)
⊢ Sigma.mk (β := ModularForm Γ) (n • (Sigma.mk (β := ModularForm Γ) k f).fst (β := ModularForm Γ))
        (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n
          ((Sigma.mk (β := ModularForm Γ) k f).snd (β := ModularForm Γ))) *
      Sigma.mk (β := ModularForm Γ) k f =
    Sigma.mk (β := ModularForm Γ) ((↑(n + 1) : ℤ) * k) (f.pow (n + 1))
have succ : Sigma.mk (β := ModularForm Γ) ((↑n : ℤ) * k) (f.pow n) * Sigma.mk (β := ModularForm Γ) k f =
  Sigma.mk (β := ModularForm Γ) ((↑(n + 1) : ℤ) * k) (f.pow (n + 1))
Tactic: refine (congrArg (fun x : GradedMonoid (ModularForm Γ) ↦ x * ⟨k, f⟩) ih).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
⊢ Sigma.mk (β := ModularForm Γ) (n • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n f) =
    Sigma.mk (β := ModularForm Γ) ((↑n : ℤ) * k) (f.pow n)
have zero : Sigma.mk (β := ModularForm Γ) (HSMul.hSMul (α := ℕ) 0 k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) 0 f) =
  Sigma.mk (β := ModularForm Γ) ((↑0 : ℤ) * k) (f.pow 0)
Tactic: induction n with
  | zero =>
    refine (GradedMonoid.GMonoid.gnpow_zero' ⟨k, f⟩).trans ?_
    exact gradedMonoid_eq_of_cast (zero_mul k).symm (ModularForm.ext fun _ ↦ rfl)
  | succ n ih =>
    refine (GradedMonoid.GMonoid.gnpow_succ' n ⟨k, f⟩).trans ?_
    refine (congrArg (fun x : GradedMonoid (ModularForm Γ) ↦ x * ⟨k, f⟩) ih).trans ?_
    exact gradedMonoid_eq_of_cast (show ((n : ℤ) * k + k = (n + 1) * k) by ring)
      (ModularForm.ext fun _ ↦ rfl)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
zero :
  Sigma.mk (β := ModularForm Γ) (HSMul.hSMul (α := ℕ) 0 k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) 0 f) =
    Sigma.mk (β := ModularForm Γ) ((↑0 : ℤ) * k) (f.pow 0)
⊢ Sigma.mk (β := ModularForm Γ) (n • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n f) =
    Sigma.mk (β := ModularForm Γ) ((↑n : ℤ) * k) (f.pow n)
have succ : ∀ (n : ℕ)
  (ih :
    Sigma.mk (β := ModularForm Γ) (n • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) n f) =
      Sigma.mk (β := ModularForm Γ) ((↑n : ℤ) * k) (f.pow n)),
  Sigma.mk (β := ModularForm Γ) ((n + 1) • k) (GradedMonoid.GMonoid.gnpow (A := ModularForm Γ) (n + 1) f) =
    Sigma.mk (β := ModularForm Γ) ((↑(n + 1) : ℤ) * k) (f.pow (n + 1))
Tactic: induction n with
  | zero =>
    refine (GradedMonoid.GMonoid.gnpow_zero' ⟨k, f⟩).trans ?_
    exact gradedMonoid_eq_of_cast (zero_mul k).symm (ModularForm.ext fun _ ↦ rfl)
  | succ n ih =>
    refine (GradedMonoid.GMonoid.gnpow_succ' n ⟨k, f⟩).trans ?_
    refine (congrArg (fun x : GradedMonoid (ModularForm Γ) ↦ x * ⟨k, f⟩) ih).trans ?_
    exact gradedMonoid_eq_of_cast (show ((n : ℤ) * k + k = (n + 1) * k) by ring)
      (ModularForm.ext fun _ ↦ rfl)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
c : OnePoint ℝ
hc : IsCusp c Γ
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty = c
⊢ IsBoundedAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ m γ
      (toFun (Γ := Γ)
        (SlashInvariantForm.prod m hm fun (i : ι) ↦
          { toFun := (⇑(F i) : (a : ℍ) → ℂ), slash_action_eq' := ⋯ : SlashInvariantForm Γ (k i) })))
have simp : atImInfty.BoundedAtFilter
  (HSMul.hSMul (β := ℍ → ℂ)
    (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) γ) : ℝ)|
      (HSub.hSub (α := ℤ) (↑s.card : ℤ) 1))
    (∏ i ∈ s,
      @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) γ (⇑(F i) : (a : ℍ) → ℂ)))
Tactic: simp only [SlashInvariantForm.toFun_eq_coe, coe_prod, SlashInvariantForm.coe_mk, hm,
      prod_slash_sum_weights, IsBoundedAtImInfty]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
c : OnePoint ℝ
hc : IsCusp c Γ
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ OnePoint.infty = c
⊢ atImInfty.BoundedAtFilter
    (HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) γ) : ℝ)|
        (HSub.hSub (α := ℤ) (↑s.card : ℤ) 1))
      (∏ i ∈ s,
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) γ (⇑(F i) : (a : ℍ) → ℂ)))
have refine : ∀ i ∈ s,
  atImInfty.BoundedAtFilter (β := ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) γ (⇑(F i) : (a : ℍ) → ℂ))
Tactic: refine BoundedAtFilter.smul _ (BoundedAtFilter.prod (s := s) ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc :
  IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ)
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ ∞ = c
⊢ IsBoundedAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (SlashInvariantForm.translate f g).toFun)
have rw : (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞).IsBoundedAt (⇑f : (a : ℍ) → ℂ) k
Tactic: rw [SlashInvariantForm.toFun_eq_coe, SlashInvariantForm.coe_translate,
      ← SlashAction.slash_mul, ← isBoundedAt_infty_iff, ← OnePoint.IsBoundedAt.smul_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc :
  IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ)
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ ∞ = c
⊢ (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞).IsBoundedAt (⇑f : (a : ℍ) → ℂ) k
have apply : IsCusp (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞) Γ
Tactic: apply ModularFormClass.bdd_at_cusps f
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc :
  IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ)
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ ∞ = c
⊢ IsZeroAtImInfty
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (ModularForm.translate f g).toFun)
have rw : (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞).IsZeroAt (⇑f : (a : ℍ) → ℂ) k
Tactic: rw [SlashInvariantForm.toFun_eq_coe, ModularForm.toSlashInvariantForm_coe,
      ModularForm.coe_translate, ← SlashAction.slash_mul, ← isZeroAt_infty_iff,
      ← OnePoint.IsZeroAt.smul_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Basic (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
inst_1 : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc :
  IsCusp c
    (HSMul.hSMul (α := ConjAct (GL (Fin 2) ℝ))
      ((toConjAct : (a : GL (Fin 2) ℝ) → ConjAct (GL (Fin 2) ℝ)) g⁻¹ : ConjAct (GL (Fin 2) ℝ)) Γ)
γ : GL (Fin 2) ℝ
hγ : HSMul.hSMul (β := OnePoint ℝ) γ ∞ = c
⊢ (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞).IsZeroAt (⇑f : (a : ℍ) → ℂ) k
have apply : IsCusp (HSMul.hSMul (β := OnePoint ℝ) (g * γ) ∞) Γ
Tactic: apply CuspFormClass.zero_at_cusps f