-- 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
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) }
a :
  ∀ (x : A),
    Eq.{u_5 + 1} (α := 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) }))
                    ((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))
                      fg)) :
                (A →ₐ[R] C) × (B →ₐ[R] C)).1 :
            (a : A) → C)
          x :
        C)
      (((↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).1 : (a : A) → C) x : 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) }))
      ((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))
        fg) =
    fg
have a₁ : ∀ (x : B),
  Eq.{u_5 + 1} (α := 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) }))
                  ((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))
                    fg)) :
              (A →ₐ[R] C) × (B →ₐ[R] C)).2 :
          (a : B) → C)
        x :
      C)
    (((↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).2 : (a : B) → C) x : C)
Tactic: ext