awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
m : ℕ
⊢ Eq (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h 1) : ℂ)
    ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) 1 : ℂ)
have h1 : cuspFunction h 1 = 1
Tactic: have h1 : cuspFunction h 1 = 1 := by
    ext q
    rcases eq_or_ne q 0 with rfl | hq
    · simpa [cuspFunction, Periodic.cuspFunction] using tendsto_const_nhds.limUnder_eq
    · simp [cuspFunction, Periodic.cuspFunction_eq_of_nonzero h _ hq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
h : ℝ
m : ℕ
h1 : cuspFunction h 1 = 1
⊢ Eq (α := ℂ) ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h 1) : ℂ)
    ((PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) 1 : ℂ)
have h2 : Eq (α := ℂ) (iteratedDeriv (𝕜 := ℂ) m 1 0) (if m = 0 then 1 else 0)
Tactic: have h2 : iteratedDeriv m (1 : ℂ → ℂ) 0 = if m = 0 then 1 else 0 := by
    simpa [ite_apply] using iteratedDeriv_const
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
k : ℤ
f : ModularForm Γ k
⊢ qExpansion h (⇑f : (a : ℍ) → ℂ) = 0 ↔ f = 0
have this : Fact (IsCusp OnePoint.infty Γ)
Tactic: have : Fact (IsCusp OnePoint.infty Γ) := ⟨Γ.isCusp_of_mem_strictPeriods hh hΓ⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n
⊢ qExpansion h (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
have succ : qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (n + 1)) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
Tactic: rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n
succ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (n + 1)) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
⊢ qExpansion h (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
have succ₁ : qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n * (⇑f : (a : ℍ) → ℂ)) =
  qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
