-- 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
f' : A ⊗[R] B →ₐ[S] C
ha :
  ∀ (x : A),
    Eq.{uC + 1} (α := C)
      ((AlgHom.comp (B := A ⊗[R] B)
              ((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))
                ((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) }))
                  f'))
              includeLeft :
            (a : A) → C)
          x :
        C)
      ((f'.comp includeLeft : (a : A) → C) x : 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))
      ((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) }))
        f') =
    f'
have hb : ∀ (x : B),
  Eq.{uC + 1} (α := C)
    ((AlgHom.comp (B := A ⊗[R] B)
            (AlgHom.restrictScalars R (S := S)
              ((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))
                ((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) }))
                  f')))
            includeRight :
          (a : B) → C)
        x :
      C)
    ((AlgHom.comp (AlgHom.restrictScalars R f') includeRight : (a : B) → C) x : C)
Tactic: ext