p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ↑(factorization (p * i + r)) p = 0
⊢ ¬p ∣ r
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
⊢ ¬p ∣ r ↔ ↑(factorization (p * i + r)) p = 0
refine' ⟨factorization_eq_zero_of_remainder i, fun h => _⟩
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
⊢ ¬p ∣ r
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ↑(factorization (p * i + r)) p = 0
⊢ ¬p ∣ r
rw [factorization_eq_zero_iff] at h
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : ¬Prime p ∨ ¬p ∣ p * i + r ∨ p * i + r = 0
⊢ ¬p ∣ r
contrapose! h
case refine'_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ p * i + r

case refine'_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ Prime p ∧ p ∣ p * i + r ∧ p * i + r ≠ 0
refine' ⟨pp, _, _⟩
no goals
case refine'_1
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p ∣ p * i + r
rwa [← Nat.dvd_add_iff_right (dvd_mul_right p i)]
case refine'_2
p r i : ℕ
pp : Prime p
h : p ∣ r
hr0 : p * i + r = 0
⊢ r = 0
case refine'_2
p r i : ℕ
pp : Prime p
hr0 : r ≠ 0
h : p ∣ r
⊢ p * i + r ≠ 0
contrapose! hr0
no goals
case refine'_2
p r i : ℕ
pp : Prime p
h : p ∣ r
hr0 : p * i + r = 0
⊢ r = 0
exact (add_eq_zero_iff.mp hr0).2