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

case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ coeff m f ≠ 0 ∧ ↑m 0 = i → ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m
case a
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) ↔ coeff m f ≠ 0 ∧ ↑m 0 = i
constructor
case a.mp.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
m' : Fin n →₀ ℕ
h : ¬coeff (cons i m') f = 0
hm' : cons i m' = m
⊢ coeff m f ≠ 0 ∧ ↑m 0 = i
case a.mp
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) → coeff m f ≠ 0 ∧ ↑m 0 = i
rintro ⟨m', ⟨h, hm'⟩⟩
case a.mp.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
m' : Fin n →₀ ℕ
h : ¬coeff (cons i m') f = 0
hm' : cons i m' = m
⊢ coeff (cons i m') f ≠ 0 ∧ ↑(cons i m') 0 = i
case a.mp.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
m' : Fin n →₀ ℕ
h : ¬coeff (cons i m') f = 0
hm' : cons i m' = m
⊢ coeff m f ≠ 0 ∧ ↑m 0 = i
simp only [← hm']
no goals
case a.mp.intro.intro
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
m' : Fin n →₀ ℕ
h : ¬coeff (cons i m') f = 0
hm' : cons i m' = m
⊢ coeff (cons i m') f ≠ 0 ∧ ↑(cons i m') 0 = i
exact ⟨h, by rw [cons_zero]⟩
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
m' : Fin n →₀ ℕ
h : ¬coeff (cons i m') f = 0
hm' : cons i m' = m
⊢ ↑(cons i m') 0 = i
rw [cons_zero]
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ coeff m f ≠ 0 ∧ ↑m 0 = i → ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m
intro h
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ¬coeff (cons i (tail m)) f = 0 ∧ cons i (tail m) = m
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m
use tail m
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ¬coeff m f = 0 ∧ m = m
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ¬coeff (cons i (tail m)) f = 0 ∧ cons i (tail m) = m
rw [← h.2, cons_tail]
no goals
case a.mpr
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1259240
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
h : coeff m f ≠ 0 ∧ ↑m 0 = i
⊢ ¬coeff m f = 0 ∧ m = m
simp [h.1]