-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem map_mvPolynomial_eq_eval₂ {S : Type*} [CommRing S] [Finite σ] (ϕ : MvPolynomial σ R →+* S)
    (p : MvPolynomial σ R) :
    ϕ p = MvPolynomial.eval₂ (ϕ.comp MvPolynomial.C) (fun s => ϕ (MvPolynomial.X s)) p

Proof state:
case intro.e_f.h
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
x✝ : σ →₀ ℕ
⊢ ϕ ((monomial x✝) (coeff x✝ p)) = (ϕ.comp C) (coeff x✝ p) * ∏ i : σ, ϕ (X i) ^ x✝ i

Tactic:
simp only [monomial_eq, ϕ.map_pow, map_prod ϕ, ϕ.comp_apply, ϕ.map_mul, Finsupp.prod_pow]

Result:
no goals

Proof state:
case intro.e_f
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ (fun x => ϕ ((monomial x) (coeff x p))) = fun d => (ϕ.comp C) (coeff d p) * ∏ i : σ, ϕ (X i) ^ d i

Tactic:
ext

Result:
case intro.e_f.h
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
x✝ : σ →₀ ℕ
⊢ ϕ ((monomial x✝) (coeff x✝ p)) = (ϕ.comp C) (coeff x✝ p) * ∏ i : σ, ϕ (X i) ^ x✝ i

Proof state:
case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ϕ (∑ v ∈ p.support, (monomial v) (coeff v p)) = eval₂ (ϕ.comp C) (fun s => ϕ (X s)) p

Tactic:
rw [MvPolynomial.eval₂_eq', map_sum ϕ]

Result:
case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ∑ x ∈ p.support, ϕ ((monomial x) (coeff x p)) = ∑ d ∈ p.support, (ϕ.comp C) (coeff d p) * ∏ i : σ, ϕ (X i) ^ d i

Proof state:
case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ϕ p = eval₂ (ϕ.comp C) (fun s => ϕ (X s)) p

Tactic:
refine Trans.trans (congr_arg ϕ (MvPolynomial.as_sum p)) ?_

Result:
case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ϕ (∑ v ∈ p.support, (monomial v) (coeff v p)) = eval₂ (ϕ.comp C) (fun s => ϕ (X s)) p

Proof state:
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
⊢ ϕ p = eval₂ (ϕ.comp C) (fun s => ϕ (X s)) p

Tactic:
cases nonempty_fintype σ

Result:
case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ϕ p = eval₂ (ϕ.comp C) (fun s => ϕ (X s)) p

Proof state:
case intro
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ ∑ x ∈ p.support, ϕ ((monomial x) (coeff x p)) = ∑ d ∈ p.support, (ϕ.comp C) (coeff d p) * ∏ i : σ, ϕ (X i) ^ d i

Tactic:
congr

Result:
case intro.e_f
R : Type u
σ : Type v
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : Finite σ
ϕ : MvPolynomial σ R →+* S
p : MvPolynomial σ R
val✝ : Fintype σ
⊢ (fun x => ϕ ((monomial x) (coeff x p))) = fun d => (ϕ.comp C) (coeff d p) * ∏ i : σ, ϕ (X i) ^ d i