-- 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
x : A
x_1 : B
⊢ Eq.{u_5 + 1} (α := C)
    (((((AlgebraTensorModule.curry
                    ((AlgHom.toLinearMap
                          ((fun
                                (fg :
                                  { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
                                    ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                                      HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C)
                                          ((fg.2 : (a : B) → C) (↑b : B) : C) =
                                        HPow.hPow (α := ℤˣ) (-1) (j * i) •
                                          HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                                            ((fg.1 : (a : A) → C) (↑a : A) : C) }) ↦
                              (lift 𝒜 ℬ (↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).2 ⋯ :
                                𝒜 ᵍ⊗[R] ℬ →ₐ[R] C))
                            ((fun (F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C) ↦
                                (Subtype.mk (p := fun (fg : (A →ₐ[R] C) × (B →ₐ[R] C)) ↦
                                    ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                                      HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C)
                                          ((fg.2 : (a : B) → C) (↑b : B) : C) =
                                        HPow.hPow (α := ℤˣ) (-1) (j * i) •
                                          HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                                            ((fg.1 : (a : A) → C) (↑a : A) : C))
                                    (F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)) ⋯ :
                                  { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
                                    ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                                      HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C)
                                          ((fg.2 : (a : B) → C) (↑b : B) : C) =
                                        HPow.hPow (α := ℤˣ) (-1) (j * i) •
                                          HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                                            ((fg.1 : (a : A) → C) (↑a : A) : C) }))
                              F)) :
                        𝒜 ᵍ⊗[R] ℬ →ₗ[R] C) ∘ₗ
                      (↑(of R 𝒜 ℬ) : A ⊗[R] B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ)) :
                  A →ₗ[R] B →ₗ[R] C) :
                (a : A) → B →ₗ[R] C)
              x :
            B →ₗ[R] C) :
          (a : B) → C)
        x_1 :
      C)
    (((((AlgebraTensorModule.curry (F.toLinearMap ∘ₗ (↑(of R 𝒜 ℬ) : A ⊗[R] B →ₗ[R] 𝒜 ᵍ⊗[R] ℬ)) : A →ₗ[R] B →ₗ[R] C) :
                (a : A) → B →ₗ[R] C)
              x :
            B →ₗ[R] C) :
          (a : B) → C)
        x_1 :
      C)
have a : HMul.hMul (α := C) (β := C) ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (x ᵍ⊗ₜ[R] 1) : C)
    ((F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) (1 ᵍ⊗ₜ[R] x_1) : C) =
  (F : (a : 𝒜 ᵍ⊗[R] ℬ) → C) ((of R 𝒜 ℬ : (a : A ⊗[R] B) → 𝒜 ᵍ⊗[R] ℬ) (x ⊗ₜ[R] x_1) : 𝒜 ᵍ⊗[R] ℬ)
Tactic: dsimp