awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine : Algebra.FormallySmooth R S
⊢ f.Smooth

Tactic:
refine ⟨?_, ‹_›⟩
-- 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
rw : (↑(⨆ i ∈ s, PrimeSpectrum.basicOpen i) : Set (PrimeSpectrum S)) ⊆ Algebra.smoothLocus R S
⊢ Algebra.FormallySmooth R S

Tactic:
rw [← Algebra.smoothLocus_eq_univ_iff, ← Set.univ_subset_iff, ← TopologicalSpace.Opens.coe_top,
    ← PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs]

Premises used: Iff.mpr, Set.univ_subset_iff, Algebra.smoothLocus_eq_univ_iff, PrimeSpectrum.iSup_basicOpen_eq_top_iff', TopologicalSpace.Opens.coe_top
-- 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
simp : ∀ (i : S) (i_1 : i ∈ s), FormallySmooth (S := Localization.Away i) (algebraMap R (Localization.Away i))
⊢ (↑(⨆ i ∈ s, PrimeSpectrum.basicOpen i) : Set (PrimeSpectrum S)) ⊆ Algebra.smoothLocus R S

Tactic:
simp only [TopologicalSpace.Opens.coe_iSup, Set.iUnion_subset_iff,
    Algebra.basicOpen_subset_smoothLocus_iff, ← formallySmooth_algebraMap]

Premises used: TopologicalSpace.Opens.coe_iSup, Set.iUnion_subset_iff, RingHom.formallySmooth_algebraMap, Algebra.basicOpen_subset_smoothLocus_iff
-- 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
⊢ ∀ (i : S) (i_1 : i ∈ s), FormallySmooth (S := Localization.Away i) (algebraMap R (Localization.Away i))

Tactic:
fun r hr ↦ (hf ⟨r, hr⟩).1

Premises used: Algebra.Smooth.formallySmooth, Set.Mem, Quotient.mk', OreLocalization.oreDiv, RingHom.FormallySmooth
-- 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
⊢ ∀ (i : S) (i_1 : i ∈ s), FormallySmooth (S := Localization.Away i) (algebraMap R (Localization.Away i))

Tactic:
exact fun r hr ↦ (hf ⟨r, hr⟩).1

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

Tactic:
propertyIsLocal.respectsIso

Premises used: RingHom.Smooth.propertyIsLocal, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.IsStandardSmooth R S ↔ Algebra.IsStandardSmooth R S
rw₁ rw₂ : Algebra.IsStandardSmooth R S ↔ Algebra.IsStandardSmooth R S
⊢ IsStandardSmooth (algebraMap R S) ↔ Algebra.IsStandardSmooth R S

Tactic:
rw [RingHom.IsStandardSmooth, toAlgebra_algebraMap]

Premises used: RingHom.IsStandardSmooth, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
⊢ Algebra.IsStandardSmooth R S

Tactic:
hf

Premises used: RingHom.IsStandardSmooth
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.IsStandardSmoothOfRelativeDimension n R S ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S
rw₁ rw₂ : Algebra.IsStandardSmoothOfRelativeDimension n R S ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S
⊢ IsStandardSmoothOfRelativeDimension n (algebraMap R S) ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S

Tactic:
rw [RingHom.IsStandardSmoothOfRelativeDimension, toAlgebra_algebraMap]

Premises used: RingHom.IsStandardSmoothOfRelativeDimension, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R S

Tactic:
hf

Premises used: RingHom.IsStandardSmoothOfRelativeDimension
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R S

Tactic:
algebraize [f]
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : IsStandardSmoothOfRelativeDimension n f
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsStandardSmoothOfRelativeDimension n R S
⊢ f.IsStandardSmooth

Tactic:
Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth n

Premises used: RingHom.IsStandardSmooth, Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : IsStandardSmoothOfRelativeDimension n f
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsStandardSmoothOfRelativeDimension n R S
⊢ f.IsStandardSmooth

Tactic:
exact Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth n

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.isStandardSmooth
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
inst : CommRing R
⊢ IsStandardSmoothOfRelativeDimension 0 (RingHom.id R)

Tactic:
Algebra.IsStandardSmoothOfRelativeDimension.id R

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.id, RingHom.IsStandardSmoothOfRelativeDimension
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
algInst : Algebra R S := e.toRingHom.toAlgebra
⊢ IsStandardSmoothOfRelativeDimension 0 (↑e : R →+* S)

Tactic:
Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective e.bijective

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective, RingHom.IsStandardSmoothOfRelativeDimension, RingEquiv.bijective
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
algInst : Algebra R S := e.toRingHom.toAlgebra
⊢ IsStandardSmoothOfRelativeDimension 0 (↑e : R →+* S)

