α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ FactorSetMem p ↑l ↔ Mem { val := p, property := hp } l
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ p ∈ ↑l ↔ { val := p, property := hp } ∈ l
dsimp only [Membership.mem]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ (if hp : Irreducible p then BfactorSetMem { val := p, property := hp } ↑l else False) ↔
    Mem { val := p, property := hp } l
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ FactorSetMem p ↑l ↔ Mem { val := p, property := hp } l
dsimp only [FactorSetMem]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ BfactorSetMem { val := p, property := hp } ↑l ↔ Mem { val := p, property := hp } l
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ (if hp : Irreducible p then BfactorSetMem { val := p, property := hp } ↑l else False) ↔
    Mem { val := p, property := hp } l
split_ifs
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
l : Multiset { a // Irreducible a }
⊢ BfactorSetMem { val := p, property := hp } ↑l ↔ Mem { val := p, property := hp } l
rfl