Tactic: rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n
succ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (n + 1)) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₁ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n * (⇑f : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
⊢ qExpansion h (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
have succ₂ : qExpansion h (HMul.hMul (α := (a : ℍ) → ℂ) (⇑(f.pow n) : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ)) =
  qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
Tactic: rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n
succ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (n + 1)) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₁ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n * (⇑f : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₂ :
  qExpansion h (HMul.hMul (α := (a : ℍ) → ℂ) (⇑(f.pow n) : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
⊢ qExpansion h (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
have succ₃ : qExpansion h (⇑((f.pow n).mul f) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
Tactic: rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n
succ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (n + 1)) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₁ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n * (⇑f : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₂ :
  qExpansion h (HMul.hMul (α := (a : ℍ) → ℂ) (⇑(f.pow n) : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₃ : qExpansion h (⇑((f.pow n).mul f) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
⊢ qExpansion h (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
have succ₄ : qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) * qExpansion h (⇑f : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
Tactic: rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n
succ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (n + 1)) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₁ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n * (⇑f : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₂ :
  qExpansion h (HMul.hMul (α := (a : ℍ) → ℂ) (⇑(f.pow n) : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₃ : qExpansion h (⇑((f.pow n).mul f) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₄ :
  qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) * qExpansion h (⇑f : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
⊢ qExpansion h (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
have succ₅ : qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n * qExpansion h (⇑f : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
Tactic: rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
ih : qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n
succ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (n + 1)) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₁ :
  qExpansion h (HPow.hPow (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) n * (⇑f : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₂ :
  qExpansion h (HMul.hMul (α := (a : ℍ) → ℂ) (⇑(f.pow n) : (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ)) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₃ : qExpansion h (⇑((f.pow n).mul f) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₄ :
  qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) * qExpansion h (⇑f : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
succ₅ :
  qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n * qExpansion h (⇑f : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
⊢ qExpansion h (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
have succ₆ : qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n * qExpansion h (⇑f : (a : ℍ) → ℂ) =
  qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n * qExpansion h (⇑f : (a : ℍ) → ℂ)
Tactic: rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
⊢ qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n
have zero : qExpansion h (⇑(f.pow 0) : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) 0
Tactic: induction n with
  | zero => simp only [coe_pow, pow_zero, qExpansion_one]
  | succ n ih =>
    rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (goal)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
zero : qExpansion h (⇑(f.pow 0) : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion h (⇑f : (a : ℍ) → ℂ)) 0
⊢ qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n
have succ : ∀ (n : ℕ) (ih : qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n),
  qExpansion h (⇑(f.pow (n + 1)) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ (n + 1)
Tactic: induction n with
  | zero => simp only [coe_pow, pow_zero, qExpansion_one]
  | succ n ih =>
    rw [coe_pow, pow_succ, ← coe_pow, ← coe_mul, ModularForm.qExpansion_mul hh hΓ, ih,
      pow_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
⊢ qExpansion h
      (⇑((HPow.hPow (α := DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i)
                ((DirectSum.of (ModularForm Γ) k : (a : ModularForm Γ k) → DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i)
                    f :
                  DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i)
                n :
              (a : ℤ) → ModularForm Γ a)
            ((↑n : ℤ) * k)) :
        (a : ℍ) → ℂ) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n
have this : (qExpansionRingHom h hh hΓ : (a : DirectSum ℤ fun (k : ℤ) ↦ ModularForm Γ k) → PowerSeries ℂ)
    (HPow.hPow (α := DirectSum ℤ fun (k : ℤ) ↦ ModularForm Γ k)
      ((DirectSum.of (ModularForm Γ) k : (a : ModularForm Γ k) → DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i) f :
        DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i)
      n) =
  HPow.hPow (α := PowerSeries ℂ)
    ((qExpansionRingHom h hh hΓ : (a : DirectSum ℤ fun (k : ℤ) ↦ ModularForm Γ k) → PowerSeries ℂ)
        ((DirectSum.of (ModularForm Γ) k : (a : ModularForm Γ k) → DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i) f :
          DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i) :
      PowerSeries ℂ)
    n
Tactic: have := (qExpansionRingHom h hh hΓ).map_pow (DirectSum.of _ k f) n
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h (⇑f : (a : ℍ) → ℂ)) 0
hf : ∀ (τ : ℍ), HasSum (α := ℂ) (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) ((f : (a : ℍ) → ℂ) τ : ℂ)
⊢ HasFPowerSeriesOnBall (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (qExpansionFormalMultilinearSeries h f) 0 1
have h1 : HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (FormalMultilinearSeries.ofScalars ℂ c) 0
Tactic: have h1 := (hasFPowerSeriesOnBall_cuspFunction hh hfanalytic hf).hasFPowerSeriesAt
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h (⇑f : (a : ℍ) → ℂ)) 0
hf : ∀ (τ : ℍ), HasSum (α := ℂ) (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) ((f : (a : ℍ) → ℂ) τ : ℂ)
h1 : HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (FormalMultilinearSeries.ofScalars ℂ c) 0
⊢ HasFPowerSeriesOnBall (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (qExpansionFormalMultilinearSeries h f) 0 1
have h2 : HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (qExpansionFormalMultilinearSeries h f) 0
Tactic: have h2 : HasFPowerSeriesAt (cuspFunction h f) (qExpansionFormalMultilinearSeries h f) 0 := by
    simpa [qExpansionFormalMultilinearSeries, qExpansion_coeff, div_eq_mul_inv, mul_comm]
      using hfanalytic.hasFPowerSeriesAt
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h (⇑f : (a : ℍ) → ℂ)) 0
hf : ∀ (τ : ℍ), HasSum (α := ℂ) (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) ((f : (a : ℍ) → ℂ) τ : ℂ)
m : ℕ
⊢ c m = (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ))
have h1 : HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (FormalMultilinearSeries.ofScalars ℂ c) 0
Tactic: have h1 := (hasFPowerSeriesOnBall_cuspFunction hh hfanalytic hf).hasFPowerSeriesAt
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.QExpansion (hypothesis)
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
h : ℝ
f : F
c : ℕ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h (⇑f : (a : ℍ) → ℂ)) 0
hf : ∀ (τ : ℍ), HasSum (α := ℂ) (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) ((f : (a : ℍ) → ℂ) τ : ℂ)
m : ℕ
h1 : HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (FormalMultilinearSeries.ofScalars ℂ c) 0
⊢ c m = (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ))
have h2 : HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (qExpansionFormalMultilinearSeries h f) 0
Tactic: have h2 := (hasFPowerSeries_cuspFunction f hh hfanalytic hf).hasFPowerSeriesAt
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
β : Type u_1
G : Type u_2
α : Type u_3
inst : Monoid G
inst_1 : AddGroup α
inst_2 : SlashAction β G α
k : β
g : G
a : α
⊢ @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (-a) + @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g a = 0
have rw : @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (-a + a) = 0
Tactic: rw [← add_slash, neg_add_cancel, zero_slash]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
β : Type u_1
G : Type u_2
α : Type u_3
inst : Monoid G
inst_1 : AddGroup α
inst_2 : SlashAction β G α
k : β
g : G
a : α
rw : @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (-a + a) = 0
⊢ @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (-a) + @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g a = 0
have rw₁ : Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g 0) 0
Tactic: rw [← add_slash, neg_add_cancel, zero_slash]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
β : Type u_1
G : Type u_2
α : Type u_3
inst : Monoid G
inst_1 : AddGroup α
inst_2 : SlashAction β G α
k : β
g : G
a : α
rw : @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (-a + a) = 0
rw₁ : Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g 0) 0
⊢ @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (-a) + @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g a = 0
have rw₂ : Eq.{u_3 + 1} (α := α) 0 0
Tactic: rw [← add_slash, neg_add_cancel, zero_slash]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
β : Type u_1
G : Type u_2
α : Type u_3
ι : Type u_4
inst : Monoid G
inst_1 : AddCommGroup α
inst_2 : SlashAction β G α
k : β
g : G
a : ι → α
s : Finset ι
⊢ Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ s, a i))
    (∑ i ∈ s, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))
have empty : Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ ∅, a i))
  (∑ i ∈ ∅, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i t hi IH => simp [hi, IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
β : Type u_1
G : Type u_2
α : Type u_3
ι : Type u_4
inst : Monoid G
inst_1 : AddCommGroup α
inst_2 : SlashAction β G α
k : β
g : G
a : ι → α
s : Finset ι
empty :
  Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ ∅, a i))
    (∑ i ∈ ∅, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))
⊢ Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ s, a i))
    (∑ i ∈ s, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))
have insert : ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
  (IH :
    Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ t, a i))
      (∑ i ∈ t, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))),
  Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ insert i t, a i))
    (∑ i ∈ insert i t, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i t hi IH => simp [hi, IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
β : Type u_1
G : Type u_2
α : Type u_3
ι : Type u_4
inst : Monoid G
inst_1 : AddCommGroup α
inst_2 : SlashAction β G α
k : β
g : G
a : ι → α
s : Finset ι
⊢ Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ s, a i))
    (∑ i ∈ s, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))
have empty : Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ ∅, a i))
  (∑ i ∈ ∅, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i t hi IH => simp [hi, IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
β : Type u_1
G : Type u_2
α : Type u_3
ι : Type u_4
inst : Monoid G
inst_1 : AddCommGroup α
inst_2 : SlashAction β G α
k : β
g : G
a : ι → α
s : Finset ι
empty :
  Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ ∅, a i))
    (∑ i ∈ ∅, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))
