α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : factors (Associates.mk a) ⊓ factors (Associates.mk b) ≠ 0
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
have hz : factors (Associates.mk a) ⊓ factors (Associates.mk b) ≠ 0 := by
  contrapose! h with hf
  change (factors (Associates.mk a) ⊓ factors (Associates.mk b)).prod = 1
  rw [hf]
  exact Multiset.prod_zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : factors (Associates.mk a) ⊓ factors (Associates.mk b) ≠ 0
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
rw [factors_mk a ha, factors_mk b hb, ← WithTop.coe_inf] at hz
case intro.mk
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p0 : Associates α
p0_irr : Irreducible p0
p0_mem : { val := p0, property := p0_irr } ∈ factors' a ⊓ factors' b
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
obtain ⟨⟨p0, p0_irr⟩, p0_mem⟩ := Multiset.exists_mem_of_ne_zero ((mt WithTop.coe_eq_coe.mpr) hz)
case intro.mk
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p0 : Associates α
p0_irr : Irreducible p0
p0_mem : { val := p0, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
case intro.mk
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p0 : Associates α
p0_irr : Irreducible p0
p0_mem : { val := p0, property := p0_irr } ∈ factors' a ⊓ factors' b
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
rw [Multiset.inf_eq_inter] at p0_mem
case intro.mk.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
case intro.mk
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p0 : Associates α
p0_irr : Irreducible p0
p0_mem : { val := p0, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
obtain ⟨p, rfl⟩ : ∃ p, Associates.mk p = p0 := Quot.exists_rep p0
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ Prime p

case intro.mk.intro.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ p ∣ a

case intro.mk.intro.refine'_3
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ p ∣ b
case intro.mk.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ ∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
refine' ⟨p, _, _, _⟩
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
hf : factors (Associates.mk a) ⊓ factors (Associates.mk b) = 0
⊢ Associates.mk a ⊓ Associates.mk b = 1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
⊢ factors (Associates.mk a) ⊓ factors (Associates.mk b) ≠ 0
contrapose! h with hf
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
hf : factors (Associates.mk a) ⊓ factors (Associates.mk b) = 0
⊢ FactorSet.prod (factors (Associates.mk a) ⊓ factors (Associates.mk b)) = 1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
hf : factors (Associates.mk a) ⊓ factors (Associates.mk b) = 0
⊢ Associates.mk a ⊓ Associates.mk b = 1
change (factors (Associates.mk a) ⊓ factors (Associates.mk b)).prod = 1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
hf : factors (Associates.mk a) ⊓ factors (Associates.mk b) = 0
⊢ FactorSet.prod 0 = 1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
hf : factors (Associates.mk a) ⊓ factors (Associates.mk b) = 0
⊢ FactorSet.prod (factors (Associates.mk a) ⊓ factors (Associates.mk b)) = 1
rw [hf]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
hf : factors (Associates.mk a) ⊓ factors (Associates.mk b) = 0
⊢ FactorSet.prod 0 = 1
exact Multiset.prod_zero
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ Irreducible (Associates.mk p)
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ Prime p
rw [← irreducible_iff_prime, ← irreducible_mk]
no goals
case intro.mk.intro.refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ Irreducible (Associates.mk p)
exact p0_irr
case intro.mk.intro.refine'_2.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ Associates.mk p ≤ Associates.mk a
case intro.mk.intro.refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ p ∣ a
apply dvd_of_mk_le_mk
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ a ≠ 0
case intro.mk.intro.refine'_2.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ Associates.mk p ≤ Associates.mk a
apply dvd_of_mem_factors' (Multiset.mem_inter.mp p0_mem).left
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ a ≠ 0
apply ha
case intro.mk.intro.refine'_3.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ Associates.mk p ≤ Associates.mk b
case intro.mk.intro.refine'_3
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ p ∣ b
apply dvd_of_mk_le_mk
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ b ≠ 0
case intro.mk.intro.refine'_3.a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ Associates.mk p ≤ Associates.mk b
apply dvd_of_mem_factors' (Multiset.mem_inter.mp p0_mem).right
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : α
ha : a ≠ 0
hb : b ≠ 0
h : Associates.mk a ⊓ Associates.mk b ≠ 1
hz : ↑(factors' a ⊓ factors' b) ≠ 0
p : α
p0_irr : Irreducible (Associates.mk p)
p0_mem : { val := Associates.mk p, property := p0_irr } ∈ factors' a ∩ factors' b
⊢ b ≠ 0
apply hb