case mp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < factors x → ¬IsUnit x

case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬IsUnit x → 0 < factors x
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < factors x ↔ ¬IsUnit x
constructor
case mp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < factors x
hx : IsUnit x
⊢ False
case mp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < factors x → ¬IsUnit x
intro h hx
case mp.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < factors x
hx : IsUnit x
p : α
hp : p ∈ factors x
⊢ False
case mp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < factors x
hx : IsUnit x
⊢ False
obtain ⟨p, hp⟩ := Multiset.exists_mem_of_ne_zero h.ne'
no goals
case mp.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < factors x
hx : IsUnit x
p : α
hp : p ∈ factors x
⊢ False
exact (prime_of_factor _ hp).not_unit (isUnit_of_dvd_unit (dvd_of_mem_factors hp) hx)
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ 0 < factors x
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬IsUnit x → 0 < factors x
intro h
case mpr.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p : α
hp : p ∈ factors x
⊢ 0 < factors x
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ 0 < factors x
obtain ⟨p, hp⟩ := exists_mem_factors hx h
no goals
case mpr.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p : α
hp : p ∈ factors x
⊢ 0 < factors x
exact
  bot_lt_iff_ne_bot.mpr
    (mt Multiset.eq_zero_iff_forall_not_mem.mp (not_forall.mpr ⟨p, not_not.mpr hp⟩))