awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
i : σ
p : MvPolynomial σ R
n : ℕ
hp : p ≠ 0
⊢ ∑ i_1 ∈ range n, degreeOf i p = n * degreeOf i p

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
a : ∀ (s : σ), Multiset.count s (p * q).degrees = Multiset.count s (p.degrees + q.degrees)
⊢ (p * q).degrees = p.degrees + q.degrees

Tactic:
ext s
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
s : σ
a : Multiset.count s (p * q).degrees = Multiset.count s p.degrees + Multiset.count s q.degrees
a₁ : degreeOf s (p * q) = degreeOf s p + degreeOf s q
⊢ Multiset.count s (p * q).degrees = Multiset.count s (p.degrees + q.degrees)

Tactic:
simp_rw [Multiset.count_add, ← degreeOf_def, degreeOf_mul_eq hp hq]

Premises used: MvPolynomial.degreeOf_def, MvPolynomial.degreeOf_mul_eq, Multiset.count_add
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
a : ∀ (s : σ), Multiset.count s (p * q).degrees = Multiset.count s (p.degrees + q.degrees)
⊢ (p * q).degrees = p.degrees + q.degrees

Tactic:
classical
  ext s
  simp_rw [Multiset.count_add, ← degreeOf_def, degreeOf_mul_eq hp hq]

Premises used: MvPolynomial.degreeOf_def, MvPolynomial.degreeOf_mul_eq, Multiset.count_add
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
intro : ∀ (w : LinearOrder σ), WellFoundedGT σ → (f * g).totalDegree = f.totalDegree + g.totalDegree
⊢ (f * g).totalDegree = f.totalDegree + g.totalDegree

Tactic:
cases exists_wellFoundedGT σ

Premises used: exists_wellFoundedGT
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
w : LinearOrder σ
h : WellFoundedGT σ
⊢ (f * g).totalDegree = f.totalDegree + g.totalDegree

Tactic:
simp [← degree_degLexDegree, MonomialOrder.degree_mul hf hg]

Premises used: MvPolynomial.degree_degLexDegree, MonomialOrder.degree_mul
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f g : MvPolynomial σ R
h : f ∣ g
hg : g ≠ 0
obtain : ∀ (r : MvPolynomial σ R) (hg : f * r ≠ 0), f.totalDegree ≤ (f * r).totalDegree
⊢ f.totalDegree ≤ g.totalDegree

Tactic:
obtain ⟨r, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ f ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ r ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
rw : f.totalDegree ≤ f.totalDegree + r.totalDegree
⊢ f.totalDegree ≤ (f * r).totalDegree

Tactic:
rw [totalDegree_mul_of_isDomain (by aesop) (by aesop)]

Premises used: MvPolynomial.totalDegree_mul_of_isDomain
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f r : MvPolynomial σ R
hg : f * r ≠ 0
⊢ f.totalDegree ≤ f.totalDegree + r.totalDegree

Tactic:
lia
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
mp : f ∣ (C : (a : R) → MvPolynomial σ R) a → ∃ (b : R), b ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) b
mpr : (∃ (b : R), b ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) b) → f ∣ (C : (a : R) → MvPolynomial σ R) a
⊢ f ∣ (C : (a : R) → MvPolynomial σ R) a ↔ ∃ (b : R), b ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) b

Tactic:
constructor
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
h : coeff 0 f ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
⊢ ∃ (b : R), b ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) b

Tactic:
use coeff 0 f

Premises used: MvPolynomial.coeff, OfNat.ofNat
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
this : f.totalDegree = 0
⊢ f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)

Tactic:
rw [totalDegree_eq_zero_iff_eq_C] at this

Premises used: MvPolynomial.totalDegree_eq_zero_iff_eq_C
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
this : f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
⊢ coeff 0 f ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)

Tactic:
⟨?_, this⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
this : f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
refine : coeff 0 f ∣ a
⊢ coeff 0 f ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)

Tactic:
refine ⟨?_, this⟩
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
this : f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
⊢ ∀ (i : σ →₀ ℕ), coeff 0 f ∣ coeff i ((C : (a : R) → MvPolynomial σ R) a)

Tactic:
rw [this, C_dvd_iff_dvd_coeff] at hf

