case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ prod l = prod (factors n)

case refine'_2
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → _root_.Prime p

case refine'_3
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ factors n → _root_.Prime p
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l ~ factors n
refine' perm_of_prod_eq_prod _ _ _
case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n = prod (factors n)
case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ prod l = prod (factors n)
rw [h₁]
case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n ≠ 0
case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n = prod (factors n)
refine' (prod_factors _).symm
case refine'_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : prod l = 0
⊢ False
case refine'_1
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n ≠ 0
rintro rfl
case refine'_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : 0 ∈ l
⊢ False
case refine'_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : prod l = 0
⊢ False
rw [prod_eq_zero_iff] at h₁
no goals
case refine'_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : 0 ∈ l
⊢ False
exact Prime.ne_zero (h₂ 0 h₁) rfl
case refine'_2
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → Prime p
case refine'_2
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → _root_.Prime p
simp_rw [← prime_iff]
no goals
case refine'_2
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → Prime p
exact h₂
case refine'_3
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ factors n → Prime p
case refine'_3
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ factors n → _root_.Prime p
simp_rw [← prime_iff]
no goals
case refine'_3
n : ℕ
l : List ℕ
h₁ : prod l = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ factors n → Prime p
exact fun p => prime_of_mem_factors