-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (goal)
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)
M : Submonoid P
inst_12 : IsLocalization M S
inst_13 : FinitePresentation R P
obtain :
  ∀ (n : ℕ) (f₀ : MvPolynomial (Fin n) R →ₐ[R] P)
    (hf₀ :
      Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P)
        (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)),
    FormallySmooth R S
obtain₁ obtain₂ obtain₃ :
  ∀ (n : ℕ) (f₀ : MvPolynomial (Fin n) R →ₐ[R] P)
    (hf₀ :
      Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P)
        (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)),
    FormallySmooth R S
obtain₄ :
  ∀ (n : ℕ) (f₀ : MvPolynomial (Fin n) R →ₐ[R] P)
    (hf₀ :
      Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P)
        (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)),
    let M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M;
    let P' := Localization M';
    let fP : P' →ₐ[R] S :=
      IsLocalization.liftAlgHom (R := MvPolynomial (Fin n) R) (M := M') (f :=
        AlgHom.comp (IsScalarTower.toAlgHom R P S) f₀) ⋯;
    ∀ (hf₁ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := P') (β := S) (⇑fP : (a : P') → S)), FormallySmooth R S
⊢ FormallySmooth R S
have obtain₅ : ∀ (n : ℕ) (f₀ : MvPolynomial (Fin n) R →ₐ[R] P)
  (hf₀ :
    Function.Surjective.{u_1 + 1, u_3 + 1} (α := MvPolynomial (Fin n) R) (β := P)
      (⇑f₀ : (a : MvPolynomial (Fin n) R) → P)),
  let M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M;
  let P' := Localization M';
  let fP : P' →ₐ[R] S :=
    IsLocalization.liftAlgHom (R := MvPolynomial (Fin n) R) (M := M') (f :=
      AlgHom.comp (IsScalarTower.toAlgHom R P S) f₀) sorry;
  ∀ (hf₁ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := P') (β := S) (⇑fP : (a : P') → S))
    (hfP : Ideal.FG (RingHom.ker fP)), FormallySmooth R S
Tactic: classical
  obtain ⟨n, f₀, hf₀⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp
    (inferInstance : Algebra.FiniteType R P)
  let M' := M.comap f₀
  let P' := Localization M'
  let fP : P' →ₐ[R] S := IsLocalization.liftAlgHom (M := M')
      (f := (IsScalarTower.toAlgHom R P S).comp f₀) fun x ↦ by
    simpa using IsLocalization.map_units (M := M) _ ⟨f₀ x.1, x.2⟩
  have hf₁ : Function.Surjective fP := by
    intro x
    obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x
    obtain ⟨x, rfl⟩ := hf₀ x
    obtain ⟨s, rfl⟩ := hf₀ s
    refine ⟨IsLocalization.mk' (M := M') _ x ⟨s, hs⟩, ?_⟩
    simp [fP, IsLocalization.lift_mk', Units.mul_inv_eq_iff_eq_mul, IsUnit.liftRight]
  have hfP : (RingHom.ker fP).FG := by
    have := Algebra.FinitePresentation.ker_fG_of_surjective _ hf₀
    convert! this.map (algebraMap _ P')
    refine le_antisymm ?_ (Ideal.map_le_iff_le_comap.mpr fun x hx ↦ by simp_all [fP])
    intro x hx
    obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M' x
    obtain ⟨a, ha, e⟩ : ∃ a ∈ M, a * f₀ x = 0 := by
      simpa [fP, IsLocalization.lift_mk', IsLocalization.map_eq_zero_iff M] using hx
    obtain ⟨a, rfl⟩ := hf₀ a
    rw [IsLocalization.mk'_mem_map_algebraMap_iff]
    exact ⟨a, ha, by simpa⟩
  algebraize [fP.toRingHom]
  have : FormallyEtale (MvPolynomial (Fin n) R) P' := .of_isLocalization M'
  have : FormallySmooth R P' := .comp _ (MvPolynomial (Fin n) R) _
  have : Module.Free P' Ω[P'⁄R] :=
    .of_equiv (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R (MvPolynomial (Fin n) R) P')
  exact FormallySmooth.of_formallySmooth_residueField_tensor_aux (R := R) (S := S) hf₁ hfP