awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f τ =
    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
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
A : GL (Fin 2) ℝ
f : ℍ → ℂ
c : ℂ
h :
  ∀ (τ : ℍ),
    @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A (c • f) τ =
      HSMul.hSMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) c : ℂ)
        (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A f) τ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A (c • f) =
    HSMul.hSMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) c : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A f)

Tactic:
ext τ : 1
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
A : GL (Fin 2) ℝ
f : ℍ → ℂ
c : ℂ
τ : ℍ
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A (c • f) τ =
    HSMul.hSMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) c : ℂ)
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A f) τ

Tactic:
simp only [slash_apply, Pi.smul_apply, smul_eq_mul, map_mul, mul_assoc]

Premises used: mul_assoc, map_mul, smul_eq_mul, ModularForm.slash_apply, Pi.smul_apply
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f =
    @SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ) :
        GL (Fin 2) ℝ)
      f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = fun (τ : ℍ) ↦
    f (γ • τ) *
      denom
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
          (↑τ : ℂ) ^
        (-k)

Tactic:
simp [SL_slash, slash_def, σ]

Premises used: ModularForm.SL_slash, ModularForm.slash_def, UpperHalfPlane.σ
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
τ : ℍ
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f τ =
    f (γ • τ) *
      denom
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
          (↑τ : ℂ) ^
        (-k)

Tactic:
simp [SL_slash, slash_def, σ]

Premises used: ModularForm.SL_slash, ModularForm.slash_def, UpperHalfPlane.σ
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
α : Type u_1
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
k : ℤ
A : SL(2, ℤ)
f : ℍ → ℂ
c : α
h :
  ∀ (τ : ℍ),
    @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A (c • f) τ =
      (c • @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A f) τ
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A (c • f) =
    c • @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A f

Tactic:
ext τ : 1
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
α : Type u_1
inst : SMul α ℂ
inst_1 : IsScalarTower α ℂ ℂ
k : ℤ
A : SL(2, ℤ)
f : ℍ → ℂ
c : α
τ : ℍ
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A (c • f) τ =
    (c • @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A f) τ

Tactic:
simp [SL_slash_apply, Pi.smul_apply, smul_mul_assoc]

Premises used: smul_mul_assoc, ModularForm.SL_slash_apply, Pi.smul_apply
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
A : SL(2, ℤ)
x : ℂ
h :
  ∀ (x_1 : ℍ),
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 A
        (Function.const ℍ x) x_1 =
      Function.const ℍ x x_1
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 A
      (Function.const ℍ x) =
    Function.const ℍ x

Tactic:
funext
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
A : SL(2, ℤ)
x : ℂ
x_1 : ℍ
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 A
      (Function.const ℍ x) x_1 =
    Function.const ℍ x x_1

Tactic:
simp [SL_slash, slash_def, σ, zero_lt_one]

Premises used: ModularForm.SL_slash, zero_lt_one, ModularForm.slash_def, UpperHalfPlane.σ
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
A : SL(2, ℤ)
⊢ Eq (α := ℍ → ℂ)
    (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 A 1) 1

Tactic:
is_invariant_const _ _

Premises used: ModularForm.is_invariant_const
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
A : SL(2, ℤ)
⊢ Eq (α := ℍ → ℂ)
    (@SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
        GL (Fin 2) ℝ)
      1)
    1

Tactic:
simpa using is_invariant_one A

