-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Local (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsLocalRing S
inst_3 : Algebra R S
P : Type u_3
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : FormallySmooth R P
inst_9 : Module.Free P Ω[P⁄R]
inst_10 : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective.{u_3 + 1, u_2 + 1} (α := P) (β := S) (⇑(algebraMap P S) : (a : P) → S)
h₂ : Ideal.FG (RingHom.ker (F := P →+* S) (algebraMap P S))
P' : Extension.{u_3, u_1, u_2} R S :=
  { Ring := P, commRing := inst_4, algebra₁ := inst_5, algebra₂ := inst_6, isScalarTower := inst_7,
    σ := Function.surjInv h₁, algebraMap_σ := ⋯ }
⊢ Function.Injective (α := TensorProduct.{u_2, u_2, u_3} S (ResidueField S) P'.Cotangent) (β :=
      ResidueField S ⊗[S] P'.CotangentSpace)
      (⇑(LinearMap.lTensor (ResidueField S) P'.cotangentComplex) :
        (a : ResidueField S ⊗[S] P'.Cotangent) → ResidueField S ⊗[S] P'.CotangentSpace) ↔
    Function.Injective (α :=
      TensorProduct.{u_3, u_2, u_3} P (ResidueField S) ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β :=
      TensorProduct.{u_3, u_2, u_3} P (ResidueField S) Ω[P⁄R])
      (⇑((↑(AlgebraTensorModule.cancelBaseChange P'.Ring S (ResidueField S) (ResidueField S) Ω[P'.Ring⁄R]) :
                ResidueField S ⊗[S] (S ⊗[P'.Ring] Ω[P'.Ring⁄R]) →ₗ[ResidueField S]
                  ResidueField S ⊗[P'.Ring] Ω[P'.Ring⁄R]) ∘ₗ
              LinearMap.baseChange (ResidueField S) P'.cotangentComplex ∘ₗ
                (↑(LinearEquiv.symm
                        (AlgebraTensorModule.cancelBaseChange P'.Ring S (ResidueField S) (ResidueField S) ↥P'.ker) ≪≫ₗ
                      LinearEquiv.baseChange S (ResidueField S) (TensorProduct.{u_3, u_2, u_3} P'.Ring S ↥P'.ker)
                        P'.Cotangent P'.cotangentEquiv) :
                  ResidueField S ⊗[P'.Ring] ↥P'.ker →ₗ[ResidueField S] ResidueField S ⊗[S] P'.Cotangent) :
            LinearMap (R := ResidueField S) (RingHom.id (ResidueField S))
              (TensorProduct.{u_3, u_2, u_3} P'.Ring (ResidueField S)
                ↥(RingHom.ker (F := RingHom.{u_3, u_2} P'.Ring S) (algebraMap P'.Ring S)))
              (TensorProduct.{u_3, u_2, u_3} P'.Ring (ResidueField S) Ω[P'.Ring⁄R])) :
        (a : ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S))) → ResidueField S ⊗[P] Ω[P⁄R])
have refine : Function.Injective (α := TensorProduct.{u_2, u_2, u_3} S (ResidueField S) P'.Cotangent) (β :=
    ResidueField S ⊗[S] P'.CotangentSpace)
    (⇑(LinearMap.lTensor (ResidueField S) P'.cotangentComplex) :
      (a : ResidueField S ⊗[S] P'.Cotangent) → ResidueField S ⊗[S] P'.CotangentSpace) ↔
  Function.Injective (α :=
    TensorProduct.{u_3, u_2, u_3} P (ResidueField S) ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β :=
    ResidueField S ⊗[S] TensorProduct.{u_3, u_2, u_3} P'.Ring S Ω[P'.Ring⁄R])
    (⇑(LinearMap.baseChange (ResidueField S) P'.cotangentComplex ∘ₗ
            (↑(LinearEquiv.symm
                    (AlgebraTensorModule.cancelBaseChange P'.Ring S (ResidueField S) (ResidueField S) ↥P'.ker) ≪≫ₗ
                  LinearEquiv.baseChange S (ResidueField S) (TensorProduct.{u_3, u_2, u_3} P'.Ring S ↥P'.ker)
                    P'.Cotangent P'.cotangentEquiv) :
              ResidueField S ⊗[P'.Ring] ↥P'.ker →ₗ[ResidueField S] ResidueField S ⊗[S] P'.Cotangent) :
          LinearMap (R := ResidueField S) (RingHom.id (ResidueField S))
            (TensorProduct.{u_3, u_2, u_3} P'.Ring (ResidueField S)
              ↥(RingHom.ker (F := RingHom.{u_3, u_2} P'.Ring S) (algebraMap P'.Ring S)))
            (ResidueField S ⊗[S] P'.CotangentSpace)) :
      (a : ResidueField S ⊗[P'.Ring] ↥(RingHom.ker (algebraMap P'.Ring S))) → ResidueField S ⊗[S] P'.CotangentSpace)
Tactic: refine .trans ?_ ((AlgebraTensorModule.cancelBaseChange P'.Ring S _ _
    Ω[P'.Ring⁄R]).comp_injective _).symm