awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this : IsPushout R Rp S Sp
⊢ FinitePresentation Rp Sp

Tactic:
.equiv (Algebra.IsPushout.equiv R Rp S Sp)

Premises used: Algebra.FinitePresentation.equiv, Algebra.IsPushout.equiv
-- 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_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this : IsPushout R Rp S Sp
⊢ FinitePresentation Rp Sp

Tactic:
exact .equiv (Algebra.IsPushout.equiv R Rp S Sp)
-- 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
⊢ 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)
-- 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_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this_5 : FinitePresentation Rp Sp
this : Algebra S (𝓀[Rp] ⊗[R] S) := TensorProduct.rightAlgebra
⊢ FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[R] S ⊗[S] Sq)

Tactic:
have : FormallySmooth 𝓀[Rp] ((𝓀[Rp] ⊗[R] S) ⊗[S] Sq) :=
      .comp _ (𝓀[Rp] ⊗[R] 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_2 : IsScalarTower R Sp Sq
this_3 : IsScalarTower Rp Sp Sq
this_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this_5 : FinitePresentation Rp Sp
this_6 : Algebra S (𝓀[Rp] ⊗[R] S) := TensorProduct.rightAlgebra
this : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[R] S ⊗[S] Sq)
e : 𝓀[Rp] ⊗[R] S ≃ₐ[S] S ⊗[R] 𝓀[Rp] :=
  let __spread.0 : 𝓀[Rp] ⊗[R] S ≃ₐ[R] S ⊗[R] 𝓀[Rp] := TensorProduct.comm R 𝓀[Rp] S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e' : 𝓀[Rp] ⊗[R] S ⊗[S] Sq ≃ₐ[R] 𝓀[Rp] ⊗[Rp] Sq :=
  AlgEquiv.trans (AlgEquiv.restrictScalars R (TensorProduct.comm S (𝓀[Rp] ⊗[R] S) Sq))
    (AlgEquiv.trans (A₂ := Sq ⊗[S] (S ⊗[R] 𝓀[Rp]))
      (AlgEquiv.restrictScalars R (S := S)
        (TensorProduct.congr AlgEquiv.refl e : Sq ⊗[S] (𝓀[Rp] ⊗[R] S) ≃ₐ[S] Sq ⊗[S] (S ⊗[R] 𝓀[Rp])))
      (AlgEquiv.trans (A₂ := Sq ⊗[R] 𝓀[Rp])
        (AlgEquiv.restrictScalars R
          (TensorProduct.cancelBaseChange R S S Sq 𝓀[Rp] : Sq ⊗[S] (S ⊗[R] 𝓀[Rp]) ≃ₐ[S] Sq ⊗[R] 𝓀[Rp]))
        (AlgEquiv.trans (TensorProduct.comm R Sq 𝓀[Rp]) (TensorProduct.equivOfCompatibleSMul Rp R R 𝓀[Rp] Sq))))
