-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval_eval₂ {S τ : Type*} {x : τ → S} [CommSemiring S]
    (f : R →+* MvPolynomial τ S) (g : σ → MvPolynomial τ S) (p : MvPolynomial σ R) :
    eval x (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => eval x (g s)) p

Proof state:
case h_add
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p✝ p q : MvPolynomial σ R
hp : (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p
hq : (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) q
⊢ (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (p + q)

Tactic:
simp [hp, hq]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p

Tactic:
apply induction_on p

Result:
case h_C
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ ∀ (a : R), (eval x) (eval₂ f g (C a)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (C a)

case h_add
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p →
      (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) q →
        (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (p + q)

case h_X
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p →
      (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (p * X n)

Proof state:
case h_C
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ ∀ (a : R), (eval x) (eval₂ f g (C a)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (C a)

Tactic:
simp

Result:
no goals

Proof state:
case h_X
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p✝ p : MvPolynomial σ R
n : σ
hp : (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p
⊢ (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (p * X n)

Tactic:
simp [hp]

Result:
no goals

Proof state:
case h_X
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p →
      (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (p * X n)

Tactic:
intro p n hp

Result:
case h_X
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p✝ p : MvPolynomial σ R
n : σ
hp : (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p
⊢ (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (p * X n)

Proof state:
case h_add
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p →
      (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) q →
        (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (p + q)

Tactic:
intro p q hp hq

Result:
case h_add
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
τ : Type u_3
x : τ → S
inst✝ : CommSemiring S
f : R →+* MvPolynomial τ S
g : σ → MvPolynomial τ S
p✝ p q : MvPolynomial σ R
hp : (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p
hq : (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) q
⊢ (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (p + q)