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