awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : X i ∣ p
⊢ p.divMonomial (Finsupp.single i 1) ∣ q
have hip₁ : p.modMonomial (Finsupp.single i 1) = 0
Tactic: rw [X_dvd_iff_modMonomial_eq_zero] at hip
Cleared hypotheses: hip
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : p.modMonomial (Finsupp.single i 1) = 0
⊢ p.divMonomial (Finsupp.single i 1) ∣ q
have hp₁ : q = p.divMonomial (Finsupp.single i 1) * r
Tactic: rw [← p.modMonomial_add_divMonomial_single i, hip,
        zero_add, mul_assoc, X_mul_cancel_left_iff] at hp
Cleared hypotheses: hp, this, hip
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
this : p = X i * p.divMonomial (Finsupp.single i 1)
⊢ p ∣ X i * q
have rw : X i * p.divMonomial (Finsupp.single i 1) ∣ X i * q
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
⊢ p ∣ X i * q
have mpr : p = X i * p.divMonomial (Finsupp.single i 1)
Tactic: suffices p = X i * p.divMonomial (Finsupp.single i 1) by
        rw [this]
        exact mul_dvd_mul_left (X i) hq
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
| p
have rw : p.modMonomial (Finsupp.single i 1) +
  (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1 * p.divMonomial (Finsupp.single i 1)
Tactic: rw [← p.modMonomial_add_divMonomial (Finsupp.single i 1)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
⊢ p = X i * p.divMonomial (Finsupp.single i 1)
have mpr : p.modMonomial (Finsupp.single i 1) +
    (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1 * p.divMonomial (Finsupp.single i 1) =
  X i * p.divMonomial (Finsupp.single i 1)
Tactic: conv_lhs => rw [← p.modMonomial_add_divMonomial (Finsupp.single i 1)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
⊢ 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
have inl : ∀ (hR : Subsingleton 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
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
inl :
  ∀ (hR : Subsingleton 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
⊢ 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
have inr : ∀ (hR : Nontrivial 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
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
hR : Subsingleton 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
have inl : ∃ (m : σ →₀ ℕ), m ≤ n
Tactic: simp only [Subsingleton.elim _ p, dvd_refl, and_self, and_true, exists_const, true_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial 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
have inr : ∀ (d : ℕ) (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
Tactic: suffices ∀ (d) (n : σ →₀ ℕ) (hd : n.degree = d) (p q : MvPolynomial σ R),
    p ∣ monomial n 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = monomial m 1 * r from this n.degree n rfl p q
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
n : σ →₀ ℕ
hn : Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n : ℕ) (0 : ℕ)
p : MvPolynomial σ R
⊢ ∀ (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
have inr : ∀ (hn : n = 0) (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
Tactic: rw [Finsupp.degree_eq_zero_iff] at hn
Cleared hypotheses: hn, p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun hp ↦ ?_, fun ⟨m, r, hmn, hrq, hp⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
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
⊢ 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
have inr₁ : (∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) →
  ∀ (m : σ →₀ ℕ) (r : MvPolynomial σ R) (hmn : m ≤ n) (hrq : r ∣ q)
    (hp : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r), p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
Tactic: refine ⟨fun hp ↦ ?_, fun ⟨m, r, hmn, hrq, hp⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ n.support.Nonempty
have rw : n ≠ 0
Tactic: rw [Finsupp.support_nonempty_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have inr : ∀ (i : σ) (hi : i ∈ n.support),
  ∃ (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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
have h : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: apply Finsupp.sub_add_single_one_cancel
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have hn' : 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have hnn' : n' ≤ n
Tactic: have hnn' : n' ≤ n := by simp [← hn']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
have rw : HAdd.hAdd (α := ℕ) (β := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' : ℕ) (1 : ℕ) =
  (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) (n' + Finsupp.single i 1)
Tactic: rw [← add_left_inj, ← hn, ← hn']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
Tactic: have hd' : n'.degree = d := by
        rw [← add_left_inj, ← hn, ← hn']
        simp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have 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
Tactic: rw [← hn', monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, dvd_X_mul_iff] at hp
Cleared hypotheses: hp, hn', hnn', hd'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have 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
Tactic: rcases hp with hp | hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have 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
Tactic: rcases hp with hp | hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have 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
Tactic: obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' p q).mp hp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have 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
Tactic: obtain ⟨p', rfl⟩ := hp.1
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ X i * p' = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have 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
Tactic: obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' _ _).mp hp.2
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ X i * p' = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have right : X i * p' = (monomial (m + Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1 * r
Tactic: use m + Finsupp.single i 1, r, ?_, hr