awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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))
⊢ 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)) *
    HMul.hMul (α := ℂ) ((σ B : (a : ℂ) → ℂ) (denom A (↑(B • τ) : ℂ)) : ℂ) (denom 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 : ℍ → ℂ
τ : ℍ
⊢ 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)
have 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)
Tactic: rw [map_mul, map_zpow₀, map_mul, map_zpow₀, σ_ofReal]
-- 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 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))
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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
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))
⊢ (f ∣[k] (A * B)) τ = ((f ∣[k] A) ∣[k] B) τ
have 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)
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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
k : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
⊢ (f + g) ∣[k] A = f ∣[k] A + g ∣[k] A
have h : ∀ (τ : ℍ), ((f + g) ∣[k] A) τ = (f ∣[k] A + g ∣[k] A) τ
Tactic: ext1 τ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
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)
have 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) τ
Tactic: ext τ : 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
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
have 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) τ
Tactic: ext τ : 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
A : SL(2, ℤ)
x : ℂ
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 A
      (Function.const ℍ x) =
    Function.const ℍ x
have 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
Tactic: funext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
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
have 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
Tactic: simp only [SL_slash_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
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) =
      f z ↔
    f (γ • z) =
      ((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k * f z
have 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)
Tactic: convert! inv_mul_eq_iff_eq_mul₀ (G₀ := ℂ) _ using 2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
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)
⊢ 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
have convert_4 : ((↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑γ : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)) ^ k ≠ 0
Tactic: convert! inv_mul_eq_iff_eq_mul₀ (G₀ := ℂ) _ using 2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
k : ℤ
f : ℍ → ℂ
γ : SL(2, ℤ)
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)
have 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)
Tactic: simp only [mul_comm (f _), denom, zpow_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
⊢ @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)
have 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
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
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
have 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)))
Tactic: simp only [slash_apply, Pi.mul_apply, Pi.smul_apply, real_smul, map_mul, neg_add,
    zpow_add₀ (denom_ne_zero _ x)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (hypothesis)
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)
have this : d ≠ 0
Tactic: have : d ≠ 0 := ofReal_ne_zero.mpr <| abs_ne_zero.mpr <| NeZero.ne _
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
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 * d ^ (k1 - 1) * d ^ (k2 - 1)
have rw : d ^ (k1 + k2 - 1) = d ^ (1 + (k1 - 1) + (k2 - 1))
Tactic: rw [← zpow_one_add₀ this, ← zpow_add₀ this]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (hypothesis)
Goal:
k1 k2 : ℤ
A : GL (Fin 2) ℝ
f g : ℍ → ℂ
x : ℍ
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)))
have h1 : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
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 ^ (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)))
have 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)))
Tactic: rw [h1]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
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
have 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)
      τ
Tactic: ext τ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
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)
      τ
have 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)⁻¹)
Tactic: simp [SL_slash_apply, zpow_sub₀ (denom_ne_zero A τ)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (∑ i ∈ ∅, k i) g (∏ i ∈ ∅, f i) =
    HSMul.hSMul (β := ℍ → ℂ)
      (HPow.hPow (α := ℝ) |(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)|
        (HSub.hSub (α := ℤ) (↑(card.{u_1} (α := ι) ∅) : ℤ) 1))
      (∏ i ∈ ∅, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k i) g (f i))
have empty : @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g 1 =
  HSMul.hSMul (β := ℍ → ℂ) |(↑g : Matrix (Fin 2) (Fin 2) ℝ).det|⁻¹ 1
Tactic: simp only [sum_empty, prod_empty, Matrix.GeneralLinearGroup.val_det_apply, card_empty,
      CharP.cast_eq_zero, zero_sub, Int.reduceNeg, zpow_neg, zpow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.SlashActions (goal)
Goal:
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
⊢ @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g 1 =
    HSMul.hSMul (β := ℍ → ℂ) |(↑g : Matrix (Fin 2) (Fin 2) ℝ).det|⁻¹ 1
have empty : ∀ (x : ℍ),
  @SlashAction.map ℤ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 0 g 1 x =
    HSMul.hSMul (β := ℍ → ℂ) |(↑g : Matrix (Fin 2) (Fin 2) ℝ).det|⁻¹ 1 x
Tactic: ext _