awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
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)
this : Ideal.FG (RingHom.ker f₀.toRingHom)
⊢ Eq (α := Ideal P') (RingHom.ker fP)
    (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
have h : LE.le (α := Ideal P') (RingHom.ker fP)
  (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
Tactic: refine le_antisymm ?_ (Ideal.map_le_iff_le_comap.mpr fun x hx ↦ by simp_all [fP])
-- 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
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)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
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)
this : Ideal.FG (RingHom.ker f₀.toRingHom)
x : P'
hx : Membership.mem (γ := Submodule P' P') (RingHom.ker fP) x
⊢ Membership.mem (γ := Submodule P' P')
    (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
    x
have h : ∀ (x : MvPolynomial (Fin n) R) (s : ↥M')
  (hx : Membership.mem (γ := Submodule P' P') (RingHom.ker fP) (IsLocalization.mk' P' x s)),
  Membership.mem (γ := Submodule P' P')
    (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
    (IsLocalization.mk' P' x s)
Tactic: obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M' x
Cleared hypotheses: x, hx
-- 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
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)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
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)
this : Ideal.FG (RingHom.ker f₀.toRingHom)
x : MvPolynomial (Fin n) R
s : ↥M'
hx : Membership.mem (γ := Submodule P' P') (RingHom.ker fP) (IsLocalization.mk' P' x s)
⊢ Membership.mem (γ := Submodule P' P')
    (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
    (IsLocalization.mk' P' x s)
have h : ∀ (a : P) (ha : a ∈ M) (e : HMul.hMul (β := P) a ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P) = 0),
  Membership.mem (γ := Submodule P' P')
    (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
    (IsLocalization.mk' P' x s)
Tactic: obtain ⟨a, ha, e⟩ : ∃ a ∈ M, a * f₀ x = 0 := by
      simpa [fP, IsLocalization.lift_mk', IsLocalization.map_eq_zero_iff M] using hx
-- 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
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)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
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)
this : Ideal.FG (RingHom.ker f₀.toRingHom)
x : MvPolynomial (Fin n) R
s : ↥M'
hx : Membership.mem (γ := Submodule P' P') (RingHom.ker fP) (IsLocalization.mk' P' x s)
a : P
ha : a ∈ M
e : HMul.hMul (β := P) a ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P) = 0
⊢ Membership.mem (γ := Submodule P' P')
    (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
    (IsLocalization.mk' P' x s)
have h : ∀ (a : MvPolynomial (Fin n) R) (ha : Membership.mem (α := P) M ((f₀ : (a : MvPolynomial (Fin n) R) → P) a : P))
  (e :
    HMul.hMul (α := P) (β := P) ((f₀ : (a : MvPolynomial (Fin n) R) → P) a : P)
        ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P) =
      0),
  Membership.mem (γ := Submodule P' P')
    (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
    (IsLocalization.mk' P' x s)
Tactic: obtain ⟨a, rfl⟩ := hf₀ a
Cleared hypotheses: a, ha, e
-- 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
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)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
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)
this : Ideal.FG (RingHom.ker f₀.toRingHom)
x : MvPolynomial (Fin n) R
s : ↥M'
hx : Membership.mem (γ := Submodule P' P') (RingHom.ker fP) (IsLocalization.mk' P' x s)
a : MvPolynomial (Fin n) R
ha : Membership.mem (α := P) M ((f₀ : (a : MvPolynomial (Fin n) R) → P) a : P)
e :
  HMul.hMul (α := P) (β := P) ((f₀ : (a : MvPolynomial (Fin n) R) → P) a : P)
      ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P) =
    0
