case inl
p : ℕ
hn : Squarefree 0
⊢ ↑(factorization 0) p ≤ 1

case inr
n p : ℕ
hn : Squarefree n
hn' : n ≠ 0
⊢ ↑(factorization n) p ≤ 1
n p : ℕ
hn : Squarefree n
⊢ ↑(factorization n) p ≤ 1
rcases eq_or_ne n 0 with (rfl | hn')
case inr
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
⊢ ↑(factorization n) p ≤ 1
case inr
n p : ℕ
hn : Squarefree n
hn' : n ≠ 0
⊢ ↑(factorization n) p ≤ 1
rw [multiplicity.squarefree_iff_multiplicity_le_one] at hn
case pos
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
⊢ ↑(factorization n) p ≤ 1

case neg
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ ↑(factorization n) p ≤ 1
case inr
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
⊢ ↑(factorization n) p ≤ 1
by_cases hp : p.Prime
no goals
case inl
p : ℕ
hn : Squarefree 0
⊢ ↑(factorization 0) p ≤ 1
simp
case pos
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : multiplicity p n ≤ 1 ∨ IsUnit p
⊢ ↑(factorization n) p ≤ 1
case pos
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
⊢ ↑(factorization n) p ≤ 1
have := hn p
case pos
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : ↑(↑(factorization n) p) ≤ 1
⊢ ↑(factorization n) p ≤ 1
case pos
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : multiplicity p n ≤ 1 ∨ IsUnit p
⊢ ↑(factorization n) p ≤ 1
simp only [multiplicity_eq_factorization hp hn', Nat.isUnit_iff, hp.ne_one, or_false_iff]
  at this
no goals
case pos
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : ↑(↑(factorization n) p) ≤ 1
⊢ ↑(factorization n) p ≤ 1
exact_mod_cast this
case neg
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ 0 ≤ 1
case neg
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ ↑(factorization n) p ≤ 1
rw [factorization_eq_zero_of_non_prime _ hp]
no goals
case neg
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ 0 ≤ 1
exact zero_le_one