-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem eq_factors_of_eq_counts {a b : Associates α} (ha : a ≠ 0) (hb : b ≠ 0)
    (h : ∀ p : Associates α, Irreducible p → p.count a.factors = p.count b.factors) :
    a.factors = b.factors

Proof state:
case intro.intro.a.h.mk
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
h_count : ∀ (p : Associates α) (hp : Irreducible p), Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb
p : Associates α
hp : Irreducible p
⊢ (toFinsupp sa) ⟨p, hp⟩ = (toFinsupp sb) ⟨p, hp⟩

Tactic:
rw [Multiset.toFinsupp_apply, Multiset.toFinsupp_apply, h_count p hp]

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
⊢ a.factors = b.factors

Tactic:
obtain ⟨sb, h_sb⟩ := factors_eq_some_iff_ne_zero.mpr hb

Result:
case intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h_sb : b.factors = ↑sb
⊢ a.factors = b.factors

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
p : Associates α
hp : Irreducible p
⊢ Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb

Tactic:
rw [← count_some, ← count_some, h p hp]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h_sb : b.factors = ↑sb
⊢ a.factors = b.factors

Tactic:
rw [h_sa, h_sb] at h ⊢

Result:
case intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
⊢ ↑sa = ↑sb

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors
⊢ a.factors = b.factors

Tactic:
obtain ⟨sa, h_sa⟩ := factors_eq_some_iff_ne_zero.mpr ha

Result:
case intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
⊢ a.factors = b.factors

Proof state:
case intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
⊢ ↑sa = ↑sb

Tactic:
rw [WithTop.coe_eq_coe]

Result:
case intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
⊢ sa = sb

Proof state:
case intro.intro.a
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
h_count : ∀ (p : Associates α) (hp : Irreducible p), Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb
⊢ toFinsupp sa = toFinsupp sb

Tactic:
ext ⟨p, hp⟩

Result:
case intro.intro.a.h.mk
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
h_count : ∀ (p : Associates α) (hp : Irreducible p), Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb
p : Associates α
hp : Irreducible p
⊢ (toFinsupp sa) ⟨p, hp⟩ = (toFinsupp sb) ⟨p, hp⟩

Proof state:
case intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
⊢ sa = sb

Tactic:
have h_count : ∀ (p : Associates α) (hp : Irreducible p),
    sa.count ⟨p, hp⟩ = sb.count ⟨p, hp⟩ := by
  intro p hp
  rw [← count_some, ← count_some, h p hp]

Result:
case intro.intro
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
ha : a ≠ 0
hb : b ≠ 0
sa : Multiset { p // Irreducible p }
h_sa : a.factors = ↑sa
sb : Multiset { p // Irreducible p }
h : ∀ (p : Associates α), Irreducible p → p.count ↑sa = p.count ↑sb
h_sb : b.factors = ↑sb
h_count : ∀ (p : Associates α) (hp : Irreducible p), Multiset.count ⟨p, hp⟩ sa = Multiset.count ⟨p, hp⟩ sb
⊢ sa = sb