awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ k * (↑(#s) : ℤ) = ∑ i ∈ s, k

Tactic:
have : k * (#s) = ∑ i ∈ s, k := by
    rw [Finset.sum_const, nsmul_eq_mul']
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
this : k * (↑(#s) : ℤ) = ∑ i ∈ s, k
rw :
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ s, k) g (∏ i ∈ s, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#s) : ℤ) 1))
      (∏ i ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (f i))
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k * (↑(#s) : ℤ)) g (∏ i ∈ s, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#s) : ℤ) 1))
      (∏ i ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (f i))

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
this : k * (↑(#s) : ℤ) = ∑ i ∈ s, k
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ s, k) g (∏ i ∈ s, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#s) : ℤ) 1))
      (∏ i ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (f i))

Tactic:
prod_slash_sum_weights

Premises used: ModularForm.prod_slash_sum_weights
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
ι : Type u_1
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
this : k * (↑(#s) : ℤ) = ∑ i ∈ s, k
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ s, k) g (∏ i ∈ s, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(#s) : ℤ) 1))
      (∏ i ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (f i))

Tactic:
exact prod_slash_sum_weights

Premises used: ModularForm.prod_slash_sum_weights
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
⊢ 0 < Fintype.card ι

Tactic:
have : 0 < Fintype.card ι := Fintype.card_pos
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : Nonempty ι
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
this : 0 < Fintype.card ι
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k * (↑(Fintype.card ι) : ℤ)) g
      (∏ i : ι, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| (Fintype.card ι - 1))
      (∏ i : ι, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g (f i))

Tactic:
simpa [← zpow_natCast, this] using ModularForm.prod_slash (s := (.univ : Finset ι))

Premises used: zpow_natCast, ModularForm.prod_slash
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : SlashInvariantForm Γ k
h : f.toFun = g.toFun
mk :
  ∀ (toFun : ℍ → ℂ)
    (slash_action_eq' :
      ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ toFun = toFun)
    (h : { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k }.toFun = g.toFun),
    { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : SlashInvariantForm Γ k
toFun : ℍ → ℂ
slash_action_eq' :
  ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ toFun = toFun
h : { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k }.toFun = g.toFun
mk :
  ∀ (toFun_1 : ℍ → ℂ)
    (slash_action_eq'_1 :
      ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ toFun_1 = toFun_1)
    (h :
      { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k }.toFun =
        { toFun := toFun_1, slash_action_eq' := slash_action_eq'_1 : SlashInvariantForm Γ k }.toFun),
    { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k } =
      { toFun := toFun_1, slash_action_eq' := slash_action_eq'_1 }
⊢ { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k } = g

Tactic:
cases g
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toFun : ℍ → ℂ
slash_action_eq' :
  ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ toFun = toFun
toFun_1 : ℍ → ℂ
slash_action_eq'_1 :
  ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ toFun_1 = toFun_1
h :
  { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k }.toFun =
    { toFun := toFun_1, slash_action_eq' := slash_action_eq'_1 : SlashInvariantForm Γ k }.toFun
⊢ { toFun := toFun, slash_action_eq' := slash_action_eq' : SlashInvariantForm Γ k } =
    { toFun := toFun_1, slash_action_eq' := slash_action_eq'_1 }

Tactic:
congr
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : SlashInvariantForm Γ k
⊢ f.toFun = (⇑f : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : ℍ → ℂ
hf : ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
⊢ (⇑{ toFun := f, slash_action_eq' := hf : SlashInvariantForm Γ k } : (a : ℍ) → ℂ) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : SlashInvariantForm Γ k
h : ∀ (x : ℍ), Eq (α := ℂ) ((f : (a : ℍ) → ℂ) x : ℂ) ((g : (a : ℍ) → ℂ) x : ℂ)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ Eq (α := (a : ℍ) → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ))
    (⇑f : (a : ℍ) → ℂ)

Tactic:
SlashInvariantFormClass.slash_action_eq f γ hγ

Premises used: SlashInvariantFormClass.slash_action_eq
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : Γ.HasDetOne
inst_2 : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
⊢ (f : (a : ℍ) → ℂ) (γ • z) = HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (denom γ (↑z : ℂ) ^ k)

Tactic:
simpa [slash_def, σ, mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ (denom_ne_zero _ _)),
      Subgroup.HasDetOne.det_eq hγ] using congr_fun (slash_action_eqn f γ hγ) z

Premises used: Subgroup.HasDetOne.det_eq, mul_inv_eq_iff_eq_mul₀, ModularForm.slash_def, zpow_ne_zero, UpperHalfPlane.σ, congr_fun, SlashInvariantForm.slash_action_eqn, UpperHalfPlane.denom_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : Γ.HasDetOne
inst_2 : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
⊢ (f : (a : ℍ) → ℂ) (γ • z) = HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (denom γ (↑z : ℂ) ^ k)

Tactic:
have : f (γ • z) = f z * denom γ z ^ k := by
    simpa [slash_def, σ, mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ (denom_ne_zero _ _)),
      Subgroup.HasDetOne.det_eq hγ] using congr_fun (slash_action_eqn f γ hγ) z
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : Γ.HasDetOne
inst_2 : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
this : (f : (a : ℍ) → ℂ) (γ • z) = HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (denom γ (↑z : ℂ) ^ k)
rw :
  HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (denom γ (↑z : ℂ) ^ k) =
    HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ)
rw₁ :
  HMul.hMul (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k) =
    HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ)
rw₂ rw₃ :
  HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ) =
    HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ (f : (a : ℍ) → ℂ) (γ • z) =
    HMul.hMul (β := ℂ)
      (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) ^ k)
      ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rw [this, denom, mul_comm]

Premises used: UpperHalfPlane.denom, mul_comm
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : Γ.HasDetOne
inst_2 : SlashInvariantFormClass F Γ k
f : F
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
z : ℍ
⊢ (f : (a : ℍ) → ℂ) (γ • z) = HMul.hMul (β := ℂ) (denom γ (↑z : ℂ) ^ k) ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
SlashInvariantForm.slash_action_eqn' f hγ z

Premises used: UpperHalfPlane.denom, SlashInvariantForm.slash_action_eqn'
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
inst_1 : SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k
f : F
γ : SL(2, ℤ)
hγ : γ ∈ Γ
z : ℍ
⊢ Membership.mem (α := GL (Fin 2) ℝ) (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ)
    ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ)

Tactic:
simpa using hγ
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
f g : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  HAdd.hAdd (α := ℍ → ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ))
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑g : (a : ℍ) → ℂ)) =
    HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
rw₁ :
  HAdd.hAdd (α := ℍ → ℂ) (⇑f : (a : ℍ) → ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑g : (a : ℍ) → ℂ)) =
    HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
rw₂ rw₃ :
  HAdd.hAdd (α := ℍ → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ) =
    HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)) =
    HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)

Tactic:
rw [SlashAction.add_slash, slash_action_eqn f γ hγ, slash_action_eqn g γ hγ]

Premises used: SlashAction.add_slash, SlashInvariantForm.slash_action_eqn
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : SlashInvariantForm Γ k
⊢ (⇑(f + g) : (a : ℍ) → ℂ) = HAdd.hAdd (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : SlashInvariantForm Γ k
z : ℍ
⊢ (f + g : (a : ℍ) → ℂ) z = HAdd.hAdd (α := ℂ) (β := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((g : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
⊢ Eq (α := (a : ℍ) → ℂ) (⇑0 : (a : ℍ) → ℂ) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : Γ.HasDetOne
α : Type u_2
inst_2 : SMul α ℂ
inst_3 : IsScalarTower α ℂ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) c 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) c 1) (⇑f : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)

Tactic:
rw [← smul_one_smul ℂ]

Premises used: smul_one_smul, Complex
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : Γ.HasDetOne
α : Type u_2
inst_2 : SMul α ℂ
inst_3 : IsScalarTower α ℂ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) c 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) c 1) (⇑f : (a : ℍ) → ℂ)

