case mp
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ DvdNotUnit x y → normalizedFactors x < normalizedFactors y

case mpr
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x < normalizedFactors y → DvdNotUnit x y
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ DvdNotUnit x y ↔ normalizedFactors x < normalizedFactors y
constructor
case mp.intro.intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx left✝ : x ≠ 0
c : α
hc : ¬IsUnit c
hy : x * c ≠ 0
⊢ normalizedFactors x < normalizedFactors (x * c)
case mp
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ DvdNotUnit x y → normalizedFactors x < normalizedFactors y
rintro ⟨_, c, hc, rfl⟩
no goals
case mp.intro.intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x : α
hx left✝ : x ≠ 0
c : α
hc : ¬IsUnit c
hy : x * c ≠ 0
⊢ normalizedFactors x < normalizedFactors (x * c)
simp only [hx, right_ne_zero_of_mul hy, normalizedFactors_mul, Ne.def, not_false_iff,
  lt_add_iff_pos_right, normalizedFactors_pos, hc]
case mpr
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalizedFactors x < normalizedFactors y
⊢ DvdNotUnit x y
case mpr
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ normalizedFactors x < normalizedFactors y → DvdNotUnit x y
intro h
no goals
case mpr
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : DecidableEq α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
h : normalizedFactors x < normalizedFactors y
⊢ DvdNotUnit x y
exact
  dvdNotUnit_of_dvd_of_not_dvd
    ((dvd_iff_normalizedFactors_le_normalizedFactors hx hy).mpr h.le)
    (mt (dvd_iff_normalizedFactors_le_normalizedFactors hy hx).mp h.not_le)