R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
⊢ ↑(eval₂Hom f g) (∑ v in support p, ↑(monomial v) (coeff v p)) = ↑f (↑constantCoeff p)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
⊢ ↑(eval₂Hom f g) p = ↑f (↑constantCoeff p)
conv_lhs => rw [p.as_sum]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
⊢ ↑(eval₂Hom f g) (∑ v in support p, ↑(monomial v) (coeff v p)) = ↑f (↑constantCoeff p)
simp only [map_sum, eval₂Hom_monomial]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)

case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
by_cases h0 : constantCoeff p = 0
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0

case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)

case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
on_goal 1 =>
  rw [h0, f.map_zero, Finset.sum_eq_zero]
  intro d hd
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0

case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0

case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0

case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
on_goal 3 =>
  rw [constantCoeff_eq, coeff, ← Ne.def, ← Finsupp.mem_support_iff] at h0
  intro
  contradiction
no goals
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0

case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
repeat'
  obtain ⟨i, hi⟩ : Finset.Nonempty (Finsupp.support d) := by
    rw [constantCoeff_eq, coeff, ← Finsupp.not_mem_support_iff] at h0
    rw [Finset.nonempty_iff_ne_empty, Ne.def, Finsupp.support_eq_empty]
    rintro rfl
    contradiction
  rw [Finsupp.prod, Finset.prod_eq_zero hi, MulZeroClass.mul_zero]
  rw [hp, zero_pow (Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)]
  rw [mem_vars]
  exact ⟨d, hd, hi⟩
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ ∀ (x : σ →₀ ℕ), x ∈ support p → (↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = 0
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
rw [h0, f.map_zero, Finset.sum_eq_zero]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ ∀ (x : σ →₀ ℕ), x ∈ support p → (↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = 0
intro d hd
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ ∀ (x : σ →₀ ℕ), x ∈ support p → (↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = 0
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
rw [h0, f.map_zero, Finset.sum_eq_zero]
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
case pos
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ↑constantCoeff p = 0
⊢ ∀ (x : σ →₀ ℕ), x ∈ support p → (↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = 0
intro d hd
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = ↑f (↑constantCoeff p)

case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ∀ (b : σ →₀ ℕ), b ∈ support p → b ≠ 0 → (↑f (coeff b p) * Finsupp.prod b fun i k => g i ^ k) = 0

case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0

case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ∀ (b : σ →₀ ℕ), b ∈ support p → b ≠ 0 → (↑f (coeff b p) * Finsupp.prod b fun i k => g i ^ k) = 0

case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
intro d hd hd0
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ↑f (coeff 0 p) = ↑f (↑constantCoeff p)
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = ↑f (↑constantCoeff p)
rw [Finsupp.prod_zero_index, mul_one]
no goals
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ↑f (coeff 0 p) = ↑f (↑constantCoeff p)
rfl
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = ↑f (↑constantCoeff p)

case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ∀ (b : σ →₀ ℕ), b ∈ support p → b ≠ 0 → (↑f (coeff b p) * Finsupp.prod b fun i k => g i ^ k) = 0

case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (∑ x in support p, ↑f (coeff x p) * Finsupp.prod x fun i k => g i ^ k) = ↑f (↑constantCoeff p)
rw [Finset.sum_eq_single (0 : σ →₀ ℕ)]
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0

case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ∀ (b : σ →₀ ℕ), b ∈ support p → b ≠ 0 → (↑f (coeff b p) * Finsupp.prod b fun i k => g i ^ k) = 0

case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
intro d hd hd0
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ↑f (coeff 0 p) = ↑f (↑constantCoeff p)
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = ↑f (↑constantCoeff p)
rw [Finsupp.prod_zero_index, mul_one]
no goals
case neg
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ↑f (coeff 0 p) = ↑f (↑constantCoeff p)
rfl
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : 0 ∈ p.support
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
rw [constantCoeff_eq, coeff, ← Ne.def, ← Finsupp.mem_support_iff] at h0
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : 0 ∈ p.support
a✝ : ¬0 ∈ support p
⊢ (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : 0 ∈ p.support
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
intro
no goals
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : 0 ∈ p.support
a✝ : ¬0 ∈ support p
⊢ (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
contradiction
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : 0 ∈ p.support
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
rw [constantCoeff_eq, coeff, ← Ne.def, ← Finsupp.mem_support_iff] at h0
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : 0 ∈ p.support
a✝ : ¬0 ∈ support p
⊢ (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : 0 ∈ p.support
⊢ ¬0 ∈ support p → (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
intro
no goals
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : 0 ∈ p.support
a✝ : ¬0 ∈ support p
⊢ (↑f (coeff 0 p) * Finsupp.prod 0 fun i k => g i ^ k) = 0
contradiction
case neg.h₀.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
case neg.h₀
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
obtain ⟨i, hi⟩ : Finset.Nonempty (Finsupp.support d) := by
  rw [constantCoeff_eq, coeff, ← Finsupp.not_mem_support_iff] at h0
  rw [Finset.nonempty_iff_ne_empty, Ne.def, Finsupp.support_eq_empty]
  rintro rfl
  contradiction
case neg.h₀.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ g i ^ ↑d i = 0
case neg.h₀.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ (↑f (coeff d p) * Finsupp.prod d fun i k => g i ^ k) = 0
rw [Finsupp.prod, Finset.prod_eq_zero hi, MulZeroClass.mul_zero]
case neg.h₀.intro.a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ i ∈ vars p
case neg.h₀.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ g i ^ ↑d i = 0
rw [hp, zero_pow (Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)]
case neg.h₀.intro.a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ ∃ d x, i ∈ d.support
case neg.h₀.intro.a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ i ∈ vars p
rw [mem_vars]
no goals
case neg.h₀.intro.a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
i : σ
hi : i ∈ d.support
⊢ ∃ d x, i ∈ d.support
exact ⟨d, hd, hi⟩
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬¬0 ∈ p.support
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ Finset.Nonempty d.support
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬↑constantCoeff p = 0
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ Finset.Nonempty d.support
rw [constantCoeff_eq, coeff, ← Finsupp.not_mem_support_iff] at h0
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬¬0 ∈ p.support
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ ¬d = 0
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬¬0 ∈ p.support
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ Finset.Nonempty d.support
rw [Finset.nonempty_iff_ne_empty, Ne.def, Finsupp.support_eq_empty]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬¬0 ∈ p.support
hd : 0 ∈ support p
hd0 : 0 ≠ 0
⊢ False
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬¬0 ∈ p.support
d : σ →₀ ℕ
hd : d ∈ support p
hd0 : d ≠ 0
⊢ ¬d = 0
rintro rfl
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.482825
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p✝ q : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ (i : σ), i ∈ vars p → g i = 0
h0 : ¬¬0 ∈ p.support
hd : 0 ∈ support p
hd0 : 0 ≠ 0
⊢ False
contradiction