case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : p = 0
⊢ Irreducible p ↔ Prime p

case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : ¬p = 0
⊢ Irreducible p ↔ Prime p
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
⊢ Irreducible p ↔ Prime p
by_cases hp0 : p = 0
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
⊢ Prime p
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : ¬p = 0
⊢ Irreducible p ↔ Prime p
refine' ⟨fun h => _, Prime.irreducible⟩
case neg.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
f : Multiset α
hf : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ p
⊢ Prime p
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
⊢ Prime p
obtain ⟨f, hf⟩ := pf p hp0
case neg.intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ (b : α), b ∈ {q} → Prime b) ∧ Multiset.prod {q} ~ᵤ p
⊢ Prime p
case neg.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
f : Multiset α
hf : (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ p
⊢ Prime p
obtain ⟨q, hq, rfl⟩ := prime_factors_irreducible h hf
case neg.intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ (b : α), b ∈ {q} → Prime b) ∧ Multiset.prod {q} ~ᵤ p
⊢ Prime q
case neg.intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ (b : α), b ∈ {q} → Prime b) ∧ Multiset.prod {q} ~ᵤ p
⊢ Prime p
rw [hq.prime_iff]
no goals
case neg.intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : ¬p = 0
h : Irreducible p
q : α
hq : p ~ᵤ q
hf : (∀ (b : α), b ∈ {q} → Prime b) ∧ Multiset.prod {q} ~ᵤ p
⊢ Prime q
exact hf.1 q (Multiset.mem_singleton_self _)
no goals
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
p : α
hp0 : p = 0
⊢ Irreducible p ↔ Prime p
simp [hp0]