Tactic:
simp [-smul_assoc, smul_slash, slash_action_eqn _ _ hγ, σ, Subgroup.HasDetOne.det_eq hγ]

Premises used: ModularForm.smul_slash, smul_assoc, Subgroup.HasDetOne.det_eq, UpperHalfPlane.σ, SlashInvariantForm.slash_action_eqn
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
α : Type u_2
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℂ ℂ
f : SlashInvariantForm Γ k
n : α
⊢ (⇑(n • f) : (a : ℍ) → ℂ) = HSMul.hSMul (β := (a : ℍ) → ℂ) n (⇑f : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : Γ.HasDetOne
α : Type u_2
inst_1 : SMul α ℂ
inst_2 : IsScalarTower α ℂ ℂ
f : SlashInvariantForm Γ k
n : α
z : ℍ
⊢ (n • f : (a : ℍ) → ℂ) z = HSMul.hSMul (β := ℂ) n ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
α : Type u_2
inst_1 : SMul α ℂ
inst_2 : SMul α ℝ
inst_3 : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℝ) c 1) (⇑f : (a : ℍ) → ℂ)
rw₁ :
  @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
rw₂ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (HSMul.hSMul (β := ℂ) (HSMul.hSMul (β := ℝ) c 1) 1) (⇑f : (a : ℍ) → ℂ)
rw₃ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) ((↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) * 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) ((↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) * 1) (⇑f : (a : ℍ) → ℂ)
rw₄ :
  HSMul.hSMul (α := ℂ) (β := ℍ → ℂ) ((σ γ : (a : ℂ) → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) (⇑f : (a : ℍ) → ℂ)
rw₅ :
  HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) (⇑f : (a : ℍ) → ℂ)
