awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
x : MvPolynomial σ R
⊢ (monomial s : (a : R) → MvPolynomial σ R) 1 * x %ᵐᵒⁿᵒᵐⁱᵃˡ s = 0

Tactic:
x.of'_mul_modOf _

Premises used: MvPolynomial.modMonomial, AddMonoidAlgebra.of'_mul_modOf, AddMonoidAlgebra.of', Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
x : MvPolynomial σ R
⊢ x * (monomial s : (a : R) → MvPolynomial σ R) 1 %ᵐᵒⁿᵒᵐⁱᵃˡ s = 0

Tactic:
x.mul_of'_modOf _

Premises used: MvPolynomial.modMonomial, AddMonoidAlgebra.mul_of'_modOf, AddMonoidAlgebra.of', Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
s : σ →₀ ℕ
⊢ Eq (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1 %ᵐᵒⁿᵒᵐⁱᵃˡ s) 0

Tactic:
AddMonoidAlgebra.of'_modOf _

Premises used: MvPolynomial.modMonomial, AddMonoidAlgebra.of', AddMonoidAlgebra.of'_modOf, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : σ →₀ ℕ
⊢ (monomial s : (a : R) → MvPolynomial σ R) 1 * (x /ᵐᵒⁿᵒᵐⁱᵃˡ s) + x %ᵐᵒⁿᵒᵐⁱᵃˡ s = x

Tactic:
AddMonoidAlgebra.divOf_add_modOf x s

Premises used: MvPolynomial.modMonomial, MvPolynomial.divMonomial, AddMonoidAlgebra.divOf_add_modOf, AddMonoidAlgebra.of', Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
s : σ →₀ ℕ
⊢ x %ᵐᵒⁿᵒᵐⁱᵃˡ s + (monomial s : (a : R) → MvPolynomial σ R) 1 * (x /ᵐᵒⁿᵒᵐⁱᵃˡ s) = x

Tactic:
AddMonoidAlgebra.modOf_add_divOf x s

Premises used: MvPolynomial.modMonomial, MvPolynomial.divMonomial, AddMonoidAlgebra.modOf_add_divOf, AddMonoidAlgebra.of', Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ →₀ ℕ
x : MvPolynomial σ R
⊢ (monomial i : (a : R) → MvPolynomial σ R) 1 ∣ x ↔ x %ᵐᵒⁿᵒᵐⁱᵃˡ i = 0

Tactic:
AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero

Premises used: MvPolynomial.modMonomial, AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero, AddMonoidAlgebra.of', Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
x : MvPolynomial σ R
⊢ X i * x /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = x

Tactic:
divMonomial_monomial_mul _ _

Premises used: MvPolynomial.X, MvPolynomial.divMonomial_monomial_mul
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
⊢ Eq (α := MvPolynomial σ R) (X i /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1) 1

Tactic:
divMonomial_monomial (Finsupp.single i 1)

Premises used: MvPolynomial.X, MvPolynomial.divMonomial_monomial, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
i : σ
⊢ x * X i /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = x

Tactic:
divMonomial_mul_monomial _ _

Premises used: MvPolynomial.X, MvPolynomial.divMonomial_mul_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
x : MvPolynomial σ R
⊢ X i * x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0

Tactic:
monomial_mul_modMonomial _ _

Premises used: MvPolynomial.X, MvPolynomial.monomial_mul_modMonomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
i : σ
⊢ x * X i %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0

Tactic:
mul_monomial_modMonomial _ _

Premises used: MvPolynomial.X, MvPolynomial.mul_monomial_modMonomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
⊢ Eq (α := MvPolynomial σ R) (X i %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1) 0

Tactic:
monomial_modMonomial _

Premises used: MvPolynomial.X, MvPolynomial.monomial_modMonomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
i : σ
⊢ X i * (x /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1) + x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = x

Tactic:
divMonomial_add_modMonomial _ _

Premises used: MvPolynomial.divMonomial_add_modMonomial, MvPolynomial.X
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
x : MvPolynomial σ R
i : σ
⊢ x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 + X i * (x /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1) = x

Tactic:
modMonomial_add_divMonomial _ _

