case pos
α : 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
hm : p ∈ factors a
ha0 : a = 0
⊢ p ∣ a

case neg
α : 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
hm : p ∈ factors a
ha0 : ¬a = 0
⊢ p ∣ 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
hm : p ∈ factors a
⊢ p ∣ a
by_cases ha0 : a = 0
case neg.intro.intro
α : 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
hm : p ∈ factors a
ha0 : ¬a = 0
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ a
case neg
α : 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
hm : p ∈ factors a
ha0 : ¬a = 0
⊢ p ∣ a
obtain ⟨a0, nza, ha'⟩ := exists_non_zero_rep ha0
case neg.intro.intro
α : 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
hm : p ∈ factors a
ha0 : ¬a = 0
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ FactorSet.prod (factors a)
case neg.intro.intro
α : 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
hm : p ∈ factors a
ha0 : ¬a = 0
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ a
rw [← Associates.factors_prod a]
case neg.intro.intro
α : 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
ha0 : ¬a = 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ FactorSet.prod ↑(factors' a0)
case neg.intro.intro
α : 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
hm : p ∈ factors a
ha0 : ¬a = 0
a0 : α
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ FactorSet.prod (factors a)
rw [← ha', factors_mk a0 nza] at hm⊢
case neg.intro.intro
α : 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
ha0 : ¬a = 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ prod (map Subtype.val (factors' a0))
case neg.intro.intro
α : 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
ha0 : ¬a = 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ FactorSet.prod ↑(factors' a0)
rw [prod_coe]
case neg.intro.intro.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
ha0 : ¬a = 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∈ map Subtype.val (factors' a0)
case neg.intro.intro
α : 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
ha0 : ¬a = 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∣ prod (map Subtype.val (factors' a0))
apply Multiset.dvd_prod
case neg.intro.intro.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
ha0 : ¬a = 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ ∃ a, a ∈ factors' a0 ∧ ↑a = p
case neg.intro.intro.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
ha0 : ¬a = 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ p ∈ map Subtype.val (factors' a0)
apply Multiset.mem_map.mpr
no goals
case neg.intro.intro.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
ha0 : ¬a = 0
a0 : α
hm : p ∈ ↑(factors' a0)
nza : a0 ≠ 0
ha' : Associates.mk a0 = a
⊢ ∃ a, a ∈ factors' a0 ∧ ↑a = p
exact ⟨⟨p, hp⟩, mem_factorSet_some.mp hm, rfl⟩
case pos
α : 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
hm : p ∈ factors a
ha0 : a = 0
⊢ p ∣ 0
case pos
α : 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
hm : p ∈ factors a
ha0 : a = 0
⊢ p ∣ a
rw [ha0]
no goals
case pos
α : 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
hm : p ∈ factors a
ha0 : a = 0
⊢ p ∣ 0
exact dvd_zero p