case mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1217460
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) → cons i m ∈ support f

case mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1217460
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ cons i m ∈ support f → m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1217460
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) ↔ cons i m ∈ support f
apply Iff.intro
case mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1217460
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
⊢ cons i m ∈ support f
case mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1217460
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i) → cons i m ∈ support f
intro h
no goals
case mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1217460
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
⊢ cons i m ∈ support f
simpa [← finSuccEquiv_coeff_coeff] using h
case mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1217460
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : cons i m ∈ support f
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
case mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1217460
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
⊢ cons i m ∈ support f → m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
intro h
no goals
case mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1217460
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
h : cons i m ∈ support f
⊢ m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) f) i)
simpa [mem_support_iff, ← finSuccEquiv_coeff_coeff m f i] using h