Tactic:
exact Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective e.bijective

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective, RingEquiv.bijective
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
T : Type u_1
inst_2 : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
⊢ Algebra.IsStandardSmooth S T

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
T : Type u_1
inst_2 : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
algebraizeInst : Algebra.IsStandardSmooth S T
⊢ Algebra.IsStandardSmooth R S

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
T : Type u_1
inst_2 : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
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.IsStandardSmooth S T
algebraizeInst_1 : Algebra.IsStandardSmooth R S
⊢ Algebra.IsStandardSmooth R T

Tactic:
Algebra.IsStandardSmooth.trans R S T

Premises used: Algebra.IsStandardSmooth.trans
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
T : Type u_1
inst_2 : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
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.IsStandardSmooth S T
algebraizeInst_1 : Algebra.IsStandardSmooth R S
⊢ Algebra.IsStandardSmooth R T

Tactic:
exact Algebra.IsStandardSmooth.trans R S T

Premises used: Algebra.IsStandardSmooth.trans
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
T : Type u_1
inst_2 : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S T

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
T : Type u_1
inst_2 : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
algebraizeInst : Algebra.IsStandardSmoothOfRelativeDimension n S T
⊢ Algebra.IsStandardSmoothOfRelativeDimension m R S

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

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
T : Type u_1
inst_2 : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
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.IsStandardSmoothOfRelativeDimension n S T
algebraizeInst_1 : Algebra.IsStandardSmoothOfRelativeDimension m R S
⊢ Algebra.IsStandardSmoothOfRelativeDimension (n + m) R T

Tactic:
Algebra.IsStandardSmoothOfRelativeDimension.trans m n R S T

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.trans
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n m : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
T : Type u_1
inst_2 : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
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.IsStandardSmoothOfRelativeDimension n S T
algebraizeInst_1 : Algebra.IsStandardSmoothOfRelativeDimension m R S
⊢ Algebra.IsStandardSmoothOfRelativeDimension (n + m) R T

Tactic:
exact Algebra.IsStandardSmoothOfRelativeDimension.trans m n R S T

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.trans
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
⊢ StableUnderComposition @IsStandardSmooth

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

Premises used: RingHom.IsStandardSmooth.comp, RingHom.StableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
apply : ∀ {R S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.IsStandardSmooth
⊢ RespectsIso @IsStandardSmooth

Tactic:
apply isStandardSmooth_stableUnderComposition.respectsIso

Premises used: RingHom.StableUnderComposition.respectsIso, RingHom.isStandardSmooth_stableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S : Type u_2
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
⊢ e.toRingHom.IsStandardSmooth

Tactic:
(IsStandardSmoothOfRelativeDimension.equiv e).isStandardSmooth

Premises used: RingHom.IsStandardSmoothOfRelativeDimension.equiv, MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, RingHomClass.toRingHom, RingEquiv.toRingHom, RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S : Type u_2
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
⊢ e.toRingHom.IsStandardSmooth

Tactic:
exact (IsStandardSmoothOfRelativeDimension.equiv e).isStandardSmooth

Premises used: RingHom.IsStandardSmoothOfRelativeDimension.equiv, RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
hf : IsStandardSmoothOfRelativeDimension n f
rw : IsStandardSmoothOfRelativeDimension (0 + n) (e.toRingHom.comp f)
⊢ IsStandardSmoothOfRelativeDimension n (e.toRingHom.comp f)

Tactic:
rw [← zero_add n]

Premises used: zero_add
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (0 + n) (e.toRingHom.comp f)

Tactic:
(IsStandardSmoothOfRelativeDimension.equiv e).comp hf

Premises used: RingHom.IsStandardSmoothOfRelativeDimension.equiv, MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, RingHomClass.toRingHom, RingEquiv.toRingHom, RingHom.IsStandardSmoothOfRelativeDimension.comp
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : R →+* S
e : S ≃+* T
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (0 + n) (e.toRingHom.comp f)

Tactic:
exact (IsStandardSmoothOfRelativeDimension.equiv e).comp hf

Premises used: RingHom.IsStandardSmoothOfRelativeDimension.equiv, RingHom.IsStandardSmoothOfRelativeDimension.comp
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
rw : IsStandardSmoothOfRelativeDimension (n + 0) (f.comp e.toRingHom)
⊢ IsStandardSmoothOfRelativeDimension n (f.comp e.toRingHom)

Tactic:
rw [← add_zero n]

Premises used: add_zero
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (n + 0) (f.comp e.toRingHom)

Tactic:
hf.comp (IsStandardSmoothOfRelativeDimension.equiv e)

Premises used: RingHom.IsStandardSmoothOfRelativeDimension.equiv, RingHom.IsStandardSmoothOfRelativeDimension.comp
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
x : CommRing R
x_1 : CommRing S
x_2 : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (n + 0) (f.comp e.toRingHom)

Tactic:
exact hf.comp (IsStandardSmoothOfRelativeDimension.equiv e)

Premises used: RingHom.IsStandardSmoothOfRelativeDimension.equiv, RingHom.IsStandardSmoothOfRelativeDimension.comp
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
h₁ : RespectsIso @IsStandardSmooth
h₂ :
  ∀ ⦃R S T : Type u_2⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    IsStandardSmooth (algebraMap R T) → IsStandardSmooth (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
⊢ IsStableUnderBaseChange @IsStandardSmooth

Tactic:
apply IsStableUnderBaseChange.mk

Premises used: RingHom.IsStableUnderBaseChange.mk
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
⊢ RespectsIso @IsStandardSmooth

Tactic:
isStandardSmooth_respectsIso

Premises used: RingHom.isStandardSmooth_respectsIso
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
⊢ RespectsIso @IsStandardSmooth

Tactic:
exact isStandardSmooth_respectsIso

Premises used: RingHom.isStandardSmooth_respectsIso
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : IsStandardSmooth (algebraMap R T)
⊢ Algebra.IsStandardSmooth R T

Tactic:
rw [RingHom.IsStandardSmooth] at h

Premises used: RingHom.IsStandardSmooth
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
⊢ Algebra.IsStandardSmooth R T

Tactic:
h
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
h₁ : inst_4 = toAlgebra (algebraMap R T)
⊢ Algebra.IsStandardSmooth R T

Tactic:
convert! h
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
h₁ :
  ∀ (r : R) (x : T),
    (have I := inst_4;
      r • x) =
      r • x
⊢ inst_4 = toAlgebra (algebraMap R T)

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
r : R
x : T
h₁ : HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) r : T) x = r • x
⊢ (have I := inst_4;
    r • x) =
    r • x

