-- Mathlib/Algebra/MvPolynomial/Eval.lean
lemma aeval_sumElim {σ τ : Type*} (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (g : σ → T) :
    (aeval (Sum.elim g (algebraMap S T ∘ f))) p =
      (aeval g) ((aeval (Sum.elim X (C ∘ f))) p)

Proof state:
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
g : σ → T
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
induction' p using MvPolynomial.induction_on with r p q hp hq p i h

Result:
case h_C
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
r : R
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (C r) = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (C r))

case h_add
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p q : MvPolynomial (σ ⊕ τ) R
hp : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
hq : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) q = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) q)
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p + q) = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p + q))

case h_X
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
i : σ ⊕ τ
h : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p * X i) = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X i))

Proof state:
case h_C
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
r : R
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (C r) = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (C r))

Tactic:
simp [← IsScalarTower.algebraMap_apply]

Result:
no goals

Proof state:
case h_X
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p : MvPolynomial (σ ⊕ τ) R
i : σ ⊕ τ
h : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p * X i) = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p * X i))

Tactic:
cases i <;> simp [h]

Result:
no goals

Proof state:
case h_add
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
f : τ → S
g : σ → T
p q : MvPolynomial (σ ⊕ τ) R
hp : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)
hq : (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) q = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) q)
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) (p + q) = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) (p + q))

Tactic:
simp [hp, hq]

Result:
no goals