⊢ Eq (α := p.ResidueField →ₐ[R] 𝓀[Rp] ⊗[Rp] Sq)
    ((↑e' : 𝓀[Rp] ⊗[R] S ⊗[S] Sq →ₐ[R] 𝓀[Rp] ⊗[Rp] Sq).comp
      (IsScalarTower.toAlgHom R p.ResidueField (𝓀[Rp] ⊗[R] S ⊗[S] Sq)))
    (IsScalarTower.toAlgHom R p.ResidueField (𝓀[Rp] ⊗[Rp] Sq))

Tactic:
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_2 : IsScalarTower R Sp Sq
this_3 : IsScalarTower Rp Sp Sq
this_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this_5 : FinitePresentation Rp Sp
this_6 : Algebra S (𝓀[Rp] ⊗[R] S) := TensorProduct.rightAlgebra
this : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[R] S ⊗[S] Sq)
e : 𝓀[Rp] ⊗[R] S ≃ₐ[S] S ⊗[R] 𝓀[Rp] :=
  let __spread.0 : 𝓀[Rp] ⊗[R] S ≃ₐ[R] S ⊗[R] 𝓀[Rp] := TensorProduct.comm R 𝓀[Rp] S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e' : 𝓀[Rp] ⊗[R] S ⊗[S] Sq ≃ₐ[R] 𝓀[Rp] ⊗[Rp] Sq :=
  AlgEquiv.trans (AlgEquiv.restrictScalars R (TensorProduct.comm S (𝓀[Rp] ⊗[R] S) Sq))
    (AlgEquiv.trans (A₂ := Sq ⊗[S] (S ⊗[R] 𝓀[Rp]))
      (AlgEquiv.restrictScalars R (S := S)
        (TensorProduct.congr AlgEquiv.refl e : Sq ⊗[S] (𝓀[Rp] ⊗[R] S) ≃ₐ[S] Sq ⊗[S] (S ⊗[R] 𝓀[Rp])))
      (AlgEquiv.trans (A₂ := Sq ⊗[R] 𝓀[Rp])
        (AlgEquiv.restrictScalars R
          (TensorProduct.cancelBaseChange R S S Sq 𝓀[Rp] : Sq ⊗[S] (S ⊗[R] 𝓀[Rp]) ≃ₐ[S] Sq ⊗[R] 𝓀[Rp]))
        (AlgEquiv.trans (TensorProduct.comm R Sq 𝓀[Rp]) (TensorProduct.equivOfCompatibleSMul Rp R R 𝓀[Rp] Sq))))
⊢ Eq (α := p.ResidueField →ₐ[R] 𝓀[Rp] ⊗[Rp] Sq)
    ((↑e' : 𝓀[Rp] ⊗[R] S ⊗[S] Sq →ₐ[R] 𝓀[Rp] ⊗[Rp] Sq).comp
      (IsScalarTower.toAlgHom R p.ResidueField (𝓀[Rp] ⊗[R] S ⊗[S] Sq)))
    (IsScalarTower.toAlgHom R p.ResidueField (𝓀[Rp] ⊗[Rp] Sq))

Tactic:
have : e'.toAlgHom.comp (IsScalarTower.toAlgHom R p.ResidueField _) =
        IsScalarTower.toAlgHom _ _ _ := by 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_2 : IsScalarTower R Sp Sq
this_3 : IsScalarTower Rp Sp Sq
this_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this_5 : FinitePresentation Rp Sp
this_6 : Algebra S (𝓀[Rp] ⊗[R] S) := TensorProduct.rightAlgebra
this_7 : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[R] S ⊗[S] Sq)
e : 𝓀[Rp] ⊗[R] S ≃ₐ[S] S ⊗[R] 𝓀[Rp] :=
  let __spread.0 : 𝓀[Rp] ⊗[R] S ≃ₐ[R] S ⊗[R] 𝓀[Rp] := TensorProduct.comm R 𝓀[Rp] S;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
e' : 𝓀[Rp] ⊗[R] S ⊗[S] Sq ≃ₐ[R] 𝓀[Rp] ⊗[Rp] Sq :=
  AlgEquiv.trans (AlgEquiv.restrictScalars R (TensorProduct.comm S (𝓀[Rp] ⊗[R] S) Sq))
    (AlgEquiv.trans (A₂ := Sq ⊗[S] (S ⊗[R] 𝓀[Rp]))
      (AlgEquiv.restrictScalars R (S := S)
        (TensorProduct.congr AlgEquiv.refl e : Sq ⊗[S] (𝓀[Rp] ⊗[R] S) ≃ₐ[S] Sq ⊗[S] (S ⊗[R] 𝓀[Rp])))
      (AlgEquiv.trans (A₂ := Sq ⊗[R] 𝓀[Rp])
        (AlgEquiv.restrictScalars R
          (TensorProduct.cancelBaseChange R S S Sq 𝓀[Rp] : Sq ⊗[S] (S ⊗[R] 𝓀[Rp]) ≃ₐ[S] Sq ⊗[R] 𝓀[Rp]))
        (AlgEquiv.trans (TensorProduct.comm R Sq 𝓀[Rp]) (TensorProduct.equivOfCompatibleSMul Rp R R 𝓀[Rp] Sq))))