rw₆ rw₇ :
  HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) (⇑f : (a : ℍ) → ℂ) =
    HSMul.hSMul (β := ℍ → ℂ) (↑(HSMul.hSMul (β := ℝ) c 1) : ℂ) (⇑f : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)) =
    HSMul.hSMul (β := ℍ → ℂ) c (⇑f : (a : ℍ) → ℂ)

Tactic:
rw [← smul_one_smul ℝ, ← smul_one_smul ℂ, smul_slash,
        Complex.real_smul, mul_one, σ_ofReal, slash_action_eqn _ _ hγ]

Premises used: ModularForm.smul_slash, Complex.real_smul, Real, UpperHalfPlane.σ_ofReal, smul_one_smul, mul_one, Complex, SlashInvariantForm.slash_action_eqn
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℂ
inst_1 : SMul α ℝ
inst_2 : IsScalarTower α ℝ ℂ
f : SlashInvariantForm Γ k
n : α
⊢ (⇑(n • f) : (a : ℍ) → ℂ) = HSMul.hSMul (β := (a : ℍ) → ℂ) n (⇑f : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_2
inst : SMul α ℂ
inst_1 : SMul α ℝ
inst_2 : IsScalarTower α ℝ ℂ
f : SlashInvariantForm Γ k
n : α
z : ℍ
⊢ (n • f : (a : ℍ) → ℂ) z = HSMul.hSMul (β := ℂ) n ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
rw :
  Eq (α := ℍ → ℂ) (-@SlashAction.map _ _ _ Units.instMonoid SubNegMonoid.toAddMonoid _ k γ (⇑f : (a : ℍ) → ℂ))
    (-(⇑f : (a : ℍ) → ℂ))
rw₁ rw₂ : Eq (α := ℍ → ℂ) (-(⇑f : (a : ℍ) → ℂ)) (-(⇑f : (a : ℍ) → ℂ))
⊢ Eq (α := ℍ → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ (-(⇑f : (a : ℍ) → ℂ)))
    (-(⇑f : (a : ℍ) → ℂ))

Tactic:
rw [SlashAction.neg_slash, slash_action_eqn f γ hγ]

Premises used: SlashAction.neg_slash, SlashInvariantForm.slash_action_eqn
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : SlashInvariantForm Γ k
⊢ Eq (α := (a : ℍ) → ℂ) (⇑(-f) : (a : ℍ) → ℂ) (-(⇑f : (a : ℍ) → ℂ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f : SlashInvariantForm Γ k
z : ℍ
⊢ Eq (α := ℂ) ((-f : (a : ℍ) → ℂ) z : ℂ) (-(f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : SlashInvariantForm Γ k
⊢ (⇑(f - g) : (a : ℍ) → ℂ) = HSub.hSub (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : SlashInvariantForm Γ k
z : ℍ
⊢ (f - g : (a : ℍ) → ℂ) z = HSub.hSub (α := ℂ) (β := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) ((g : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
⊢ Function.Injective (α := SlashInvariantForm Γ k) (β := ℍ → ℂ) (⇑coeHom : (a : SlashInvariantForm Γ k) → ℍ → ℂ)

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : Γ.HasDetOne
x : ℂ
g : GL (Fin 2) ℝ
hg : g ∈ Γ
h :
  ∀ (x_1 : ℍ),
    @SlashAction.map (outParam ℤ) _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g (Function.const ℍ x)
        x_1 =
      Function.const ℍ x x_1
⊢ @SlashAction.map (outParam ℤ) _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g (Function.const ℍ x) =
    Function.const ℍ x

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : Γ.HasDetOne
x : ℂ
g : GL (Fin 2) ℝ
hg : g ∈ Γ
x_1 : ℍ
⊢ @SlashAction.map (outParam ℤ) _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g (Function.const ℍ x)
      x_1 =
    Function.const ℍ x x_1

Tactic:
simp [slash_def, σ, Subgroup.HasDetOne.det_eq hg]

Premises used: Subgroup.HasDetOne.det_eq, ModularForm.slash_def, UpperHalfPlane.σ
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : Γ.HasDetPlusMinusOne
x : ℝ
g : GL (Fin 2) ℝ
hg : g ∈ Γ
τ : ℍ
⊢ @SlashAction.map (outParam ℤ) _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g
      (Function.const ℍ (↑x : ℂ)) τ =
    Function.const ℍ (↑x : ℂ) τ

Tactic:
simp [slash_apply,
    Subgroup.HasDetPlusMinusOne.abs_det hg, -Matrix.GeneralLinearGroup.val_det_apply]

Premises used: Subgroup.HasDetPlusMinusOne.abs_det, ModularForm.slash_apply, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
⊢ Eq (α := (a : ℍ) → ℂ) (⇑1 : (a : ℍ) → ℂ) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst : FunLike F ℍ ℂ
inst_1 : Γ.HasDetPlusMinusOne
k₁ k₂ : ℤ
f : SlashInvariantForm Γ k₁
g : SlashInvariantForm Γ k₂
A : GL (Fin 2) ℝ
hA : A ∈ Γ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k₁ + k₂) A
      (HMul.hMul (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)) =
    HMul.hMul (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)

Tactic:
simp [mul_slash, Subgroup.HasDetPlusMinusOne.abs_det hA,
    -Matrix.GeneralLinearGroup.val_det_apply, slash_action_eqn f A hA, slash_action_eqn g A hA]

Premises used: ModularForm.mul_slash, Subgroup.HasDetPlusMinusOne.abs_det, SlashInvariantForm.slash_action_eqn, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
inst : Γ.HasDetPlusMinusOne
k₁ k₂ : ℤ
f : SlashInvariantForm Γ k₁
g : SlashInvariantForm Γ k₂
⊢ (⇑(f.mul g) : (a : ℍ) → ℂ) = HMul.hMul (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑g : (a : ℍ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms
Goal:
F : Type u_1
Γ_1 : Subgroup (GL (Fin 2) ℝ)
k_1 : ℤ
inst : FunLike F ℍ ℂ
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst_1 : Γ.HasDetPlusMinusOne
f : (i : ι) → SlashInvariantForm Γ (k i)
A : GL (Fin 2) ℝ
hA : A ∈ Γ
⊢ Eq (α := ℍ → ℂ)
    (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ m A
      (∏ i ∈ s, (⇑(f i) : (a : ℍ) → ℂ)))
    (∏ i ∈ s, (⇑(f i) : (a : ℍ) → ℂ))

Tactic:
simp [hm, prod_slash_sum_weights, -Matrix.GeneralLinearGroup.val_det_apply,
       Subgroup.HasDetPlusMinusOne.abs_det hA, SlashInvariantForm.slash_action_eqn (f _) A hA]

Premises used: ModularForm.prod_slash_sum_weights, Subgroup.HasDetPlusMinusOne.abs_det, SlashInvariantForm.slash_action_eqn, Matrix.GeneralLinearGroup.val_det_apply