-- Mathlib/Data/Nat/Squarefree.lean
theorem Squarefree.ext_iff {n m : ℕ} (hn : Squarefree n) (hm : Squarefree m) :
    n = m ↔ ∀ p, Prime p → (p ∣ n ↔ p ∣ m)

Proof state:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
⊢ n = m ↔ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)

Tactic:
refine ⟨by rintro rfl; simp, fun h => eq_of_factorization_eq hn.ne_zero hm.ne_zero fun p => ?_⟩

Result:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
⊢ n.factorization p = m.factorization p

Proof state:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
⊢ n.factorization p = m.factorization p

Tactic:
by_cases hp : p.Prime

Result:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
⊢ n.factorization p = m.factorization p

case neg
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : ¬Prime p
⊢ n.factorization p = m.factorization p

Proof state:
case neg
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : ¬Prime p
⊢ n.factorization p = m.factorization p

Tactic:
rw [factorization_eq_zero_of_non_prime _ hp, factorization_eq_zero_of_non_prime _ hp]

Result:
no goals

Proof state:
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
⊢ n.factorization p = m.factorization p

Tactic:
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₁

Result:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : n.factorization p = 0 ↔ m.factorization p = 0
⊢ n.factorization p = m.factorization p

Proof state:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : n.factorization p = 0 ↔ m.factorization p = 0
⊢ n.factorization p = m.factorization p

Tactic:
have h₂ := hn.natFactorization_le_one p

Result:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : n.factorization p = 0 ↔ m.factorization p = 0
h₂ : n.factorization p ≤ 1
⊢ n.factorization p = m.factorization p

Proof state:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : n.factorization p = 0 ↔ m.factorization p = 0
h₂ : n.factorization p ≤ 1
h₃ : m.factorization p ≤ 1
⊢ n.factorization p = m.factorization p

Tactic:
omega

Result:
no goals

Proof state:
n m : ℕ
hn : Squarefree n
hm : Squarefree m
⊢ n = m → ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)

Tactic:
rintro rfl

Result:
n : ℕ
hn hm : Squarefree n
⊢ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ n)

Proof state:
n : ℕ
hn hm : Squarefree n
⊢ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ n)

Tactic:
simp

Result:
no goals

Proof state:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : n.factorization p = 0 ↔ m.factorization p = 0
h₂ : n.factorization p ≤ 1
⊢ n.factorization p = m.factorization p

Tactic:
have h₃ := hm.natFactorization_le_one p

Result:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
h₁ : n.factorization p = 0 ↔ m.factorization p = 0
h₂ : n.factorization p ≤ 1
h₃ : m.factorization p ≤ 1
⊢ n.factorization p = m.factorization p

Proof state:
case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
⊢ n.factorization p = m.factorization p

Tactic:
have h₁ := h _ hp

Result:
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
⊢ n.factorization p = m.factorization p