-- Mathlib/Algebra/MvPolynomial/Equiv.lean
/--
The `totalDegree` of a multivariable polynomial `p` is at least `i` more than the `totalDegree` of
the `i`th coefficient of `finSuccEquiv` applied to `p`, if this is nonzero.
-/
lemma totalDegree_coeff_finSuccEquiv_add_le (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ)
    (hi : (finSuccEquiv R n f).coeff i ≠ 0) :
    totalDegree ((finSuccEquiv R n f).coeff i) + i ≤ totalDegree f

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree

Tactic:
let σ' : Fin (n+1) →₀ ℕ := cons i σ

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ ¬((finSuccEquiv R n) f).coeff i = 0

Tactic:
exact hi

Result:
no goals

Proof state:
case convert_4
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ σ ∈ (((finSuccEquiv R n) f).coeff i).support

Tactic:
exact hσ1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree

Tactic:
have ⟨σ, hσ1, hσ2⟩ := Finset.exists_mem_eq_sup (support _) hf'_sup
                        (fun s => Finsupp.sum s fun _ e => e)

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree

Tactic:
convert le_totalDegree (s := σ') _

Result:
case h.e'_3
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i = σ'.sum fun x e => e

case convert_4
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ σ' ∈ f.support

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree

Tactic:
have hf'_sup : ((finSuccEquiv R n f).coeff i).support.Nonempty := by
  rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]
  exact hi

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i ≤ f.totalDegree

Proof state:
case h.e'_3
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ (((finSuccEquiv R n) f).coeff i).totalDegree + i = σ'.sum fun x e => e

Tactic:
rw [totalDegree, hσ2, sum_cons, add_comm]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ (((finSuccEquiv R n) f).coeff i).support.Nonempty

Tactic:
rw [Finset.nonempty_iff_ne_empty, ne_eq, support_eq_empty]

Result:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
⊢ ¬((finSuccEquiv R n) f).coeff i = 0

Proof state:
case convert_4
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ σ' ∈ f.support

Tactic:
rw [← support_coeff_finSuccEquiv]

Result:
case convert_4
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
hi : ((finSuccEquiv R n) f).coeff i ≠ 0
hf'_sup : (((finSuccEquiv R n) f).coeff i).support.Nonempty
σ : Fin n →₀ ℕ
hσ1 : σ ∈ (((finSuccEquiv R n) f).coeff i).support
hσ2 : ((((finSuccEquiv R n) f).coeff i).support.sup fun s => s.sum fun x e => e) = σ.sum fun x e => e
σ' : Fin (n + 1) →₀ ℕ := cons i σ
⊢ σ ∈ (((finSuccEquiv R n) f).coeff i).support