-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_mul_X_eq_degreeOf_add_one_iff (j : σ) (f : MvPolynomial σ R) :
    degreeOf j (f * X j) = degreeOf j f + 1 ↔ f ≠ 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : degreeOf j (f * X j) = degreeOf j f + 1
ha : f = 0
⊢ False

Tactic:
simp [ha] at h

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
⊢ (f.support.sup fun m => m j + 1) ≤ (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun m => m j

Tactic:
apply Finset.sup_le

Result:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
⊢ ∀ b ∈ f.support, b j + 1 ≤ (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun m => m j

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
⊢ degreeOf j f + 1 ≤ degreeOf j (f * X j)

Tactic:
have : (f.support.sup fun m ↦ m j) + 1 = (f.support.sup fun m ↦ (m j + 1)) :=
  Finset.comp_sup_eq_sup_comp_of_nonempty @Nat.succ_le_succ (support_nonempty.mpr h)

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
⊢ degreeOf j f + 1 ≤ degreeOf j (f * X j)

Proof state:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
⊢ ∀ b ∈ f.support, b j + 1 ≤ (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun m => m j

Tactic:
intro x hx

Result:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ x j + 1 ≤ (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun m => m j

Proof state:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ x j + 1 ≤ (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun m => m j

Tactic:
simp only [Finset.sup_map, bot_eq_zero', add_pos_iff, zero_lt_one, or_true, Finset.le_sup_iff]

Result:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ ∃ b ∈ f.support, x j + 1 ≤ ((fun m => m j) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) b

Proof state:
case h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ x ∈ f.support ∧ x j + 1 ≤ ((fun m => m j) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) x

Tactic:
simpa using mem_support_iff.mp hx

Result:
no goals

Proof state:
case a
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ ∃ b ∈ f.support, x j + 1 ≤ ((fun m => m j) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) b

Tactic:
use x

Result:
case h
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
x : σ →₀ ℕ
hx : x ∈ f.support
⊢ x ∈ f.support ∧ x j + 1 ≤ ((fun m => m j) ∘ ⇑(addRightEmbedding (Finsupp.single j 1))) x

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
⊢ degreeOf j (f * X j) = degreeOf j f + 1

Tactic:
apply Nat.le_antisymm (degreeOf_mul_X_self j f)

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
⊢ degreeOf j f + 1 ≤ degreeOf j (f * X j)

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
⊢ degreeOf j f + 1 ≤ degreeOf j (f * X j)

Tactic:
simp only [degreeOf_eq_sup, support_mul_X, this]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
this : (f.support.sup fun m => m j) + 1 = f.support.sup fun m => m j + 1
⊢ (f.support.sup fun m => m j + 1) ≤ (Finset.map (addRightEmbedding (Finsupp.single j 1)) f.support).sup fun m => m j

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) = degreeOf j f + 1 ↔ f ≠ 0

Tactic:
refine ⟨fun h => by by_contra ha; simp [ha] at h, fun h => ?_⟩

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : f ≠ 0
⊢ degreeOf j (f * X j) = degreeOf j f + 1

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : degreeOf j (f * X j) = degreeOf j f + 1
⊢ f ≠ 0

Tactic:
by_contra ha

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
h : degreeOf j (f * X j) = degreeOf j f + 1
ha : f = 0
⊢ False