this :
  Eq (α := p.ResidueField →ₐ[R] 𝓀[Rp] ⊗[Rp] Sq)
    ((↑e' : 𝓀[Rp] ⊗[R] S ⊗[S] Sq →ₐ[R] 𝓀[Rp] ⊗[Rp] Sq).comp
      (IsScalarTower.toAlgHom R p.ResidueField (𝓀[Rp] ⊗[R] S ⊗[S] Sq)))
    (IsScalarTower.toAlgHom R p.ResidueField (𝓀[Rp] ⊗[Rp] Sq))
e'' : 𝓀[Rp] ⊗[R] S ⊗[S] Sq ≃ₐ[𝓀[Rp]] 𝓀[Rp] ⊗[Rp] Sq :=
  let __spread.0 := e';
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq)

Tactic:
.of_equiv e''

Premises used: Algebra.FormallySmooth.of_equiv
-- 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_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this : FinitePresentation Rp Sp
⊢ FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq)

Tactic:
have : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq) := by
    let : Algebra S (𝓀[Rp] ⊗[R] S) := TensorProduct.rightAlgebra
    have : FormallySmooth 𝓀[Rp] ((𝓀[Rp] ⊗[R] S) ⊗[S] Sq) :=
      .comp _ (𝓀[Rp] ⊗[R] S) _
    let e : 𝓀[Rp] ⊗[R] S ≃ₐ[S] S ⊗[R] 𝓀[Rp] :=
      { __ := TensorProduct.comm _ _ _, commutes' _ := rfl }
    let e' : (𝓀[Rp] ⊗[R] S) ⊗[S] Sq ≃ₐ[R] 𝓀[Rp] ⊗[Rp] Sq :=
      ((TensorProduct.comm _ _ _).restrictScalars R).trans <|
      ((TensorProduct.congr (.refl (R := S)) e).restrictScalars R).trans <|
      ((TensorProduct.cancelBaseChange _ _ S _ _).restrictScalars R).trans <|
      (TensorProduct.comm _ _ _).trans (TensorProduct.equivOfCompatibleSMul ..)
    have : e'.toAlgHom.comp (IsScalarTower.toAlgHom R p.ResidueField _) =
        IsScalarTower.toAlgHom _ _ _ := by ext
    let e'' : (𝓀[Rp] ⊗[R] S) ⊗[S] Sq ≃ₐ[𝓀[Rp]] 𝓀[Rp] ⊗[Rp] Sq :=
      { __ := e', commutes' r := congr($this r) }
    exact .of_equiv e''
-- 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_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this_5 : FinitePresentation Rp Sp
this : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq)
⊢ FormallySmooth Rp Sq

Tactic:
have := FormallySmooth.of_formallySmooth_residueField_tensor
    (R := Rp) (S := Sq) (P := Sp) (algebraMapSubmonoid _ q.primeCompl)
-- 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_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this_5 : FinitePresentation Rp Sp
this_6 : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq)
this : FormallySmooth Rp Sq
⊢ IsSmoothAt R q

Tactic:
.comp R Rp Sq

Premises used: Algebra.FormallySmooth.comp
-- 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_4 : IsLocalization (algebraMapSubmonoid Sp q.primeCompl) Sq
this_5 : FinitePresentation Rp Sp
this_6 : FormallySmooth 𝓀[Rp] (𝓀[Rp] ⊗[Rp] Sq)
this : FormallySmooth Rp Sq
⊢ IsSmoothAt R q

Tactic:
exact .comp R Rp Sq
-- 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
H : ∀ (I : Ideal R) [inst_5 : I.IsPrime], FormallySmooth I.ResidueField (I.Fiber S)
⊢ Smooth R S

