awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
m : { b : σ // b ≠ j } →₀ ℕ
neg :
  c *
      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))) =
    0
⊢ 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)

Tactic:
apply hc.1

Premises used: And.left
-- 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
m : { b : σ // b ≠ j } →₀ ℕ
⊢ c *
      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))) =
    0

Tactic:
simpa using congr_arg (coeff m) hp'

Premises used: MvPolynomial.coeff, congr_arg
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
rw :
  (monomial n : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
      ((monomial n : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R) ((monomial n : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial n : (a : R) → MvPolynomial σ R) (a * 1) : MvPolynomial σ R)
rw₂ rw₃ :
  Eq (α := MvPolynomial σ R) ((monomial n : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
    ((monomial n : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)
⊢ (monomial n : (a : R) → MvPolynomial σ R) a =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial n : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R)

Tactic:
rw [mul_comm, C_mul_monomial, mul_one]

Premises used: MvPolynomial.C_mul_monomial, mul_comm, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
rw :
  (∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R),
      m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) ↔
    ∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) a ↔
    ∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b

Tactic:
rw [show monomial n a = monomial n 1 * C a by rw [mul_comm, C_mul_monomial, mul_one],
    dvd_monomial_mul_iff_exists]

Premises used: MvPolynomial.dvd_monomial_mul_iff_exists
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
h :
  ∀ (a_1 : σ →₀ ℕ),
    (∃ (r : MvPolynomial σ R),
        a_1 ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial a_1 : (a : R) → MvPolynomial σ R) 1 * r) ↔
      ∃ (b : R), a_1 ≤ n ∧ b ∣ a ∧ p = (monomial a_1 : (a : R) → MvPolynomial σ R) b
⊢ (∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R),
      m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) ↔
    ∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
h :
  (∃ (r : MvPolynomial σ R),
      m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) →
    ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
h₁ :
  (∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b) →
    ∃ (r : MvPolynomial σ R),
      m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ (∃ (r : MvPolynomial σ R),
      m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) ↔
    ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b

Tactic:
constructor
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hr : r ∣ (C : (a : R) → MvPolynomial σ R) a
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∃ (b : R), b ∣ a ∧ r = (C : (a : R) → MvPolynomial σ R) b

Tactic:
rw [dvd_C_iff_exists ha] at hr

Premises used: MvPolynomial.dvd_C_iff_exists
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hr : r ∣ (C : (a : R) → MvPolynomial σ R) a
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
hr₁ : ∃ (b : R), b ∣ a ∧ r = (C : (a : R) → MvPolynomial σ R) b
⊢ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
rw [dvd_C_iff_exists ha] at hr

Premises used: MvPolynomial.dvd_C_iff_exists
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hr : ∃ (b : R), b ∣ a ∧ r = (C : (a : R) → MvPolynomial σ R) b
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
h₁ :
  ∀ (b : R) (hb : b ∣ a) (hr : r = (C : (a : R) → MvPolynomial σ R) b),
    ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b
⊢ ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b

Tactic:
obtain ⟨b, hb, hr⟩ := hr
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
b : R
hb : b ∣ a
hr : r = (C : (a : R) → MvPolynomial σ R) b
right : p = (monomial m : (a : R) → MvPolynomial σ R) b
⊢ ∃ (b : R), m ≤ n ∧ b ∣ a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b

Tactic:
use b, hmn, hb
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
h : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
b : R
hb : b ∣ a
hr : r = (C : (a : R) → MvPolynomial σ R) b
right : (monomial m : (a : R) → MvPolynomial σ R) 1 * r = (monomial m : (a : R) → MvPolynomial σ R) b
right₁ : r * (monomial m : (a : R) → MvPolynomial σ R) 1 = (monomial m : (a : R) → MvPolynomial σ R) b
right₂ :
  HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R) =
    (monomial m : (a : R) → MvPolynomial σ R) b
right₃ :
  Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) (b * 1) : MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
right₄ right₅ :
  Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
    ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
⊢ p = (monomial m : (a : R) → MvPolynomial σ R) b

Tactic:
rw [h, mul_comm, hr, C_mul_monomial, mul_one]

