-- Mathlib/Algebra/MvPolynomial/Division.lean
theorem monomial_dvd_monomial {r s : R} {i j : σ →₀ ℕ} :
    monomial i r ∣ monomial j s ↔ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Proof state:
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

Tactic:
rintro ⟨h | hij, d, rfl⟩

Result:
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)

Proof state:
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

Tactic:
rw [MvPolynomial.ext_iff] at hx

Result:
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

Proof state:
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

Tactic:
exact ⟨Or.inr hi, _, hj⟩

Result:
no goals

Proof state:
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

Tactic:
have hi := hx i

Result:
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

Proof state:
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)

Tactic:
simp_rw [h, monomial_zero, dvd_zero]

Result:
no goals

Proof state:
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

Tactic:
split_ifs at hi hj with hi hi

Result:
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

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

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

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

Proof state:
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

Tactic:
have hj := hx j

Result:
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

Proof state:
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)

Tactic:
refine ⟨monomial (j - i) d, ?_⟩

Result:
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

Proof state:
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

Tactic:
simp_rw [coeff_monomial, if_pos] at hj hi

Result:
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

Proof state:
σ : 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

Tactic:
constructor

Result:
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

Proof state:
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

Tactic:
simp_all only [ite_self, le_refl, ite_true, dvd_mul_right, or_false, and_self]

Result:
no goals

Proof state:
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

Tactic:
simp_all only [or_true, dvd_mul_right, and_self]

Result:
no goals

Proof state:
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

Tactic:
exact ⟨Or.inl hj, hj.symm ▸ dvd_zero _⟩

Result:
no goals