Tactic:
⟨smoothLocus_eq_univ_iff.mp (Set.eq_univ_iff_forall.mpr fun q ↦ ?_), ‹_›⟩

Premises used: Iff.mpr, Algebra.Smooth.mk, Algebra.smoothLocus_eq_univ_iff, Set.eq_univ_iff_forall, Iff.mp
-- 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
H : ∀ (I : Ideal R) [inst_5 : I.IsPrime], FormallySmooth I.ResidueField (I.Fiber S)
refine : ∀ (q : PrimeSpectrum S), Membership.mem (γ := Set (PrimeSpectrum S)) (smoothLocus R S) q
⊢ Smooth R S

Tactic:
refine ⟨smoothLocus_eq_univ_iff.mp (Set.eq_univ_iff_forall.mpr fun q ↦ ?_), ‹_›⟩
-- 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
H : ∀ (I : Ideal R) [inst_5 : I.IsPrime], FormallySmooth I.ResidueField (I.Fiber S)
q : PrimeSpectrum S
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) (smoothLocus R S) q

Tactic:
.of_formallySmooth_fiber (q.asIdeal.under R) _

Premises used: Set.Mem, Algebra.IsSmoothAt.of_formallySmooth_fiber, setOf, Algebra.smoothLocus, PrimeSpectrum.asIdeal, Ideal.under
-- 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
H : ∀ (I : Ideal R) [inst_5 : I.IsPrime], FormallySmooth I.ResidueField (I.Fiber S)
q : PrimeSpectrum S
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) (smoothLocus R S) q

Tactic:
exact .of_formallySmooth_fiber (q.asIdeal.under R) _
-- Module: Mathlib.RingTheory.Smooth.Fiber
Goal:
R : Type u_4
S : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FinitePresentation R S
inst_4 : Module.Flat R S
inst_5 : FormallyUnramified R S
⊢ Etale R S

Tactic:
have : Smooth R S := .of_formallySmooth_fiber inferInstance
  ⟨⟨inferInstance, inferInstance⟩, ‹_›⟩

Premises used: Algebra.Etale.mk, Algebra.FormallyEtale.mk, inferInstance, Algebra.Smooth.of_formallySmooth_fiber
-- 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
q : Ideal S
inst_5 : q.IsPrime
inst_6 : IsUnramifiedAt R q
obtain : ∀ (f : S) (hfp : f ∉ q) (H : Unramified.{u_1, u_2} R (Localization.Away f)), IsEtaleAt R q
⊢ IsEtaleAt R q

Tactic:
obtain ⟨f, hfp, H⟩ := exists_unramified_of_isUnramifiedAt (R := R) q

Premises used: Algebra.exists_unramified_of_isUnramifiedAt
-- 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
q : Ideal S
inst_5 : q.IsPrime
inst_6 : IsUnramifiedAt R q
f : S
hfp : f ∉ q
H : Unramified.{u_1, u_2} R (Localization.Away f)
change :
  Membership.mem (γ := Set (PrimeSpectrum S)) (etaleLocus R S) { asIdeal := q, isPrime := inst_5 : PrimeSpectrum S }
⊢ IsEtaleAt R q

Tactic:
change ⟨q, ‹_›⟩ ∈ etaleLocus R S

Premises used: Algebra.etaleLocus
-- 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
q : Ideal S
inst_5 : q.IsPrime
inst_6 : IsUnramifiedAt R q
f : S
hfp : f ∉ q
H : Unramified.{u_1, u_2} R (Localization.Away f)
suffices : Etale.{u_1, u_2} R (Localization.Away f)
⊢ Membership.mem (γ := Set (PrimeSpectrum S)) (etaleLocus R S) { asIdeal := q, isPrime := inst_5 : PrimeSpectrum S }

