awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
pos : ∀ (hc : c = 0), coeff.{u_2, u_1} (σ := σ) 0 ((monomial d : (a : R) → MvPolynomial σ R) c) = c
⊢ coeff (if c = 0 then 0 else d) ((monomial d : (a : R) → MvPolynomial σ R) c) = c
have neg : ∀ (hc : ¬c = 0), coeff d ((monomial d : (a : R) → MvPolynomial σ R) c) = c
Tactic: split_ifs with hc
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ m.leadingCoeff ((monomial d : (a : R) → MvPolynomial σ R) c) = c
have simp : coeff (if c = 0 then 0 else d) ((monomial d : (a : R) → MvPolynomial σ R) c) = c
Tactic: classical
  simp only [leadingCoeff, degree_monomial]
  split_ifs with hc <;> simp [hc]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
⊢ Monic.{u_1, u_2, u_3} m (R := R) ((monomial d : (a : R) → MvPolynomial σ R) c) ↔ c = 1
have rw : Eq.{u_2 + 1} (α := R) (m.leadingCoeff ((monomial d : (a : R) → MvPolynomial σ R) c)) 1 ↔ c = 1
Tactic: rw [Monic, m.leadingCoeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
d : σ →₀ ℕ
c : R
rw : Eq.{u_2 + 1} (α := R) (m.leadingCoeff ((monomial d : (a : R) → MvPolynomial σ R) c)) 1 ↔ c = 1
⊢ Monic.{u_1, u_2, u_3} m (R := R) ((monomial d : (a : R) → MvPolynomial σ R) c) ↔ c = 1
have rw₁ : c = 1 ↔ c = 1
Tactic: rw [Monic, m.leadingCoeff_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
    ∀ c ∈ f.support,
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
have unfold : LE.le.{u_3} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
  ∀ c ∈ f.support,
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
Tactic: unfold degree
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
    ∀ c ∈ f.support,
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
have hd₁ : LT.lt.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
Tactic: simp only [map_zero] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : LT.lt.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
    ∀ c ∈ f.support,
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
have unfold : LT.lt.{u_3} (α := m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))) :
      m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
  ∀ c ∈ f.support,
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
Tactic: unfold degree
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : LT.lt.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ LT.lt.{u_3} (α := m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
          ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))) :
        m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
    ∀ c ∈ f.support,
      LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
have simp : LT.lt.{u_3} (α := m.syn) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ↔
  ∀ c ∈ f.support,
    LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
Tactic: simp only [AddEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
have unfold : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
      ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))) :
    m.syn)
Tactic: unfold degree
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd :
  LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
⊢ coeff d f = 0
have hd₁ : ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
Tactic: rw [← not_le] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd :
  ¬LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
⊢ coeff d f = 0
have by_contra : ∀ (hf : ¬coeff d f = 0), False
Tactic: by_contra hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ m.leadingCoeff f ≠ 0 ↔ f ≠ 0
have mp : m.leadingCoeff f ≠ 0 → f ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
mp : m.leadingCoeff f ≠ 0 → f ≠ 0
⊢ m.leadingCoeff f ≠ 0 ↔ f ≠ 0
have mpr : f ≠ 0 → m.leadingCoeff f ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ m.leadingCoeff f ≠ 0 → f ≠ 0
have mp : f = 0 → m.leadingCoeff f = 0
Tactic: rw [not_imp_not]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f = 0
⊢ m.leadingCoeff f = 0
have mp : Eq.{u_2 + 1} (α := R) (m.leadingCoeff 0) 0
Tactic: rw [hf, leadingCoeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f = 0
mp : Eq.{u_2 + 1} (α := R) (m.leadingCoeff 0) 0
⊢ m.leadingCoeff f = 0
have mp₁ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [hf, leadingCoeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (hypothesis)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f ≠ 0
⊢ m.leadingCoeff f ≠ 0
have hf₁ : f.support.Nonempty
Tactic: rw [← support_nonempty] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ m.leadingCoeff f ≠ 0
have mpr : (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) ∈ f.support
Tactic: rw [leadingCoeff, ← mem_support_iff, degree]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
this :
  Membership.mem (γ := Set m.syn) ((⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) '' (↑f.support : Set (σ →₀ ℕ)))
    (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))
⊢ (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) ∈ f.support
have obtain : ∀ (d : σ →₀ ℕ) (hd : d ∈ (↑f.support : Set (σ →₀ ℕ)))
  (hd' :
    Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
      (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)),
  (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) ∈ f.support
Tactic: obtain ⟨d, hd, hd'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
d : σ →₀ ℕ
hd : d ∈ (↑f.support : Set (σ →₀ ℕ))
hd' :
  Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
    (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) : m.syn)
