awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ FormallySmooth R S

Tactic:
obtain ⟨n, f₀, hf₀⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp
    (inferInstance : Algebra.FiniteType R P)

Premises used: inferInstance, Iff.mp, Algebra.FiniteType.iff_quotient_mvPolynomial''
-- 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)
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'
x : ↥M'
⊢ IsUnit.{u_2} (M := S)
    ((AlgHom.comp (IsScalarTower.toAlgHom R P S) f₀ : (a : MvPolynomial (Fin n) R) → S) (↑x : MvPolynomial (Fin n) R) :
      S)

Tactic:
simpa using IsLocalization.map_units (M := M) _ ⟨f₀ x.1, x.2⟩

Premises used: Subtype.mk, IsLocalization.map_units, Subtype.val, DFunLike.coe, Subtype.property
-- 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)
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₀)
    ⋯
x : S
obtain :
  ∀ (x s : P) (hs : s ∈ M),
    ∃ (a : P'), (fP : (a : P') → S) a = IsLocalization.mk' S x (Subtype.mk (p := fun (x : P) ↦ x ∈ M) s hs)
⊢ ∃ (a : P'), (fP : (a : P') → S) a = x

Tactic:
obtain ⟨x, ⟨s, hs⟩, rfl⟩ := IsLocalization.exists_mk'_eq M x

Premises used: rfl, IsLocalization.exists_mk'_eq
-- 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)
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₀)
    ⋯
x s : P
hs : s ∈ M
obtain :
  ∀ (x : MvPolynomial (Fin n) R),
    ∃ (a : P'),
      (fP : (a : P') → S) a =
        IsLocalization.mk' S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ M) s hs)
⊢ ∃ (a : P'), (fP : (a : P') → S) a = IsLocalization.mk' S x (Subtype.mk (p := fun (x : P) ↦ x ∈ M) s hs)

Tactic:
obtain ⟨x, rfl⟩ := hf₀ x

Premises used: rfl
-- 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)
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₀)
    ⋯
s : P
hs : s ∈ M
x : MvPolynomial (Fin n) R
obtain :
  ∀ (s : MvPolynomial (Fin n) R) (hs : Membership.mem (α := P) M ((f₀ : (a : MvPolynomial (Fin n) R) → P) s : P)),
    ∃ (a : P'),
      (fP : (a : P') → S) a =
        IsLocalization.mk'.{u_3, u_2} (R := P) (M := M) S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P)
          (Subtype.mk (p := fun (x : P) ↦ x ∈ M) ((f₀ : (a : MvPolynomial (Fin n) R) → P) s) hs : ↥M)
⊢ ∃ (a : P'),
    (fP : (a : P') → S) a =
      IsLocalization.mk' S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x) (Subtype.mk (p := fun (x : P) ↦ x ∈ M) s hs)

Tactic:
obtain ⟨s, rfl⟩ := hf₀ s

Premises used: rfl
-- 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)
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₀)
    ⋯
x s : MvPolynomial (Fin n) R
hs : Membership.mem (α := P) M ((f₀ : (a : MvPolynomial (Fin n) R) → P) s : P)
⊢ ∃ (a : P'),
    (fP : (a : P') → S) a =
      IsLocalization.mk'.{u_3, u_2} (R := P) (M := M) S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P)
        (Subtype.mk (p := fun (x : P) ↦ x ∈ M) ((f₀ : (a : MvPolynomial (Fin n) R) → P) s) hs : ↥M)

Tactic:
⟨IsLocalization.mk' (M := M') _ x ⟨s, hs⟩, ?_⟩

Premises used: Subtype.mk, IsLocalization.mk', Exists.intro
-- 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)
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₀)
    ⋯
x s : MvPolynomial (Fin n) R
hs : Membership.mem (α := P) M ((f₀ : (a : MvPolynomial (Fin n) R) → P) s : P)
refine :
  (fP : (a : P') → S)
      (IsLocalization.mk' (M := M') P' x (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦ x ∈ M') s hs)) =
    IsLocalization.mk'.{u_3, u_2} (R := P) (M := M) S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ M) ((f₀ : (a : MvPolynomial (Fin n) R) → P) s) hs : ↥M)
⊢ ∃ (a : P'),
    (fP : (a : P') → S) a =
      IsLocalization.mk'.{u_3, u_2} (R := P) (M := M) S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P)
        (Subtype.mk (p := fun (x : P) ↦ x ∈ M) ((f₀ : (a : MvPolynomial (Fin n) R) → P) s) hs : ↥M)

Tactic:
refine ⟨IsLocalization.mk' (M := M') _ x ⟨s, hs⟩, ?_⟩
-- 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)
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₀)
    ⋯
x s : MvPolynomial (Fin n) R
hs : Membership.mem (α := P) M ((f₀ : (a : MvPolynomial (Fin n) R) → P) s : P)
⊢ (fP : (a : P') → S)
      (IsLocalization.mk' (M := M') P' x (Subtype.mk (p := fun (x : MvPolynomial (Fin n) R) ↦ x ∈ M') s hs)) =
    IsLocalization.mk'.{u_3, u_2} (R := P) (M := M) S ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ M) ((f₀ : (a : MvPolynomial (Fin n) R) → P) s) hs : ↥M)

Tactic:
simp [fP, IsLocalization.lift_mk', Units.mul_inv_eq_iff_eq_mul, IsUnit.liftRight]

Premises used: IsUnit.liftRight, Units.mul_inv_eq_iff_eq_mul, IsLocalization.lift_mk'
-- 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)
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₀)
    ⋯
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := P') (β := S) (⇑fP : (a : P') → S)

Tactic:
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]
-- 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)
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)
⊢ Ideal.FG (RingHom.ker f₀.toRingHom)

Tactic:
have := Algebra.FinitePresentation.ker_fG_of_surjective _ hf₀
-- 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)
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)
⊢ Ideal.FG (R := P')
    (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))

Tactic:
this.map (algebraMap _ P')

Premises used: Algebra.algebraMap, Ideal.FG.map
-- 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)
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)
h :
  Eq (α := Ideal P') (RingHom.ker fP)
    (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
⊢ Ideal.FG (RingHom.ker fP)

Tactic:
convert! this.map (algebraMap _ P')

Premises used: Algebra.algebraMap, Ideal.FG.map
-- 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)
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
hx : Membership.mem (γ := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)) (RingHom.ker f₀.toRingHom) x
⊢ Membership.mem (γ := Submodule (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R))
    (Ideal.comap (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker fP)) x

Tactic:
simp_all [fP]
-- 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)
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)
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))
⊢ Eq (α := 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])

Premises used: Iff.mpr, Ideal.map_le_iff_le_comap, le_antisymm
-- 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)
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
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)
⊢ Membership.mem (γ := Submodule P' P')
    (Ideal.map (F := MvPolynomial (Fin n) R →+* P') (algebraMap (MvPolynomial (Fin n) R) P') (RingHom.ker f₀.toRingHom))
    x

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M' x

Premises used: rfl, IsLocalization.exists_mk'_eq
-- 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)
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 ∈ M, HMul.hMul (β := P) a ((f₀ : (a : MvPolynomial (Fin n) R) → P) x : P) = 0

Tactic:
simpa [fP, IsLocalization.lift_mk', IsLocalization.map_eq_zero_iff M] using hx

Premises used: IsLocalization.map_eq_zero_iff, IsLocalization.lift_mk'
-- 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)
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)
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)
⊢ 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

Premises used: DFunLike.coe