Premises used: MvPolynomial.C_dvd_iff_dvd_coeff
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
this : f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
hf₁ : ∀ (i : σ →₀ ℕ), coeff 0 f ∣ coeff i ((C : (a : R) → MvPolynomial σ R) a)
⊢ f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)

Tactic:
rw [this, C_dvd_iff_dvd_coeff] at hf

Premises used: MvPolynomial.C_dvd_iff_dvd_coeff
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : ∀ (i : σ →₀ ℕ), coeff 0 f ∣ coeff i ((C : (a : R) → MvPolynomial σ R) a)
this : f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)
⊢ coeff 0 f ∣ a

Tactic:
simpa using hf 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
h : f.totalDegree = 0
⊢ coeff 0 f ∣ a ∧ f = (C : (a : R) → MvPolynomial σ R) (coeff 0 f)

Tactic:
suffices f.totalDegree = 0 by
      rw [totalDegree_eq_zero_iff_eq_C] at this
      refine ⟨?_, this⟩
      rw [this, C_dvd_iff_dvd_coeff] at hf
      simpa using hf 0
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
h : f.totalDegree ≤ 0
⊢ f.totalDegree = 0

Tactic:
apply Nat.eq_zero_of_le_zero

Premises used: Nat.eq_zero_of_le_zero
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
⊢ Ne (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) (0 : MvPolynomial σ R)

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ (C : (a : R) → MvPolynomial σ R) a
⊢ f.totalDegree ≤ 0

Tactic:
simpa using totalDegree_le_of_dvd_of_isDomain hf (by simp [ha])

Premises used: MvPolynomial.totalDegree_le_of_dvd_of_isDomain
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
a : R
ha : a ≠ 0
b : R
hab : b ∣ a
⊢ Dvd.dvd (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)

Tactic:
map_dvd C hab

Premises used: map_dvd, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : NoZeroDivisors R
a : R
ha : a ≠ 0
b : R
hab : b ∣ a
⊢ Dvd.dvd (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)

Tactic:
exact map_dvd C hab

Premises used: map_dvd, MvPolynomial.C
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
pos :
  ∀ (hp : p = 0),
    degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
      degreeOf j p
neg :
  ∀ (hp : ¬p = 0),
    degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
      degreeOf j p
⊢ degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    degreeOf j p

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : p = 0
⊢ degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    degreeOf j p

