no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
⊢ degrees (↑(rename f) φ) ⊆ Multiset.map f (degrees φ)
classical
intro i
rw [mem_degrees, Multiset.mem_map]
rintro ⟨d, hd, hi⟩
obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
rw [sum_apply, Finsupp.sum] at hi
contrapose! hi
rw [Finset.sum_eq_zero]
intro j hj
simp only [exists_prop, mem_degrees] at hi
specialize hi j ⟨x, hx, hj⟩
rw [Finsupp.single_apply, if_neg hi]
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ i ∈ degrees (↑(rename f) φ) → i ∈ Multiset.map f (degrees φ)
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
⊢ degrees (↑(rename f) φ) ⊆ Multiset.map f (degrees φ)
intro i
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ (∃ d, coeff d (↑(rename f) φ) ≠ 0 ∧ i ∈ d.support) → ∃ a, a ∈ degrees φ ∧ f a = i
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ i ∈ degrees (↑(rename f) φ) → i ∈ Multiset.map f (degrees φ)
rw [mem_degrees, Multiset.mem_map]
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
d : τ →₀ ℕ
hd : coeff d (↑(rename f) φ) ≠ 0
hi : i ∈ d.support
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ (∃ d, coeff d (↑(rename f) φ) ≠ 0 ∧ i ∈ d.support) → ∃ a, a ∈ degrees φ ∧ f a = i
rintro ⟨d, hd, hi⟩
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : i ∈ (Finsupp.mapDomain f x).support
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
case intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
d : τ →₀ ℕ
hd : coeff d (↑(rename f) φ) ≠ 0
hi : i ∈ d.support
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ↑(sum x fun a => Finsupp.single (f a)) i ≠ 0
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : i ∈ (Finsupp.mapDomain f x).support
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∑ a in x.support, ↑(Finsupp.single (f a) (↑x a)) i ≠ 0
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ↑(sum x fun a => Finsupp.single (f a)) i ≠ 0
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
rw [sum_apply, Finsupp.sum] at hi
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∀ (a : σ), a ∈ degrees φ → f a ≠ i
⊢ ∑ x_1 in x.support, ↑(Finsupp.single (f x_1) (↑x x_1)) i = 0
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∑ a in x.support, ↑(Finsupp.single (f a) (↑x a)) i ≠ 0
⊢ ∃ a, a ∈ degrees φ ∧ f a = i
contrapose! hi
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∀ (a : σ), a ∈ degrees φ → f a ≠ i
⊢ ∀ (x_1 : σ), x_1 ∈ x.support → ↑(Finsupp.single (f x_1) (↑x x_1)) i = 0
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∀ (a : σ), a ∈ degrees φ → f a ≠ i
⊢ ∑ x_1 in x.support, ↑(Finsupp.single (f x_1) (↑x x_1)) i = 0
rw [Finset.sum_eq_zero]
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∀ (a : σ), a ∈ degrees φ → f a ≠ i
j : σ
hj : j ∈ x.support
⊢ ↑(Finsupp.single (f j) (↑x j)) i = 0
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∀ (a : σ), a ∈ degrees φ → f a ≠ i
⊢ ∀ (x_1 : σ), x_1 ∈ x.support → ↑(Finsupp.single (f x_1) (↑x x_1)) i = 0
intro j hj
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : ∀ (a : σ), (∃ d, coeff d φ ≠ 0 ∧ a ∈ d.support) → f a ≠ i
⊢ ↑(Finsupp.single (f j) (↑x j)) i = 0
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
hi : ∀ (a : σ), a ∈ degrees φ → f a ≠ i
j : σ
hj : j ∈ x.support
⊢ ↑(Finsupp.single (f j) (↑x j)) i = 0
simp only [exists_prop, mem_degrees] at hi
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : f j ≠ i
⊢ ↑(Finsupp.single (f j) (↑x j)) i = 0
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : ∀ (a : σ), (∃ d, coeff d φ ≠ 0 ∧ a ∈ d.support) → f a ≠ i
⊢ ↑(Finsupp.single (f j) (↑x j)) i = 0
specialize hi j ⟨x, hx, hj⟩
no goals
case intro.intro.intro.intro
R : Type u
S : Type v
σ : Type u_1
τ : Type u_2
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : coeff (Finsupp.mapDomain f x) (↑(rename f) φ) ≠ 0
j : σ
hj : j ∈ x.support
hi : f j ≠ i
⊢ ↑(Finsupp.single (f j) (↑x j)) i = 0
rw [Finsupp.single_apply, if_neg hi]