-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
/-- The dimension of the composition of two finite submersive presentations is
the sum of the dimensions. -/
lemma dimension_comp_eq_dimension_add_dimension [Q.IsFinite] [P.IsFinite] :
    (Q.comp P).dimension = Q.dimension + P.dimension

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : Q.IsFinite
inst✝ : P.IsFinite
this✝ : Nat.card P.rels ≤ Nat.card P.vars
this : Nat.card Q.rels ≤ Nat.card Q.vars
⊢ Nat.card Q.vars + Nat.card P.vars - (Nat.card Q.rels + Nat.card P.rels) =
    Nat.card Q.vars - Nat.card Q.rels + (Nat.card P.vars - Nat.card P.rels)

Tactic:
omega

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : Q.IsFinite
inst✝ : P.IsFinite
⊢ (Q.comp P).dimension = Q.dimension + P.dimension

Tactic:
simp only [Presentation.dimension]

Result:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : Q.IsFinite
inst✝ : P.IsFinite
⊢ Nat.card (Q.comp P).vars - Nat.card (Q.comp P).rels =
    Nat.card Q.vars - Nat.card Q.rels + (Nat.card P.vars - Nat.card P.rels)

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : Q.IsFinite
inst✝ : P.IsFinite
⊢ Nat.card (Q.comp P).vars - Nat.card (Q.comp P).rels =
    Nat.card Q.vars - Nat.card Q.rels + (Nat.card P.vars - Nat.card P.rels)

Tactic:
erw [Presentation.comp_rels, Generators.comp_vars]

Result:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : Q.IsFinite
inst✝ : P.IsFinite
⊢ Nat.card (Q.vars ⊕ P.vars) - Nat.card (Q.rels ⊕ P.rels) =
    Nat.card Q.vars - Nat.card Q.rels + (Nat.card P.vars - Nat.card P.rels)

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : Q.IsFinite
inst✝ : P.IsFinite
this✝ : Nat.card P.rels ≤ Nat.card P.vars
this : Nat.card Q.rels ≤ Nat.card Q.vars
⊢ Nat.card (Q.vars ⊕ P.vars) - Nat.card (Q.rels ⊕ P.rels) =
    Nat.card Q.vars - Nat.card Q.rels + (Nat.card P.vars - Nat.card P.rels)

Tactic:
simp only [Nat.card_sum]

Result:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : Q.IsFinite
inst✝ : P.IsFinite
this✝ : Nat.card P.rels ≤ Nat.card P.vars
this : Nat.card Q.rels ≤ Nat.card Q.vars
⊢ Nat.card Q.vars + Nat.card P.vars - (Nat.card Q.rels + Nat.card P.rels) =
    Nat.card Q.vars - Nat.card Q.rels + (Nat.card P.vars - Nat.card P.rels)

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : Q.IsFinite
inst✝ : P.IsFinite
⊢ Nat.card (Q.vars ⊕ P.vars) - Nat.card (Q.rels ⊕ P.rels) =
    Nat.card Q.vars - Nat.card Q.rels + (Nat.card P.vars - Nat.card P.rels)

Tactic:
have : Nat.card P.rels ≤ Nat.card P.vars :=
  card_relations_le_card_vars_of_isFinite P

Result:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : Q.IsFinite
inst✝ : P.IsFinite
this : Nat.card P.rels ≤ Nat.card P.vars
⊢ Nat.card (Q.vars ⊕ P.vars) - Nat.card (Q.rels ⊕ P.rels) =
    Nat.card Q.vars - Nat.card Q.rels + (Nat.card P.vars - Nat.card P.rels)

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : Q.IsFinite
inst✝ : P.IsFinite
this : Nat.card P.rels ≤ Nat.card P.vars
⊢ Nat.card (Q.vars ⊕ P.vars) - Nat.card (Q.rels ⊕ P.rels) =
    Nat.card Q.vars - Nat.card Q.rels + (Nat.card P.vars - Nat.card P.rels)

Tactic:
have : Nat.card Q.rels ≤ Nat.card Q.vars :=
  card_relations_le_card_vars_of_isFinite Q

Result:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
Q : PreSubmersivePresentation S T
P : PreSubmersivePresentation R S
inst✝¹ : Q.IsFinite
inst✝ : P.IsFinite
this✝ : Nat.card P.rels ≤ Nat.card P.vars
this : Nat.card Q.rels ≤ Nat.card Q.vars
⊢ Nat.card (Q.vars ⊕ P.vars) - Nat.card (Q.rels ⊕ P.rels) =
    Nat.card Q.vars - Nat.card Q.rels + (Nat.card P.vars - Nat.card P.rels)