Premises used: MvPolynomial.C_mul_monomial, mul_comm, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
b : R
hmn : m ≤ n
hb : b ∣ a
h : p = (monomial m : (a : R) → MvPolynomial σ R) b
right :
  p =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
⊢ ∃ (r : MvPolynomial σ R),
    m ≤ n ∧ r ∣ (C : (a : R) → MvPolynomial σ R) a ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
use C b, hmn, map_dvd C hb

Premises used: map_dvd, MvPolynomial.C, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
b : R
hmn : m ≤ n
hb : b ∣ a
h : p = (monomial m : (a : R) → MvPolynomial σ R) b
right :
  p =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
right₁ : p = (monomial m : (a : R) → MvPolynomial σ R) (b * 1)
right₂ right₃ right₄ right₅ : p = (monomial m : (a : R) → MvPolynomial σ R) b
⊢ p =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial m : (a : R) → MvPolynomial σ R) 1 : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)

Tactic:
rwa [mul_comm, C_mul_monomial, mul_one]

Premises used: MvPolynomial.C_mul_monomial, mul_comm, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
inl :
  ∀ (hR : Subsingleton R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
      ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
inr :
  ∀ (hR : Nontrivial R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
      ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Subsingleton R
this : ∃ (m : σ →₀ ℕ), m ≤ n
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u

Tactic:
simpa [Subsingleton.elim _ p]

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Subsingleton R
inl : ∃ (m : σ →₀ ℕ), m ≤ n
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u

Tactic:
suffices ∃ m, m ≤ n by simpa [Subsingleton.elim _ p]
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Subsingleton R
w : σ →₀ ℕ
h : n ≤ n
⊢ ∃ (m : σ →₀ ℕ), m ≤ n

Tactic:
use n
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Nontrivial R
inr :
  (∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ 1 ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b) ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u

Tactic:
rw [dvd_monomial_iff_exists (one_ne_zero' R)]

Premises used: one_ne_zero', MvPolynomial.dvd_monomial_iff_exists
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Nontrivial R
inr :
  ∀ (a : σ →₀ ℕ),
    (∃ (b : R), a ≤ n ∧ b ∣ 1 ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) ↔
      ∃ (u : R), a ≤ n ∧ IsUnit u ∧ p = (monomial a : (a : R) → MvPolynomial σ R) u
⊢ (∃ (m : σ →₀ ℕ) (b : R), m ≤ n ∧ b ∣ 1 ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b) ↔
    ∃ (m : σ →₀ ℕ) (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Nontrivial R
m : σ →₀ ℕ
⊢ (∃ (b : R), m ≤ n ∧ b ∣ 1 ∧ p = (monomial m : (a : R) → MvPolynomial σ R) b) ↔
    ∃ (u : R), m ≤ n ∧ IsUnit u ∧ p = (monomial m : (a : R) → MvPolynomial σ R) u

Tactic:
simp_rw [isUnit_iff_dvd_one]

Premises used: isUnit_iff_dvd_one
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
rw :
  (∃ (b : R), ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) ↔
    ∃ (s : R),
      s ∣ r ∧
        (p = (C : (a : R) → MvPolynomial σ R) s ∨
          p = HSMul.hSMul (β := MvPolynomial σ R) s ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
⊢ p ∣ HSMul.hSMul (β := MvPolynomial σ R) r (X i) ↔
    ∃ (s : R), s ∣ r ∧ (p = (C : (a : R) → MvPolynomial σ R) s ∨ p = HSMul.hSMul (β := MvPolynomial σ R) s (X i))

Tactic:
rw [X, smul_monomial, smul_eq_mul, mul_one, dvd_monomial_iff_exists hr, exists_comm]

Premises used: MvPolynomial.smul_monomial, MvPolynomial.X, MvPolynomial.dvd_monomial_iff_exists, exists_comm, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
h :
  ∀ (a : R),
    (∃ a_1 ≤ Finsupp.single i 1, a ∣ r ∧ p = (monomial a_1 : (a : R) → MvPolynomial σ R) a) ↔
      a ∣ r ∧
        (p = (C : (a : R) → MvPolynomial σ R) a ∨
          p = HSMul.hSMul (β := MvPolynomial σ R) a ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
⊢ (∃ (b : R), ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) ↔
    ∃ (s : R),
      s ∣ r ∧
        (p = (C : (a : R) → MvPolynomial σ R) s ∨
          p = HSMul.hSMul (β := MvPolynomial σ R) s ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
h :
  (∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) →
    b ∣ r ∧
      (p = (C : (a : R) → MvPolynomial σ R) b ∨
        p = HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))
h₁ :
  b ∣ r ∧
      (p = (C : (a : R) → MvPolynomial σ R) b ∨
        p = HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)) →
    ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b
⊢ (∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a : (a : R) → MvPolynomial σ R) b) ↔
    b ∣ r ∧
      (p = (C : (a : R) → MvPolynomial σ R) b ∨
        p = HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))

Tactic:
constructor
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
h :
  Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) ∨
    (monomial m : (a : R) → MvPolynomial σ R) b =
      HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
⊢ b ∣ r ∧
    (Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) ∨
      (monomial m : (a : R) → MvPolynomial σ R) b =
        HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1))

Tactic:
simp only [hb, true_and]

Premises used: true_and
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
this : m = 0 ∨ m = Finsupp.single i 1
f :
  m = 0 →
    Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
g :
  m = Finsupp.single i 1 →
    (monomial m : (a : R) → MvPolynomial σ R) b =
      HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)
