awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
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)
⊢ qExpansion h (⇑(f.pow n) : (a : ℍ) → ℂ) = qExpansion h (⇑f : (a : ℍ) → ℂ) ^ n

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]

Premises used: ModularForm.coe_mul, UpperHalfPlane.qExpansion_one, pow_succ, ModularForm.coe_pow, pow_zero, ModularForm.qExpansion_mul
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
k : ℤ
f : ModularForm Γ k
⊢ (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) =
    qExpansion h (⇑f : (a : ℍ) → ℂ)

Tactic:
DirectSum.toSemiring_of ..

Premises used: UpperHalfPlane.qExpansion, DirectSum.toSemiring_of, PowerSeries.mk
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
a b : ℤ
f : ModularForm Γ a
g : ModularForm Γ b
⊢ qExpansion h
      (⇑((HMul.hMul (α := DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i) (β := DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i)
                ((DirectSum.of (ModularForm Γ) a : (a : ModularForm Γ a) → DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i)
                    f :
                  DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i)
                ((DirectSum.of (ModularForm Γ) b : (a : ModularForm Γ b) → DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i)
                    g :
                  DirectSum ℤ fun (i : ℤ) ↦ ModularForm Γ i) :
              (a : ℤ) → ModularForm Γ a)
            (a + b)) :
        (a : ℍ) → ℂ) =
    qExpansion h (⇑f : (a : ℍ) → ℂ) * qExpansion h (⇑g : (a : ℍ) → ℂ)

Tactic:
simpa [DirectSum.of_mul_of] using ModularForm.qExpansion_mul hh hΓ f g

Premises used: DirectSum.of_mul_of, ModularForm.qExpansion_mul
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
⊢ (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
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
inst : Γ.HasDetPlusMinusOne
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : ModularForm Γ k
n : ℕ
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
⊢ 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

Tactic:
simpa [DirectSum.ofPow]

Premises used: DirectSum.ofPow
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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 : ℍ) → ℂ) τ : ℂ)
⊢ HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (FormalMultilinearSeries.ofScalars ℂ c) 0

Tactic:
have h1 := (hasFPowerSeriesOnBall_cuspFunction hh hfanalytic hf).hasFPowerSeriesAt
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
⊢ HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (qExpansionFormalMultilinearSeries h f) 0

Tactic:
simpa [qExpansionFormalMultilinearSeries, qExpansion_coeff, div_eq_mul_inv, mul_comm]
      using hfanalytic.hasFPowerSeriesAt

Premises used: UpperHalfPlane.qExpansionFormalMultilinearSeries, UpperHalfPlane.qExpansion_coeff, div_eq_mul_inv, AnalyticAt.hasFPowerSeriesAt, mul_comm
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
⊢ 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
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
h2 : HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (qExpansionFormalMultilinearSeries h f) 0
⊢ HasFPowerSeriesOnBall (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (qExpansionFormalMultilinearSeries h f) 0 1

Tactic:
simpa [h1.eq_formalMultilinearSeries h2] using hasFPowerSeriesOnBall_cuspFunction hh hfanalytic hf

Premises used: HasFPowerSeriesAt.eq_formalMultilinearSeries, UpperHalfPlane.hasFPowerSeriesOnBall_cuspFunction
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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 : ℕ
⊢ HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (FormalMultilinearSeries.ofScalars ℂ c) 0

Tactic:
have h1 := (hasFPowerSeriesOnBall_cuspFunction hh hfanalytic hf).hasFPowerSeriesAt
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
⊢ HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (qExpansionFormalMultilinearSeries h f) 0

Tactic:
have h2 := (hasFPowerSeries_cuspFunction f hh hfanalytic hf).hasFPowerSeriesAt
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
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
h2 : HasFPowerSeriesAt (cuspFunction h (⇑f : (a : ℍ) → ℂ)) (qExpansionFormalMultilinearSeries h f) 0
⊢ c m = (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ))

Tactic:
simpa using congr_arg (FormalMultilinearSeries.coeff · m) (h1.eq_formalMultilinearSeries h2)

Premises used: FormalMultilinearSeries.coeff, HasFPowerSeriesAt.eq_formalMultilinearSeries, congr_arg
-- Module: Mathlib.NumberTheory.ModularForms.QExpansion
Goal:
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
c : ℕ → ℂ
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
f : F
inst_1 : ModularFormClass F Γ k
hf : ∀ (τ : ℍ), HasSum (α := ℂ) (fun (m : ℕ) ↦ c m • 𝕢 h (↑τ : ℂ) ^ m) ((f : (a : ℍ) → ℂ) τ : ℂ)
m : ℕ
⊢ c m = (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion h (⇑f : (a : ℍ) → ℂ))

Tactic:
qExpansion_coeff_unique f hh (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ) hf m

