awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this_2 : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
a : P.Fiber S
ha :
  Eq (α := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a :
      (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (0 : (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : (↑(P.primesOver S) : Type u_6) :=
  (OrderIso.symm (PrimeSpectrum.primesOverOrderIsoFiber R S P) :
      (a : PrimeSpectrum (P.Fiber S)) → (↑(P.primesOver S) : Type u_6))
    { asIdeal := J, isPrime := ⋯ }
this : ¬(↑s : Set S) ⊆ (↑(↑I : Ideal S) : Set S)
r : S
hrs : r ∈ (↑s : Set S)
hrI : r ∉ (↑(↑I : Ideal S) : Set S)
ψ : P.Fiber (Localization.Away r) →ₐ[P.ResidueField] Localization.AtPrime J :=
  Algebra.TensorProduct.lift (Algebra.ofId P.ResidueField (Localization.AtPrime J))
    {
      toRingHom :=
        IsLocalization.map (T := J.primeCompl) (Localization.AtPrime J)
          (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ⋯,
      commutes' := ⋯ }
    ⋯
hψ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := Localization.AtPrime J)
    ((ψ : (a : P.Fiber (Localization.Away r)) → Localization.AtPrime J)
        ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a
          (Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hrs)) :
      Localization.AtPrime J)
    (0 : Localization.AtPrime J)

Tactic:
simp only [ha, Pi.zero_apply, map_zero]

Premises used: Pi.zero_apply, map_zero
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f_1 : R →+* S
s : Finset S
hs : Eq (α := Ideal S) (Ideal.span (↑s : Set S)) ⊤
H :
  ∀ (r : ↥s),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (QuasiFinite : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f_1)
algInst : Algebra R S := f_1.toAlgebra
P : Ideal R
h : P.IsPrime
this_1 : ∀ (r : ↥s), Module.Finite.{u_6, u_6} P.ResidueField (P.Fiber (Localization.Away (↑r : S)))
φ : (r : ↥s) → P.Fiber S →ₐ[P.ResidueField] P.Fiber (Localization.Away (↑r : S)) :=
  fun (r : ↥s) ↦
    Algebra.TensorProduct.map (AlgHom.id P.ResidueField P.ResidueField)
      (IsScalarTower.toAlgHom R S (Localization.Away (↑r : S)))
f : P.Fiber S →ₐ[P.ResidueField] (r : ↥s) → P.Fiber (Localization.Away (↑r : S)) :=
  Pi.algHom P.ResidueField (fun (r : ↥s) ↦ P.Fiber (Localization.Away (↑r : S))) φ
this_2 : IsNoetherian.{u_6, u_6} P.ResidueField ((r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
a : P.Fiber S
ha :
  Eq (α := (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    ((f : (a : P.Fiber S) → (r : ↥s) → P.Fiber (Localization.Away (↑r : S))) a :
      (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
    (0 : (r : ↥s) → P.Fiber (Localization.Away (↑r : S)))
J : Ideal (P.Fiber S)
hJ : J.IsMaximal
I : (↑(P.primesOver S) : Type u_6) :=
  (OrderIso.symm (PrimeSpectrum.primesOverOrderIsoFiber R S P) :
      (a : PrimeSpectrum (P.Fiber S)) → (↑(P.primesOver S) : Type u_6))
    { asIdeal := J, isPrime := ⋯ }
this : ¬(↑s : Set S) ⊆ (↑(↑I : Ideal S) : Set S)
r : S
hrs : r ∈ (↑s : Set S)
hrI : r ∉ (↑(↑I : Ideal S) : Set S)
ψ : P.Fiber (Localization.Away r) →ₐ[P.ResidueField] Localization.AtPrime J :=
  Algebra.TensorProduct.lift (Algebra.ofId P.ResidueField (Localization.AtPrime J))
    {
      toRingHom :=
        IsLocalization.map (T := J.primeCompl) (Localization.AtPrime J)
          (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ⋯,
      commutes' := ⋯ }
    ⋯
hψ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := Localization.AtPrime J)
    ((algebraMap (P.Fiber S) (Localization.AtPrime J) : (a : P.Fiber S) → Localization.AtPrime J) a :
      Localization.AtPrime J)
    (0 : Localization.AtPrime J)

Tactic:
refine congr($hψ a).symm.trans
    (show ψ (f a ⟨r, hrs⟩) = 0 by simp only [ha, Pi.zero_apply, map_zero])

Premises used: congrArg, id, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R : Type u_6
S : Type u_7
T : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.IsIntegral
g : S →+* T
hg_1 : g.IsStandardOpenImmersion
hg : (g.comp f).FiniteType
⊢ let algInst := f.toAlgebra;
  Algebra.IsIntegral R S

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R : Type u_6
S : Type u_7
T : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.IsIntegral
g : S →+* T
hg_1 : g.IsStandardOpenImmersion
hg : (g.comp f).FiniteType
algebraizeInst :
  let algInst := f.toAlgebra;
  Algebra.IsIntegral R S
⊢ Algebra.IsStandardOpenImmersion S T

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R : Type u_6
S : Type u_7
T : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.IsIntegral
g : S →+* T
hg_1 : g.IsStandardOpenImmersion
hg : (g.comp f).FiniteType
algebraizeInst :
  let algInst := f.toAlgebra;
  Algebra.IsIntegral R S
algebraizeInst₁ : Algebra.IsStandardOpenImmersion S T
⊢ Algebra.FiniteType R T

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R : Type u_6
S : Type u_7
T : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.IsIntegral
g : S →+* T
hg_1 : g.IsStandardOpenImmersion
hg : (g.comp f).FiniteType
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.IsIntegral R S
algebraizeInst_1 : Algebra.IsStandardOpenImmersion S T
algebraizeInst_2 : Algebra.FiniteType R T
obtain : ∀ (s : S) (hs : IsLocalization.Away s T), (g.comp f).QuasiFinite
⊢ (g.comp f).QuasiFinite

Tactic:
obtain ⟨s, hs⟩ := Algebra.IsStandardOpenImmersion.exists_away S T

Premises used: Algebra.IsStandardOpenImmersion.exists_away
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R : Type u_6
S : Type u_7
T : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.IsIntegral
g : S →+* T
hg_1 : g.IsStandardOpenImmersion
hg : (g.comp f).FiniteType
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.IsIntegral R S
algebraizeInst_1 : Algebra.IsStandardOpenImmersion S T
algebraizeInst_2 : Algebra.FiniteType R T
s : S
hs : IsLocalization.Away s T
⊢ (g.comp f).QuasiFinite

Tactic:
Algebra.QuasiFinite.of_isIntegral_of_finiteType s

Premises used: RingHom.QuasiFinite, Algebra.QuasiFinite.of_isIntegral_of_finiteType
-- Module: Mathlib.RingTheory.RingHom.QuasiFinite
Goal:
R : Type u_6
S : Type u_7
T : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
hf : f.IsIntegral
g : S →+* T
hg_1 : g.IsStandardOpenImmersion
hg : (g.comp f).FiniteType
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.IsIntegral R S
algebraizeInst_1 : Algebra.IsStandardOpenImmersion S T
algebraizeInst_2 : Algebra.FiniteType R T
s : S
hs : IsLocalization.Away s T
⊢ (g.comp f).QuasiFinite

Tactic:
exact Algebra.QuasiFinite.of_isIntegral_of_finiteType s

Premises used: Algebra.QuasiFinite.of_isIntegral_of_finiteType
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FormallySmooth
⊢ Algebra.FormallySmooth R S

Tactic:
hf

Premises used: RingHom.FormallySmooth
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.FormallySmooth R S ↔ Algebra.FormallySmooth R S
rw₁ rw₂ : Algebra.FormallySmooth R S ↔ Algebra.FormallySmooth R S
⊢ FormallySmooth (algebraMap R S) ↔ Algebra.FormallySmooth R S

Tactic:
rw [FormallySmooth, toAlgebra_algebraMap]

Premises used: RingHom.FormallySmooth, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallySmooth
hg : g.FormallySmooth
⊢ Algebra.FormallySmooth R S

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallySmooth
hg : g.FormallySmooth
algebraizeInst : Algebra.FormallySmooth R S
⊢ Algebra.FormallySmooth S T

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallySmooth
hg : g.FormallySmooth
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.FormallySmooth R S
algebraizeInst_1 : Algebra.FormallySmooth S T
⊢ (g.comp f).FormallySmooth

Tactic:
Algebra.FormallySmooth.comp R S T

Premises used: RingHom.FormallySmooth, Algebra.FormallySmooth.comp
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallySmooth
hg : g.FormallySmooth
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.FormallySmooth R S
algebraizeInst_1 : Algebra.FormallySmooth S T
⊢ (g.comp f).FormallySmooth

Tactic:
exact Algebra.FormallySmooth.comp R S T

Premises used: Algebra.FormallySmooth.comp
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
algInst : Algebra R S := f.toAlgebra
⊢ f.FormallySmooth

Tactic:
Algebra.FormallySmooth.of_equiv (AlgEquiv.ofBijective (Algebra.ofId R S) hf)

Premises used: AlgEquiv.ofBijective, Algebra.FormallySmooth.of_equiv, Algebra.ofId, RingHom.FormallySmooth
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
algInst : Algebra R S := f.toAlgebra
⊢ f.FormallySmooth

Tactic:
exact Algebra.FormallySmooth.of_equiv (AlgEquiv.ofBijective (Algebra.ofId R S) hf)

Premises used: AlgEquiv.ofBijective, Algebra.FormallySmooth.of_equiv, Algebra.ofId
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
⊢ HoldsForLocalizationAway @FormallySmooth

Tactic:
fun _ _ _ _ _ r _ ↦ formallySmooth_algebraMap.mpr <| .of_isLocalization (.powers r)

Premises used: Iff.mpr, Algebra.FormallySmooth.of_isLocalization, RingHom.HoldsForLocalizationAway, RingHom.formallySmooth_algebraMap, Submonoid.powers
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
⊢ StableUnderComposition @FormallySmooth

Tactic:
fun _ _ _ _ _ _ _ _ hf hg ↦ hf.comp hg

Premises used: RingHom.FormallySmooth.comp, RingHom.StableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
⊢ RespectsIso @FormallySmooth

Tactic:
stableUnderComposition.respectsIso fun e ↦ holdsForLocalizationAway.of_bijective _ _ e.bijective

Premises used: RingHom.StableUnderComposition.respectsIso, RingHom.HoldsForLocalizationAway.of_bijective, RingHom.FormallySmooth.stableUnderComposition, RingEquiv.toRingHom, RingHom.FormallySmooth.holdsForLocalizationAway, RingEquiv.bijective, RingHom.FormallySmooth
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
⊢ IsStableUnderBaseChange @FormallySmooth

Tactic:
.mk respectsIso ?_

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.FormallySmooth.respectsIso
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
refine :
  ∀ ⦃R S T : Type u_3⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], FormallySmooth (algebraMap R T) → FormallySmooth (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
⊢ IsStableUnderBaseChange @FormallySmooth

Tactic:
refine .mk respectsIso ?_
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R S T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
H : FormallySmooth (algebraMap R T)
rw : ∀ (H : Algebra.FormallySmooth R T), Algebra.FormallySmooth S (S ⊗[R] T)
⊢ FormallySmooth (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))

Tactic:
rw [formallySmooth_algebraMap] at H ⊢

Premises used: RingHom.formallySmooth_algebraMap
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R S T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
H : Algebra.FormallySmooth R T
⊢ Algebra.FormallySmooth S (S ⊗[R] T)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
⊢ LocalizationPreserves @FormallySmooth

Tactic:
isStableUnderBaseChange.localizationPreserves

Premises used: RingHom.FormallySmooth.isStableUnderBaseChange, RingHom.IsStableUnderBaseChange.localizationPreserves
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
⊢ Algebra.Smooth R S

Tactic:
hf

Premises used: RingHom.Smooth
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.Smooth R S ↔ Algebra.Smooth R S
rw₁ rw₂ : Algebra.Smooth R S ↔ Algebra.Smooth R S
⊢ Smooth (algebraMap R S) ↔ Algebra.Smooth R S

Tactic:
rw [RingHom.Smooth, toAlgebra_algebraMap]

Premises used: RingHom.Smooth, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ f.Smooth ↔ f.FormallySmooth ∧ f.FinitePresentation

Tactic:
letI := f.toAlgebra
  Algebra.smooth_iff _ _

Premises used: RingHom.FinitePresentation, Algebra.smooth_iff, RingHom.Smooth, RingHom.FormallySmooth
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
⊢ f.FormallySmooth ∧ f.FinitePresentation

Tactic:
rw [smooth_def] at hf

Premises used: RingHom.smooth_def
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FormallySmooth ∧ f.FinitePresentation
⊢ f.FormallySmooth

Tactic:
hf.1

Premises used: And.left
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FormallySmooth ∧ f.FinitePresentation
⊢ f.FormallySmooth

Tactic:
exact hf.1

Premises used: And.left
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FormallySmooth ∧ f.FinitePresentation
⊢ f.FinitePresentation

Tactic:
hf.2

Premises used: And.right
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.FormallySmooth ∧ f.FinitePresentation
⊢ f.FinitePresentation

Tactic:
exact hf.2

Premises used: And.right
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.Smooth
hg : g.Smooth
⊢ Algebra.Smooth R S

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.Smooth
hg : g.Smooth
algebraizeInst : Algebra.Smooth R S
⊢ Algebra.Smooth S T

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.Smooth
hg : g.Smooth
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.Smooth R S
algebraizeInst_1 : Algebra.Smooth S T
⊢ (g.comp f).Smooth

Tactic:
Algebra.Smooth.comp R S T

Premises used: Algebra.Smooth.comp, RingHom.Smooth
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
T : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.Smooth
hg : g.Smooth
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.Smooth R S
algebraizeInst_1 : Algebra.Smooth S T
⊢ (g.comp f).Smooth

Tactic:
exact Algebra.Smooth.comp R S T

Premises used: Algebra.Smooth.comp
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
⊢ StableUnderComposition.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ Smooth

Tactic:
fun _ _ _ _ _ _ _ _ ↦ RingHom.Smooth.comp

Premises used: RingHom.Smooth.comp, RingHom.StableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
⊢ IsStableUnderBaseChange.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] (f : R →+* S) ↦
    f.FormallySmooth ∧ f.FinitePresentation

Tactic:
RingHom.FormallySmooth.isStableUnderBaseChange.and
      RingHom.finitePresentation_isStableUnderBaseChange

Premises used: RingHom.FormallySmooth.isStableUnderBaseChange, RingHom.IsStableUnderBaseChange.and, RingHom.finitePresentation_isStableUnderBaseChange
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
h :
  ∀ (x x_1 : Type u_6) (x_2 : CommRing x) (x_3 : CommRing x_1) (x_4 : x →+* x_1),
    x_4.Smooth ↔ x_4.FormallySmooth ∧ x_4.FinitePresentation
⊢ IsStableUnderBaseChange.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ Smooth

Tactic:
convert!
    RingHom.FormallySmooth.isStableUnderBaseChange.and
      RingHom.finitePresentation_isStableUnderBaseChange

Premises used: RingHom.FormallySmooth.isStableUnderBaseChange, RingHom.IsStableUnderBaseChange.and, RingHom.finitePresentation_isStableUnderBaseChange
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
x x_1 : Type u_6
x_2 : CommRing x
x_3 : CommRing x_1
x_4 : x →+* x_1
h h₁ : x_4.FormallySmooth ∧ x_4.FinitePresentation ↔ x_4.FormallySmooth ∧ x_4.FinitePresentation
⊢ x_4.Smooth ↔ x_4.FormallySmooth ∧ x_4.FinitePresentation

Tactic:
rw [smooth_def]

Premises used: RingHom.smooth_def
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
h : IsLocalization.Away r S
rw : Algebra.Smooth R S
⊢ Smooth (algebraMap R S)

Tactic:
rw [smooth_algebraMap]

Premises used: RingHom.smooth_algebraMap
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ Algebra.Smooth R S

Tactic:
⟨Algebra.FormallySmooth.of_isLocalization (.powers r),
    IsLocalization.Away.finitePresentation r⟩

Premises used: Algebra.Smooth.mk, Algebra.FormallySmooth.of_isLocalization, IsLocalization.Away.finitePresentation, Submonoid.powers
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ Algebra.Smooth R S

Tactic:
exact ⟨Algebra.FormallySmooth.of_isLocalization (.powers r),
    IsLocalization.Away.finitePresentation r⟩
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
rw : f.FormallySmooth ∧ f.FinitePresentation
⊢ f.Smooth

Tactic:
rw [RingHom.smooth_def]

Premises used: RingHom.smooth_def
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.FormallySmooth ∧ f.FinitePresentation

Tactic:
⟨.of_bijective hf, .of_bijective hf⟩

Premises used: And.intro, RingHom.FinitePresentation.of_bijective, RingHom.FormallySmooth.of_bijective
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Bijective.{u_3 + 1, u_4 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ f.FormallySmooth ∧ f.FinitePresentation

Tactic:
exact ⟨.of_bijective hf, .of_bijective hf⟩
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R : Type u_3
inst : CommRing R
⊢ Smooth (RingHom.id R)

Tactic:
holdsForLocalizationAway.containsIdentities R

Premises used: RingHom.HoldsForLocalizationAway.containsIdentities, RingHom.Smooth.holdsForLocalizationAway
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u_6)),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (Smooth : (f : R →+* S) → Prop)) _ (Localization.Away (↑r : S)) _
      _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
⊢ f.FinitePresentation

Tactic:
have : f.FinitePresentation :=
    finitePresentation_ofLocalizationSpanTarget _ s hs fun r ↦ (hf r).finitePresentation
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u_6)),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (Smooth : (f : R →+* S) → Prop)) _ (Localization.Away (↑r : S)) _
      _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
this : f.FinitePresentation
⊢ Algebra.FinitePresentation R S

Tactic:
algebraize [f]
-- Module: Mathlib.RingTheory.RingHom.Smooth
Goal:
R S : Type u_6
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
hf :
  ∀ (r : (↑s : Type u_6)),
    (@fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ (Smooth : (f : R →+* S) → Prop)) _ (Localization.Away (↑r : S)) _
      _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
this : f.FinitePresentation
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.FinitePresentation R S
⊢ f.Smooth

Tactic:
⟨?_, ‹_›⟩

Premises used: Algebra.Smooth.mk, RingHom.Smooth