-- 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
⊢ 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)) =
    F.toLinearMap
have a : ∀ (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 sorry :
                                𝒜 ᵍ⊗[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 𝒜 ℬ)) sorry :
                                  { 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)
Tactic: ext