-- 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)))
this :
  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)
⊢ Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥p) (β := ↥(span A (↑p : Set M)))
    (⇑(tensorToSpan A p) : (a : A ⊗[R] ↥p) → ↥(span A (↑p : Set M)))
have rw : Injective (α := TensorProduct.{u_1, u_2, u_3} R A ↥p) (β := ↥(span A (↑p : Set M)))
  (Function.comp (β := TensorProduct.{u_1, u_2, u_3} R A ↥(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₂)
          f) :
      (a : A ⊗[R] ↥(span A (↑p : Set M))) → ↥(span A (↑p : Set M)))
    (⇑g : (a : A ⊗[R] ↥p) → A ⊗[R] ↥(span A (↑p : Set M))))
Tactic: rw [← LinearMap.coe_restrictScalars R, this, coe_comp]