-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem normalizedFactors_pos (x : α) (hx : x ≠ 0) : 0 < normalizedFactors x ↔ ¬IsUnit x

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < normalizedFactors x ↔ ¬IsUnit x

Tactic:
constructor

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

case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬IsUnit x → 0 < normalizedFactors x

Proof state:
case mp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ 0 < normalizedFactors x → ¬IsUnit x

Tactic:
intro h hx

Result:
case mp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < normalizedFactors x
hx : IsUnit x
⊢ False

Proof state:
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ 0 < normalizedFactors x

Tactic:
obtain ⟨p, hp⟩ := exists_mem_normalizedFactors hx h

Result:
case mpr.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p : α
hp : p ∈ normalizedFactors x
⊢ 0 < normalizedFactors x

Proof state:
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
⊢ ¬IsUnit x → 0 < normalizedFactors x

Tactic:
intro h

Result:
case mpr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
⊢ 0 < normalizedFactors x

Proof state:
case mp.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < normalizedFactors x
hx : IsUnit x
p : α
hp : p ∈ normalizedFactors x
⊢ False

Tactic:
exact
  (prime_of_normalized_factor _ hp).not_unit
    (isUnit_of_dvd_unit (dvd_of_mem_normalizedFactors hp) hx)

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < normalizedFactors x
hx : IsUnit x
⊢ False

Tactic:
obtain ⟨p, hp⟩ := Multiset.exists_mem_of_ne_zero h.ne'

Result:
case mp.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx✝ : x ≠ 0
h : 0 < normalizedFactors x
hx : IsUnit x
p : α
hp : p ∈ normalizedFactors x
⊢ False

Proof state:
case mpr.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx : x ≠ 0
h : ¬IsUnit x
p : α
hp : p ∈ normalizedFactors x
⊢ 0 < normalizedFactors x

Tactic:
exact
  bot_lt_iff_ne_bot.mpr
    (mt Multiset.eq_zero_iff_forall_not_mem.mp (not_forall.mpr ⟨p, not_not.mpr hp⟩))

Result:
no goals