⊢ Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ s, a i))
    (∑ i ∈ s, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))
have insert : ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
  (IH :
    Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ t, a i))
      (∑ i ∈ t, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))),
  Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ insert i t, a i))
    (∑ i ∈ insert i t, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i t hi IH => simp [hi, IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
β : Type u_1
G : Type u_2
α : Type u_3
inst : Group G
inst_1 : AddGroup α
inst_2 : SlashAction β G α
k : β
g : G
a : α
⊢ @map _ _ _ DivInvMonoid.toMonoid SubNegMonoid.toAddMonoid _ k g a = 0 ↔ a = 0
have refine : ∀ (h : @map _ _ _ DivInvMonoid.toMonoid SubNegMonoid.toAddMonoid _ k g a = 0), a = 0
Tactic: refine ⟨fun h ↦ ?_, by simp +contextual⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (hypothesis)
Goal:
β : Type u_1
G : Type u_2
α : Type u_3
inst : Group G
inst_1 : AddGroup α
inst_2 : SlashAction β G α
k : β
g : G
a : α
h : @map _ _ _ DivInvMonoid.toMonoid SubNegMonoid.toAddMonoid _ k g a = 0
⊢ a = 0
have h₁ : @map _ _ _ DivInvMonoid.toMonoid SubNegMonoid.toAddMonoid _ k g⁻¹
    (@map _ _ _ DivInvMonoid.toMonoid SubNegMonoid.toAddMonoid _ k g a) =
  @map _ _ _ DivInvMonoid.toMonoid SubNegMonoid.toAddMonoid _ k g⁻¹ 0
Tactic: apply_fun (· ∣[k] g⁻¹) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
⊢ f ∣[k] (A * B) = (f ∣[k] A) ∣[k] B
have h : ∀ (τ : ℍ), (f ∣[k] (A * B)) τ = ((f ∣[k] A) ∣[k] B) τ
Tactic: ext1 τ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ HMul.hMul (α := ℂ) ((σ (A * B) : (a : ℂ) → ℂ) (f ((A * B) • τ)) : ℂ)
        ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) (A * B)) : ℝ)| : ℂ) ^ (k - 1)) *
      denom (A * B) (↑τ : ℂ) ^ (-k) =
    HMul.hMul (α := ℂ) ((σ B : (a : ℂ) → ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • B • τ)) : ℂ) : ℂ)
        ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k - 1) *
          (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) B) : ℝ)| : ℂ) ^ (k - 1)) *
      HMul.hMul (α := ℂ) ((σ B : (a : ℂ) → ℂ) (denom A (↑(B • τ) : ℂ) ^ (-k)) : ℂ) (denom B (↑τ : ℂ) ^ (-k))
