-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
C : Type u_5
inst_10 : Ring C
inst_11 : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
i j : ι
a : ↥(𝒜 i)
b : ↥(ℬ j)
rw :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
        ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
rw₁ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) (1 ᵍ⊗ₜ[R] (↑b : B)) ((↑a : A) ᵍ⊗ₜ[R] 1)) : C)
rw₂ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C)
          (HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((1 * (↑a : A)) ᵍ⊗ₜ[R] ((↑b : B) * 1))) :
        C)
rw₃ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C)
          (HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((↑a : A) ᵍ⊗ₜ[R] ((↑b : B) * 1))) :
        C)
rw₄ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i))
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C)
          (HSMul.hSMul (β := 𝒜 ᵍ⊗[R] ℬ) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((↑a : A) ᵍ⊗ₜ[R] (↑b : B))) :
        C)
rw₅ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (HMul.hMul (α := 𝒜 ᵍ⊗[R] ℬ) ((↑a : A) ᵍ⊗ₜ[R] 1) (1 ᵍ⊗ₜ[R] (↑b : B))) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] (↑b : B)) : C)
rw₆ :
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] (↑b : B)) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i)) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] (↑b : B)) : C)
⊢ HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
      ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C) =
    HPow.hPow (α := ℤˣ) (-1) (j * i) •
      HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] (↑b : B)) : C)
        ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] 1) : C)
have rw₇ : (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] (↑b : B)) =
  HSMul.hSMul (β := C) (HPow.hPow (α := ℤˣ) (-1) (j * i) * HPow.hPow (α := ℤˣ) (-1) (j * i))
    ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((↑a : A) ᵍ⊗ₜ[R] (↑b : B)) : C)
Tactic: rw [← map_mul, ← map_mul F, tmul_coe_mul_coe_tmul, one_mul, mul_one, AlgHom.map_smul_of_tower,
      tmul_one_mul_one_tmul, smul_smul, Int.units_mul_self, one_smul]