⊢ (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) ∈ f.support
have rw : d ∈ f.support
Tactic: rw [← hd', AddEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : f.support.Nonempty
⊢ (m.toSyn.symm : (a : m.syn) → σ →₀ ℕ) (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn)) ∈ f.support
have mpr : Membership.mem (γ := Set m.syn) ((⇑m.toSyn : (a : σ →₀ ℕ) → m.syn) '' (↑f.support : Set (σ →₀ ℕ)))
  (f.support.sup (⇑m.toSyn : (a : σ →₀ ℕ) → m.syn))
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
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
hp : p ≠ 0
⊢ m.degree p ∈ p.support
have rwa : coeff (m.degree p) p ≠ 0
Tactic: rwa [MvPolynomial.mem_support_iff, coeff_degree_ne_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ m.degree f = 0 ↔ f.totalDegree = 0
have rw : Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
  f.totalDegree = 0
Tactic: rw [← m.toSyn.injective.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    f.totalDegree = 0
have rw : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
  f.totalDegree = 0
Tactic: rw [map_zero, ← m.bot_eq_zero, eq_bot_iff, m.bot_eq_zero, ← m.toSyn.map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    f.totalDegree = 0
have rw : (∀ c ∈ f.support,
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)) ↔
  f.totalDegree = 0
Tactic: rw [degree_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support,
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)) ↔
    f.totalDegree = 0
have rw : (∀ c ∈ f.support,
    LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
      ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)) ↔
  ∀ m ∈ f.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: rw [totalDegree_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
⊢ (∀ c ∈ f.support,
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn)) ↔
    ∀ m ∈ f.support, ∀ (x : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have h : ∀ (a : σ →₀ ℕ),
  a ∈ f.support →
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) a : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    a ∈ f.support → ∀ (x : σ), Eq (α := ℕ) ((a : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ d ∈ f.support →
      LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
        ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    d ∈ f.support → ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have h : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
  ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: apply imp_congr (rfl.to_iff)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) 0 : m.syn) ↔
    ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have h : Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) (0 : m.syn) ↔
  ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: rw [map_zero, ← m.bot_eq_zero, ← eq_bot_iff, m.bot_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
⊢ Eq.{u_3 + 1} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) (0 : m.syn) ↔
    ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