have rw : HMul.hMul (α := ℂ) ((σ (A * B) : (a : ℂ) → ℂ) (f ((A * B) • τ)) : ℂ)
      ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) (A * B)) : ℝ)| : ℂ) ^ (k - 1)) *
    denom (A * B) (↑τ : ℂ) ^ (-k) =
  HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) ((σ B : (a : ℂ) → ℂ) (f (A • B • τ)) : ℂ) : ℂ)
      ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k - 1) *
        (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) B) : ℝ)| : ℂ) ^ (k - 1)) *
    HMul.hMul (α := ℂ) ((σ B : (a : ℂ) → ℂ) (denom A (↑(B • τ) : ℂ) ^ (-k)) : ℂ) (denom B (↑τ : ℂ) ^ (-k))
Tactic: rw [σ_mul_comm, σ_mul, denom_cocycle_σ, mul_zpow, mul_smul, map_mul, Units.val_mul,
      abs_mul, ofReal_mul, mul_zpow, map_zpow₀]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
rw :
  HMul.hMul (α := ℂ) ((σ (A * B) : (a : ℂ) → ℂ) (f ((A * B) • τ)) : ℂ)
        ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) (A * B)) : ℝ)| : ℂ) ^ (k - 1)) *
      denom (A * B) (↑τ : ℂ) ^ (-k) =
    HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) ((σ B : (a : ℂ) → ℂ) (f (A • B • τ)) : ℂ) : ℂ)
        ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k - 1) *
          (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) B) : ℝ)| : ℂ) ^ (k - 1)) *
      HMul.hMul (α := ℂ) ((σ B : (a : ℂ) → ℂ) (denom A (↑(B • τ) : ℂ) ^ (-k)) : ℂ) (denom B (↑τ : ℂ) ^ (-k))
⊢ HMul.hMul (α := ℂ) ((σ (A * B) : (a : ℂ) → ℂ) (f ((A * B) • τ)) : ℂ)
        ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) (A * B)) : ℝ)| : ℂ) ^ (k - 1)) *
      denom (A * B) (↑τ : ℂ) ^ (-k) =
    HMul.hMul (α := ℂ) ((σ B : (a : ℂ) → ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • B • τ)) : ℂ) : ℂ)
        ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k - 1) *
          (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) B) : ℝ)| : ℂ) ^ (k - 1)) *
      HMul.hMul (α := ℂ) ((σ B : (a : ℂ) → ℂ) (denom A (↑(B • τ) : ℂ) ^ (-k)) : ℂ) (denom B (↑τ : ℂ) ^ (-k))
have rw₁ : HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) ((σ B : (a : ℂ) → ℂ) (f ((A * B) • τ)) : ℂ) : ℂ)
      ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) (A * B)) : ℝ)| : ℂ) ^ (k - 1)) *
    denom (A * B) (↑τ : ℂ) ^ (-k) =
  HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) ((σ B : (a : ℂ) → ℂ) (f (A • B • τ)) : ℂ) : ℂ)
      ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k - 1) *
        (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) B) : ℝ)| : ℂ) ^ (k - 1)) *
    HMul.hMul (α := ℂ) ((σ B : (a : ℂ) → ℂ) (denom A (↑(B • τ) : ℂ) ^ (-k)) : ℂ) (denom B (↑τ : ℂ) ^ (-k))
Tactic: rw [σ_mul_comm, σ_mul, denom_cocycle_σ, mul_zpow, mul_smul, map_mul, Units.val_mul,
      abs_mul, ofReal_mul, mul_zpow, map_zpow₀]