-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_ne_zero_iff {f : MvPolynomial σ R} :
    m.leadingCoeff f ≠ 0 ↔ f ≠ 0

Proof state:
case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f = 0
⊢ m.leadingCoeff f = 0

Tactic:
rw [hf, leadingCoeff_zero]

Result:
no goals

Proof state:
case intro.intro
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
d : σ →₀ ℕ
hd : d ∈ ↑f.support
hd' : m.toSyn d = f.support.sup ⇑m.toSyn
⊢ m.toSyn.symm (f.support.sup ⇑m.toSyn) ∈ f.support

Tactic:
rw [← hd', AddEquiv.symm_apply_apply]

Result:
case intro.intro
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
d : σ →₀ ℕ
hd : d ∈ ↑f.support
hd' : m.toSyn d = f.support.sup ⇑m.toSyn
⊢ d ∈ f.support

Proof state:
case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.leadingCoeff f ≠ 0 → f ≠ 0

Tactic:
rw [not_imp_not]

Result:
case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ f = 0 → m.leadingCoeff f = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
this : f.support.sup ⇑m.toSyn ∈ ⇑m.toSyn '' ↑f.support
⊢ m.toSyn.symm (f.support.sup ⇑m.toSyn) ∈ f.support

Tactic:
obtain ⟨d, hd, hd'⟩ := this

Result:
case intro.intro
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
d : σ →₀ ℕ
hd : d ∈ ↑f.support
hd' : m.toSyn d = f.support.sup ⇑m.toSyn
⊢ m.toSyn.symm (f.support.sup ⇑m.toSyn) ∈ f.support

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.leadingCoeff f ≠ 0 ↔ f ≠ 0

Tactic:
constructor

Result:
case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.leadingCoeff f ≠ 0 → f ≠ 0

case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ f ≠ 0 → m.leadingCoeff f ≠ 0

Proof state:
case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ f = 0 → m.leadingCoeff f = 0

Tactic:
intro hf

Result:
case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f = 0
⊢ m.leadingCoeff f = 0

Proof state:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f ≠ 0
⊢ m.leadingCoeff f ≠ 0

Tactic:
rw [← support_nonempty] at hf

Result:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.leadingCoeff f ≠ 0

Proof state:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.toSyn.symm (f.support.sup ⇑m.toSyn) ∈ f.support

Tactic:
suffices f.support.sup m.toSyn ∈ m.toSyn '' f.support by
  obtain ⟨d, hd, hd'⟩ := this
  rw [← hd', AddEquiv.symm_apply_apply]
  exact hd

Result:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ f.support.sup ⇑m.toSyn ∈ ⇑m.toSyn '' ↑f.support

Proof state:
case intro.intro
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
d : σ →₀ ℕ
hd : d ∈ ↑f.support
hd' : m.toSyn d = f.support.sup ⇑m.toSyn
⊢ d ∈ f.support

Tactic:
exact hd

Result:
no goals

Proof state:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ f.support.sup ⇑m.toSyn ∈ ⇑m.toSyn '' ↑f.support

Tactic:
exact Finset.sup_mem_of_nonempty hf

Result:
no goals

Proof state:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ f ≠ 0 → m.leadingCoeff f ≠ 0

Tactic:
intro hf

Result:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f ≠ 0
⊢ m.leadingCoeff f ≠ 0

Proof state:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.leadingCoeff f ≠ 0

Tactic:
rw [leadingCoeff, ← mem_support_iff, degree]

Result:
case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.toSyn.symm (f.support.sup ⇑m.toSyn) ∈ f.support