-- 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))
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))
⊢ 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)) *
    (HPow.hPow (α := ℂ) ((σ B : (a : ℂ) → ℂ) (denom A (↑(B • τ) : ℂ)) : ℂ) (-k) * 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₀]