case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ i ∈ Polynomial.support (↑(finSuccEquiv R n) f) ↔ i ∈ Finset.image (fun m => ↑m 0) (support f)
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ Polynomial.support (↑(finSuccEquiv R n) f) = Finset.image (fun m => ↑m 0) (support f)
ext i
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0) ↔ ∃ a, a ∈ support f ∧ ↑a 0 = i
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ i ∈ Polynomial.support (↑(finSuccEquiv R n) f) ↔ i ∈ Finset.image (fun m => ↑m 0) (support f)
rw [Polynomial.mem_support_iff, Finset.mem_image, nonzero_iff_exists]
case a.mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0) → ∃ a, a ∈ support f ∧ ↑a 0 = i

case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, a ∈ support f ∧ ↑a 0 = i) → ∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0) ↔ ∃ a, a ∈ support f ∧ ↑a 0 = i
constructor
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ ∃ a, a ∈ support f ∧ ↑a 0 = i
case a.mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0) → ∃ a, a ∈ support f ∧ ↑a 0 = i
rintro ⟨m, hm⟩
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ cons i m ∈ support f
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ ∃ a, a ∈ support f ∧ ↑a 0 = i
refine' ⟨cons i m, _, cons_zero _ _⟩
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ cons i m ∈ support f
rw [← support_coeff_finSuccEquiv]
no goals
case a.mp.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) m ≠ 0
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
simpa using hm
case a.mpr.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ support f
⊢ ∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) (↑m 0)) a ≠ 0
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, a ∈ support f ∧ ↑a 0 = i) → ∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) i) a ≠ 0
rintro ⟨m, h, rfl⟩
case a.mpr.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ support f
⊢ ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) (↑m 0)) (tail m) ≠ 0
case a.mpr.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ support f
⊢ ∃ a, ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) (↑m 0)) a ≠ 0
refine' ⟨tail m, _⟩
no goals
case a.mpr.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1237859
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ support f
⊢ ↑(Polynomial.coeff (↑(finSuccEquiv R n) f) (↑m 0)) (tail m) ≠ 0
rwa [← coeff, ← mem_support_iff, support_coeff_finSuccEquiv, cons_tail]