-- Module: Mathlib.RingTheory.Smooth.Local
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
K : Type u_4
inst_4 : Field K
inst_5 : CommRing P
inst_6 : Algebra R P
inst_7 : Algebra P S
inst_8 : IsScalarTower R P S
inst_9 : Algebra S K
inst_10 : Algebra P K
inst_11 : IsScalarTower P S K
inst_12 : FormallySmooth R P
inst_13 : Module.Free P Ω[P⁄R]
inst_14 : 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))
h₃ : LE.le (α := Ideal S) (maximalIdeal S) (RingHom.ker (F := S →+* K) (algebraMap S K))
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this_1 : Algebra.{u_2, u_4} (ResidueField S) K := f.toAlgebra
this_2 : IsScalarTower S (ResidueField S) K
this_3 : IsScalarTower.{u_3, u_2, u_4} P (ResidueField S) K
this :
  Eq (α := K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[K] K ⊗[P] Ω[P⁄R])
    ((↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) :
          K ⊗[ResidueField S] (ResidueField S ⊗[P] Ω[P⁄R]) →ₗ[K] K ⊗[P] Ω[P⁄R]) ∘ₗ
        LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
          (↑(LinearEquiv.symm
                (AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K
                  ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))) :
            K ⊗[P] ↥(RingHom.ker (algebraMap P S)) →ₗ[K]
              K ⊗[ResidueField S] (ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S)))) :
      K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[K] K ⊗[P] Ω[P⁄R])
    (cotangentComplexBaseChange R S P K : K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[K] K ⊗[P] Ω[P⁄R])
refine :
  Function.Injective (α :=
      K ⊗[ResidueField S]
        TensorProduct.{u_3, u_2, u_3} P (ResidueField S) ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))
      (β := K ⊗[ResidueField S] TensorProduct.{u_3, u_2, u_3} P (ResidueField S) Ω[P⁄R])
      (⇑(LinearMap.lTensor K (cotangentComplexBaseChange R S P (ResidueField S))) :
        (a : K ⊗[ResidueField S] (ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S)))) →
          K ⊗[ResidueField S] (ResidueField S ⊗[P] Ω[P⁄R])) ↔
    Function.Injective (α := K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β :=
      K ⊗[ResidueField S] TensorProduct.{u_3, u_2, u_3} P (ResidueField S) Ω[P⁄R])
      (⇑(LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
              (↑(LinearEquiv.symm
                    (AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K
                      ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))) :
                K ⊗[P] ↥(RingHom.ker (algebraMap P S)) →ₗ[K]
                  K ⊗[ResidueField S] (ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S)))) :
            K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[K]
              K ⊗[ResidueField S] TensorProduct.{u_3, u_2, u_3} P (ResidueField S) Ω[P⁄R]) :
        (a : K ⊗[P] ↥(RingHom.ker (algebraMap P S))) → K ⊗[ResidueField S] (ResidueField S ⊗[P] Ω[P⁄R]))
⊢ Function.Injective (α :=
      K ⊗[ResidueField S]
        TensorProduct.{u_3, u_2, u_3} P (ResidueField S) ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))
      (β := K ⊗[ResidueField S] TensorProduct.{u_3, u_2, u_3} P (ResidueField S) Ω[P⁄R])
      (⇑(LinearMap.lTensor K (cotangentComplexBaseChange R S P (ResidueField S))) :
        (a : K ⊗[ResidueField S] (ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S)))) →
          K ⊗[ResidueField S] (ResidueField S ⊗[P] Ω[P⁄R])) ↔
    Function.Injective (α := K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) (β := K ⊗[P] Ω[P⁄R])
      (⇑((↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) :
                K ⊗[ResidueField S] (ResidueField S ⊗[P] Ω[P⁄R]) →ₗ[K] K ⊗[P] Ω[P⁄R]) ∘ₗ
              LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
                (↑(LinearEquiv.symm
                      (AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K
                        ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))) :
                  K ⊗[P] ↥(RingHom.ker (algebraMap P S)) →ₗ[K]
                    K ⊗[ResidueField S] (ResidueField S ⊗[P] ↥(RingHom.ker (algebraMap P S)))) :
            K ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) →ₗ[K] K ⊗[P] Ω[P⁄R]) :
        (a : K ⊗[P] ↥(RingHom.ker (algebraMap P S))) → K ⊗[P] Ω[P⁄R])

Tactic:
refine .trans ?_ ((AlgebraTensorModule.cancelBaseChange _ _ _ _ _).comp_injective _).symm