-- Module: Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
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
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 ⋯ :
                                  𝒜 ᵍ⊗[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)
⊢ 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

Tactic:
ext