⊢ Membership.mem (γ := Submodule P' P')
    (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
    (IsLocalization.mk' P' x s)
have h : ∃ s ∈ M', Membership.mem (γ := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker f₀.toRingHom) (s * x)
Tactic: rw [IsLocalization.mk'_mem_map_algebraMap_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
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
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)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
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
have hfP : Ideal.FG (RingHom.ker fP)
Tactic: 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
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
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)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
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)
hfP : Ideal.FG (RingHom.ker fP)
algInst : Algebra P' S := fP.toAlgebra
⊢ FormallySmooth R S
have this : FormallyEtale (MvPolynomial (Fin n) R) P'
Tactic: have : FormallyEtale (MvPolynomial (Fin n) R) P' := .of_isLocalization M'
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
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
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)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
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)
hfP : Ideal.FG (RingHom.ker fP)
algInst : Algebra P' S := fP.toAlgebra
this : FormallyEtale (MvPolynomial (Fin n) R) P'
⊢ FormallySmooth R S
have this₁ : FormallySmooth R P'
Tactic: have : FormallySmooth R P' := .comp _ (MvPolynomial (Fin n) R) _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
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
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)
M' : Submonoid (MvPolynomial (Fin n) R) := Submonoid.comap f₀ M
P' : Type u_1 := Localization M'
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)
hfP : Ideal.FG (RingHom.ker fP)
algInst : Algebra P' S := fP.toAlgebra
this_1 : FormallyEtale (MvPolynomial (Fin n) R) P'
this : FormallySmooth R P'
⊢ FormallySmooth R S
have this₁ : Module.Free P' Ω[P'⁄R]
Tactic: have : Module.Free P' Ω[P'⁄R] :=
    .of_equiv (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R (MvPolynomial (Fin n) R) P')
-- 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
⊢ 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)),
  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
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
p : Ideal R
q : Ideal S
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
inst_8 : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom (R := S) (M := algebraMapSubmonoid S p.primeCompl) (f := ofId S Sq) ⋯
algInst : Algebra Sp Sq := f.toAlgebra
⊢ IsSmoothAt R q
have this₁ : IsScalarTower R Sp Sq
Tactic: have : IsScalarTower R Sp Sq := .to₁₃₄ _ S _ _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
p : Ideal R
q : Ideal S
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
inst_8 : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom (R := S) (M := algebraMapSubmonoid S p.primeCompl) (f := ofId S Sq) ⋯
algInst : Algebra Sp Sq := f.toAlgebra
this : IsScalarTower R Sp Sq
⊢ algebraMap Rp Sq = RingHom.comp (algebraMap Sp Sq) (algebraMap Rp Sp)
have h : Eq (α := R →+* Sq) (RingHom.comp (algebraMap Rp Sq) (algebraMap R Rp))
  (RingHom.comp (RingHom.comp (algebraMap Sp Sq) (algebraMap Rp Sp)) (algebraMap R Rp))
Tactic: apply IsLocalization.ringHom_ext p.primeCompl
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
p : Ideal R
q : Ideal S
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
inst_8 : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom (R := S) (M := algebraMapSubmonoid S p.primeCompl) (f := ofId S Sq) ⋯
algInst : Algebra Sp Sq := f.toAlgebra
this : IsScalarTower R Sp Sq
⊢ IsSmoothAt R q
have this₁ : IsScalarTower Rp Sp Sq
Tactic: have : IsScalarTower Rp Sp Sq := .of_algebraMap_eq' <| by
    apply IsLocalization.ringHom_ext p.primeCompl
    simp only [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
p : Ideal R
q : Ideal S
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
inst_8 : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom (R := S) (M := algebraMapSubmonoid S p.primeCompl) (f := ofId S Sq) ⋯
algInst : Algebra Sp Sq := f.toAlgebra
this_2 : IsScalarTower R Sp Sq
this : IsScalarTower Rp Sp Sq
⊢ IsSmoothAt R q
have this₁ : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
Tactic: have : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq :=
    .isLocalization_of_submonoid_le _ _ (algebraMapSubmonoid S p.primeCompl) _
    (by rintro _ ⟨x, hx, rfl⟩; simp_all [q.over_def p])
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
p : Ideal R
q : Ideal S
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
inst_8 : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom (R := S) (M := algebraMapSubmonoid S p.primeCompl) (f := ofId S Sq) ⋯
algInst : Algebra Sp Sq := f.toAlgebra
this_2 : IsScalarTower R Sp Sq
this_3 : IsScalarTower Rp Sp Sq
this : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
⊢ FinitePresentation Rp Sp
have this₁ : IsPushout R Rp S Sp
Tactic: have : Algebra.IsPushout R Rp S Sp :=
      .symm <| Algebra.isPushout_of_isLocalization p.primeCompl _ _ _
-- Lean 4 proof step from Mathlib.RingTheory.Smooth.Fiber (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Flat R S
inst_4 : FinitePresentation R S
p : Ideal R
q : Ideal S
inst_5 : p.IsPrime
inst_6 : q.IsPrime
inst_7 : q.LiesOver p
inst_8 : FormallySmooth p.ResidueField (p.Fiber S)
Rp : Type u_1 := Localization.AtPrime p
Sp : Type u_2 := Localization (M := S) (algebraMapSubmonoid S p.primeCompl)
Sq : Type u_2 := Localization.AtPrime q
this_1 : Algebra.{u_1, u_2} (Localization.AtPrime p) (Localization.AtPrime q) :=
  Localization.AtPrime.algebraOfLiesOver p q
f : Sp →ₐ[S] Sq := IsLocalization.liftAlgHom (R := S) (M := algebraMapSubmonoid S p.primeCompl) (f := ofId S Sq) ⋯
algInst : Algebra Sp Sq := f.toAlgebra
this_2 : IsScalarTower R Sp Sq
this_3 : IsScalarTower Rp Sp Sq
this : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
⊢ IsSmoothAt R q
have this₁ : FinitePresentation Rp Sp
Tactic: have : FinitePresentation Rp Sp := by
    have : Algebra.IsPushout R Rp S Sp :=
      .symm <| Algebra.isPushout_of_isLocalization p.primeCompl _ _ _
    exact .equiv (Algebra.IsPushout.equiv R Rp S Sp)