Premises used: ModularForm.is_invariant_one
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
simp :
  f (γ • z) *
        denom
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
            (↑z : ℂ) ^
          (-k) =
      f z ↔
    f (γ • z) =
      ((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k * f z
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f z = f z ↔
    f (γ • z) =
      ((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k * f z

Tactic:
simp only [SL_slash_apply]

Premises used: ModularForm.SL_slash_apply
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k)⁻¹ *
        f (γ • z) =
      f z ↔
    f (γ • z) =
      ((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k * f z

Tactic:
inv_mul_eq_iff_eq_mul₀ (G₀ := ℂ) _

Premises used: inv_mul_eq_iff_eq_mul₀
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
h :
  f (γ • z) *
      denom
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
          (↑z : ℂ) ^
        (-k) =
    (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k)⁻¹ *
      f (γ • z)
convert_4 :
  ((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k ≠ 0
⊢ f (γ • z) *
        denom
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
            (↑z : ℂ) ^
          (-k) =
      f z ↔
    f (γ • z) =
      ((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k * f z

Tactic:
convert! inv_mul_eq_iff_eq_mul₀ (G₀ := ℂ) _ using 2

Premises used: inv_mul_eq_iff_eq_mul₀
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
h :
  (((↑((↑((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ)) :
                      Matrix (Fin 2) (Fin 2) ℝ)
                    1 0) :
                ℂ) *
              (↑z : ℂ) +
            (↑((↑((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                        ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ)) :
                    Matrix (Fin 2) (Fin 2) ℝ)
                  1 1) :
              ℂ)) ^
          k)⁻¹ *
      f (γ • z) =
    (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k)⁻¹ *
      f (γ • z)
⊢ f (γ • z) *
      denom
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ))
          (↑z : ℂ) ^
        (-k) =
    (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k)⁻¹ *
      f (γ • z)

Tactic:
simp only [mul_comm (f _), denom, zpow_neg]

Premises used: UpperHalfPlane.denom, zpow_neg, mul_comm
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ (((↑((↑((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ)) :
                      Matrix (Fin 2) (Fin 2) ℝ)
                    1 0) :
                ℂ) *
              (↑z : ℂ) +
            (↑((↑((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                        ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ)) :
                    Matrix (Fin 2) (Fin 2) ℝ)
                  1 1) :
              ℂ)) ^
          k)⁻¹ *
      f (γ • z) =
    (((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k)⁻¹ *
      f (γ • z)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ ((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k ≠ 0

Tactic:
zpow_ne_zero k (denom_ne_zero γ z)

Premises used: Real, Matrix.SpecialLinearGroup.map, Int.castRingHom, zpow_ne_zero, DFunLike.coe, UpperHalfPlane.denom_ne_zero, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
z : ℍ
⊢ ((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k ≠ 0

Tactic:
exact zpow_ne_zero k (denom_ne_zero γ z)

Premises used: Real, Matrix.SpecialLinearGroup.map, Int.castRingHom, zpow_ne_zero, DFunLike.coe, UpperHalfPlane.denom_ne_zero, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
h :
  ∀ (x : ℍ),
    @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k1 + k2) A (f * g) x =
      HSMul.hSMul (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)|
        (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k1 A f *
          @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k2 A g)
        x
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k1 + k2) A (f * g) =
    HSMul.hSMul (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)|
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k1 A f *
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k2 A g)

Tactic:
ext1 x
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
h :
  HMul.hMul (α := ℂ) (β := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ) *
        (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k1 + k2 - 1) *
      (denom A (↑x : ℂ) ^ (-k1) * denom A (↑x : ℂ) ^ (-k2)) =
    (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) *
      (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ)
            ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k1 - 1)) *
          denom A (↑x : ℂ) ^ (-k1) *
        (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ)
            ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k2 - 1)) *
          denom A (↑x : ℂ) ^ (-k2)))
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k1 + k2) A (f * g) x =
    HSMul.hSMul (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)|
      (@SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k1 A f *
        @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k2 A g)
      x

Tactic:
simp only [slash_apply, Pi.mul_apply, Pi.smul_apply, real_smul, map_mul, neg_add,
    zpow_add₀ (denom_ne_zero _ x)]

Premises used: Complex.real_smul, Pi.mul_apply, neg_add, map_mul, zpow_add₀, UpperHalfPlane.denom_ne_zero, ModularForm.slash_apply, Pi.smul_apply
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
h :
  let d := (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ);
  HMul.hMul (α := ℂ) (β := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ) *
        d ^ (k1 + k2 - 1) *
      (denom A (↑x : ℂ) ^ (-k1) * denom A (↑x : ℂ) ^ (-k2)) =
    d *
      (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ) (d ^ (k1 - 1)) * denom A (↑x : ℂ) ^ (-k1) *
        (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ) (d ^ (k2 - 1)) * denom A (↑x : ℂ) ^ (-k2)))
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ) *
        (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k1 + k2 - 1) *
      (denom A (↑x : ℂ) ^ (-k1) * denom A (↑x : ℂ) ^ (-k2)) =
    (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) *
      (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ)
            ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k1 - 1)) *
          denom A (↑x : ℂ) ^ (-k1) *
        (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ)
            ((↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ) ^ (k2 - 1)) *
          denom A (↑x : ℂ) ^ (-k2)))

Tactic:
set d := (↑|A.det.val| : ℂ)

Premises used: Units.val, abs, Complex.ofReal, Matrix.GeneralLinearGroup.det, DFunLike.coe
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ)
⊢ d ≠ 0

