α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
⊢ FactorSetMem p ⊤
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
⊢ p ∈ ⊤
dsimp only [Membership.mem]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
⊢ if hp : Irreducible p then BfactorSetMem { val := p, property := hp } ⊤ else False
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
⊢ FactorSetMem p ⊤
dsimp only [FactorSetMem]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
⊢ BfactorSetMem { val := p, property := hp } ⊤
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
⊢ if hp : Irreducible p then BfactorSetMem { val := p, property := hp } ⊤ else False
split_ifs
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
p : Associates α
hp : Irreducible p
⊢ BfactorSetMem { val := p, property := hp } ⊤
exact trivial