have h : d = 0 ↔ ∀ (x : σ), Eq (α := ℕ) ((d : (a : σ) → ℕ) x : ℕ) (0 : ℕ)
Tactic: simp only [EmbeddingLike.map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
r : R
⊢ degree.{u_1, u_2, u_3} m (R := R) ((C : (a : R) → MvPolynomial σ R) r) = 0
have rw : totalDegree.{u_2, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) r) = 0
Tactic: rw [degree_eq_zero_iff_totalDegree_eq_zero, totalDegree_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
r : R
rw : totalDegree.{u_2, u_1} (R := R) (σ := σ) ((C : (a : R) → MvPolynomial σ R) r) = 0
⊢ degree.{u_1, u_2, u_3} m (R := R) ((C : (a : R) → MvPolynomial σ R) r) = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [degree_eq_zero_iff_totalDegree_eq_zero, totalDegree_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
⊢ f = (C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)
have a : ∀ (d : σ →₀ ℕ), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
⊢ coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f))
have a : coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
Tactic: simp only [leadingCoeff, hf]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
⊢ coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
have pos : ∀ (hd : d = 0), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
Tactic: by_cases hd : d = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
pos : ∀ (hd : d = 0), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
⊢ coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
have neg : ∀ (hd : ¬d = 0), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
Tactic: by_cases hd : d = 0
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
have neg : coeff d f = 0
Tactic: rw [coeff_C, if_neg (Ne.symm hd)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ coeff d f = 0
have neg : LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
Tactic: apply coeff_eq_zero_of_lt (m := m)
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
hd : ¬d = 0
⊢ LT.lt.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn)
have neg : LE.le.{u_3} (α := m.syn) (0 : m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) d : m.syn) ∧ ¬d = 0
Tactic: rw [hf, map_zero, lt_iff_le_and_ne, ne_eq, eq_comm, EmbeddingLike.map_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
⊢ coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
have pos : ∀ (hd : d = 0), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
Tactic: classical
  by_cases hd : d = 0
  · simp [hd]
  · rw [coeff_C, if_neg (Ne.symm hd)]
    apply coeff_eq_zero_of_lt (m := m)
    rw [hf, map_zero, lt_iff_le_and_ne, ne_eq, eq_comm, EmbeddingLike.map_eq_zero_iff]
    exact ⟨bot_le, hd⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
hf : m.degree f = 0
d : σ →₀ ℕ
pos : ∀ (hd : d = 0), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
⊢ coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
have neg : ∀ (hd : ¬d = 0), coeff d f = coeff d ((C : (a : R) → MvPolynomial σ R) (coeff 0 f))
Tactic: classical
  by_cases hd : d = 0
  · simp [hd]
  · rw [coeff_C, if_neg (Ne.symm hd)]
    apply coeff_eq_zero_of_lt (m := m)
    rw [hf, map_zero, lt_iff_le_and_ne, ne_eq, eq_comm, EmbeddingLike.map_eq_zero_iff]
    exact ⟨bot_le, hd⟩
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
h : f = (C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)
⊢ m.degree f = 0
have rw : degree.{u_1, u_2, u_3} m (R := R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)) = 0
Tactic: rw [h, MonomialOrder.degree_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f : MvPolynomial σ R
h : f = (C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)
rw : degree.{u_1, u_2, u_3} m (R := R) ((C : (a : R) → MvPolynomial σ R) (m.leadingCoeff f)) = 0
⊢ m.degree f = 0
have rw₁ : Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0
Tactic: rw [h, MonomialOrder.degree_C]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
| (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
have rw : ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
    ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ)
      (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)))) :
  m.syn)
Tactic: rw [← m.toSyn.apply_symm_apply (_ ⊔ _)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)) : m.syn)
have conv_rhs : LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
  ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
      ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ)
        (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)))) :
    m.syn)
Tactic: conv_rhs => rw [← m.toSyn.apply_symm_apply (_ ⊔ _)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.MonomialOrder (goal)
Goal:
σ : Type u_1
m : MonomialOrder.{u_1, u_3} σ
R : Type u_2
inst : CommSemiring R
f g : MvPolynomial σ R
⊢ LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree (f + g)) : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ)
          (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)))) :
      m.syn)
have rw : ∀ c ∈ (f + g).support,
  LE.le.{u_3} (α := m.syn) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) c : m.syn)
    ((m.toSyn : (a : σ →₀ ℕ) → m.syn)
        ((m.toSyn.symm : (a : m.syn) → σ →₀ ℕ)
          (max ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree f)) ((m.toSyn : (a : σ →₀ ℕ) → m.syn) (m.degree g)))) :
      m.syn)
Tactic: rw [degree_le_iff]