-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem support_finSuccEquiv (f : MvPolynomial (Fin (n + 1)) R) :
    (finSuccEquiv R n f).support = Finset.image (fun m : Fin (n + 1) →₀ ℕ => m 0) f.support

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, (((finSuccEquiv R n) f).coeff i) a ≠ 0 a) ↔ ∃ a ∈ f.support, a 0 = i

Tactic:
constructor

Result:
case h.mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, (((finSuccEquiv R n) f).coeff i) a ≠ 0 a) → ∃ a ∈ f.support, a 0 = i

case h.mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a ∈ f.support, a 0 = i) → ∃ a, (((finSuccEquiv R n) f).coeff i) a ≠ 0 a

Proof state:
case h.mpr.intro.intro
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ f.support
⊢ ∃ a, (((finSuccEquiv R n) f).coeff (m 0)) a ≠ 0 a

Tactic:
refine ⟨tail m, ?_⟩

Result:
case h.mpr.intro.intro
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ f.support
⊢ (((finSuccEquiv R n) f).coeff (m 0)) m.tail ≠ 0 m.tail

Proof state:
case h.mp.intro
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : (((finSuccEquiv R n) f).coeff i) m ≠ 0 m
⊢ cons i m ∈ f.support

Tactic:
rw [← support_coeff_finSuccEquiv]

Result:
case h.mp.intro
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : (((finSuccEquiv R n) f).coeff i) m ≠ 0 m
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support

Proof state:
case h.mp.intro
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : (((finSuccEquiv R n) f).coeff i) m ≠ 0 m
⊢ ∃ a ∈ f.support, a 0 = i

Tactic:
refine ⟨cons i m, ?_, cons_zero _ _⟩

Result:
case h.mp.intro
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : (((finSuccEquiv R n) f).coeff i) m ≠ 0 m
⊢ cons i m ∈ f.support

Proof state:
case h.mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, (((finSuccEquiv R n) f).coeff i) a ≠ 0 a) → ∃ a ∈ f.support, a 0 = i

Tactic:
rintro ⟨m, hm⟩

Result:
case h.mp.intro
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : (((finSuccEquiv R n) f).coeff i) m ≠ 0 m
⊢ ∃ a ∈ f.support, a 0 = i

Proof state:
case h.mpr.intro.intro
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ f.support
⊢ (((finSuccEquiv R n) f).coeff (m 0)) m.tail ≠ 0 m.tail

Tactic:
rwa [← coeff, zero_apply, ← mem_support_iff, support_coeff_finSuccEquiv, cons_tail]

Result:
no goals

Proof state:
case h.mpr
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a ∈ f.support, a 0 = i) → ∃ a, (((finSuccEquiv R n) f).coeff i) a ≠ 0 a

Tactic:
rintro ⟨m, h, rfl⟩

Result:
case h.mpr.intro.intro
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
m : Fin (n + 1) →₀ ℕ
h : m ∈ f.support
⊢ ∃ a, (((finSuccEquiv R n) f).coeff (m 0)) a ≠ 0 a

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ i ∈ ((finSuccEquiv R n) f).support ↔ i ∈ Finset.image (fun m => m 0) f.support

Tactic:
rw [Polynomial.mem_support_iff, Finset.mem_image, Finsupp.ne_iff]

Result:
case h
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ (∃ a, (((finSuccEquiv R n) f).coeff i) a ≠ 0 a) ↔ ∃ a ∈ f.support, a 0 = i

Proof state:
case h.mp.intro
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin n →₀ ℕ
hm : (((finSuccEquiv R n) f).coeff i) m ≠ 0 m
⊢ m ∈ (((finSuccEquiv R n) f).coeff i).support

Tactic:
simpa using hm

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
⊢ ((finSuccEquiv R n) f).support = Finset.image (fun m => m 0) f.support

Tactic:
ext i

Result:
case h
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ i ∈ ((finSuccEquiv R n) f).support ↔ i ∈ Finset.image (fun m => m 0) f.support