-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
p : Submodule R M
inst_7 : Algebra.IsEpi R A
inst_8 : Module.Flat R A
f : TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) →ₗ[A] ↥(span A (↑p : Set M)) :=
  AlgebraTensorModule.lift
    (restrictScalarsₗ R A (↥(span A (↑p : Set M))) (↥(span A (↑p : Set M))) A ∘ₗ lsmul A ↥(span A (↑p : Set M)))
g : TensorProduct.{u_1, u_2, u_3} R A ↥p →ₗ[R] TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)) :=
  lTensor A (inclusionSpan A p)
hf :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M))) (β := ↥(span A (↑p : Set M)))
    (⇑f : (a : A ⊗[R] ↥(span A (↑p : Set M))) → ↥(span A (↑p : Set M)))
hg :
  Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥p) (β := TensorProduct.{u_1, u_2, u_3} R A ↥(span A (↑p : Set M)))
    (⇑g : (a : A ⊗[R] ↥p) → A ⊗[R] ↥(span A (↑p : Set M)))
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R A ↥p →ₗ[R] ↥(span A (↑p : Set M)))
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_2 u_3)} →
            {M₂ : Type u_3} →
              [inst : Semiring R] →
                [inst_9 : Semiring S] →
                  [inst_10 : AddCommMonoid M] →
                    [inst_11 : AddCommMonoid M₂] →
                      [inst_12 : Module R M] →
                        [inst_13 : Module R M₂] →
                          [inst_14 : Module S M] →
                            [inst_15 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (tensorToSpan A p))
    ((↑R :
          {S : Type u_2} →
            {M : Type (max u_2 u_3)} →
              {M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        f ∘ₗ
      g)
have a : ∀ (x : A) (x_1 : ↥p),
  Eq.{u_3 + 1} (α := M)
    (↑(((((AlgebraTensorModule.curry
                      ((↑R :
                          {S : Type u_2} →
                            {M : Type (max u_2 u_3)} →
                              {M₂ : Type u_3} →
                                [inst : Semiring R] →
                                  [inst_9 : Semiring S] →
                                    [inst_10 : AddCommMonoid M] →
                                      [inst_11 : AddCommMonoid M₂] →
                                        [inst_12 : Module R M] →
                                          [inst_13 : Module R M₂] →
                                            [inst_14 : Module S M] →
                                              [inst_15 : Module S M₂] →
                                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                        (tensorToSpan A p)) :
                    LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) A (↥p →ₗ[R] ↥(span A (↑p : Set M)))) :
                  (a : A) → ↥p →ₗ[R] ↥(span A (↑p : Set M)))
                x :
              ↥p →ₗ[R] ↥(span A (↑p : Set M))) :
            (a : ↥p) → ↥(span A (↑p : Set M)))
          x_1) :
      M)
    (↑(((((AlgebraTensorModule.curry
                      ((↑R :
                            {S : Type u_2} →
                              {M : Type (max u_2 u_3)} →
                                {M₂ : Type u_3} →
                                  [inst : Semiring R] →
                                    [inst_9 : Semiring S] →
                                      [inst_10 : AddCommMonoid M] →
                                        [inst_11 : AddCommMonoid M₂] →
                                          [inst_12 : Module R M] →
                                            [inst_13 : Module R M₂] →
                                              [inst_14 : Module S M] →
                                                [inst_15 : Module S M₂] →
                                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                          f ∘ₗ
                        g) :
                    LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) A (↥p →ₗ[R] ↥(span A (↑p : Set M)))) :
                  (a : A) → ↥p →ₗ[R] ↥(span A (↑p : Set M)))
                x :
              ↥p →ₗ[R] ↥(span A (↑p : Set M))) :
            (a : ↥p) → ↥(span A (↑p : Set M)))
          x_1) :
      M)
Tactic: ext