α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
have hdiva : p ^ get (multiplicity p a) ((finite_mul_iff hp).1 h).1 ∣ a := pow_multiplicity_dvd _
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
have hdivb : p ^ get (multiplicity p b) ((finite_mul_iff hp).1 h).2 ∣ b := pow_multiplicity_dvd _
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
have hpoweq :
  p ^ (get (multiplicity p a) ((finite_mul_iff hp).1 h).1 +
        get (multiplicity p b) ((finite_mul_iff hp).1 h).2) =
    p ^ get (multiplicity p a) ((finite_mul_iff hp).1 h).1 *
      p ^ get (multiplicity p b) ((finite_mul_iff hp).1 h).2 :=
  by simp [pow_add]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
hdiv : p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
have hdiv :
  p ^ (get (multiplicity p a) ((finite_mul_iff hp).1 h).1 +
        get (multiplicity p b) ((finite_mul_iff hp).1 h).2) ∣
    a * b :=
  by rw [hpoweq]; apply mul_dvd_mul <;> assumption
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
hdiv : p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b
hsucc : ¬p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b) + 1) ∣ a * b
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
hdiv : p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
have hsucc :
  ¬p ^ (get (multiplicity p a) ((finite_mul_iff hp).1 h).1 +
            get (multiplicity p b) ((finite_mul_iff hp).1 h).2 +
          1) ∣
      a * b :=
  fun h =>
  not_or_of_not (is_greatest' _ (lt_succ_self _)) (is_greatest' _ (lt_succ_self _))
    (_root_.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul hp hdiva hdivb h)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
hdiv : p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b
hsucc : ¬p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b) + 1) ∣ a * b
⊢ p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b ∧
    ¬p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b) + 1) ∣ a * b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
hdiv : p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b
hsucc : ¬p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b) + 1) ∣ a * b
⊢ Part.get (multiplicity p (a * b)) h =
    Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)
rw [← PartENat.natCast_inj, PartENat.natCast_get, eq_coe_iff]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
hdiv : p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b
hsucc : ¬p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b) + 1) ∣ a * b
⊢ p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b ∧
    ¬p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b) + 1) ∣ a * b
exact ⟨hdiv, hsucc⟩
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
⊢ p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
simp [pow_add]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
⊢ p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ a * b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
⊢ p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) ∣ a * b
rw [hpoweq]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a b : α
hp : Prime p
h : (multiplicity p (a * b)).Dom
hdiva : p ^ Part.get (multiplicity p a) (_ : Finite p a) ∣ a
hdivb : p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ b
hpoweq :
  p ^ (Part.get (multiplicity p a) (_ : Finite p a) + Part.get (multiplicity p b) (_ : Finite p b)) =
    p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b)
⊢ p ^ Part.get (multiplicity p a) (_ : Finite p a) * p ^ Part.get (multiplicity p b) (_ : Finite p b) ∣ a * b
apply mul_dvd_mul <;> assumption