-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
fg :
  { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
    ∀ (x : A) (y : B), Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }
a :
  ∀ (x : A),
    Eq.{uC + 1} (α := C)
      (((↑((fun (f' : A ⊗[R] B →ₐ[S] C) ↦
                      (Subtype.mk (p := fun (fg : (A →ₐ[S] C) × (B →ₐ[R] C)) ↦
                          ∀ (x : A) (y : B),
                            Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C))
                          (f'.comp includeLeft, AlgHom.comp (AlgHom.restrictScalars R f') includeRight) ⋯ :
                        { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                          ∀ (x : A) (y : B),
                            Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }))
                    ((fun
                          (fg :
                            { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                              ∀ (x : A) (y : B),
                                Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }) ↦
                        (lift (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).2 ⋯ :
                          A ⊗[R] B →ₐ[S] C))
                      fg)) :
                (A →ₐ[S] C) × (B →ₐ[R] C)).1 :
            (a : A) → C)
          x :
        C)
      (((↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).1 : (a : A) → C) x : C)
⊢ (fun (f' : A ⊗[R] B →ₐ[S] C) ↦
        (Subtype.mk (p := fun (fg : (A →ₐ[S] C) × (B →ₐ[R] C)) ↦
            ∀ (x : A) (y : B), Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C))
            (f'.comp includeLeft, AlgHom.comp (AlgHom.restrictScalars R f') includeRight) ⋯ :
          { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
            ∀ (x : A) (y : B), Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }))
      ((fun
            (fg :
              { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                ∀ (x : A) (y : B), Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }) ↦
          (lift (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).2 ⋯ : A ⊗[R] B →ₐ[S] C))
        fg) =
    fg
have a₁ : ∀ (x : B),
  Eq.{uC + 1} (α := C)
    (((↑((fun (f' : A ⊗[R] B →ₐ[S] C) ↦
                    (Subtype.mk (p := fun (fg : (A →ₐ[S] C) × (B →ₐ[R] C)) ↦
                        ∀ (x : A) (y : B),
                          Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C))
                        (f'.comp includeLeft, AlgHom.comp (AlgHom.restrictScalars R f') includeRight) sorry :
                      { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                        ∀ (x : A) (y : B),
                          Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }))
                  ((fun
                        (fg :
                          { fg : (A →ₐ[S] C) × (B →ₐ[R] C) //
                            ∀ (x : A) (y : B),
                              Commute.{uC} (S := C) ((fg.1 : (a : A) → C) x : C) ((fg.2 : (a : B) → C) y : C) }) ↦
                      (lift (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).2 sorry :
                        A ⊗[R] B →ₐ[S] C))
                    fg)) :
              (A →ₐ[S] C) × (B →ₐ[R] C)).2 :
          (a : B) → C)
        x :
      C)
    (((↑fg : (A →ₐ[S] C) × (B →ₐ[R] C)).2 : (a : B) → C) x : C)
Tactic: ext