-- Mathlib/Data/Nat/Squarefree.lean
theorem divisors_filter_squarefree {n : ℕ} (h0 : n ≠ 0) :
    {d ∈ n.divisors | Squarefree d}.val =
      (UniqueFactorizationMonoid.normalizedFactors n).toFinset.powerset.val.map fun x =>
        x.val.prod

Proof state:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ z ∈ normalizedFactors ?m.57670

Tactic:
rw [← Multiset.mem_toFinset]

Result:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ z ∈ (normalizedFactors ?m.57670).toFinset

n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ ℕ

Proof state:
case h
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ (normalizedFactors a).toFinset ∈ (normalizedFactors n).toFinset.powerset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
simp only [id, Finset.mem_powerset]

Result:
case h
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors n).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Proof state:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ Irreducible z

Tactic:
apply irreducible_of_normalized_factor z

Result:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ z ∈ normalizedFactors ?m.57670

n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ ℕ

Proof state:
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ a ∈ (filter (fun d => Squarefree d) n.divisors).val ↔
    a ∈ Multiset.map (fun x => x.val.prod) (normalizedFactors n).toFinset.powerset.val

Tactic:
simp only [Multiset.mem_filter, id, Multiset.mem_map, Finset.filter_val, ← Finset.mem_def,
  mem_divisors]

Result:
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (a ∣ n ∧ n ≠ 0) ∧ Squarefree a ↔ ∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a

Proof state:
case h.intro
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors a + normalizedFactors b ∧ Associated (normalizedFactors a).prod a

Tactic:
exact ⟨Multiset.subset_of_le (Multiset.le_add_right _ _), prod_normalizedFactors h0.1⟩

Result:
no goals

Proof state:
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s ∈ (normalizedFactors n).toFinset.powerset
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod

Tactic:
rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs

Result:
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod

Proof state:
case h.intro
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
rw [Multiset.toFinset_subset, Multiset.toFinset_val, hsq.dedup, ← associated_iff_eq,
  normalizedFactors_mul h0.1 h0.2]

Result:
case h.intro
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors a + normalizedFactors b ∧ Associated (normalizedFactors a).prod a

Proof state:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ x.val
⊢ z ∈ normalizedFactors ?m.57463

Tactic:
rw [← Multiset.mem_toFinset]

Result:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ x.val
⊢ z ∈ (normalizedFactors ?m.57463).toFinset

n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ x.val
⊢ ℕ

Proof state:
case h
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors n).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
rcases an with ⟨b, rfl⟩

Result:
case h.intro
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ h0 : a * b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Proof state:
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
con : 0 ∈ s.val
⊢ False

Tactic:
apply
  not_irreducible_zero
    (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))

Result:
no goals

Proof state:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 => Associated x1 x2) x.val y.val

Tactic:
apply UniqueFactorizationMonoid.factors_unique _ _ (associated_iff_eq.2 h)

Result:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
⊢ ∀ x_1 ∈ x.val, Irreducible x_1

n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
⊢ ∀ x ∈ y.val, Irreducible x

Proof state:
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : Multiset.Rel Associated (normalizedFactors s.val.prod) s.val
⊢ Squarefree s.val.prod

Tactic:
rw [associated_eq_eq, Multiset.rel_eq] at h

Result:
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : normalizedFactors s.val.prod = s.val
⊢ Squarefree s.val.prod

Proof state:
n : ℕ
h0 : n ≠ 0
⊢ (filter (fun d => Squarefree d) n.divisors).val =
    Multiset.map (fun x => x.val.prod) (normalizedFactors n).toFinset.powerset.val

Tactic:
rw [(Finset.nodup _).ext ((Finset.nodup _).map_on _)]

Result:
n : ℕ
h0 : n ≠ 0
⊢ ∀ (a : ℕ),
    a ∈ (filter (fun d => Squarefree d) n.divisors).val ↔
      a ∈ Multiset.map (fun x => x.val.prod) (normalizedFactors n).toFinset.powerset.val

n : ℕ
h0 : n ≠ 0
⊢ ∀ x ∈ (normalizedFactors n).toFinset.powerset.val,
    ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y

Proof state:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ x = y

Tactic:
rw [← Finset.val_inj, ← Multiset.rel_eq, ← associated_eq_eq]

Result:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (normalizedFactors n).toFinset.powerset.val
y : Finset ℕ
hy : y ∈ (normalizedFactors n).toFinset.powerset.val
h : x.val.prod = y.val.prod
⊢ Multiset.Rel (fun x1 x2 => Associated x1 x2) x.val y.val

Proof state:
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod

Tactic:
rw [(prod_normalizedFactors h0).symm.dvd_iff_dvd_right]

Result:
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
⊢ (s.val.prod ∣ (normalizedFactors n).prod ∧ n ≠ 0) ∧ Squarefree s.val.prod