-- Mathlib/RingTheory/RingHom/StandardSmooth.lean
lemma isStandardSmoothOfRelativeDimension_isStableUnderBaseChange :
    IsStableUnderBaseChange (@IsStandardSmoothOfRelativeDimension.{t, w} n)

Proof state:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)

Tactic:
convert this

Result:
case h.e'_6
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ Algebra.TensorProduct.includeLeftRingHom.toAlgebra = Algebra.TensorProduct.leftAlgebra

Proof state:
case h₂
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)

Tactic:
infer_instance

Result:
no goals

Proof state:
n : ℕ
⊢ IsStableUnderBaseChange (@IsStandardSmoothOfRelativeDimension n)

Tactic:
apply IsStableUnderBaseChange.mk

Result:
case h₁
n : ℕ
⊢ RespectsIso (@IsStandardSmoothOfRelativeDimension n)

case h₂
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],
    IsStandardSmoothOfRelativeDimension n (algebraMap R T) →
      IsStandardSmoothOfRelativeDimension n Algebra.TensorProduct.includeLeftRingHom

Proof state:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsStandardSmoothOfRelativeDimension n (algebraMap R T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T

Tactic:
rw [RingHom.IsStandardSmoothOfRelativeDimension] at h

Result:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T

Proof state:
case h₂
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsStandardSmoothOfRelativeDimension n (algebraMap R T)
⊢ IsStandardSmoothOfRelativeDimension n Algebra.TensorProduct.includeLeftRingHom

Tactic:
replace h : Algebra.IsStandardSmoothOfRelativeDimension n R T := by
  rw [RingHom.IsStandardSmoothOfRelativeDimension] at h
  convert h; ext; simp_rw [Algebra.smul_def]; rfl

Result:
case h₂
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ IsStandardSmoothOfRelativeDimension n Algebra.TensorProduct.includeLeftRingHom

Proof state:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T

Tactic:
convert h

Result:
case h.e'_6
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ inst✝ = (algebraMap R T).toAlgebra

Proof state:
case h.e'_6
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ inst✝ = (algebraMap R T).toAlgebra

Tactic:
ext

Result:
case h.e'_6.h
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
r✝ : R
x✝ : T
⊢ (let_fun I := inst✝;
    r✝ • x✝) =
    r✝ • x✝

Proof state:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ IsStandardSmoothOfRelativeDimension n Algebra.TensorProduct.includeLeftRingHom

Tactic:
rw [RingHom.IsStandardSmoothOfRelativeDimension]

Result:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)

Proof state:
case h₂
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ IsStandardSmoothOfRelativeDimension n Algebra.TensorProduct.includeLeftRingHom

Tactic:
suffices Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T) by
  rw [RingHom.IsStandardSmoothOfRelativeDimension]
  convert this; ext; simp_rw [Algebra.smul_def]; rfl

Result:
case h₂
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)

Proof state:
case h.e'_6.h
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
r✝ : R
x✝ : T
⊢ (algebraMap R T) r✝ * x✝ = (algebraMap R T) r✝ * x✝

Tactic:
rfl

Result:
no goals

Proof state:
case h₁
n : ℕ
⊢ RespectsIso (@IsStandardSmoothOfRelativeDimension n)

Tactic:
exact isStandardSmoothOfRelativeDimension_respectsIso

Result:
no goals

Proof state:
case h.e'_6.h
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
r✝ : S
x✝ : S ⊗[R] T
⊢ (let_fun I := Algebra.TensorProduct.includeLeftRingHom.toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Tactic:
simp_rw [Algebra.smul_def]

Result:
case h.e'_6.h
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
r✝ : S
x✝ : S ⊗[R] T
⊢ (algebraMap S (S ⊗[R] T)) r✝ * x✝ = (algebraMap S (S ⊗[R] T)) r✝ * x✝

Proof state:
case h₂
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],
    IsStandardSmoothOfRelativeDimension n (algebraMap R T) →
      IsStandardSmoothOfRelativeDimension n Algebra.TensorProduct.includeLeftRingHom

Tactic:
introv h

Result:
case h₂
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : IsStandardSmoothOfRelativeDimension n (algebraMap R T)
⊢ IsStandardSmoothOfRelativeDimension n Algebra.TensorProduct.includeLeftRingHom

Proof state:
case h.e'_6.h
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
r✝ : S
x✝ : S ⊗[R] T
⊢ (algebraMap S (S ⊗[R] T)) r✝ * x✝ = (algebraMap S (S ⊗[R] T)) r✝ * x✝

Tactic:
rfl

Result:
no goals