Premises used: UpperHalfPlane.qExpansion_coeff_unique, ModularFormClass.analyticAt_cuspFunction_zero
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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
rw₂ rw₃ : Eq.{u_3 + 1} (α := α) 0 0
⊢ @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (-a) + @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g a = 0

Tactic:
rw [← add_slash, neg_add_cancel, zero_slash]

Premises used: SlashAction.zero_slash, neg_add_cancel, SlashAction.add_slash
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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 : ι → α
⊢ Eq.{u_3 + 1} (α := α) (@map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (∑ i ∈ ∅, a i))
    (∑ i ∈ ∅, @map _ _ _ inst SubNegMonoid.toAddMonoid _ k g (a i))

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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 : ι → α
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:
simp [hi, IH]
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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))
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.insert i t, a i))
      (∑ i ∈ Insert.insert i t, @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))

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i t hi IH => simp [hi, IH]

Premises used: Insert.insert
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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))
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.insert i t, a i))
      (∑ i ∈ Insert.insert i t, @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))

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i t hi IH => simp [hi, IH]

Premises used: Insert.insert
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
β : Type u_1
G : Type u_2
H : Type u_3
α : Type u_4
inst : Monoid G
inst_1 : AddMonoid α
inst_2 : Monoid H
inst_3 : SlashAction β G α
h : H →* G
k : β
a : α
⊢ @SlashAction.map.{u_1, u_2, u_4} _ G _ inst inst_1 _ k ((h : (a : H) → G) 1 : G) a = a

Tactic:
simp only [map_one, SlashAction.slash_one]

Premises used: SlashAction.slash_one, map_one
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
β : Type u_1
G : Type u_2
H : Type u_3
α : Type u_4
inst : Monoid G
inst_1 : AddMonoid α
inst_2 : Monoid H
inst_3 : SlashAction β G α
h : H →* G
k : β
g gg : H
a : α
⊢ @SlashAction.map.{u_1, u_2, u_4} _ G _ inst inst_1 _ k ((h : (a : H) → G) (g * gg) : G) a =
    @SlashAction.map.{u_1, u_2, u_4} _ G _ inst inst_1 _ k ((h : (a : H) → G) gg : G)
      (@SlashAction.map.{u_1, u_2, u_4} _ G _ inst inst_1 _ k ((h : (a : H) → G) g : G) a)

Tactic:
simp only [map_mul, SlashAction.slash_mul]

Premises used: map_mul, SlashAction.slash_mul
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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 : α
⊢ a = 0 → @map _ _ _ DivInvMonoid.toMonoid SubNegMonoid.toAddMonoid _ k g a = 0

Tactic:
simp +contextual
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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 : α
refine : ∀ (h : @map _ _ _ DivInvMonoid.toMonoid SubNegMonoid.toAddMonoid _ k g a = 0), a = 0
⊢ @map _ _ _ DivInvMonoid.toMonoid SubNegMonoid.toAddMonoid _ k g a = 0 ↔ a = 0

Tactic:
refine ⟨fun h ↦ ?_, by simp +contextual⟩
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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
⊢ @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

Premises used: SlashAction.map, Inv.inv
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
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⁻¹
      (@map _ _ _ DivInvMonoid.toMonoid SubNegMonoid.toAddMonoid _ k g a) =
    @map _ _ _ DivInvMonoid.toMonoid SubNegMonoid.toAddMonoid _ k g⁻¹ 0
⊢ a = 0

Tactic:
simpa [← SlashAction.slash_mul] using h

Premises used: SlashAction.slash_mul
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
h : ∀ (τ : ℍ), (f ∣[k] (A * B)) τ = ((f ∣[k] A) ∣[k] B) τ
⊢ f ∣[k] (A * B) = (f ∣[k] A) ∣[k] B

Tactic:
ext1 τ
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
rw :
  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)) *
      (HPow.hPow (α := ℂ) ((σ B : (a : ℂ) → ℂ) (denom A (↑(B • τ) : ℂ)) : ℂ) (-k) * denom B (↑τ : ℂ) ^ (-k)) =
    HMul.hMul (α := ℂ) ((σ B : (a : ℂ) → ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • B • τ)) : ℂ) : ℂ)
            ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k - 1)) *
          HPow.hPow (α := ℂ) ((σ B : (a : ℂ) → ℂ) (denom A (↑(B • τ) : ℂ)) : ℂ) (-k) *
        (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) B) : ℝ)| : ℂ) ^ (k - 1) *
      denom 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)) =
    HMul.hMul (α := ℂ)
        ((σ B : (a : ℂ) → ℂ)
            (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • B • τ)) : ℂ)
                ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k - 1)) *
              denom A (↑(B • τ) : ℂ) ^ (-k)) :
          ℂ)
        ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) B) : ℝ)| : ℂ) ^ (k - 1)) *
      denom B (↑τ : ℂ) ^ (-k)