Premises used: MvPolynomial.X, MvPolynomial.modMonomial_add_divMonomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
x : MvPolynomial σ R
⊢ X i ∣ x ↔ x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 = 0

Tactic:
monomial_one_dvd_iff_modMonomial_eq_zero

Premises used: MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero, MvPolynomial.X
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
mp :
  Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((monomial j : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) →
    (s = 0 ∨ i ≤ j) ∧ r ∣ s
mpr :
  (s = 0 ∨ i ≤ j) ∧ r ∣ s →
    Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((monomial j : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R)
⊢ Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((monomial j : (a : R) → MvPolynomial σ R) s : MvPolynomial σ R) ↔
    (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
constructor
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  (monomial j : (a : R) → MvPolynomial σ R) s =
    HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x
⊢ ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)

Tactic:
rw [MvPolynomial.ext_iff] at hx

Premises used: MvPolynomial.ext_iff
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
⊢ coeff j ((monomial j : (a : R) → MvPolynomial σ R) s) =
    coeff j (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)

Tactic:
have hj := hx j
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hj :
  coeff j ((monomial j : (a : R) → MvPolynomial σ R) s) =
    coeff j (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
⊢ coeff i ((monomial j : (a : R) → MvPolynomial σ R) s) =
    coeff i (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)

Tactic:
have hi := hx i
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hj :
  coeff j ((monomial j : (a : R) → MvPolynomial σ R) s) =
    coeff j (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi :
  coeff i ((monomial j : (a : R) → MvPolynomial σ R) s) =
    coeff i (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
⊢ (if j = i then s else 0) =
    coeff i (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)

Tactic:
simp_rw [coeff_monomial, if_pos] at hj hi

Premises used: if_pos, MvPolynomial.coeff_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hj :
  coeff j ((monomial j : (a : R) → MvPolynomial σ R) s) =
    coeff j (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi :
  coeff i ((monomial j : (a : R) → MvPolynomial σ R) s) =
    coeff i (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi₁ :
  (if j = i then s else 0) =
    coeff i (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
⊢ s = coeff j (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)

Tactic:
simp_rw [coeff_monomial, if_pos] at hj hi

Premises used: if_pos, MvPolynomial.coeff_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi :
  (if j = i then s else 0) =
    coeff i (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hj : s = coeff j (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
⊢ (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0

Tactic:
simp_rw [coeff_monomial_mul'] at hi hj

Premises used: MvPolynomial.coeff_monomial_mul'
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi :
  (if j = i then s else 0) =
    coeff i (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hj : s = coeff j (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi₁ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
⊢ s = if i ≤ j then r * coeff (j - i) x else 0

Tactic:
simp_rw [coeff_monomial_mul'] at hi hj

Premises used: MvPolynomial.coeff_monomial_mul'
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hj : s = if i ≤ j then r * coeff (j - i) x else 0
pos : ∀ (hi : i ≤ j) (hj : s = r * coeff (j - i) x), (s = 0 ∨ i ≤ j) ∧ r ∣ s
neg : ∀ (hi : ¬i ≤ j) (hj : s = 0), (s = 0 ∨ i ≤ j) ∧ r ∣ s
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
split_ifs at hj with hi
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi_1 : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : i ≤ j
hj : s = r * coeff (j - i) x
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
⟨Or.inr hi, _, hj⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi_1 : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : i ≤ j
hj : s = r * coeff (j - i) x
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
exact ⟨Or.inr hi, _, hj⟩
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi_1 : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : ¬i ≤ j
hj : s = 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩

Premises used: dvd_zero, Eq.rec, And.intro, Or.inl, Eq.symm
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi_1 : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : ¬i ≤ j
hj : s = 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
exact ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx :
  ∀ (m : σ →₀ ℕ),
    coeff m ((monomial j : (a : R) → MvPolynomial σ R) s) =
      coeff m (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hj :
  coeff j ((monomial j : (a : R) → MvPolynomial σ R) s) =
    coeff j (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
hi :
  coeff i ((monomial j : (a : R) → MvPolynomial σ R) s) =
    coeff i (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)
mp mp₁ : (s = 0 ∨ i ≤ j) ∧ r ∣ s
mp₂ :
  ∀
    (hj :
      (if True then s else 0) =
        coeff j (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x))
    (hi :
      (if j = i then s else 0) =
        coeff i (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)),
    (s = 0 ∨ i ≤ j) ∧ r ∣ s
mp₃ :
  ∀
    (hi :
      (if j = i then s else 0) =
        coeff i (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x))
    (hj :
      s =
        coeff j (HMul.hMul (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) x)),
    (s = 0 ∨ i ≤ j) ∧ r ∣ s
mp₄ :
  ∀ (hi : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0)
    (hj : s = if i ≤ j then r * coeff (j - i) x else 0), (s = 0 ∨ i ≤ j) ∧ r ∣ s
pos :
  ∀ (hi : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0) (hi : i ≤ j)
    (hj : s = r * coeff (j - i) x), (s = 0 ∨ i ≤ j) ∧ r ∣ s
neg neg₁ :
  ∀ (hi : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0) (hi : ¬i ≤ j) (hj : s = 0),
    (s = 0 ∨ i ≤ j) ∧ r ∣ s
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
classical
    simp_rw [coeff_monomial, if_pos] at hj hi
    simp_rw [coeff_monomial_mul'] at hi hj
    split_ifs at hj with hi
    · exact ⟨Or.inr hi, _, hj⟩
    · exact ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩

Premises used: if_pos, MvPolynomial.coeff_monomial_mul', MvPolynomial.coeff_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r : R
i j : σ →₀ ℕ
d : R
h : r * d = 0
mpr :
  Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((monomial j : (a : R) → MvPolynomial σ R) 0 : MvPolynomial σ R)
mpr₁ :
  Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    (0 : MvPolynomial σ R)
⊢ Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((monomial j : (a : R) → MvPolynomial σ R) (r * d) : MvPolynomial σ R)

Tactic:
simp_rw [h, monomial_zero, dvd_zero]

Premises used: dvd_zero, MvPolynomial.monomial_zero
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : R
⊢ Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((monomial j : (a : R) → MvPolynomial σ R) (r * d) : MvPolynomial σ R)

Tactic:
⟨monomial (j - i) d, ?_⟩

Premises used: MvPolynomial.monomial, HSub.hSub, Exists.intro, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : R
mpr :
  (monomial j : (a : R) → MvPolynomial σ R) (r * d) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((monomial (j - i) : (a : R) → MvPolynomial σ R) d : MvPolynomial σ R)
⊢ Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((monomial j : (a : R) → MvPolynomial σ R) (r * d) : MvPolynomial σ R)

Tactic:
refine ⟨monomial (j - i) d, ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : R
mpr :
  Eq (α := MvPolynomial σ R) ((monomial j : (a : R) → MvPolynomial σ R) (r * d) : MvPolynomial σ R)
    ((monomial (i + (j - i)) : (a : R) → MvPolynomial σ R) (r * d) : MvPolynomial σ R)
mpr₁ mpr₂ :
  Eq (α := MvPolynomial σ R) ((monomial j : (a : R) → MvPolynomial σ R) (r * d) : MvPolynomial σ R)
    ((monomial j : (a : R) → MvPolynomial σ R) (r * d) : MvPolynomial σ R)
⊢ (monomial j : (a : R) → MvPolynomial σ R) (r * d) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      ((monomial (j - i) : (a : R) → MvPolynomial σ R) d : MvPolynomial σ R)

Tactic:
rw [monomial_mul, add_tsub_cancel_of_le hij]

Premises used: MvPolynomial.monomial_mul, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
i j : σ →₀ ℕ
rw : (Eq.{u_2 + 1} (α := R) 1 0 ∨ i ≤ j) ∧ Dvd.dvd.{u_2} (α := R) 1 1 ↔ i ≤ j
⊢ Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) 1)
      ((monomial j : (a : R) → MvPolynomial σ R) 1) ↔
    i ≤ j

Tactic:
rw [monomial_dvd_monomial]

Premises used: MvPolynomial.monomial_dvd_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
i j : σ →₀ ℕ
simp_rw : (False ∨ i ≤ j) ∧ Dvd.dvd.{u_2} (α := R) 1 1 ↔ i ≤ j
simp_rw₁ : i ≤ j ∧ Dvd.dvd.{u_2} (α := R) 1 1 ↔ i ≤ j
simp_rw₂ : i ≤ j ∧ True ↔ i ≤ j
⊢ (Eq.{u_2 + 1} (α := R) 1 0 ∨ i ≤ j) ∧ Dvd.dvd.{u_2} (α := R) 1 1 ↔ i ≤ j

Tactic:
simp_rw [one_ne_zero, false_or, dvd_rfl, and_true]

Premises used: and_true, false_or, dvd_rfl, one_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
i j : σ
⊢ Dvd.dvd (α := MvPolynomial σ R) (X i) (X j) ↔ i = j

Tactic:
monomial_one_dvd_monomial_one.trans ?_

Premises used: MvPolynomial.X, Iff.trans, MvPolynomial.monomial_one_dvd_monomial_one
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
i j : σ
refine : LE.le (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single j 1) ↔ i = j
⊢ Dvd.dvd (α := MvPolynomial σ R) (X i) (X j) ↔ i = j

Tactic:
refine monomial_one_dvd_monomial_one.trans ?_

Premises used: Iff.trans, MvPolynomial.monomial_one_dvd_monomial_one
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
i j : σ
simp_rw : LE.le (α := ℕ) (1 : ℕ) ((Finsupp.single j 1 : (a : σ) → ℕ) i : ℕ) ↔ i = j
simp_rw₁ : Ne (α := ℕ) ((Finsupp.single j 1 : (a : σ) → ℕ) i : ℕ) (0 : ℕ) ↔ i = j
simp_rw₂ : i = j ∧ Ne (α := ℕ) 1 0 ↔ i = j
simp_rw₃ : i = j ∧ ¬Eq (α := ℕ) 1 0 ↔ i = j
simp_rw₄ : i = j ∧ ¬False ↔ i = j
simp_rw₅ : i = j ∧ True ↔ i = j
⊢ LE.le (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single j 1) ↔ i = j

Tactic:
simp_rw [Finsupp.single_le_iff, Nat.one_le_iff_ne_zero, Finsupp.single_apply_ne_zero,
    ne_eq, reduceCtorEq, not_false_eq_true, and_true]

Premises used: reduceCtorEq, and_true, Finsupp.single_apply_ne_zero, ne_eq, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero, not_false_eq_true
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ Dvd.dvd (α := MvPolynomial σ R) (X i) ((monomial j : (a : R) → MvPolynomial σ R) r) ↔
    r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
monomial_dvd_monomial.trans ?_

Premises used: MvPolynomial.X, Iff.trans, MvPolynomial.monomial_dvd_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
refine : (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ Dvd.dvd (α := MvPolynomial σ R) (X i) ((monomial j : (a : R) → MvPolynomial σ R) r) ↔
    r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
refine monomial_dvd_monomial.trans ?_

Premises used: Iff.trans, MvPolynomial.monomial_dvd_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
simp_rw : (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ True ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
simp_rw₁ : r = 0 ∨ Finsupp.single i 1 ≤ j ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
simp_rw₂ :
  r = 0 ∨ LE.le (α := ℕ) (1 : ℕ) ((j : (a : σ) → ℕ) i : ℕ) ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
simp_rw [one_dvd, and_true, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]

Premises used: and_true, one_dvd, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
a : ∀ (n : σ →₀ ℕ), coeff n q = coeff n (p.divMonomial (Finsupp.single i 1))
⊢ q = p.divMonomial (Finsupp.single i 1)

Tactic:
ext n
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
n : σ →₀ ℕ
a : Finsupp.single i 1 + n ∉ r.support
⊢ coeff n q = coeff n (p.divMonomial (Finsupp.single i 1))

Tactic:
rw [coeff_divMonomial, h, coeff_add, coeff_X_mul, left_eq_add, ← notMem_support_iff]

Premises used: MvPolynomial.coeff_divMonomial, left_eq_add, MvPolynomial.notMem_support_iff, MvPolynomial.coeff_add, MvPolynomial.coeff_X_mul
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
n : σ →₀ ℕ
hn : Finsupp.single i 1 + n ∈ r.support
⊢ False

Tactic:
simpa using hr _ hn