Tactic:
simp_rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
r : R
x : T
⊢ HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) r : T) x = r • x

Tactic:
rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : IsStandardSmooth (algebraMap R T)
⊢ Algebra.IsStandardSmooth R T

Tactic:
replace h : Algebra.IsStandardSmooth R T := by
      rw [RingHom.IsStandardSmooth] at h; convert! h; ext; simp_rw [Algebra.smul_def]; rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
⊢ Algebra.IsStandardSmooth S (S ⊗[R] T)

Tactic:
this
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
h₁ : Eq (α := Algebra S (S ⊗[R] T)) (toAlgebra (algebraMap S (S ⊗[R] T))) Algebra.TensorProduct.leftAlgebra
⊢ Algebra.IsStandardSmooth S (S ⊗[R] T)

Tactic:
convert! this
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
h₁ :
  ∀ (r : S) (x : S ⊗[R] T),
    (have I : Algebra S (S ⊗[R] T) := toAlgebra (algebraMap S (S ⊗[R] T));
      r • x) =
      r • x
⊢ Eq (α := Algebra S (S ⊗[R] T)) (toAlgebra (algebraMap S (S ⊗[R] T))) Algebra.TensorProduct.leftAlgebra

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
r : S
x : S ⊗[R] T
h₁ : r • x = HMul.hMul (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) x
⊢ (have I : Algebra S (S ⊗[R] T) := toAlgebra (algebraMap S (S ⊗[R] T));
    r • x) =
    r • x

Tactic:
simp_rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
r : S
x : S ⊗[R] T
⊢ r • x = HMul.hMul (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) x

Tactic:
rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
h₂ : Algebra.IsStandardSmooth S (S ⊗[R] T)
⊢ IsStandardSmooth (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))

Tactic:
suffices Algebra.IsStandardSmooth S (S ⊗[R] T) by
      rw [RingHom.IsStandardSmooth]; convert! this; ext; simp_rw [Algebra.smul_def]; rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmooth R T
⊢ Algebra.IsStandardSmooth S (S ⊗[R] T)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
h₁ : RespectsIso.{u_2} (@IsStandardSmoothOfRelativeDimension n)
h₂ :
  ∀ ⦃R S T : Type u_2⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    IsStandardSmoothOfRelativeDimension n (algebraMap R T) →
      IsStandardSmoothOfRelativeDimension n (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
⊢ IsStableUnderBaseChange.{u_2} (@IsStandardSmoothOfRelativeDimension n)

Tactic:
apply IsStableUnderBaseChange.mk

Premises used: RingHom.IsStableUnderBaseChange.mk
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
⊢ RespectsIso.{u_2} (@IsStandardSmoothOfRelativeDimension n)

Tactic:
isStandardSmoothOfRelativeDimension_respectsIso

Premises used: RingHom.isStandardSmoothOfRelativeDimension_respectsIso
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
⊢ RespectsIso.{u_2} (@IsStandardSmoothOfRelativeDimension n)

Tactic:
exact isStandardSmoothOfRelativeDimension_respectsIso

Premises used: RingHom.isStandardSmoothOfRelativeDimension_respectsIso
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : IsStandardSmoothOfRelativeDimension n (algebraMap R T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T

Tactic:
rw [RingHom.IsStandardSmoothOfRelativeDimension] at h

Premises used: RingHom.IsStandardSmoothOfRelativeDimension