-- Mathlib/RingTheory/Presentation.lean
private lemma aeval_comp_val_eq :
    (aeval (Q.comp P.toGenerators).val) =
      (aevalTower (IsScalarTower.toAlgHom R S T) Q.val).comp (Q.aux P)

Proof state:
case hf
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 S T
Q : Presentation S T
P : Presentation R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
i : (Q.comp P.toGenerators).vars
⊢ (aeval (Q.comp P.toGenerators).val) (X i) =
    (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) ((Algebra.Presentation.aux Q P) (X i))

Tactic:
erw [Q.aux_X P i]

Result:
case hf
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 S T
Q : Presentation S T
P : Presentation R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
i : (Q.comp P.toGenerators).vars
⊢ (aeval (Q.comp P.toGenerators).val) (X i) =
    (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) (Sum.elim X (⇑C ∘ P.val) i)

Proof state:
case hf
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 S T
Q : Presentation S T
P : Presentation R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
i : (Q.comp P.toGenerators).vars
⊢ (aeval (Q.comp P.toGenerators).val) (X i) =
    (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) (Sum.elim X (⇑C ∘ P.val) i)

Tactic:
cases i <;> simp

Result:
no goals

Proof state:
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 S T
Q : Presentation S T
P : Presentation R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
⊢ aeval (Q.comp P.toGenerators).val =
    (aevalTower (IsScalarTower.toAlgHom R S T) Q.val).comp (Algebra.Presentation.aux Q P)

Tactic:
ext i

Result:
case hf
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 S T
Q : Presentation S T
P : Presentation R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
i : (Q.comp P.toGenerators).vars
⊢ (aeval (Q.comp P.toGenerators).val) (X i) =
    ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val).comp (Algebra.Presentation.aux Q P)) (X i)

Proof state:
case hf
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 S T
Q : Presentation S T
P : Presentation R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
i : (Q.comp P.toGenerators).vars
⊢ (aeval (Q.comp P.toGenerators).val) (X i) =
    ((aevalTower (IsScalarTower.toAlgHom R S T) Q.val).comp (Algebra.Presentation.aux Q P)) (X i)

Tactic:
simp only [AlgHom.coe_comp, Function.comp_apply]

Result:
case hf
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 S T
Q : Presentation S T
P : Presentation R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
i : (Q.comp P.toGenerators).vars
⊢ (aeval (Q.comp P.toGenerators).val) (X i) =
    (aevalTower (IsScalarTower.toAlgHom R S T) Q.val) ((Algebra.Presentation.aux Q P) (X i))