-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
lemma IsStandardSmoothOfRelativeDimension.trans [IsStandardSmoothOfRelativeDimension.{t, w} n R S]
    [IsStandardSmoothOfRelativeDimension.{t', w'} m S T] :
    IsStandardSmoothOfRelativeDimension.{max t t', max w w'} (m + n) R T where
  out

Proof state:
n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
⊢ ∃ P, P.dimension = m + n

Tactic:
obtain ⟨P, hP⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›

Result:
case mk.intro
n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
P : SubmersivePresentation R S
hP : P.dimension = n
⊢ ∃ P, P.dimension = m + n

Proof state:
case mk.intro.mk.intro
n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
P : SubmersivePresentation R S
hP : P.dimension = n
Q : SubmersivePresentation S T
hQ : Q.dimension = m
⊢ (Q.comp P).dimension = Q.dimension + P.dimension

Tactic:
apply PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension

Result:
no goals

Proof state:
case mk.intro
n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
P : SubmersivePresentation R S
hP : P.dimension = n
⊢ ∃ P, P.dimension = m + n

Tactic:
obtain ⟨Q, hQ⟩ := ‹IsStandardSmoothOfRelativeDimension m S T›

Result:
case mk.intro.mk.intro
n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
P : SubmersivePresentation R S
hP : P.dimension = n
Q : SubmersivePresentation S T
hQ : Q.dimension = m
⊢ ∃ P, P.dimension = m + n

Proof state:
case mk.intro.mk.intro
n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
P : SubmersivePresentation R S
hP : P.dimension = n
Q : SubmersivePresentation S T
hQ : Q.dimension = m
⊢ ∃ P, P.dimension = m + n

Tactic:
refine ⟨Q.comp P, hP ▸ hQ ▸ ?_⟩

Result:
case mk.intro.mk.intro
n m : ℕ
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmoothOfRelativeDimension n R S
inst✝ : IsStandardSmoothOfRelativeDimension m S T
P : SubmersivePresentation R S
hP : P.dimension = n
Q : SubmersivePresentation S T
hQ : Q.dimension = m
⊢ (Q.comp P).dimension = Q.dimension + P.dimension