R : Type ?u.569435
n : ℕ
h0 : n ≠ 0
⊢ List.length (List.dedup (factors n)) = ↑Ω n ↔ List.Nodup (factors n)
R : Type ?u.569435
n : ℕ
h0 : n ≠ 0
⊢ ↑ω n = ↑Ω n ↔ Squarefree n
rw [squarefree_iff_nodup_factors h0, cardDistinctFactors_apply]
case mp
R : Type ?u.569435
n : ℕ
h0 : n ≠ 0
h : List.length (List.dedup (factors n)) = ↑Ω n
⊢ List.Nodup (factors n)

case mpr
R : Type ?u.569435
n : ℕ
h0 : n ≠ 0
h : List.Nodup (factors n)
⊢ List.length (List.dedup (factors n)) = ↑Ω n
R : Type ?u.569435
n : ℕ
h0 : n ≠ 0
⊢ List.length (List.dedup (factors n)) = ↑Ω n ↔ List.Nodup (factors n)
constructor <;> intro h
case mp
R : Type ?u.569435
n : ℕ
h0 : n ≠ 0
h : List.length (List.dedup (factors n)) = ↑Ω n
⊢ List.Nodup (List.dedup (factors n))
case mp
R : Type ?u.569435
n : ℕ
h0 : n ≠ 0
h : List.length (List.dedup (factors n)) = ↑Ω n
⊢ List.Nodup (factors n)
rw [← n.factors.dedup_sublist.eq_of_length h]
no goals
case mp
R : Type ?u.569435
n : ℕ
h0 : n ≠ 0
h : List.length (List.dedup (factors n)) = ↑Ω n
⊢ List.Nodup (List.dedup (factors n))
apply List.nodup_dedup
case mpr
R : Type ?u.569435
n : ℕ
h0 : n ≠ 0
h : List.Nodup (factors n)
⊢ List.length (factors n) = ↑Ω n
case mpr
R : Type ?u.569435
n : ℕ
h0 : n ≠ 0
h : List.Nodup (factors n)
⊢ List.length (List.dedup (factors n)) = ↑Ω n
rw [h.dedup]
no goals
case mpr
R : Type ?u.569435
n : ℕ
h0 : n ≠ 0
h : List.Nodup (factors n)
⊢ List.length (factors n) = ↑Ω n
rfl