Tactic:
suffices Algebra.Etale R (Localization.Away f) from
    (basicOpen_subset_etaleLocus_iff (R := R) (f := f)).mpr inferInstance hfp
-- 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
q : Ideal S
inst_5 : q.IsPrime
inst_6 : IsUnramifiedAt R q
f : S
hfp : f ∉ q
H : Unramified.{u_1, u_2} R (Localization.Away f)
⊢ Etale.{u_1, u_2} R (Localization.Away f)

Tactic:
.of_formallyUnramified_of_flat

Premises used: Algebra.Etale.of_formallyUnramified_of_flat
-- 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
q : Ideal S
inst_5 : q.IsPrime
inst_6 : IsUnramifiedAt R q
f : S
hfp : f ∉ q
H : Unramified.{u_1, u_2} R (Localization.Away f)
⊢ Etale.{u_1, u_2} R (Localization.Away f)

Tactic:
exact .of_formallyUnramified_of_flat
-- Module: Mathlib.RingTheory.Smooth.Field
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
⊢ FormallySmooth.{u_1, u_2} K ↥(adjoin K (Set.range v))

Tactic:
have : Algebra.FormallySmooth K (adjoin K (Set.range v)) :=
    .of_equiv hb.aevalEquiv
-- Module: Mathlib.RingTheory.Smooth.Field
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
this : FormallySmooth.{u_1, u_2} K ↥(adjoin K (Set.range v))
⊢ FormallySmooth.{u_2, u_2} ↥(adjoin K (Set.range v)) ↥(IntermediateField.adjoin K (Set.range v))

Tactic:
have : Algebra.FormallySmooth (adjoin K (Set.range v))
      (IntermediateField.adjoin K (Set.range v)) :=
    .of_isLocalization (nonZeroDivisors _)
-- Module: Mathlib.RingTheory.Smooth.Field
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
this_1 : FormallySmooth.{u_1, u_2} K ↥(adjoin K (Set.range v))
this : FormallySmooth.{u_2, u_2} ↥(adjoin K (Set.range v)) ↥(IntermediateField.adjoin K (Set.range v))
⊢ FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))

Tactic:
.comp _ (adjoin K (Set.range v)) _

Premises used: Algebra.adjoin, Membership.mem, Subtype, Set.range, Algebra.FormallySmooth.comp
-- Module: Mathlib.RingTheory.Smooth.Field
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
this_1 : FormallySmooth.{u_1, u_2} K ↥(adjoin K (Set.range v))
this : FormallySmooth.{u_2, u_2} ↥(adjoin K (Set.range v)) ↥(IntermediateField.adjoin K (Set.range v))
⊢ FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))

Tactic:
exact .comp _ (adjoin K (Set.range v)) _
-- Module: Mathlib.RingTheory.Smooth.Field
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
hb' : Eq (α := IntermediateField K L) (IntermediateField.adjoin K (Set.range v)) ⊤
⊢ FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))

Tactic:
have := Algebra.FormallySmooth.adjoin_of_algebraicIndependent hb
-- Module: Mathlib.RingTheory.Smooth.Field
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
hb' : Eq (α := IntermediateField K L) (IntermediateField.adjoin K (Set.range v)) ⊤
this : FormallySmooth.{u_1, u_2} K ↥(IntermediateField.adjoin K (Set.range v))
⊢ FormallySmooth.{u_1, u_2} K ↥⊤

Tactic:
rw [hb'] at this
-- Module: Mathlib.RingTheory.Smooth.Field
Goal:
K : Type u_1
L : Type u_2
ι : Type u_3
inst : Field L
inst_1 : Field K
inst_2 : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
hb' : Eq (α := IntermediateField K L) (IntermediateField.adjoin K (Set.range v)) ⊤
this : FormallySmooth.{u_1, u_2} K ↥⊤
⊢ FormallySmooth K L

Tactic:
.of_equiv IntermediateField.topEquiv

Premises used: Algebra.FormallySmooth.of_equiv, IntermediateField.topEquiv