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

n : ℕ
h0 : n ≠ 0
⊢ ∀ (x : Finset ℕ),
    x ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val →
      ∀ (y : Finset ℕ),
        y ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val →
          Multiset.prod x.val = Multiset.prod y.val → x = y
n : ℕ
h0 : n ≠ 0
⊢ (Finset.filter Squarefree (divisors n)).val =
    Multiset.map (fun x => Multiset.prod x.val) (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
rw [(Finset.nodup _).ext ((Finset.nodup _).map_on _)]
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ a ∈ (Finset.filter Squarefree (divisors n)).val ↔
    a ∈ Multiset.map (fun x => Multiset.prod x.val) (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
n : ℕ
h0 : n ≠ 0
⊢ ∀ (a : ℕ),
    a ∈ (Finset.filter Squarefree (divisors n)).val ↔
      a ∈ Multiset.map (fun x => Multiset.prod x.val) (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
intro a
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (a ∣ n ∧ n ≠ 0) ∧ Squarefree a ↔
    ∃ a_1, a_1 ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n)) ∧ Multiset.prod a_1.val = a
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ a ∈ (Finset.filter Squarefree (divisors n)).val ↔
    a ∈ Multiset.map (fun x => Multiset.prod x.val) (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
simp only [Multiset.mem_filter, id.def, Multiset.mem_map, Finset.filter_val, ← Finset.mem_def,
  mem_divisors]
case mp
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (a ∣ n ∧ n ≠ 0) ∧ Squarefree a →
    ∃ a_2, a_2 ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n)) ∧ Multiset.prod a_2.val = a

case mpr
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (∃ a_1, a_1 ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n)) ∧ Multiset.prod a_1.val = a) →
    (a ∣ n ∧ n ≠ 0) ∧ Squarefree a
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (a ∣ n ∧ n ≠ 0) ∧ Squarefree a ↔
    ∃ a_1, a_1 ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n)) ∧ Multiset.prod a_1.val = a
constructor
case mp.intro.intro
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ ∃ a_1, a_1 ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n)) ∧ Multiset.prod a_1.val = a
case mp
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (a ∣ n ∧ n ≠ 0) ∧ Squarefree a →
    ∃ a_2, a_2 ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n)) ∧ Multiset.prod a_2.val = a
rintro ⟨⟨an, h0⟩, hsq⟩
case mp.intro.intro
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ Multiset.toFinset (normalizedFactors a) ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n)) ∧
    Multiset.prod (Multiset.toFinset (normalizedFactors a)).val = a
case mp.intro.intro
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ ∃ a_1, a_1 ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n)) ∧ Multiset.prod a_1.val = a
use (UniqueFactorizationMonoid.normalizedFactors a).toFinset
case mp.intro.intro
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ Multiset.toFinset (normalizedFactors a) ⊆ Multiset.toFinset (normalizedFactors n) ∧
    Multiset.prod (Multiset.toFinset (normalizedFactors a)).val = a
case mp.intro.intro
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ Multiset.toFinset (normalizedFactors a) ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n)) ∧
    Multiset.prod (Multiset.toFinset (normalizedFactors a)).val = a
simp only [id.def, Finset.mem_powerset]
case mp.intro.intro.intro
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ h0 : a * b ≠ 0
⊢ Multiset.toFinset (normalizedFactors a) ⊆ Multiset.toFinset (normalizedFactors (a * b)) ∧
    Multiset.prod (Multiset.toFinset (normalizedFactors a)).val = a
case mp.intro.intro
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ Multiset.toFinset (normalizedFactors a) ⊆ Multiset.toFinset (normalizedFactors n) ∧
    Multiset.prod (Multiset.toFinset (normalizedFactors a)).val = a
rcases an with ⟨b, rfl⟩
case mp.intro.intro.intro
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ Multiset.toFinset (normalizedFactors a) ⊆ Multiset.toFinset (normalizedFactors (a * b)) ∧
    Multiset.prod (Multiset.toFinset (normalizedFactors a)).val = a
case mp.intro.intro.intro
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ h0 : a * b ≠ 0
⊢ Multiset.toFinset (normalizedFactors a) ⊆ Multiset.toFinset (normalizedFactors (a * b)) ∧
    Multiset.prod (Multiset.toFinset (normalizedFactors a)).val = a
