-- Mathlib/RingTheory/Generators.lean
lemma ofComp_toAlgHom_monomial_sumElim (Q : Generators S T) (P : Generators R S) (v₁ v₂ a) :
    (Q.ofComp P).toAlgHom (monomial (Finsupp.sumElim v₁ v₂) a) =
      monomial v₁ (aeval P.val (monomial v₂ a))

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
v₁ : Q.vars →₀ ℕ
v₂ : P.vars →₀ ℕ
a : R
⊢ (a • (v₁.sumElim v₂).prod fun x1 x2 => (Q.ofComp P).val x1 ^ x2) =
    C ((aeval P.val) ((monomial v₂) a)) * v₁.prod fun n e => X n ^ e

Tactic:
simp only [MvPolynomial.algebraMap_apply, ofComp_val, aeval_monomial]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
v₁ : Q.vars →₀ ℕ
v₂ : P.vars →₀ ℕ
a : R
⊢ (a • (v₁.sumElim v₂).prod fun x1 x2 => Sum.elim X (⇑C ∘ P.val) x1 ^ x2) =
    C ((algebraMap R S) a * v₂.prod fun i k => P.val i ^ k) * v₁.prod fun n e => X n ^ e

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
v₁ : Q.vars →₀ ℕ
v₂ : P.vars →₀ ℕ
a : R
⊢ C ((algebraMap R S) a) * ((v₁.prod fun x x2 => X x ^ x2) * C (v₂.prod fun a => HPow.hPow (P.val a))) =
    C ((algebraMap R S) a) * (C (v₂.prod fun i k => P.val i ^ k) * v₁.prod fun n e => X n ^ e)

Tactic:
nth_rw 2 [mul_comm]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
v₁ : Q.vars →₀ ℕ
v₂ : P.vars →₀ ℕ
a : R
⊢ (Q.ofComp P).toAlgHom ((monomial (v₁.sumElim v₂)) a) = (monomial v₁) ((aeval P.val) ((monomial v₂) a))

Tactic:
erw [Hom.toAlgHom_monomial]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
v₁ : Q.vars →₀ ℕ
v₂ : P.vars →₀ ℕ
a : R
⊢ (a • (v₁.sumElim v₂).prod fun x1 x2 => (Q.ofComp P).val x1 ^ x2) = (monomial v₁) ((aeval P.val) ((monomial v₂) a))

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
v₁ : Q.vars →₀ ℕ
v₂ : P.vars →₀ ℕ
a : R
⊢ (a • (v₁.sumElim v₂).prod fun x1 x2 => Sum.elim X (⇑C ∘ P.val) x1 ^ x2) =
    C ((algebraMap R S) a * v₂.prod fun i k => P.val i ^ k) * v₁.prod fun n e => X n ^ e

Tactic:
rw [Finsupp.prod_sumElim]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
v₁ : Q.vars →₀ ℕ
v₂ : P.vars →₀ ℕ
a : R
⊢ a •
      (v₁.prod ((fun x1 x2 => Sum.elim X (⇑C ∘ P.val) x1 ^ x2) ∘ Sum.inl) *
        v₂.prod ((fun x1 x2 => Sum.elim X (⇑C ∘ P.val) x1 ^ x2) ∘ Sum.inr)) =
    C ((algebraMap R S) a * v₂.prod fun i k => P.val i ^ k) * v₁.prod fun n e => X n ^ e

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
v₁ : Q.vars →₀ ℕ
v₂ : P.vars →₀ ℕ
a : R
⊢ (a • (v₁.sumElim v₂).prod fun x1 x2 => (Q.ofComp P).val x1 ^ x2) = (monomial v₁) ((aeval P.val) ((monomial v₂) a))

Tactic:
rw [monomial_eq]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
v₁ : Q.vars →₀ ℕ
v₂ : P.vars →₀ ℕ
a : R
⊢ (a • (v₁.sumElim v₂).prod fun x1 x2 => (Q.ofComp P).val x1 ^ x2) =
    C ((aeval P.val) ((monomial v₂) a)) * v₁.prod fun n e => X n ^ e

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
v₁ : Q.vars →₀ ℕ
v₂ : P.vars →₀ ℕ
a : R
⊢ a •
      (v₁.prod ((fun x1 x2 => Sum.elim X (⇑C ∘ P.val) x1 ^ x2) ∘ Sum.inl) *
        v₂.prod ((fun x1 x2 => Sum.elim X (⇑C ∘ P.val) x1 ^ x2) ∘ Sum.inr)) =
    C ((algebraMap R S) a * v₂.prod fun i k => P.val i ^ k) * v₁.prod fun n e => X n ^ e

Tactic:
simp only [Function.comp_def, Sum.elim_inl, Sum.elim_inr, ← map_pow, ← map_finsupp_prod,
  C_mul, Algebra.smul_def, MvPolynomial.algebraMap_apply, mul_assoc]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_2
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
P : Generators R S
v₁ : Q.vars →₀ ℕ
v₂ : P.vars →₀ ℕ
a : R
⊢ C ((algebraMap R S) a) * ((v₁.prod fun x x2 => X x ^ x2) * C (v₂.prod fun a => HPow.hPow (P.val a))) =
    C ((algebraMap R S) a) * (C (v₂.prod fun i k => P.val i ^ k) * v₁.prod fun n e => X n ^ e)