awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ FormallySmooth (algebraMap R S) ↔ Algebra.FormallySmooth R S
have rw : Algebra.FormallySmooth R S ↔ Algebra.FormallySmooth R S
Tactic: rw [FormallySmooth, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
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
⊢ FormallySmooth (algebraMap R S) ↔ Algebra.FormallySmooth R S
have rw₁ : Algebra.FormallySmooth R S ↔ Algebra.FormallySmooth R S
Tactic: rw [FormallySmooth, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (hypothesis)
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
⊢ (g.comp f).FormallySmooth
have algebraizeInst : Algebra.FormallySmooth R S
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (hypothesis)
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
⊢ (g.comp f).FormallySmooth
have algebraizeInst₁ : Algebra.FormallySmooth S T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
Goal:
⊢ IsStableUnderBaseChange @FormallySmooth
have 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))
Tactic: refine .mk respectsIso ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
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)
⊢ FormallySmooth (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have rw : ∀ (H : Algebra.FormallySmooth R T), Algebra.FormallySmooth S (S ⊗[R] T)
Tactic: rw [formallySmooth_algebraMap] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Smooth (algebraMap R S) ↔ Algebra.Smooth R S
have rw : Algebra.Smooth R S ↔ Algebra.Smooth R S
Tactic: rw [RingHom.Smooth, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
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
⊢ Smooth (algebraMap R S) ↔ Algebra.Smooth R S
have rw₁ : Algebra.Smooth R S ↔ Algebra.Smooth R S
Tactic: rw [RingHom.Smooth, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
⊢ f.FormallySmooth
have hf₁ : f.FormallySmooth ∧ f.FinitePresentation
Tactic: rw [smooth_def] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (hypothesis)
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
⊢ f.FinitePresentation
have hf₁ : f.FormallySmooth ∧ f.FinitePresentation
Tactic: rw [smooth_def] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (hypothesis)
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
⊢ (g.comp f).Smooth
have algebraizeInst : Algebra.Smooth R S
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (hypothesis)
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
⊢ (g.comp f).Smooth
have algebraizeInst₁ : Algebra.Smooth S T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
Goal:
⊢ IsStableUnderBaseChange.{u_6} fun {R S : Type u_6} [CommRing R] [CommRing S] ↦ Smooth
have 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
Tactic: convert!
    RingHom.FormallySmooth.isStableUnderBaseChange.and
      RingHom.finitePresentation_isStableUnderBaseChange
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
Goal:
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
have h : x_4.FormallySmooth ∧ x_4.FinitePresentation ↔ x_4.FormallySmooth ∧ x_4.FinitePresentation
Tactic: rw [smooth_def]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
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
⊢ Smooth (algebraMap R S)
have rw : Algebra.Smooth R S
Tactic: rw [smooth_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
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.Smooth
have rw : f.FormallySmooth ∧ f.FinitePresentation
Tactic: rw [RingHom.smooth_def]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (hypothesis)
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.Smooth
have this : f.FinitePresentation
Tactic: have : f.FinitePresentation :=
    finitePresentation_ofLocalizationSpanTarget _ s hs fun r ↦ (hf r).finitePresentation
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (hypothesis)
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
⊢ f.Smooth
have algebraizeInst : Algebra.FinitePresentation R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
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
have refine : Algebra.FormallySmooth R S
Tactic: refine ⟨?_, ‹_›⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
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
⊢ Algebra.FormallySmooth R S
have rw : (↑(⨆ i ∈ s, PrimeSpectrum.basicOpen i) : Set (PrimeSpectrum S)) ⊆ Algebra.smoothLocus 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]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Smooth (goal)
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, PrimeSpectrum.basicOpen i) : Set (PrimeSpectrum S)) ⊆ Algebra.smoothLocus R S
have simp : ∀ (i : S) (i_1 : i ∈ s), FormallySmooth (S := Localization.Away i) (algebraMap R (Localization.Away i))
Tactic: simp only [TopologicalSpace.Opens.coe_iSup, Set.iUnion_subset_iff,
    Algebra.basicOpen_subset_smoothLocus_iff, ← formallySmooth_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ IsStandardSmooth (algebraMap R S) ↔ Algebra.IsStandardSmooth R S
have rw : Algebra.IsStandardSmooth R S ↔ Algebra.IsStandardSmooth R S
Tactic: rw [RingHom.IsStandardSmooth, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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
⊢ IsStandardSmooth (algebraMap R S) ↔ Algebra.IsStandardSmooth R S
have rw₁ : Algebra.IsStandardSmooth R S ↔ Algebra.IsStandardSmooth R S
Tactic: rw [RingHom.IsStandardSmooth, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ IsStandardSmoothOfRelativeDimension n (algebraMap R S) ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S
have rw : Algebra.IsStandardSmoothOfRelativeDimension n R S ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S
Tactic: rw [RingHom.IsStandardSmoothOfRelativeDimension, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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
⊢ IsStandardSmoothOfRelativeDimension n (algebraMap R S) ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S
have rw₁ : Algebra.IsStandardSmoothOfRelativeDimension n R S ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S
Tactic: rw [RingHom.IsStandardSmoothOfRelativeDimension, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ f.IsStandardSmooth
have algebraizeInst : Algebra.IsStandardSmoothOfRelativeDimension n R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
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 R T
have algebraizeInst : Algebra.IsStandardSmooth S T
Tactic: algebraize [f, g, (g.comp f)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
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 T
have algebraizeInst₁ : Algebra.IsStandardSmooth R S
Tactic: algebraize [f, g, (g.comp f)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
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 + m) R T
have algebraizeInst : Algebra.IsStandardSmoothOfRelativeDimension n S T
Tactic: algebraize [f, g, (g.comp f)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
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 (n + m) R T
have algebraizeInst₁ : Algebra.IsStandardSmoothOfRelativeDimension m R S
Tactic: algebraize [f, g, (g.comp f)]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
⊢ RespectsIso @IsStandardSmooth
have apply : ∀ {R S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.IsStandardSmooth
Tactic: apply isStandardSmooth_stableUnderComposition.respectsIso
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 n (e.toRingHom.comp f)
have rw : IsStandardSmoothOfRelativeDimension (0 + n) (e.toRingHom.comp f)
Tactic: rw [← zero_add n]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 (f.comp e.toRingHom)
have rw : IsStandardSmoothOfRelativeDimension (n + 0) (f.comp e.toRingHom)
Tactic: rw [← add_zero n]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
⊢ IsStableUnderBaseChange @IsStandardSmooth
have h₁ : RespectsIso @IsStandardSmooth
Tactic: apply IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
h₁ : RespectsIso @IsStandardSmooth
⊢ IsStableUnderBaseChange @IsStandardSmooth
have 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))
Tactic: apply IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
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
have h₁ : Algebra.IsStandardSmooth R T
Tactic: rw [RingHom.IsStandardSmooth] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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
have h₁ : inst_4 = toAlgebra (algebraMap R T)
Tactic: convert! h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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
⊢ inst_4 = toAlgebra (algebraMap R T)
have h₁ : ∀ (r : R) (x : T),
  (have I := inst_4;
    r • x) =
    r • x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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
⊢ (have I := inst_4;
    r • x) =
    r • x
have h₁ : HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) r : T) x = r • x
Tactic: simp_rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
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)
⊢ IsStandardSmooth (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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)
have h₁ : Eq (α := Algebra S (S ⊗[R] T)) (toAlgebra (algebraMap S (S ⊗[R] T))) Algebra.TensorProduct.leftAlgebra
Tactic: convert! this
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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)
⊢ Eq (α := Algebra S (S ⊗[R] T)) (toAlgebra (algebraMap S (S ⊗[R] T))) Algebra.TensorProduct.leftAlgebra
have h₁ : ∀ (r : S) (x : S ⊗[R] T),
  (have I : Algebra S (S ⊗[R] T) := toAlgebra (algebraMap S (S ⊗[R] T));
    r • x) =
    r • x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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
⊢ (have I : Algebra S (S ⊗[R] T) := toAlgebra (algebraMap S (S ⊗[R] T));
    r • x) =
    r • x
have h₁ : r • x = HMul.hMul (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) x
Tactic: simp_rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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
⊢ IsStandardSmooth (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have h₂ : Algebra.IsStandardSmooth 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
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
n : ℕ
⊢ IsStableUnderBaseChange.{u_2} (@IsStandardSmoothOfRelativeDimension n)
have h₁ : RespectsIso.{u_2} (@IsStandardSmoothOfRelativeDimension n)
Tactic: apply IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
n : ℕ
h₁ : RespectsIso.{u_2} (@IsStandardSmoothOfRelativeDimension n)
⊢ IsStableUnderBaseChange.{u_2} (@IsStandardSmoothOfRelativeDimension n)
have 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))
Tactic: apply IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
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
have h₁ : Algebra.IsStandardSmoothOfRelativeDimension n R T
Tactic: rw [RingHom.IsStandardSmoothOfRelativeDimension] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T
have h₁ : inst_4 = toAlgebra (algebraMap R T)
Tactic: convert! h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ inst_4 = toAlgebra (algebraMap R T)
have h₁ : ∀ (r : R) (x : T),
  (have I := inst_4;
    r • x) =
    r • x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 : Algebra.IsStandardSmoothOfRelativeDimension n R T
r : R
x : T
⊢ (have I := inst_4;
    r • x) =
    r • x
have h₁ : HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) r : T) x = r • x
Tactic: simp_rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
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)
⊢ IsStandardSmoothOfRelativeDimension n (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have h₁ : Algebra.IsStandardSmoothOfRelativeDimension n R T
Tactic: replace h : Algebra.IsStandardSmoothOfRelativeDimension n R T := by
      rw [RingHom.IsStandardSmoothOfRelativeDimension] at h
      convert! h; ext; simp_rw [Algebra.smul_def]; rfl
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
have h₁ : Eq (α := Algebra S (S ⊗[R] T)) (toAlgebra (algebraMap S (S ⊗[R] T))) Algebra.TensorProduct.leftAlgebra
Tactic: convert! this
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ Eq (α := Algebra S (S ⊗[R] T)) (toAlgebra (algebraMap S (S ⊗[R] T))) Algebra.TensorProduct.leftAlgebra
have h₁ : ∀ (r : S) (x : S ⊗[R] T),
  (have I : Algebra S (S ⊗[R] T) := toAlgebra (algebraMap S (S ⊗[R] T));
    r • x) =
    r • x
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
r : S
x : S ⊗[R] T
⊢ (have I : Algebra S (S ⊗[R] T) := toAlgebra (algebraMap S (S ⊗[R] T));
    r • x) =
    r • x
have h₁ : r • x = HMul.hMul (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) x
Tactic: simp_rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ IsStandardSmoothOfRelativeDimension n (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
have h₂ : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
Tactic: suffices Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T) by
      rw [RingHom.IsStandardSmoothOfRelativeDimension]
      convert! this; ext; simp_rw [Algebra.smul_def]; rfl
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
R : Type u
inst : CommRing R
Rᵣ : Type u_2
inst_1 : CommRing Rᵣ
inst_2 : Algebra R Rᵣ
r : R
inst_3 : IsLocalization.Away r Rᵣ
⊢ RingHom.toAlgebra (algebraMap R Rᵣ) = inst_2
have h : ∀ (r : R) (x : Rᵣ),
  (have I : Algebra R Rᵣ := RingHom.toAlgebra (algebraMap R Rᵣ);
    r • x) =
    r • x
Tactic: ext