-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors'_cong {a b : α} (h : a ~ᵤ b) : factors' a = factors' b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
⊢ factors' a = factors' b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Result:
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a ~ᵤ 0
⊢ factors' a = factors' 0

case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
⊢ factors' a = factors' b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
⊢ a ≠ 0

Tactic:
contrapose! hb with ha

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b = 0

Proof state:
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a ~ᵤ 0
⊢ factors' a = factors' 0

Tactic:
rw [associated_zero_iff_eq_zero] at h

Result:
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a = 0
⊢ factors' a = factors' 0

Proof state:
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ factors' a = factors' b

Tactic:
rw [← Multiset.map_eq_map Subtype.coe_injective, map_subtype_coe_factors',
  map_subtype_coe_factors', ← rel_associated_iff_map_eq_map]

Result:
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ Rel Associated (factors a) (factors b)

Proof state:
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
h : a = 0
⊢ factors' a = factors' 0

Tactic:
rw [h]

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ Rel Associated (factors a) (factors b)

Tactic:
exact
  factors_unique irreducible_of_factor irreducible_of_factor
    ((factors_prod ha).trans <| h.trans <| (factors_prod hb).symm)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b = 0

Tactic:
rw [← associated_zero_iff_eq_zero, ← ha]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b ~ᵤ a

Proof state:
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
⊢ factors' a = factors' b

Tactic:
have ha : a ≠ 0 := by
  contrapose! hb with ha
  rw [← associated_zero_iff_eq_zero, ← ha]
  exact h.symm

Result:
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
hb : b ≠ 0
ha : a ≠ 0
⊢ factors' a = factors' b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : a ~ᵤ b
ha : a = 0
⊢ b ~ᵤ a

Tactic:
exact h.symm

Result:
no goals