n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
⊢ ↑(factorization n) p = ↑(factorization m) p
n m : ℕ
hn : Squarefree n
hm : Squarefree m
⊢ n = m ↔ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
refine' ⟨by rintro rfl; simp, fun h => eq_of_factorization_eq hn.ne_zero hm.ne_zero fun p => _⟩
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
⊢ ↑(factorization n) p = ↑(factorization m) p

case neg
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : ¬Prime p
⊢ ↑(factorization n) p = ↑(factorization m) p
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
⊢ ↑(factorization n) p = ↑(factorization m) p
by_cases hp : p.Prime
no goals
case neg
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : ¬Prime p
⊢ ↑(factorization n) p = ↑(factorization m) p
rw [factorization_eq_zero_of_non_prime _ hp, factorization_eq_zero_of_non_prime _ hp]
n : ℕ
hn hm : Squarefree n
⊢ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ n)
n m : ℕ
hn : Squarefree n
hm : Squarefree m
⊢ n = m → ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
rintro rfl
no goals
n : ℕ
hn hm : Squarefree n
⊢ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ n)
simp
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : p ∣ n ↔ p ∣ m
⊢ ↑(factorization n) p = ↑(factorization m) p
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
⊢ ↑(factorization n) p = ↑(factorization m) p
have h₁ := h _ hp
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
⊢ ↑(factorization n) p = ↑(factorization m) p
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : p ∣ n ↔ p ∣ m
⊢ ↑(factorization n) p = ↑(factorization m) p
rw [← not_iff_not, hp.dvd_iff_one_le_factorization hn.ne_zero, not_le, lt_one_iff,
  hp.dvd_iff_one_le_factorization hm.ne_zero, not_le, lt_one_iff] at h₁
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₂ : ↑(factorization n) p ≤ 1
⊢ ↑(factorization n) p = ↑(factorization m) p
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
⊢ ↑(factorization n) p = ↑(factorization m) p
have h₂ := Squarefree.factorization_le_one p hn
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₂ : ↑(factorization n) p ≤ 1
h₃ : ↑(factorization m) p ≤ 1
⊢ ↑(factorization n) p = ↑(factorization m) p
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₂ : ↑(factorization n) p ≤ 1
⊢ ↑(factorization n) p = ↑(factorization m) p
have h₃ := Squarefree.factorization_le_one p hm
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₂ : ↑(factorization n) p = 0 ∨ ↑(factorization n) p = 0 + 1
h₃ : ↑(factorization m) p = 0 ∨ ↑(factorization m) p = 0 + 1
⊢ ↑(factorization n) p = ↑(factorization m) p
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₂ : ↑(factorization n) p ≤ 1
h₃ : ↑(factorization m) p ≤ 1
⊢ ↑(factorization n) p = ↑(factorization m) p
rw [Nat.le_add_one_iff, le_zero_iff] at h₂ h₃
case pos.inl
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₃ : ↑(factorization m) p = 0 ∨ ↑(factorization m) p = 0 + 1
h₂ : ↑(factorization n) p = 0
⊢ ↑(factorization n) p = ↑(factorization m) p

case pos.inr
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₃ : ↑(factorization m) p = 0 ∨ ↑(factorization m) p = 0 + 1
h₂ : ↑(factorization n) p = 0 + 1
⊢ ↑(factorization n) p = ↑(factorization m) p
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₂ : ↑(factorization n) p = 0 ∨ ↑(factorization n) p = 0 + 1
h₃ : ↑(factorization m) p = 0 ∨ ↑(factorization m) p = 0 + 1
⊢ ↑(factorization n) p = ↑(factorization m) p
cases' h₂ with h₂ h₂
no goals
case pos.inl
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₃ : ↑(factorization m) p = 0 ∨ ↑(factorization m) p = 0 + 1
h₂ : ↑(factorization n) p = 0
⊢ ↑(factorization n) p = ↑(factorization m) p
rwa [h₂, eq_comm, ← h₁]
case pos.inr
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₃ : ↑(factorization m) p = 0 ∨ ↑(factorization m) p = 0 + 1
h₂ : ↑(factorization n) p = 0 + 1
⊢ ¬↑(factorization m) p = 0
case pos.inr
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₃ : ↑(factorization m) p = 0 ∨ ↑(factorization m) p = 0 + 1
h₂ : ↑(factorization n) p = 0 + 1
⊢ ↑(factorization n) p = ↑(factorization m) p
rw [h₂, h₃.resolve_left]
case pos.inr
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₃ : ↑(factorization m) p = 0 ∨ ↑(factorization m) p = 0 + 1
h₂ : ↑(factorization n) p = 0 + 1
⊢ ¬0 + 1 = 0
case pos.inr
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₃ : ↑(factorization m) p = 0 ∨ ↑(factorization m) p = 0 + 1
h₂ : ↑(factorization n) p = 0 + 1
⊢ ¬↑(factorization m) p = 0
rw [← h₁, h₂]
no goals
case pos.inr
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : ↑(factorization n) p = 0 ↔ ↑(factorization m) p = 0
h₃ : ↑(factorization m) p = 0 ∨ ↑(factorization m) p = 0 + 1
h₂ : ↑(factorization n) p = 0 + 1
⊢ ¬0 + 1 = 0
simp only [Nat.one_ne_zero, not_false_iff]