-- Module: Mathlib.RingTheory.Smooth.Fiber
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : CommRing P
inst_5 : Algebra R P
inst_6 : Algebra P S
inst_7 : IsScalarTower R P S
inst_8 : IsLocalRing R
inst_9 : IsLocalRing S
inst_10 : IsLocalHom (R := R) (S := S) (F := R →+* S) (algebraMap R S)
inst_11 : FormallySmooth 𝓀[R] (𝓀[R] ⊗[R] S)
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))
Sp : Type (max u_1 u_2) := 𝓀[R] ⊗[R] S
Pp : Type (max u_1 u_3) := 𝓀[R] ⊗[R] P
φ : Pp →ₐ[𝓀[R]] Sp := TensorProduct.map (AlgHom.id 𝓀[R] 𝓀[R]) (IsScalarTower.toAlgHom R P S)
ψ : Sp →ₐ[R] 𝓀[S] := TensorProduct.lift (IsScalarTower.toAlgHom R 𝓀[R] 𝓀[S]) (IsScalarTower.toAlgHom R S 𝓀[S]) ⋯
algInst : Algebra Pp Sp := φ.toAlgebra
algInst_1 : Algebra P Sp := RingHom.toAlgebra (φ.comp (algebraMap P Pp))
algInst_2 : Algebra Sp 𝓀[S] := ψ.toAlgebra
algInst_3 : Algebra Pp 𝓀[S] := (ψ.comp φ.toRingHom).toAlgebra
scalarTowerInst : IsScalarTower P Pp Sp := ⋯
scalarTowerInst_1 : IsScalarTower Pp Sp 𝓀[S] := ⋯
this_1 : IsScalarTower 𝓀[R] Pp Sp
this_2 : IsScalarTower R Sp 𝓀[S]
this_3 : IsScalarTower P S Sp
this_4 : IsScalarTower S Sp 𝓀[S]
this_5 : IsScalarTower P Sp 𝓀[S]
this_6 : IsScalarTower P Pp 𝓀[S]
ePp : Pp ≃ₐ[P] P ⊗[R] 𝓀[R] :=
  let __spread.0 : 𝓀[R] ⊗[R] P ≃ₐ[R] P ⊗[R] 𝓀[R] := TensorProduct.comm R 𝓀[R] P;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e₀ : Ω[Pp⁄𝓀[R]] ≃ₗ[Pp] Pp ⊗[P] Ω[P⁄R] := LinearEquiv.symm (KaehlerDifferential.tensorKaehlerEquiv R 𝓀[R] P Pp)
this_7 : Module.Free Pp Ω[Pp⁄𝓀[R]]
this_8 : Module.Finite Pp Ω[Pp⁄𝓀[R]]
e₁ : ↥(RingHom.ker φ) ≃ₗ[Pp] Pp ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) :=
  kerTensorProductMapIdToAlgHomEquiv R P S 𝓀[R] h₁
h₁' : Function.Surjective (α := Pp) (β := Sp) (⇑φ : (a : Pp) → Sp)
h₂' : Ideal.FG (RingHom.ker φ)
h₃ : LE.le (α := Ideal Sp) 𝓂[Sp] (RingHom.ker ψ)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
eᵣ : 𝓀[S] ⊗[Pp] Ω[Pp⁄𝓀[R]] ≃ₗ[S] TensorProduct.{u_3, u_2, u_3} P 𝓀[S] Ω[P⁄R] :=
  LinearEquiv.restrictScalars S (S := 𝓀[S])
      (AlgebraTensorModule.congr (LinearEquiv.refl 𝓀[S] 𝓀[S]) e₀ :
        𝓀[S] ⊗[Pp] Ω[Pp⁄𝓀[R]] ≃ₗ[𝓀[S]] 𝓀[S] ⊗[Pp] (Pp ⊗[P] Ω[P⁄R])) ≪≫ₗ
    LinearEquiv.restrictScalars S
      (AlgebraTensorModule.cancelBaseChange P Pp Sp 𝓀[S] Ω[P⁄R] :
        𝓀[S] ⊗[Pp] (Pp ⊗[P] Ω[P⁄R]) ≃ₗ[Sp] TensorProduct.{u_3, u_2, u_3} P 𝓀[S] Ω[P⁄R])
eₗ : 𝓀[S] ⊗[Pp] ↥(RingHom.ker φ) ≃ₗ[S]
  TensorProduct.{u_3, u_2, u_3} P 𝓀[S] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) :=
  LinearEquiv.restrictScalars S (S := 𝓀[S])
      (AlgebraTensorModule.congr (LinearEquiv.refl 𝓀[S] 𝓀[S]) e₁ :
        𝓀[S] ⊗[Pp] ↥(RingHom.ker φ) ≃ₗ[𝓀[S]] 𝓀[S] ⊗[Pp] (Pp ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))) ≪≫ₗ
    LinearEquiv.restrictScalars S
      (AlgebraTensorModule.cancelBaseChange P Pp Sp 𝓀[S] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)) :
        𝓀[S] ⊗[Pp] (Pp ⊗[P] ↥(RingHom.ker (F := P →+* S) (algebraMap P S))) ≃ₗ[Sp]
          TensorProduct.{u_3, u_2, u_3} P 𝓀[S] ↥(RingHom.ker (F := P →+* S) (algebraMap P S)))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
(eᵣ.injective.comp this).comp eₗ.symm.injective

Premises used: LinearEquiv.symm, Function.Injective.comp, LinearEquiv.injective