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

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
σ : 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
constructor
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
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
rintro ⟨x, hx⟩
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
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
rw [MvPolynomial.ext_iff] at hx
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
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
have hj := hx j
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
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
have hi := hx i
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
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
simp_rw [coeff_monomial, if_pos] at hj hi
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
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
simp_rw [coeff_monomial_mul'] at hi hj
case mp.intro.inl.inl
σ : 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

case mp.intro.inl.inr
σ : 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

case mp.intro.inr.inl
σ : 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

case mp.intro.inr.inr
σ : 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
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
split_ifs  at hi hj with hi hi
no goals
case mp.intro.inl.inl
σ : 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
exact ⟨Or.inr hi, _, hj⟩
no goals
case mp.intro.inl.inr
σ : 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
exact ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩
no goals
case mp.intro.inr.inl
σ : 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
simp_all only [or_true, dvd_mul_right]
no goals
case mp.intro.inr.inr
σ : 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
simp_all only [ite_self, le_refl, ite_true, dvd_mul_right]
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)

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)
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
rintro ⟨h | hij, d, rfl⟩
no goals
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)
simp_rw [h, monomial_zero, dvd_zero]
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
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)
refine' ⟨monomial (j - i) d, _⟩
no goals
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
rw [monomial_mul, add_tsub_cancel_of_le hij]