awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
inr :
  ∀ (i : σ) (hi : i ∈ n.support),
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
obtain ⟨i, hi⟩ : n.support.Nonempty := by
        rw [Finsupp.support_nonempty_iff]
        intro hn'
        simp [hn'] at hn

Premises used: Finsupp.support, Finset.Nonempty
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
h : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ n' + Finsupp.single i 1 = n

Tactic:
apply Finsupp.sub_add_single_one_cancel

Premises used: Finsupp.sub_add_single_one_cancel
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
h h₁ h₂ h₃ : i ∈ n.support
⊢ Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
rwa [← Finsupp.mem_support_iff]

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
⊢ n' + Finsupp.single i 1 = n

Tactic:
have hn' : n' + Finsupp.single i 1 = n := by
        apply Finsupp.sub_add_single_one_cancel
        rwa [← Finsupp.mem_support_iff]
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
⊢ n' ≤ n

Tactic:
simp [← hn']
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
⊢ n' ≤ n

Tactic:
have hnn' : n' ≤ n := by simp [← hn']
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
rw :
  HAdd.hAdd (α := ℕ) (β := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' : ℕ) (1 : ℕ) =
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (n' + Finsupp.single i 1)
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d

Tactic:
rw [← add_left_inj, ← hn, ← hn']

Premises used: add_left_inj
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
⊢ HAdd.hAdd (α := ℕ) (β := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' : ℕ) (1 : ℕ) =
    (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (n' + Finsupp.single i 1)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d

Tactic:
have hd' : n'.degree = d := by
        rw [← add_left_inj, ← hn, ← hn']
        simp
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
⊢ p ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q ∨
    X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q

Tactic:
rw [← hn', monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, dvd_X_mul_iff] at hp

Premises used: mul_assoc, MvPolynomial.X, MvPolynomial.dvd_X_mul_iff, MvPolynomial.monomial_add_single, pow_one, mul_comm
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
hp₁ :
  p ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q ∨
    X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
⊢ n' + Finsupp.single i 1 = n

Tactic:
rw [← hn', monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, dvd_X_mul_iff] at hp

Premises used: mul_assoc, MvPolynomial.X, MvPolynomial.dvd_X_mul_iff, MvPolynomial.monomial_add_single, pow_one, mul_comm
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
hp₁ :
  p ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q ∨
    X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
hn'₁ : n' + Finsupp.single i 1 = n
⊢ n' ≤ n

Tactic:
rw [← hn', monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, dvd_X_mul_iff] at hp

Premises used: mul_assoc, MvPolynomial.X, MvPolynomial.dvd_X_mul_iff, MvPolynomial.monomial_add_single, pow_one, mul_comm
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
hp₁ :
  p ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q ∨
    X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
hn'₁ : n' + Finsupp.single i 1 = n
hnn'₁ : n' ≤ n
⊢ (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d

Tactic:
rw [← hn', monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, dvd_X_mul_iff] at hp

Premises used: mul_assoc, MvPolynomial.X, MvPolynomial.dvd_X_mul_iff, MvPolynomial.monomial_add_single, pow_one, mul_comm
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hp :
  p ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q ∨
    X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
inr :
  ∀ (hp : p ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q),
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
inr₁ :
  ∀ (hp : X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q),
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
rcases hp with hp | hp
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
hp : p ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
inr :
  ∀ (m : σ →₀ ℕ) (r : MvPolynomial σ R) (hm : m ≤ n') (hr : r ∣ q)
    (hp : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r),
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' p q).mp hp

Premises used: Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
hp_1 : p ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
m : σ →₀ ℕ
r : MvPolynomial σ R
hm : m ≤ n'
hr : r ∣ q
hp : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
⟨m, r, le_trans hm hnn', hr, hp⟩

Premises used: And.intro, Exists.intro, le_trans
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
hp_1 : p ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
m : σ →₀ ℕ
r : MvPolynomial σ R
hm : m ≤ n'
hr : r ∣ q
hp : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
exact ⟨m, r, le_trans hm hnn', hr, hp⟩
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
hp : X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
inr :
  ∀ (p' : MvPolynomial σ R)
    (hp :
      X i ∣ X i * p' ∧ (X i * p').divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q),
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ X i * p' = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
obtain ⟨p', rfl⟩ := hp.1

Premises used: And.left, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
p' : MvPolynomial σ R
hp : X i ∣ X i * p' ∧ (X i * p').divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
inr :
  ∀ (m : σ →₀ ℕ) (r : MvPolynomial σ R) (hm : m ≤ n') (hr : r ∣ q)
    (hp : (X i * p').divMonomial (Finsupp.single i 1) = (monomial m : (a : R) → MvPolynomial σ R) 1 * r),
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ X i * p' = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ X i * p' = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' _ _).mp hp.2

Premises used: And.right, Iff.mp
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
p' : MvPolynomial σ R
hp_1 : X i ∣ X i * p' ∧ (X i * p').divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
m : σ →₀ ℕ
r : MvPolynomial σ R
hm : m ≤ n'
hr : r ∣ q
hp : (X i * p').divMonomial (Finsupp.single i 1) = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
right : X i * p' = (monomial (m + Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1 * r
left : m + Finsupp.single i 1 ≤ n
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ X i * p' = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
use m + Finsupp.single i 1, r, ?_, hr

Premises used: OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
p' : MvPolynomial σ R
hp_1 : X i ∣ X i * p' ∧ (X i * p').divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
m : σ →₀ ℕ
r : MvPolynomial σ R
hm : m ≤ n'
hr : r ∣ q
hp : (X i * p').divMonomial (Finsupp.single i 1) = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ X i * p' = (monomial (m + Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
simp [monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, ← hp]

Premises used: mul_assoc, MvPolynomial.X, MvPolynomial.monomial_add_single, pow_one, mul_comm
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
p' : MvPolynomial σ R
hp_1 : X i ∣ X i * p' ∧ (X i * p').divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
m : σ →₀ ℕ
r : MvPolynomial σ R
hm : m ≤ n'
hr : r ∣ q
hp : (X i * p').divMonomial (Finsupp.single i 1) = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ m + Finsupp.single i 1 ≤ n

Tactic:
simpa [← hn'] using hm