case refine'_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ prod (factors a ++ factors b) = a * b

case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ (p : ℕ), p ∈ factors a ++ factors b → Prime p
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ factors (a * b) ~ factors a ++ factors b
refine' (factors_unique _ _).symm
no goals
case refine'_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ prod (factors a ++ factors b) = a * b
rw [List.prod_append, prod_factors ha, prod_factors hb]
case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ factors a ++ factors b
⊢ Prime p
case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ (p : ℕ), p ∈ factors a ++ factors b → Prime p
intro p hp
case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ factors a ∨ p ∈ factors b
⊢ Prime p
case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ factors a ++ factors b
⊢ Prime p
rw [List.mem_append] at hp
no goals
case refine'_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ factors a ∨ p ∈ factors b
⊢ Prime p
cases' hp with hp' hp' <;> exact prime_of_mem_factors hp'