case intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
⊢ p ≤ q
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
⊢ prod p ≤ prod q → p ≤ q
rintro ⟨c, eqc⟩
case intro.refine'_1
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
x : Associates α
hx : x ∈ p + factors c
⊢ Irreducible x

case intro.refine'_2
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
⊢ prod q = prod (p + factors c)
case intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
⊢ p ≤ q
refine' Multiset.le_iff_exists_add.2 ⟨factors c, unique' hq (fun x hx => _) _⟩
case intro.refine'_1.inl
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
x : Associates α
hx : x ∈ p + factors c
h : x ∈ p
⊢ Irreducible x

case intro.refine'_1.inr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
x : Associates α
hx : x ∈ p + factors c
h : x ∈ factors c
⊢ Irreducible x
case intro.refine'_1
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
x : Associates α
hx : x ∈ p + factors c
⊢ Irreducible x
obtain h | h := Multiset.mem_add.1 hx
no goals
case intro.refine'_1.inl
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
x : Associates α
hx : x ∈ p + factors c
h : x ∈ p
⊢ Irreducible x
exact hp x h
no goals
case intro.refine'_1.inr
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
x : Associates α
hx : x ∈ p + factors c
h : x ∈ factors c
⊢ Irreducible x
exact irreducible_of_factor _ h
case intro.refine'_2
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
⊢ prod p * c = prod p * prod (factors c)
case intro.refine'_2
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
⊢ prod q = prod (p + factors c)
rw [eqc, Multiset.prod_add]
case intro.refine'_2.e_a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
⊢ c = prod (factors c)
case intro.refine'_2
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
⊢ prod p * c = prod p * prod (factors c)
congr
case intro.refine'_2.e_a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
hc : c = 0
⊢ False
case intro.refine'_2.e_a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
⊢ c = prod (factors c)
refine' associated_iff_eq.mp (factors_prod fun hc => _).symm
case intro.refine'_2.e_a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
hc : c = 0
⊢ 0 ∈ q
case intro.refine'_2.e_a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
hc : c = 0
⊢ False
refine' not_irreducible_zero (hq _ _)
no goals
case intro.refine'_2.e_a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : Multiset (Associates α)
hp : ∀ (a : Associates α), a ∈ p → Irreducible a
hq : ∀ (a : Associates α), a ∈ q → Irreducible a
c : Associates α
eqc : prod q = prod p * c
hc : c = 0
⊢ 0 ∈ q
rw [← prod_eq_zero_iff, eqc, hc, MulZeroClass.mul_zero]