-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_mul {p a b : α} (hp : Prime p) (hfin : FiniteMultiplicity p (a * b)) :
    multiplicity p (a * b) = multiplicity p a + multiplicity p b

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b

Tactic:
rw [pow_add]

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ multiplicity p a * p ^ multiplicity p b ∣ a * b

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
rw [hfin.multiplicity_eq_iff]

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b ∧ ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
have hdivb : p ^ multiplicity p b ∣ b := pow_multiplicity_dvd ..

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ multiplicity p a * p ^ multiplicity p b ∣ a * b

Tactic:
apply mul_dvd_mul <;> assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
have hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b :=
  fun h =>
  not_or_intro (hfin.mul_left.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
    (hfin.mul_right.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
    (_root_.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul hp hdiva hdivb h)

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b ∧ ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b

Tactic:
exact ⟨hdiv, hsucc⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
have hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b := by
  rw [pow_add]; apply mul_dvd_mul <;> assumption

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b

Tactic:
have hdiva : p ^ multiplicity p a ∣ a := pow_multiplicity_dvd ..

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b