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
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
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)
⊢ 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

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₀)
    ⋯
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
h : ∃ s ∈ M', Membership.mem (γ := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker f₀.toRingHom) (s * x)
⊢ 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:
rw [IsLocalization.mk'_mem_map_algebraMap_iff]

Premises used: IsLocalization.mk'_mem_map_algebraMap_iff
-- 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 : 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 (γ := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker f₀.toRingHom) (a * x)

Tactic:
simpa
-- 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 : 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
⊢ ∃ s ∈ M', Membership.mem (γ := Ideal (MvPolynomial (Fin n) R)) (RingHom.ker f₀.toRingHom) (s * x)

Tactic:
exact ⟨a, ha, by simpa⟩
-- 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 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⟩
-- 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)
hfP : Ideal.FG (RingHom.ker fP)
algInst : Algebra P' S := fP.toAlgebra
⊢ FormallyEtale (MvPolynomial (Fin n) R) P'

Tactic:
have : FormallyEtale (MvPolynomial (Fin n) R) P' := .of_isLocalization M'
-- 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)
hfP : Ideal.FG (RingHom.ker fP)
algInst : Algebra P' S := fP.toAlgebra
this : FormallyEtale (MvPolynomial (Fin n) R) P'
⊢ FormallySmooth R P'

Tactic:
have : FormallySmooth R P' := .comp _ (MvPolynomial (Fin n) R) _
-- 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)
hfP : Ideal.FG (RingHom.ker fP)
algInst : Algebra P' S := fP.toAlgebra
this_1 : FormallyEtale (MvPolynomial (Fin n) R) P'
this : FormallySmooth R P'
⊢ Module.Free P' Ω[P'⁄R]

Tactic:
have : Module.Free P' Ω[P'⁄R] :=
    .of_equiv (KaehlerDifferential.tensorKaehlerEquivOfFormallyEtale R (MvPolynomial (Fin n) R) P')
-- 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)
hfP : Ideal.FG (RingHom.ker fP)
algInst : Algebra P' S := fP.toAlgebra
this_1 : FormallyEtale (MvPolynomial (Fin n) R) P'
this_2 : FormallySmooth R P'
this : Module.Free P' Ω[P'⁄R]
⊢ FormallySmooth R S

Tactic:
FormallySmooth.of_formallySmooth_residueField_tensor_aux (R := R) (S := S) hf₁ hfP

Premises used: _private.0.Algebra.FormallySmooth.of_formallySmooth_residueField_tensor_aux
-- 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)
hfP : Ideal.FG (RingHom.ker fP)
algInst : Algebra P' S := fP.toAlgebra
this_1 : FormallyEtale (MvPolynomial (Fin n) R) P'
this_2 : FormallySmooth R P'
this : Module.Free P' Ω[P'⁄R]
⊢ FormallySmooth R S

Tactic:
exact FormallySmooth.of_formallySmooth_residueField_tensor_aux (R := R) (S := S) hf₁ hfP

Premises used: _private.0.Algebra.FormallySmooth.of_formallySmooth_residueField_tensor_aux
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
x : R
hx : x ∈ (↑p.primeCompl : Set R)
⊢ Membership.mem (α := S) q.primeCompl ((algebraMap R S : (a : R) → S) x : S)

Tactic:
simp_all [q.over_def p]

Premises used: Ideal.over_def
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
x : R
hx : x ∈ (↑p.primeCompl : Set R)
⊢ IsUnit (M := Sq)
    ((ofId S Sq : (a : S) → Sq)
        (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (algebraMapSubmonoid S p.primeCompl) x)
              ((algebraMap R S : (a : R) → S) x) ⋯) :
          S) :
      Sq)

Tactic:
simpa using IsLocalization.map_units (M := q.primeCompl) Sq ⟨algebraMap _ _ x,
        by simp_all [q.over_def p]⟩

Premises used: Algebra.algebraMap, Subtype.mk, IsLocalization.map_units, DFunLike.coe
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
⊢ IsScalarTower R Sp Sq

Tactic:
have : IsScalarTower R Sp Sq := .to₁₃₄ _ S _ _
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
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))
⊢ algebraMap Rp Sq = RingHom.comp (algebraMap Sp Sq) (algebraMap Rp Sp)

Tactic:
apply IsLocalization.ringHom_ext p.primeCompl

Premises used: Ideal.primeCompl, IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
⊢ 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:
simp only [RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq]

Premises used: RingHom.comp_assoc, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
⊢ 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]
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
x : R
hx : x ∈ (↑p.primeCompl : Set R)
⊢ Membership.mem (α := S) q.primeCompl ((algebraMap R S : (a : R) → S) x : S)

Tactic:
simp_all [q.over_def p]

Premises used: Ideal.over_def
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
⊢ 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])
-- Module: Mathlib.RingTheory.Smooth.Fiber
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
⊢ IsPushout R Rp S Sp

Tactic:
have : Algebra.IsPushout R Rp S Sp :=
      .symm <| Algebra.isPushout_of_isLocalization p.primeCompl _ _ _