α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : { val := p, property := hp } ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∣ Associates.mk a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : { val := p, property := hp } ∈ factors' a
⊢ p ∣ Associates.mk a
haveI := Classical.decEq (Associates α)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : { val := p, property := hp } ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∈ factors (Associates.mk a)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : { val := p, property := hp } ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∣ Associates.mk a
apply dvd_of_mem_factors (hp := hp)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : { val := p, property := hp } ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∈ ↑(factors' a)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : { val := p, property := hp } ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∈ factors (Associates.mk a)
rw [factors_mk _ hz]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : { val := p, property := hp } ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∈ ↑(factors' a)
apply mem_factorSet_some.2 h_mem