⊢ Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) ∨
    (monomial m : (a : R) → MvPolynomial σ R) b =
      HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)

Tactic:
apply this.imp

Premises used: Or.imp
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
this : m = 0 ∨ m = Finsupp.single i 1
⊢ m = 0 →
    Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)

Tactic:
simp +contextual [smul_monomial, smul_eq_mul, mul_one]

Premises used: MvPolynomial.smul_monomial, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
this : m = 0 ∨ m = Finsupp.single i 1
⊢ m = Finsupp.single i 1 →
    (monomial m : (a : R) → MvPolynomial σ R) b =
      HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)

Tactic:
simp +contextual [smul_monomial, smul_eq_mul, mul_one]

Premises used: MvPolynomial.smul_monomial, smul_eq_mul, mul_one
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
h : m = 0 ∨ m = Finsupp.single i 1
⊢ Eq (α := MvPolynomial σ R) ((monomial m : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R)
      ((C : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) ∨
    (monomial m : (a : R) → MvPolynomial σ R) b =
      HSMul.hSMul (β := MvPolynomial σ R) b ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1)

Tactic:
suffices m = 0 ∨ m = Finsupp.single i 1 by
      apply this.imp <;> simp +contextual [smul_monomial, smul_eq_mul, mul_one]
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
pos : ∀ (hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), m = 0 ∨ m = Finsupp.single i 1
neg : ∀ (hm : ¬Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), m = 0 ∨ m = Finsupp.single i 1
⊢ m = 0 ∨ m = Finsupp.single i 1

Tactic:
by_cases hm : m i = 0

Premises used: DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
pos : m = 0
⊢ m = 0 ∨ m = Finsupp.single i 1

Tactic:
left
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
pos : ∀ (j : σ), Eq (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) ((0 : (a : σ) → ℕ) j : ℕ)
⊢ m = 0

Tactic:
ext j
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
pos : LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) ((0 : (a : σ) → ℕ) j : ℕ)

Tactic:
simp only [Finsupp.coe_zero, Pi.zero_apply, ← Nat.le_zero]

Premises used: Nat.le_zero, Pi.zero_apply, Finsupp.coe_zero
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
pos : ∀ (hj : j = i), LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
neg : ∀ (hj : ¬j = i), LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)
⊢ LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)

Tactic:
by_cases hj : j = i
-- Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors
Goal:
R : Type u_1
σ : Type u_2
inst : CommRing R
inst_1 : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : Eq (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
j : σ
hj : j = i
pos : LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) ((m : (a : σ) → ℕ) i : ℕ)
pos₁ pos₂ : LE.le (α := ℕ) ((m : (a : σ) → ℕ) i : ℕ) ((m : (a : σ) → ℕ) i : ℕ)
⊢ LE.le (α := ℕ) ((m : (a : σ) → ℕ) j : ℕ) (0 : ℕ)

Tactic:
rw [← hm, hj]