rw [mul_ne_zero_iff] at h0
case mp.intro.intro.intro
a : ℕ
hsq : Multiset.Nodup (normalizedFactors a)
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ Multiset.toFinset (normalizedFactors a) ⊆ Multiset.toFinset (normalizedFactors (a * b)) ∧
    Multiset.prod (Multiset.toFinset (normalizedFactors a)).val = a
case mp.intro.intro.intro
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ Multiset.toFinset (normalizedFactors a) ⊆ Multiset.toFinset (normalizedFactors (a * b)) ∧
    Multiset.prod (Multiset.toFinset (normalizedFactors a)).val = a
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0.1] at hsq
case mp.intro.intro.intro
a : ℕ
hsq : Multiset.Nodup (normalizedFactors a)
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors a + normalizedFactors b ∧ Associated (Multiset.prod (normalizedFactors a)) a
case mp.intro.intro.intro
a : ℕ
hsq : Multiset.Nodup (normalizedFactors a)
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ Multiset.toFinset (normalizedFactors a) ⊆ Multiset.toFinset (normalizedFactors (a * b)) ∧
    Multiset.prod (Multiset.toFinset (normalizedFactors a)).val = a
rw [Multiset.toFinset_subset, Multiset.toFinset_val, hsq.dedup, ← associated_iff_eq,
  normalizedFactors_mul h0.1 h0.2]
no goals
case mp.intro.intro.intro
a : ℕ
hsq : Multiset.Nodup (normalizedFactors a)
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors a + normalizedFactors b ∧ Associated (Multiset.prod (normalizedFactors a)) a
exact ⟨Multiset.subset_of_le (Multiset.le_add_right _ _), normalizedFactors_prod h0.1⟩
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n))
⊢ (Multiset.prod s.val ∣ n ∧ n ≠ 0) ∧ Squarefree (Multiset.prod s.val)
case mpr
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (∃ a_1, a_1 ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n)) ∧ Multiset.prod a_1.val = a) →
    (a ∣ n ∧ n ≠ 0) ∧ Squarefree a
