R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
⊢ b ≠ 0 → Finite a b
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
hb : b ≠ 0
⊢ Finite a b
revert hb
case refine'_1
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
u : R
hu : IsUnit u
x✝ : u ≠ 0
⊢ Finite a u

case refine'_2
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b✝ : R
ha : Prime a
b p : R
hb : b ≠ 0
hp : Irreducible p
ih : b ≠ 0 → Finite a b
x✝ : p * b ≠ 0
⊢ Finite a (p * b)
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
⊢ b ≠ 0 → Finite a b
refine'
  WfDvdMonoid.induction_on_irreducible b (fun c => c.irrefl.elim) (fun u hu _ => _)
    fun b p hb hp ih _ => _
case refine'_1
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
u : R
hu : IsUnit u
x✝ : u ≠ 0
⊢ 0.Dom
case refine'_1
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
u : R
hu : IsUnit u
x✝ : u ≠ 0
⊢ Finite a u
rw [multiplicity.finite_iff_dom, multiplicity.isUnit_right ha.not_unit hu]
no goals
case refine'_1
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b : R
ha : Prime a
u : R
hu : IsUnit u
x✝ : u ≠ 0
⊢ 0.Dom
exact PartENat.dom_natCast 0
case refine'_2
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b✝ : R
ha : Prime a
b p : R
hb : b ≠ 0
hp : Irreducible p
ih : b ≠ 0 → Finite a b
x✝ : p * b ≠ 0
⊢ multiplicity a p ≤ 1
case refine'_2
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b✝ : R
ha : Prime a
b p : R
hb : b ≠ 0
hp : Irreducible p
ih : b ≠ 0 → Finite a b
x✝ : p * b ≠ 0
⊢ Finite a (p * b)
refine'
  multiplicity.finite_mul ha
    (multiplicity.finite_iff_dom.mpr
      (PartENat.dom_of_le_natCast (show multiplicity a p ≤ ↑1 from _)))
    (ih hb)
case refine'_2
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b✝ : R
ha : Prime a
b p : R
hb : b ≠ 0
hp : Irreducible p
ih : b ≠ 0 → Finite a b
x✝ : p * b ≠ 0
⊢ multiplicity a p ≤ 1
case refine'_2
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b✝ : R
ha : Prime a
b p : R
hb : b ≠ 0
hp : Irreducible p
ih : b ≠ 0 → Finite a b
x✝ : p * b ≠ 0
⊢ multiplicity a p ≤ 1
norm_cast
no goals
case refine'_2
R : Type u_1
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : WfDvdMonoid R
a b✝ : R
ha : Prime a
b p : R
hb : b ≠ 0
hp : Irreducible p
ih : b ≠ 0 → Finite a b
x✝ : p * b ≠ 0
⊢ multiplicity a p ≤ 1
exact
  ((multiplicity.squarefree_iff_multiplicity_le_one p).mp hp.squarefree a).resolve_right
    ha.not_unit