-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_eq_zero_iff_totalDegree_eq_zero {f : MvPolynomial σ R} :
    m.degree f = 0 ↔ f.totalDegree = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) ≤ m.toSyn 0 ↔ f.totalDegree = 0

Tactic:
rw [degree_le_iff]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support, m.toSyn c ≤ m.toSyn 0) ↔ f.totalDegree = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support, m.toSyn c ≤ m.toSyn 0) ↔ ∀ m ∈ f.support, ∀ (x : σ), m x = 0

Tactic:
apply forall_congr'

Result:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ ∀ (a : σ →₀ ℕ), a ∈ f.support → m.toSyn a ≤ m.toSyn 0 ↔ a ∈ f.support → ∀ (x : σ), a x = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.degree f = 0 ↔ f.totalDegree = 0

Tactic:
rw [← m.toSyn.injective.eq_iff]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) = m.toSyn 0 ↔ f.totalDegree = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) = m.toSyn 0 ↔ f.totalDegree = 0

Tactic:
rw [map_zero, ← m.bot_eq_zero, eq_bot_iff, m.bot_eq_zero, ← m.toSyn.map_zero]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree f) ≤ m.toSyn 0 ↔ f.totalDegree = 0

Proof state:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d = 0 ↔ ∀ (x : σ), d x = 0

Tactic:
simp only [EmbeddingLike.map_eq_zero_iff]

Result:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ d = 0 ↔ ∀ (x : σ), d x = 0

Proof state:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d ≤ m.toSyn 0 ↔ ∀ (x : σ), d x = 0

Tactic:
rw [map_zero, ← m.bot_eq_zero, ← eq_bot_iff, m.bot_eq_zero]

Result:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d = 0 ↔ ∀ (x : σ), d x = 0

Proof state:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ ∀ (a : σ →₀ ℕ), a ∈ f.support → m.toSyn a ≤ m.toSyn 0 ↔ a ∈ f.support → ∀ (x : σ), a x = 0

Tactic:
intro d

Result:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ d ∈ f.support → m.toSyn d ≤ m.toSyn 0 ↔ d ∈ f.support → ∀ (x : σ), d x = 0

Proof state:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ d = 0 ↔ ∀ (x : σ), d x = 0

Tactic:
exact Finsupp.ext_iff

Result:
no goals

Proof state:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ d ∈ f.support → m.toSyn d ≤ m.toSyn 0 ↔ d ∈ f.support → ∀ (x : σ), d x = 0

Tactic:
apply imp_congr (rfl.to_iff)

Result:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ m.toSyn d ≤ m.toSyn 0 ↔ ∀ (x : σ), d x = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support, m.toSyn c ≤ m.toSyn 0) ↔ f.totalDegree = 0

Tactic:
rw [totalDegree_eq_zero_iff]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support, m.toSyn c ≤ m.toSyn 0) ↔ ∀ m ∈ f.support, ∀ (x : σ), m x = 0