R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ ↑(eval₂Hom f₁ g₁) p₁ = ↑(eval₂Hom f₁ g₂) p₁
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ f₂ : R →+* S
g₁ g₂ : σ → S
p₁ p₂ : MvPolynomial σ R
⊢ f₁ = f₂ → (∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₂ → g₁ i = g₂ i) → p₁ = p₂ → ↑(eval₂Hom f₁ g₁) p₁ = ↑(eval₂Hom f₂ g₂) p₂
rintro rfl h rfl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ ↑(eval₂Hom f₁ g₁) (∑ v in support p₁, ↑(monomial v) (coeff v p₁)) =
    ↑(eval₂Hom f₁ g₂) (∑ v in support p₁, ↑(monomial v) (coeff v p₁))
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ ↑(eval₂Hom f₁ g₁) p₁ = ↑(eval₂Hom f₁ g₂) p₁
rw [p₁.as_sum]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ (∑ x in support p₁, ↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₁ i ^ k) =
    ∑ x in support p₁, ↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₂ i ^ k
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ ↑(eval₂Hom f₁ g₁) (∑ v in support p₁, ↑(monomial v) (coeff v p₁)) =
    ↑(eval₂Hom f₁ g₂) (∑ v in support p₁, ↑(monomial v) (coeff v p₁))
simp only [map_sum, eval₂Hom_monomial]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ ∀ (x : σ →₀ ℕ),
    x ∈ support p₁ →
      (↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₁ i ^ k) = ↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₂ i ^ k
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ (∑ x in support p₁, ↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₁ i ^ k) =
    ∑ x in support p₁, ↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₂ i ^ k
apply Finset.sum_congr rfl
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ (↑f₁ (coeff d p₁) * Finsupp.prod d fun i k => g₁ i ^ k) = ↑f₁ (coeff d p₁) * Finsupp.prod d fun i k => g₂ i ^ k
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
⊢ ∀ (x : σ →₀ ℕ),
    x ∈ support p₁ →
      (↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₁ i ^ k) = ↑f₁ (coeff x p₁) * Finsupp.prod x fun i k => g₂ i ^ k
intro d hd
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ (Finsupp.prod d fun i k => g₁ i ^ k) = Finsupp.prod d fun i k => g₂ i ^ k
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ (↑f₁ (coeff d p₁) * Finsupp.prod d fun i k => g₁ i ^ k) = ↑f₁ (coeff d p₁) * Finsupp.prod d fun i k => g₂ i ^ k
congr 1
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ ∏ x in d.support, g₁ x ^ ↑d x = ∏ x in d.support, g₂ x ^ ↑d x
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ (Finsupp.prod d fun i k => g₁ i ^ k) = Finsupp.prod d fun i k => g₂ i ^ k
simp only [Finsupp.prod]
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ ∀ (x : σ), x ∈ d.support → g₁ x ^ ↑d x = g₂ x ^ ↑d x
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ ∏ x in d.support, g₁ x ^ ↑d x = ∏ x in d.support, g₂ x ^ ↑d x
apply Finset.prod_congr rfl
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
i : σ
hi : i ∈ d.support
⊢ g₁ i ^ ↑d i = g₂ i ^ ↑d i
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
⊢ ∀ (x : σ), x ∈ d.support → g₁ x ^ ↑d x = g₂ x ^ ↑d x
intro i hi
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
i : σ
hi : i ∈ d.support
this : i ∈ vars p₁
⊢ g₁ i ^ ↑d i = g₂ i ^ ↑d i
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
i : σ
hi : i ∈ d.support
⊢ g₁ i ^ ↑d i = g₂ i ^ ↑d i
have : i ∈ p₁.vars := by
  rw [mem_vars]
  exact ⟨d, hd, hi⟩
no goals
case e_a
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
i : σ
hi : i ∈ d.support
this : i ∈ vars p₁
⊢ g₁ i ^ ↑d i = g₂ i ^ ↑d i
rw [h i this this]
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
i : σ
hi : i ∈ d.support
⊢ ∃ d x, i ∈ d.support
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
i : σ
hi : i ∈ d.support
⊢ i ∈ vars p₁
rw [mem_vars]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.629877
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ (i : σ), i ∈ vars p₁ → i ∈ vars p₁ → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ support p₁
i : σ
hi : i ∈ d.support
⊢ ∃ d x, i ∈ d.support
exact ⟨d, hd, hi⟩