case h_X
σ : Type u_1
τ : Type u_3
α : Type ?u.539883
R : Type u_2
S : Type ?u.539889
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : ↑(rename k) (eval₂ C (g ∘ k) p✝) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p✝)
⊢ ↑(rename k) (eval₂ C (g ∘ k) (p✝ * X n✝)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (p✝ * X n✝))
case h_X
σ : Type u_1
τ : Type u_3
α : Type ?u.539883
R : Type u_2
S : Type ?u.539889
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    ↑(rename k) (eval₂ C (g ∘ k) p) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p) →
      ↑(rename k) (eval₂ C (g ∘ k) (p * X n)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (p * X n))
intros
no goals
case h_X
σ : Type u_1
τ : Type u_3
α : Type ?u.539883
R : Type u_2
S : Type ?u.539889
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : ↑(rename k) (eval₂ C (g ∘ k) p✝) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p✝)
⊢ ↑(rename k) (eval₂ C (g ∘ k) (p✝ * X n✝)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (p✝ * X n✝))
simp [*]