-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
T : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : Algebra S T
inst_6 : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
g : σ → T
C :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := T)
      ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T)
          ((MvPolynomial.C : (a : R) → MvPolynomial (σ ⊕ τ) R) r : MvPolynomial (σ ⊕ τ) R) :
        T)
      ((aeval g : (a : MvPolynomial σ S) → T)
          ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              ((MvPolynomial.C : (a : R) → MvPolynomial (σ ⊕ τ) R) r) :
            MvPolynomial σ S) :
        T)
add :
  ∀ (p q : MvPolynomial (σ ⊕ τ) R)
    (hp :
      Eq.{u_3 + 1} (α := T)
        ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) p : T)
        ((aeval g : (a : MvPolynomial σ S) → T)
            ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
                  (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
                p :
              MvPolynomial σ S) :
          T))
    (hq :
      Eq.{u_3 + 1} (α := T)
        ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) q : T)
        ((aeval g : (a : MvPolynomial σ S) → T)
            ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
                  (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
                q :
              MvPolynomial σ S) :
          T)),
    Eq.{u_3 + 1} (α := T)
      ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) (p + q) : T)
      ((aeval g : (a : MvPolynomial σ S) → T)
          ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              (p + q) :
            MvPolynomial σ S) :
        T)
⊢ Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) p : T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
              (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            p :
          MvPolynomial σ S) :
      T)
have mul_X : ∀ (p : MvPolynomial (σ ⊕ τ) R) (i : σ ⊕ τ)
  (h :
    Eq.{u_3 + 1} (α := T)
      ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) p : T)
      ((aeval g : (a : MvPolynomial σ S) → T)
          ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
                (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
              p :
            MvPolynomial σ S) :
        T)),
  Eq.{u_3 + 1} (α := T)
    ((aeval (Sum.elim g ((⇑(algebraMap S T) : (a : S) → T) ∘ f)) : (a : MvPolynomial (σ ⊕ τ) R) → T) (p * X i) : T)
    ((aeval g : (a : MvPolynomial σ S) → T)
        ((aeval (Sum.elim X ((⇑MvPolynomial.C : (a : S) → MvPolynomial σ S) ∘ f)) :
              (a : MvPolynomial (σ ⊕ τ) R) → MvPolynomial σ S)
            (p * X i) :
          MvPolynomial σ S) :
      T)
Tactic: induction p using MvPolynomial.induction_on with
  | C r => simp [← IsScalarTower.algebraMap_apply]
  | add p q hp hq => simp [hp, hq]
  | mul_X p i h => cases i <;> simp [h]
Cleared hypotheses: p