[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s' s : σ →₀ ℕ
x : MvPolynomial σ R
h : ¬s ≤ s'
⊢ ¬∃ d, s' = s + d
[PROOFSTEP]
rintro ⟨d, rfl⟩
[GOAL]
case intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
x : MvPolynomial σ R
d : σ →₀ ℕ
h : ¬s ≤ s + d
⊢ False
[PROOFSTEP]
exact h le_self_add
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ ↑(monomial i) r ∣ ↑(monomial j) s ↔ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
constructor
[GOAL]
case mp
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ ↑(monomial i) r ∣ ↑(monomial j) s → (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ↑(monomial j) s = ↑(monomial i) r * x
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
rw [MvPolynomial.ext_iff] at hx 
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
have hj := hx j
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hj : coeff j (↑(monomial j) s) = coeff j (↑(monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
have hi := hx i
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hj : coeff j (↑(monomial j) s) = coeff j (↑(monomial i) r * x)
hi : coeff i (↑(monomial j) s) = coeff i (↑(monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
classical
simp_rw [coeff_monomial, if_pos] at hj hi 
simp_rw [coeff_monomial_mul'] at hi hj 
split_ifs at hi hj  with hi hi
· exact ⟨Or.inr hi, _, hj⟩
·
  exact
    ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩
      -- Porting note: two goals remain at this point in Lean 4
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hj : coeff j (↑(monomial j) s) = coeff j (↑(monomial i) r * x)
hi : coeff i (↑(monomial j) s) = coeff i (↑(monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
simp_rw [coeff_monomial, if_pos] at hj hi 
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hi : (if j = i then s else 0) = coeff i (↑(monomial i) r * x)
hj : s = coeff j (↑(monomial i) r * x)
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
simp_rw [coeff_monomial_mul'] at hi hj 
[GOAL]
case mp.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) 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
[PROOFSTEP]
split_ifs at hi hj  with hi hi
[GOAL]
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hi✝¹ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi✝ : j = i
hi : i ≤ j
hj : s = r * coeff (j - i) x
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
exact ⟨Or.inr hi, _, hj⟩
[GOAL]
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hi✝¹ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi✝ : j = i
hi : ¬i ≤ j
hj : s = 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
exact
  ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩
    -- Porting note: two goals remain at this point in Lean 4
[GOAL]
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hi✝ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : ¬j = i
h✝ : i ≤ j
hj : s = r * coeff (j - i) x
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
simp_all only [or_true, dvd_mul_right]
[GOAL]
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
x : MvPolynomial σ R
hx : ∀ (m : σ →₀ ℕ), coeff m (↑(monomial j) s) = coeff m (↑(monomial i) r * x)
hi✝ : (if j = i then s else 0) = if i ≤ i then r * coeff (i - i) x else 0
hi : ¬j = i
h✝ : ¬i ≤ j
hj : s = 0
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s
[PROOFSTEP]
simp_all only [ite_self, le_refl, ite_true, dvd_mul_right]
[GOAL]
case mpr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s → ↑(monomial i) r ∣ ↑(monomial j) s
[PROOFSTEP]
rintro ⟨h | hij, d, rfl⟩
[GOAL]
case mpr.intro.inl.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
i j : σ →₀ ℕ
d : R
h : r * d = 0
⊢ ↑(monomial i) r ∣ ↑(monomial j) (r * d)
[PROOFSTEP]
simp_rw [h, monomial_zero, dvd_zero]
[GOAL]
case mpr.intro.inr.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : R
⊢ ↑(monomial i) r ∣ ↑(monomial j) (r * d)
[PROOFSTEP]
refine' ⟨monomial (j - i) d, _⟩
[GOAL]
case mpr.intro.inr.intro
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : R
⊢ ↑(monomial j) (r * d) = ↑(monomial i) r * ↑(monomial (j - i)) d
[PROOFSTEP]
rw [monomial_mul, add_tsub_cancel_of_le hij]
[GOAL]
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ ↑(monomial i) 1 ∣ ↑(monomial j) 1 ↔ i ≤ j
[PROOFSTEP]
rw [monomial_dvd_monomial]
[GOAL]
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ (1 = 0 ∨ i ≤ j) ∧ 1 ∣ 1 ↔ i ≤ j
[PROOFSTEP]
simp_rw [one_ne_zero, false_or_iff, dvd_rfl, and_true_iff]
[GOAL]
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ X i ∣ X j ↔ i = j
[PROOFSTEP]
refine' monomial_one_dvd_monomial_one.trans _
[GOAL]
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ
⊢ Finsupp.single i 1 ≤ Finsupp.single j 1 ↔ i = j
[PROOFSTEP]
simp_rw [Finsupp.single_le_iff, Nat.one_le_iff_ne_zero, Finsupp.single_apply_ne_zero, and_true_iff]
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ X i ∣ ↑(monomial j) r ↔ r = 0 ∨ ↑j i ≠ 0
[PROOFSTEP]
refine' monomial_dvd_monomial.trans _
[GOAL]
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ ↑j i ≠ 0
[PROOFSTEP]
simp_rw [one_dvd, and_true_iff, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]