Tactic:
simp [hp]
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : ¬p = 0
neg :
  (HMul.hMul (α := Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)) (β :=
        Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))
        ((optionEquivLeft R { b : σ // b ≠ j } :
              (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
            ((renameEquiv R (optionSubtypeNe j).symm :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
              ((C : (a : R) → MvPolynomial σ R) c)) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))
        ((optionEquivLeft R { b : σ // b ≠ j } :
              (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
            ((renameEquiv R (optionSubtypeNe j).symm :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
              p) :
          Polynomial (MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R))).natDegree =
    Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((renameEquiv R (optionSubtypeNe j).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p))
⊢ degreeOf j (HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R) p) =
    degreeOf j p

Tactic:
simp_rw [degreeOf_eq_natDegree, map_mul, ← renameEquiv_apply]

Premises used: MvPolynomial.renameEquiv_apply, map_mul, MvPolynomial.degreeOf_eq_natDegree
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : ¬p = 0
⊢ Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            ((C : (a : R) → MvPolynomial σ R) c))) +
      Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            p)) =
    Polynomial.natDegree (R := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((renameEquiv R (optionSubtypeNe j).symm : (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : ¬p = 0
h :
  Eq (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p)))
    0
⊢ Eq (α := MvPolynomial.{u_2, u_1} (Option { b : σ // ¬b = j }) R)
    ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // ¬b = j }) :
          (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // ¬b = j }) R)
        p :
      MvPolynomial.{u_2, u_1} (Option { b : σ // ¬b = j }) R)
    ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // ¬b = j }) :
          (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // ¬b = j }) R)
        0 :
      MvPolynomial.{u_2, u_1} (Option { b : σ // ¬b = j }) R)

Tactic:
simpa using h
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : ¬p = 0
h :
  Eq (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p)))
    0
⊢ False

Tactic:
exact hp (rename_injective _ (Equiv.injective _) (by simpa using h))

Premises used: MvPolynomial.rename_injective, Equiv.injective
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : ¬p = 0
⊢ Ne (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p)))
    0

Tactic:
have hp' : (optionEquivLeft R _ ((rename (optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0 := by
      intro h
      exact hp (rename_injective _ (Equiv.injective _) (by simpa using h))
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : ¬p = 0
hp' :
  Ne (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p)))
    0
neg :
  ¬HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) (β := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
        ((C : (a : R) → MvPolynomial { b : σ // ¬b = j } R) c : MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
        (Polynomial.leadingCoeff
            ((optionEquivLeft R { b : σ // ¬b = j } :
                (a : MvPolynomial (Option { b : σ // ¬b = j }) R) → Polynomial (MvPolynomial { b : σ // ¬b = j } R))
              ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // ¬b = j }) :
                  (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // ¬b = j }) R)
                p)) :
          MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) =
      0
⊢ HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
      (Polynomial.leadingCoeff
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            ((C : (a : R) → MvPolynomial σ R) c))))
      (Polynomial.leadingCoeff
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((renameEquiv R (optionSubtypeNe j).symm :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            p))) ≠
    0

Tactic:
simp_rw [ne_eq, renameEquiv_apply, algHom_C, algebraMap_eq, optionEquivLeft_C,
      Polynomial.leadingCoeff_C]

Premises used: MvPolynomial.optionEquivLeft_C, MvPolynomial.renameEquiv_apply, ne_eq, MvPolynomial.algHom_C, MvPolynomial.algebraMap_eq, Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : ¬p = 0
hp' :
  Ne (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p)))
    0
neg :
  ∀
    (hp' :
      HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) (β :=
          MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
          ((C : (a : R) → MvPolynomial { b : σ // ¬b = j } R) c : MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
          (Polynomial.leadingCoeff
              ((optionEquivLeft R { b : σ // ¬b = j } :
                  (a : MvPolynomial (Option { b : σ // ¬b = j }) R) → Polynomial (MvPolynomial { b : σ // ¬b = j } R))
                ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // ¬b = j }) :
                    (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // ¬b = j }) R)
                  p)) :
            MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) =
        0),
    Eq (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
      (Polynomial.leadingCoeff
        ((optionEquivLeft R { b : σ // b ≠ j } :
            (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
          ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
              (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
            p)))
      0
⊢ ¬HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) (β := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
        ((C : (a : R) → MvPolynomial { b : σ // ¬b = j } R) c : MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
        (Polynomial.leadingCoeff
            ((optionEquivLeft R { b : σ // ¬b = j } :
                (a : MvPolynomial (Option { b : σ // ¬b = j }) R) → Polynomial (MvPolynomial { b : σ // ¬b = j } R))
              ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // ¬b = j }) :
                  (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // ¬b = j }) R)
                p)) :
          MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) =
      0

Tactic:
contrapose hp'
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : Membership.mem (γ := Submonoid R) R⁰ c
hp : ¬p = 0
hp' :
  HMul.hMul (α := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) (β := MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
      ((C : (a : R) → MvPolynomial { b : σ // ¬b = j } R) c : MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R)
      (Polynomial.leadingCoeff
          ((optionEquivLeft R { b : σ // ¬b = j } :
              (a : MvPolynomial (Option { b : σ // ¬b = j }) R) → Polynomial (MvPolynomial { b : σ // ¬b = j } R))
            ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // ¬b = j }) :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // ¬b = j }) R)
              p)) :
        MvPolynomial.{u_2, u_1} { b : σ // ¬b = j } R) =
    0
neg :
  ∀ (m : { b : σ // b ≠ j } →₀ ℕ),
    Eq.{u_1 + 1} (α := R)
      (coeff m
        (Polynomial.leadingCoeff
          ((optionEquivLeft R { b : σ // b ≠ j } :
              (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
            ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
                (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
              p))))
      (coeff m 0)
⊢ Eq (α := MvPolynomial.{u_2, u_1} { b : σ // b ≠ j } R)
    (Polynomial.leadingCoeff
      ((optionEquivLeft R { b : σ // b ≠ j } :
          (a : MvPolynomial (Option { b : σ // b ≠ j }) R) → Polynomial (MvPolynomial { b : σ // b ≠ j } R))
        ((rename (⇑(optionSubtypeNe j).symm : (a : σ) → Option { b : σ // b ≠ j }) :
            (a : MvPolynomial σ R) → MvPolynomial (Option { b : σ // b ≠ j }) R)
          p)))
    0

Tactic:
ext m