case mp
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset n → m ∣ n

case mpr
m n : ℕ+
⊢ m ∣ n → factorMultiset m ≤ factorMultiset n
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset n ↔ m ∣ n
constructor
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ m ∣ n
case mp
m n : ℕ+
⊢ factorMultiset m ≤ factorMultiset n → m ∣ n
intro h
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ PrimeMultiset.prod (factorMultiset (PrimeMultiset.prod (factorMultiset m))) ∣ n
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ m ∣ n
rw [← prod_factorMultiset m, ← prod_factorMultiset m]
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ PrimeMultiset.prod (factorMultiset (PrimeMultiset.prod (factorMultiset m))) *
      PrimeMultiset.prod (factorMultiset n - factorMultiset m) =
    n
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ PrimeMultiset.prod (factorMultiset (PrimeMultiset.prod (factorMultiset m))) ∣ n
apply Dvd.intro (n.factorMultiset - m.factorMultiset).prod
no goals
case mp
m n : ℕ+
h : factorMultiset m ≤ factorMultiset n
⊢ PrimeMultiset.prod (factorMultiset (PrimeMultiset.prod (factorMultiset m))) *
      PrimeMultiset.prod (factorMultiset n - factorMultiset m) =
    n
rw [← PrimeMultiset.prod_add, PrimeMultiset.factorMultiset_prod, add_tsub_cancel_of_le h,
  prod_factorMultiset]
case mpr
m n : ℕ+
h : m ∣ n
⊢ factorMultiset m ≤ factorMultiset n
case mpr
m n : ℕ+
⊢ m ∣ n → factorMultiset m ≤ factorMultiset n
intro h
case mpr
m n : ℕ+
h : m ∣ n
⊢ factorMultiset m ≤ factorMultiset m + factorMultiset (divExact n m)
case mpr
m n : ℕ+
h : m ∣ n
⊢ factorMultiset m ≤ factorMultiset n
rw [← mul_div_exact h, factorMultiset_mul]
no goals
case mpr
m n : ℕ+
h : m ∣ n
⊢ factorMultiset m ≤ factorMultiset m + factorMultiset (divExact n m)
exact le_self_add