Tactic:
have : d ≠ 0 := ofReal_ne_zero.mpr <| abs_ne_zero.mpr <| NeZero.ne _
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ)
this : d ≠ 0
rw : d ^ (k1 + k2 - 1) = d ^ (1 + (k1 - 1) + (k2 - 1))
⊢ d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)

Tactic:
rw [← zpow_one_add₀ this, ← zpow_add₀ this]

Premises used: zpow_add₀, zpow_one_add₀
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ)
this : d ≠ 0
⊢ d ^ (k1 + k2 - 1) = d ^ (1 + (k1 - 1) + (k2 - 1))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ)
⊢ d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)

Tactic:
have h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1) := by
    have : d ≠ 0 := ofReal_ne_zero.mpr <| abs_ne_zero.mpr <| NeZero.ne _
    rw [← zpow_one_add₀ this, ← zpow_add₀ this]
    ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ)
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
h :
  HMul.hMul (α := ℂ) (β := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ) *
        (d * d ^ (k1 - 1) * d ^ (k2 - 1)) *
      (denom A (↑x : ℂ) ^ (-k1) * denom A (↑x : ℂ) ^ (-k2)) =
    d *
      (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ) (d ^ (k1 - 1)) * denom A (↑x : ℂ) ^ (-k1) *
        (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ) (d ^ (k2 - 1)) * denom A (↑x : ℂ) ^ (-k2)))
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ) *
        d ^ (k1 + k2 - 1) *
      (denom A (↑x : ℂ) ^ (-k1) * denom A (↑x : ℂ) ^ (-k2)) =
    d *
      (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ) (d ^ (k1 - 1)) * denom A (↑x : ℂ) ^ (-k1) *
        (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ) (d ^ (k2 - 1)) * denom A (↑x : ℂ) ^ (-k2)))

Tactic:
rw [h1]
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
d : ℂ := (↑|(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) A) : ℝ)| : ℂ)
h1 : d ^ (k1 + k2 - 1) = d * d ^ (k1 - 1) * d ^ (k2 - 1)
⊢ HMul.hMul (α := ℂ) (β := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ) *
        (d * d ^ (k1 - 1) * d ^ (k2 - 1)) *
      (denom A (↑x : ℂ) ^ (-k1) * denom A (↑x : ℂ) ^ (-k2)) =
    d *
      (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (f (A • x)) : ℂ) (d ^ (k1 - 1)) * denom A (↑x : ℂ) ^ (-k1) *
        (HMul.hMul (α := ℂ) ((σ A : (a : ℂ) → ℂ) (g (A • x)) : ℂ) (d ^ (k2 - 1)) * denom A (↑x : ℂ) ^ (-k2)))

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k1 + k2) A (f * g) =
    @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k1 A f *
      @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k2 A g

Tactic:
simp [SL_slash, mul_slash]

Premises used: ModularForm.mul_slash, ModularForm.SL_slash
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
h :
  ∀ (τ : ℍ),
    @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k1 - k2) A (f / g)
        τ =
      (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k1 A f /
          @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k2 A g)
        τ
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k1 - k2) A (f / g) =
    @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k1 A f /
      @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k2 A g

Tactic:
ext τ
-- Module: Mathlib.NumberTheory.ModularForms.SlashActions
Goal:
k1 k2 : ℤ
A : SL(2, ℤ)
f g : ℍ → ℂ
τ : ℍ
h :
  f
          (HSMul.hSMul (α := GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
              GL (Fin 2) ℝ)
            τ) /
        g
          (HSMul.hSMul (α := GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
              GL (Fin 2) ℝ)
            τ) *
      (denom
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
            (↑τ : ℂ) ^
          k2 /
        denom
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
            (↑τ : ℂ) ^
          k1) =
    f
          (HSMul.hSMul (α := GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
              GL (Fin 2) ℝ)
            τ) *
        (denom
              ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
              (↑τ : ℂ) ^
            k1)⁻¹ /
      (g
          (HSMul.hSMul (α := GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A) :
              GL (Fin 2) ℝ)
            τ) *
        (denom
              ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) A))
              (↑τ : ℂ) ^
            k2)⁻¹)
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k1 - k2) A (f / g)
      τ =
    (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k1 A f /
        @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k2 A g)
      τ

Tactic:
simp [SL_slash_apply, zpow_sub₀ (denom_ne_zero A τ)]

Premises used: Real, zpow_sub₀, Matrix.SpecialLinearGroup.map, Int.castRingHom, ModularForm.SL_slash_apply, DFunLike.coe, UpperHalfPlane.denom_ne_zero, Matrix.SpecialLinearGroup.toGL