awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have 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)
Tactic: have hj := hx j
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have 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)
Tactic: have hi := hx i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have hi₁ : (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
Cleared hypotheses: hj, hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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 = 0 ∨ i ≤ j) ∧ r ∣ s
have hj₁ : 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
Cleared hypotheses: hj, hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have hi₁ : (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
Cleared hypotheses: hi, hj
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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 = 0 ∨ i ≤ j) ∧ r ∣ s
have hj₁ : s = if i ≤ j then r * coeff (j - i) x else 0
Tactic: simp_rw [coeff_monomial_mul'] at hi hj
Cleared hypotheses: hi, hj
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have pos : ∀ (hi : i ≤ j) (hj : s = r * coeff (j - i) x), (s = 0 ∨ i ≤ j) ∧ r ∣ s
Tactic: split_ifs at hj with hi
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have neg : ∀ (hi : ¬i ≤ j) (hj : s = 0), (s = 0 ∨ i ≤ j) ∧ r ∣ s
Tactic: split_ifs at hj with hi
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have 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
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 _⟩
Cleared hypotheses: hj, hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have 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
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 _⟩
Cleared hypotheses: hj, hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have 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
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 _⟩
Cleared hypotheses: hj, hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have 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
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 _⟩
Cleared hypotheses: hj, hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
have 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
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 _⟩
Cleared hypotheses: hj, hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r : R
i j : σ →₀ ℕ
d : R
h : r * d = 0
⊢ Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((monomial j : (a : R) → MvPolynomial σ R) (r * d) : MvPolynomial σ R)
have mpr : Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
  ((monomial j : (a : R) → MvPolynomial σ R) 0 : MvPolynomial σ R)
Tactic: simp_rw [h, monomial_zero, dvd_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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)
⊢ Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((monomial j : (a : R) → MvPolynomial σ R) (r * d) : MvPolynomial σ R)
have mpr₁ : Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) (0 : MvPolynomial σ R)
Tactic: simp_rw [h, monomial_zero, dvd_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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)
have 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)
Tactic: refine ⟨monomial (j - i) d, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : 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)
have 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)
Tactic: rw [monomial_mul, add_tsub_cancel_of_le hij]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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)
⊢ (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)
have mpr₁ : Eq (α := MvPolynomial σ R) ((monomial j : (a : R) → MvPolynomial σ R) (r * d) : MvPolynomial σ R)
  ((monomial j : (a : R) → MvPolynomial σ R) (r * d) : MvPolynomial σ R)
Tactic: rw [monomial_mul, add_tsub_cancel_of_le hij]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
i j : σ →₀ ℕ
⊢ Dvd.dvd (α := MvPolynomial σ R) ((monomial i : (a : R) → MvPolynomial σ R) 1)
      ((monomial j : (a : R) → MvPolynomial σ R) 1) ↔
    i ≤ j
have rw : (Eq.{u_2 + 1} (α := R) 1 0 ∨ i ≤ j) ∧ Dvd.dvd.{u_2} (α := R) 1 1 ↔ i ≤ j
Tactic: rw [monomial_dvd_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
i j : σ →₀ ℕ
⊢ (Eq.{u_2 + 1} (α := R) 1 0 ∨ i ≤ j) ∧ Dvd.dvd.{u_2} (α := R) 1 1 ↔ i ≤ j
have simp_rw : (False ∨ i ≤ j) ∧ Dvd.dvd.{u_2} (α := R) 1 1 ↔ i ≤ j
Tactic: simp_rw [one_ne_zero, false_or, dvd_rfl, and_true]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ (Eq.{u_2 + 1} (α := R) 1 0 ∨ i ≤ j) ∧ Dvd.dvd.{u_2} (α := R) 1 1 ↔ i ≤ j
have simp_rw₁ : i ≤ j ∧ Dvd.dvd.{u_2} (α := R) 1 1 ↔ i ≤ j
Tactic: simp_rw [one_ne_zero, false_or, dvd_rfl, and_true]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ (Eq.{u_2 + 1} (α := R) 1 0 ∨ i ≤ j) ∧ Dvd.dvd.{u_2} (α := R) 1 1 ↔ i ≤ j
have simp_rw₂ : i ≤ j ∧ True ↔ i ≤ j
Tactic: simp_rw [one_ne_zero, false_or, dvd_rfl, and_true]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
have refine : LE.le (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single j 1) ↔ i = j
Tactic: refine monomial_one_dvd_monomial_one.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
i j : σ
⊢ LE.le (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single j 1) ↔ i = j
have simp_rw : LE.le (α := ℕ) (1 : ℕ) ((Finsupp.single j 1 : (a : σ) → ℕ) i : ℕ) ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ LE.le (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single j 1) ↔ i = j
have simp_rw₁ : Ne (α := ℕ) ((Finsupp.single j 1 : (a : σ) → ℕ) i : ℕ) (0 : ℕ) ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ LE.le (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single j 1) ↔ i = j
have simp_rw₂ : i = j ∧ Ne (α := ℕ) 1 0 ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ LE.le (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single j 1) ↔ i = j
have simp_rw₃ : i = j ∧ ¬Eq (α := ℕ) 1 0 ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ LE.le (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single j 1) ↔ i = j
have simp_rw₄ : i = j ∧ ¬False ↔ 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]