Tactic:
rw [map_mul, map_zpow₀, map_mul, map_zpow₀, σ_ofReal]

Premises used: map_mul, UpperHalfPlane.σ_ofReal, map_zpow₀
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ 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)) *
      (HPow.hPow (α := ℂ) ((σ B : (a : ℂ) → ℂ) (denom A (↑(B • τ) : ℂ)) : ℂ) (-k) * denom B (↑τ : ℂ) ^ (-k)) =
    HMul.hMul (α := ℂ) ((σ B : (a : ℂ) → ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • B • τ)) : ℂ) : ℂ)
            ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k - 1)) *
          HPow.hPow (α := ℂ) ((σ B : (a : ℂ) → ℂ) (denom A (↑(B • τ) : ℂ)) : ℂ) (-k) *
        (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) B) : ℝ)| : ℂ) ^ (k - 1) *
      denom B (↑τ : ℂ) ^ (-k)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ HMul.hMul (α := ℂ)
        ((σ B : (a : ℂ) → ℂ)
            (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • B • τ)) : ℂ)
                ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k - 1)) *
              denom A (↑(B • τ) : ℂ) ^ (-k)) :
          ℂ)
        ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) B) : ℝ)| : ℂ) ^ (k - 1)) *
      denom B (↑τ : ℂ) ^ (-k) =
    ((f ∣[k] A) ∣[k] B) τ

Tactic:
rfl

Premises used: _private.0.ModularForm.privateSlash, rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
calc :
  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))
calc₁ :
  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)) =
    HMul.hMul (α := ℂ)
        ((σ B : (a : ℂ) → ℂ)
            (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • B • τ)) : ℂ)
                ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k - 1)) *
              denom A (↑(B • τ) : ℂ) ^ (-k)) :
          ℂ)
        ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) B) : ℝ)| : ℂ) ^ (k - 1)) *
      denom B (↑τ : ℂ) ^ (-k)
⊢ (f ∣[k] (A * B)) τ = ((f ∣[k] A) ∣[k] B) τ

Tactic:
calc σ (A * B) (f ((A * B) • τ)) * |(A * B).det.val| ^ (k - 1) * denom (A * B) τ ^ (-k)
  _ = σ B (σ A (f (A • B • τ))) * (|A.det.val| ^ (k - 1) * |B.det.val| ^ (k - 1)) *
      (((σ B) (denom A ↑(B • τ) ^ (-k))) * denom B τ ^ (-k)) := by
    rw [σ_mul_comm, σ_mul, denom_cocycle_σ, mul_zpow, mul_smul, map_mul, Units.val_mul,
      abs_mul, ofReal_mul, mul_zpow, map_zpow₀]
  _ = σ B (σ A (f (A • B • τ)) * |A.det.val| ^ (k - 1) * (denom A ↑(B • τ) ^ (-k)))
        * |B.det.val| ^ (k - 1) * denom B τ ^ (-k) := by
     rw [map_mul, map_zpow₀, map_mul, map_zpow₀, σ_ofReal]
     ring
  _ = ((f ∣[k] A) ∣[k] B) τ := rfl

Premises used: Units.val, HMul.hMul, UpperHalfPlane.coe, abs, HSub.hSub, Complex.ofReal, UpperHalfPlane.denom, HPow.hPow, HSMul.hSMul, _private.0.ModularForm.privateSlash, UpperHalfPlane.σ, OfNat.ofNat, Matrix.GeneralLinearGroup.det, DFunLike.coe, Neg.neg, rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
h : ∀ (τ : ℍ), ((f + g) ∣[k] A) τ = (f ∣[k] A + g ∣[k] A) τ
⊢ (f + g) ∣[k] A = f ∣[k] A + g ∣[k] A

Tactic:
ext1 τ
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
τ : ℍ
⊢ ((f + g) ∣[k] A) τ = (f ∣[k] A + g ∣[k] A) τ

Tactic:
simp [privateSlash, add_mul]

Premises used: add_mul, _private.0.ModularForm.privateSlash
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
⊢ ∀ (x : ℍ), (f ∣[k] 1) x = f x

Tactic:
simp [privateSlash, σ, denom]

Premises used: UpperHalfPlane.denom, _private.0.ModularForm.privateSlash, UpperHalfPlane.σ
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
A : GL (Fin 2) ℝ
x : ℍ
⊢ (0 ∣[k] A) x = 0 x

Tactic:
simp [privateSlash]

Premises used: _private.0.ModularForm.privateSlash
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
g : GL (Fin 2) ℝ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f = fun (τ : ℍ) ↦
    HMul.hMul (α := ℂ) ((σ g : (a : ℂ) → ℂ) (f (g • τ)) : ℂ)
        ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| : ℂ) ^ (k - 1)) *
      denom g (↑τ : ℂ) ^ (-k)

Tactic:
rfl

Premises used: _private.0.ModularForm.privateSlash, rfl