case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
h : a ~ᵤ 0
⊢ factors' a = factors' 0

case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
hb : b ≠ 0
⊢ factors' a = factors' b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
⊢ factors' a = factors' b
obtain rfl | hb := eq_or_ne b 0
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ factors' a = factors' b
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
hb : b ≠ 0
⊢ factors' a = factors' b
have ha : a ≠ 0 := by
  contrapose! hb with ha
  rw [← associated_zero_iff_eq_zero, ← ha]
  exact h.symm
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ Rel Associated (factors a) (factors b)
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ factors' a = factors' b
rw [← Multiset.map_eq_map Subtype.coe_injective, map_subtype_coe_factors',
  map_subtype_coe_factors', ← rel_associated_iff_map_eq_map]
no goals
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ Rel Associated (factors a) (factors b)
exact
  factors_unique irreducible_of_factor irreducible_of_factor
    ((factors_prod ha).trans <| h.trans <| (factors_prod hb).symm)
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
h : a = 0
⊢ factors' a = factors' 0
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
h : a ~ᵤ 0
⊢ factors' a = factors' 0
rw [associated_zero_iff_eq_zero] at h
no goals
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
h : a = 0
⊢ factors' a = factors' 0
rw [h]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b = 0
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
hb : b ≠ 0
⊢ a ≠ 0
contrapose! hb with ha
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b ~ᵤ a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b = 0
rw [← associated_zero_iff_eq_zero, ← ha]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b ~ᵤ a
exact h.symm