rintro ⟨s, hs, rfl⟩
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
⊢ (Multiset.prod s.val ∣ n ∧ n ≠ 0) ∧ Squarefree (Multiset.prod s.val)
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s ∈ Finset.powerset (Multiset.toFinset (normalizedFactors n))
⊢ (Multiset.prod s.val ∣ n ∧ n ≠ 0) ∧ Squarefree (Multiset.prod s.val)
rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
⊢ (Multiset.prod s.val ∣ n ∧ n ≠ 0) ∧ Squarefree (Multiset.prod s.val)
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
⊢ (Multiset.prod s.val ∣ n ∧ n ≠ 0) ∧ Squarefree (Multiset.prod s.val)
have hs0 : s.val.prod ≠ 0 := by
  rw [Ne.def, Multiset.prod_eq_zero_iff]
  simp only [exists_prop, id.def, exists_eq_right]
  intro con
  apply
    not_irreducible_zero
      (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
⊢ (Multiset.prod s.val ∣ Multiset.prod (normalizedFactors n) ∧ n ≠ 0) ∧ Squarefree (Multiset.prod s.val)
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
⊢ (Multiset.prod s.val ∣ n ∧ n ≠ 0) ∧ Squarefree (Multiset.prod s.val)
rw [(normalizedFactors_prod h0).symm.dvd_iff_dvd_right]
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
⊢ Squarefree (Multiset.prod s.val)
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
⊢ (Multiset.prod s.val ∣ Multiset.prod (normalizedFactors n) ∧ n ≠ 0) ∧ Squarefree (Multiset.prod s.val)
refine' ⟨⟨Multiset.prod_dvd_prod_of_le (le_trans hs (Multiset.dedup_le _)), h0⟩, _⟩
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
h : Multiset.Rel Associated (normalizedFactors (Multiset.prod s.val)) s.val
⊢ Squarefree (Multiset.prod s.val)
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
⊢ Squarefree (Multiset.prod s.val)
have h :=
  UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor
    (fun x hx =>
      irreducible_of_normalized_factor x
        (Multiset.mem_of_le (le_trans hs (Multiset.dedup_le _)) hx))
    (normalizedFactors_prod hs0)
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
h : normalizedFactors (Multiset.prod s.val) = s.val
⊢ Squarefree (Multiset.prod s.val)
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
h : Multiset.Rel Associated (normalizedFactors (Multiset.prod s.val)) s.val
⊢ Squarefree (Multiset.prod s.val)
rw [associated_eq_eq, Multiset.rel_eq] at h
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
h : normalizedFactors (Multiset.prod s.val) = s.val
⊢ Multiset.Nodup s.val
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
h : normalizedFactors (Multiset.prod s.val) = s.val
⊢ Squarefree (Multiset.prod s.val)
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hs0, h]
no goals
case mpr.intro.intro
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
hs0 : Multiset.prod s.val ≠ 0
h : normalizedFactors (Multiset.prod s.val) = s.val
⊢ Multiset.Nodup s.val
apply s.nodup
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
⊢ ¬0 ∈ s.val
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
⊢ Multiset.prod s.val ≠ 0
rw [Ne.def, Multiset.prod_eq_zero_iff]
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
⊢ ¬0 ∈ s.val
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
⊢ ¬0 ∈ s.val
simp only [exists_prop, id.def, exists_eq_right]
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
con : 0 ∈ s.val
⊢ False
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
⊢ ¬0 ∈ s.val
intro con
no goals
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
con : 0 ∈ s.val
⊢ False
apply
  not_irreducible_zero
    (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
y : Finset ℕ
hy : y ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
h : Multiset.prod x.val = Multiset.prod y.val
⊢ x = y
n : ℕ
h0 : n ≠ 0
⊢ ∀ (x : Finset ℕ),
    x ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val →
      ∀ (y : Finset ℕ),
        y ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val →
          Multiset.prod x.val = Multiset.prod y.val → x = y
intro x hx y hy h
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
y : Finset ℕ
hy : y ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
h : Multiset.prod x.val = Multiset.prod y.val
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) x.val y.val
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
y : Finset ℕ
hy : y ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
h : Multiset.prod x.val = Multiset.prod y.val
⊢ x = y
rw [← Finset.val_inj, ← Multiset.rel_eq, ← associated_eq_eq]
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) x.val y.val
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
y : Finset ℕ
hy : y ∈ (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val
h : Multiset.prod x.val = Multiset.prod y.val
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) x.val y.val
rw [← Finset.mem_def, Finset.mem_powerset] at hx hy
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
⊢ ∀ (x_1 : ℕ), x_1 ∈ x.val → Irreducible x_1

n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
⊢ ∀ (x : ℕ), x ∈ y.val → Irreducible x
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
⊢ Multiset.Rel (fun x x_1 => Associated x x_1) x.val y.val
apply UniqueFactorizationMonoid.factors_unique _ _ (associated_iff_eq.2 h)
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ x.val
⊢ Irreducible z
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
⊢ ∀ (x_1 : ℕ), x_1 ∈ x.val → Irreducible x_1
intro z hz
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ x.val
⊢ z ∈ normalizedFactors ?m.114917

n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ x.val
⊢ ℕ
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ x.val
⊢ Irreducible z
apply irreducible_of_normalized_factor z
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ x.val
⊢ z ∈ Multiset.toFinset (normalizedFactors ?m.114917)

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

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

n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ x.val
⊢ ℕ
rw [← Multiset.mem_toFinset]
no goals
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ x.val
⊢ z ∈ Multiset.toFinset (normalizedFactors ?m.114917)

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

n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ x.val
⊢ ℕ
apply hx hz
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ y.val
⊢ Irreducible z
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
⊢ ∀ (x : ℕ), x ∈ y.val → Irreducible x
intro z hz
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ y.val
⊢ z ∈ normalizedFactors ?m.115154

n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ y.val
⊢ ℕ
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ y.val
⊢ Irreducible z
apply irreducible_of_normalized_factor z
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ y.val
⊢ z ∈ Multiset.toFinset (normalizedFactors ?m.115154)

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

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

n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ y.val
⊢ ℕ
rw [← Multiset.mem_toFinset]
no goals
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ Multiset.toFinset (normalizedFactors n)
y : Finset ℕ
hy : y ⊆ Multiset.toFinset (normalizedFactors n)
h : Multiset.prod x.val = Multiset.prod y.val
z : ℕ
hz : z ∈ y.val
⊢ z ∈ Multiset.toFinset (normalizedFactors ?m.115154)

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

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