[GOAL]
n : ℕ
h0 : n ≠ 0
⊢ Squarefree n ↔ List.Nodup (factors n)
[PROOFSTEP]
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0, Nat.factors_eq]
[GOAL]
n : ℕ
h0 : n ≠ 0
⊢ Multiset.Nodup ↑(factors n) ↔ List.Nodup (factors n)
[PROOFSTEP]
simp
[GOAL]
n p : ℕ
hn : Squarefree n
⊢ ↑(factorization n) p ≤ 1
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn')
[GOAL]
case inl
p : ℕ
hn : Squarefree 0
⊢ ↑(factorization 0) p ≤ 1
[PROOFSTEP]
simp
[GOAL]
case inr
n p : ℕ
hn : Squarefree n
hn' : n ≠ 0
⊢ ↑(factorization n) p ≤ 1
[PROOFSTEP]
rw [multiplicity.squarefree_iff_multiplicity_le_one] at hn 
[GOAL]
case inr
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
⊢ ↑(factorization n) p ≤ 1
[PROOFSTEP]
by_cases hp : p.Prime
[GOAL]
case pos
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
⊢ ↑(factorization n) p ≤ 1
[PROOFSTEP]
have := hn p
[GOAL]
case pos
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : multiplicity p n ≤ 1 ∨ IsUnit p
⊢ ↑(factorization n) p ≤ 1
[PROOFSTEP]
simp only [multiplicity_eq_factorization hp hn', Nat.isUnit_iff, hp.ne_one, or_false_iff] at this 
[GOAL]
case pos
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
this : ↑(↑(factorization n) p) ≤ 1
⊢ ↑(factorization n) p ≤ 1
[PROOFSTEP]
exact_mod_cast this
[GOAL]
case neg
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ ↑(factorization n) p ≤ 1
[PROOFSTEP]
rw [factorization_eq_zero_of_non_prime _ hp]
[GOAL]
case neg
n p : ℕ
hn✝ : Squarefree n
hn : ∀ (x : ℕ), multiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : ¬Prime p
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), ↑(factorization n) p ≤ 1
⊢ Squarefree n
[PROOFSTEP]
rw [squarefree_iff_nodup_factors hn, List.nodup_iff_count_le_one]
[GOAL]
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), ↑(factorization n) p ≤ 1
⊢ ∀ (a : ℕ), List.count a (factors n) ≤ 1
[PROOFSTEP]
intro a
[GOAL]
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), ↑(factorization n) p ≤ 1
a : ℕ
⊢ List.count a (factors n) ≤ 1
[PROOFSTEP]
rw [factors_count_eq]
[GOAL]
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), ↑(factorization n) p ≤ 1
a : ℕ
⊢ ↑(factorization n) a ≤ 1
[PROOFSTEP]
apply hn'
[GOAL]
n m : ℕ
hn : Squarefree n
hm : Squarefree m
⊢ n = m ↔ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
[PROOFSTEP]
refine' ⟨by rintro rfl; simp, fun h => eq_of_factorization_eq hn.ne_zero hm.ne_zero fun p => _⟩
[GOAL]
n m : ℕ
hn : Squarefree n
hm : Squarefree m
⊢ n = m → ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
[PROOFSTEP]
rintro rfl
[GOAL]
n : ℕ
hn hm : Squarefree n
⊢ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ n)
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
⊢ ↑(factorization n) p = ↑(factorization m) p
[PROOFSTEP]
by_cases hp : p.Prime
[GOAL]
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
[PROOFSTEP]
have h₁ := h _ hp
[GOAL]
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
[PROOFSTEP]
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₁ 
[GOAL]
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
[PROOFSTEP]
have h₂ := Squarefree.factorization_le_one p hn
[GOAL]
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
[PROOFSTEP]
have h₃ := Squarefree.factorization_le_one p hm
[GOAL]
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
[PROOFSTEP]
rw [Nat.le_add_one_iff, le_zero_iff] at h₂ h₃ 
[GOAL]
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
[PROOFSTEP]
cases' h₂ with h₂ h₂
[GOAL]
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
[PROOFSTEP]
rwa [h₂, eq_comm, ← h₁]
[GOAL]
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
[PROOFSTEP]
rw [h₂, h₃.resolve_left]
[GOAL]
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
[PROOFSTEP]
rw [← h₁, h₂]
[GOAL]
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
[PROOFSTEP]
simp only [Nat.one_ne_zero, not_false_iff]
[GOAL]
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
[PROOFSTEP]
rw [factorization_eq_zero_of_non_prime _ hp, factorization_eq_zero_of_non_prime _ hp]
[GOAL]
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
⊢ Squarefree (n ^ k) ↔ Squarefree n ∧ k = 1
[PROOFSTEP]
refine' ⟨fun h => _, by rintro ⟨hn, rfl⟩; simpa⟩
[GOAL]
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
⊢ Squarefree n ∧ k = 1 → Squarefree (n ^ k)
[PROOFSTEP]
rintro ⟨hn, rfl⟩
[GOAL]
case intro
n : ℕ
hn✝ : n ≠ 1
hn : Squarefree n
hk : 1 ≠ 0
⊢ Squarefree (n ^ 1)
[PROOFSTEP]
simpa
[GOAL]
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | -)
[GOAL]
case inl
k : ℕ
hk : k ≠ 0
hn : 0 ≠ 1
h : Squarefree (0 ^ k)
⊢ Squarefree 0 ∧ k = 1
[PROOFSTEP]
simp [zero_pow hk.bot_lt] at h 
[GOAL]
case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
⊢ Squarefree n ∧ k = 1
[PROOFSTEP]
refine' ⟨h.squarefree_of_dvd (dvd_pow_self _ hk), by_contradiction fun h₁ => _⟩
[GOAL]
case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
⊢ False
[PROOFSTEP]
have : 2 ≤ k := k.two_le_iff.mpr ⟨hk, h₁⟩
[GOAL]
case inr
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ False
[PROOFSTEP]
apply hn (Nat.isUnit_iff.1 (h _ _))
[GOAL]
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ n * n ∣ n ^ k
[PROOFSTEP]
rw [← sq]
[GOAL]
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ n ^ 2 ∣ n ^ k
[PROOFSTEP]
exact pow_dvd_pow _ this
[GOAL]
n : ℕ
⊢ Squarefree n ∧ IsPrimePow n ↔ Prime n
[PROOFSTEP]
refine' ⟨_, fun hn => ⟨hn.squarefree, hn.isPrimePow⟩⟩
[GOAL]
n : ℕ
⊢ Squarefree n ∧ IsPrimePow n → Prime n
[PROOFSTEP]
rw [isPrimePow_nat_iff]
[GOAL]
n : ℕ
⊢ (Squarefree n ∧ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n) → Prime n
[PROOFSTEP]
rintro ⟨h, p, k, hp, hk, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree (p ^ k)
⊢ Prime (p ^ k)
[PROOFSTEP]
rw [squarefree_pow_iff hp.ne_one hk.ne'] at h 
[GOAL]
case intro.intro.intro.intro.intro
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ k)
[PROOFSTEP]
rwa [h.2, pow_one]
[GOAL]
n k : ℕ
h : ¬n < k * k
⊢ sqrt n - k < sqrt n + 2 - k
[PROOFSTEP]
exact Nat.minFac_lemma n k h
[GOAL]
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : MinSqFacProp (n / k) o
⊢ MinSqFacProp n o
[PROOFSTEP]
have : ∀ p, Prime p → p * p ∣ n → k * (p * p) ∣ n := fun p pp dp =>
  have :=
    (coprime_primes pk pp).2 fun e => by
      subst e
      contradiction
  (coprime_mul_iff_right.2 ⟨this, this⟩).mul_dvd_of_dvd_of_dvd dk dp
[GOAL]
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : MinSqFacProp (n / k) o
p : ℕ
pp : Prime p
dp : p * p ∣ n
e : k = p
⊢ False
[PROOFSTEP]
subst e
[GOAL]
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : MinSqFacProp (n / k) o
pp : Prime k
dp : k * k ∣ n
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : MinSqFacProp (n / k) o
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
⊢ MinSqFacProp n o
[PROOFSTEP]
cases' o with d
[GOAL]
case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : MinSqFacProp (n / k) none
⊢ MinSqFacProp n none
[PROOFSTEP]
rw [MinSqFacProp, squarefree_iff_prime_squarefree] at H ⊢
[GOAL]
case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H :
  match none with
  | none => ∀ (x : ℕ), Prime x → ¬x * x ∣ n / k
  | some d => Prime d ∧ d * d ∣ n / k ∧ ∀ (p : ℕ), Prime p → p * p ∣ n / k → d ≤ p
⊢ match none with
  | none => ∀ (x : ℕ), Prime x → ¬x * x ∣ n
  | some d => Prime d ∧ d * d ∣ n ∧ ∀ (p : ℕ), Prime p → p * p ∣ n → d ≤ p
[PROOFSTEP]
exact fun p pp dp => H p pp ((dvd_div_iff dk).2 (this _ pp dp))
[GOAL]
case some
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H : MinSqFacProp (n / k) (some d)
⊢ MinSqFacProp n (some d)
[PROOFSTEP]
obtain ⟨H1, H2, H3⟩ := H
[GOAL]
case some.intro.intro
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H1 : Prime d
H2 : d * d ∣ n / k
H3 : ∀ (p : ℕ), Prime p → p * p ∣ n / k → d ≤ p
⊢ MinSqFacProp n (some d)
[PROOFSTEP]
simp only [dvd_div_iff dk] at H2 H3 
[GOAL]
case some.intro.intro
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H1 : Prime d
H2 : k * (d * d) ∣ n
H3 : ∀ (p : ℕ), Prime p → k * (p * p) ∣ n → d ≤ p
⊢ MinSqFacProp n (some d)
[PROOFSTEP]
exact ⟨H1, dvd_trans (dvd_mul_left _ _) H2, fun p pp dp => H3 _ pp (this _ pp dp)⟩
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
⊢ MinSqFacProp n (minSqFacAux n k)
[PROOFSTEP]
rw [minSqFacAux]
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
⊢ MinSqFacProp n
    (if h : n < k * k then none
    else
      let_fun this := (_ : sqrt n - k < sqrt n + 2 - k);
      if k ∣ n then
        let n' := n / k;
        let_fun this := (_ : sqrt n' - k < sqrt n + 2 - k);
        if k ∣ n' then some k else minSqFacAux n' (k + 2)
      else minSqFacAux n (k + 2))
[PROOFSTEP]
by_cases h : n < k * k
[GOAL]
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
⊢ MinSqFacProp n
    (if h : n < k * k then none
    else
      let_fun this := (_ : sqrt n - k < sqrt n + 2 - k);
      if k ∣ n then
        let n' := n / k;
        let_fun this := (_ : sqrt n' - k < sqrt n + 2 - k);
        if k ∣ n' then some k else minSqFacAux n' (k + 2)
      else minSqFacAux n (k + 2))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ MinSqFacProp n
    (if h : n < k * k then none
    else
      let_fun this := (_ : sqrt n - k < sqrt n + 2 - k);
      if k ∣ n then
        let n' := n / k;
        let_fun this := (_ : sqrt n' - k < sqrt n + 2 - k);
        if k ∣ n' then some k else minSqFacAux n' (k + 2)
      else minSqFacAux n (k + 2))
[PROOFSTEP]
simp [h]
[GOAL]
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
⊢ MinSqFacProp n none
[PROOFSTEP]
refine' squarefree_iff_prime_squarefree.2 fun p pp d => _
[GOAL]
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
⊢ False
[PROOFSTEP]
have := ih p pp (dvd_trans ⟨_, rfl⟩ d)
[GOAL]
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
this : k ≤ p
⊢ False
[PROOFSTEP]
have := Nat.mul_le_mul this this
[GOAL]
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
p : ℕ
pp : Prime p
d : p * p ∣ n
this✝ : k ≤ p
this : k * k ≤ p * p
⊢ False
[PROOFSTEP]
exact not_le_of_lt h (le_trans this (le_of_dvd n0 d))
[GOAL]
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
[PROOFSTEP]
have k2 : 2 ≤ k := by
  subst e
  linarith
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ 2 ≤ k
[PROOFSTEP]
subst e
[GOAL]
n : ℕ
n0 : 0 < n
i : ℕ
ih : ∀ (m : ℕ), Prime m → m ∣ n → 2 * i + 3 ≤ m
h : ¬n < (2 * i + 3) * (2 * i + 3)
⊢ 2 ≤ 2 * i + 3
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
[PROOFSTEP]
have k0 : 0 < k := lt_of_lt_of_le (by decide) k2
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
[PROOFSTEP]
have IH : ∀ n', n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (n'.minSqFacAux (k + 2)) :=
  by
  intro n' nd' nk
  have hn' := le_of_dvd n0 nd'
  refine'
    have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k :=
      lt_of_le_of_lt (Nat.sub_le_sub_right (Nat.sqrt_le_sqrt hn') _) (Nat.minFac_lemma n k h)
    @minSqFacAux_has_prop n' (k + 2) (pos_of_dvd_of_pos nd' n0) (i + 1) (by simp [e, left_distrib]) fun m m2 d => _
  cases' Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with me ml
  · subst me
    contradiction
  apply (Nat.eq_or_lt_of_le ml).resolve_left
  intro me
  rw [← me, e] at d 
  change 2 * (i + 2) ∣ n' at d 
  have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd')
  rw [e] at this 
  exact absurd this (by linarith)
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
⊢ ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
[PROOFSTEP]
intro n' nd' nk
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
⊢ MinSqFacProp n' (minSqFacAux n' (k + 2))
[PROOFSTEP]
have hn' := le_of_dvd n0 nd'
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
⊢ MinSqFacProp n' (minSqFacAux n' (k + 2))
[PROOFSTEP]
refine'
  have : Nat.sqrt n' - k < Nat.sqrt n + 2 - k :=
    lt_of_le_of_lt (Nat.sub_le_sub_right (Nat.sqrt_le_sqrt hn') _) (Nat.minFac_lemma n k h)
  @minSqFacAux_has_prop n' (k + 2) (pos_of_dvd_of_pos nd' n0) (i + 1) (by simp [e, left_distrib]) fun m m2 d => _
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
⊢ k + 2 = 2 * (i + 1) + 3
[PROOFSTEP]
simp [e, left_distrib]
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
⊢ k + 2 ≤ m
[PROOFSTEP]
cases' Nat.eq_or_lt_of_le (ih m m2 (dvd_trans d nd')) with me ml
[GOAL]
case inl
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
me : k = m
⊢ k + 2 ≤ m
[PROOFSTEP]
subst me
[GOAL]
case inl
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m2 : Prime k
d : k ∣ n'
⊢ k + 2 ≤ k
[PROOFSTEP]
contradiction
[GOAL]
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
⊢ k + 2 ≤ m
[PROOFSTEP]
apply (Nat.eq_or_lt_of_le ml).resolve_left
[GOAL]
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
⊢ ¬succ k = m
[PROOFSTEP]
intro me
[GOAL]
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : m ∣ n'
ml : k < m
me : succ k = m
⊢ False
[PROOFSTEP]
rw [← me, e] at d 
[GOAL]
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
d : succ (2 * i + 3) ∣ n'
ml : k < m
me : succ k = m
⊢ False
[PROOFSTEP]
change 2 * (i + 2) ∣ n' at d 
[GOAL]
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : succ k = m
d : 2 * (i + 2) ∣ n'
⊢ False
[PROOFSTEP]
have := ih _ prime_two (dvd_trans (dvd_of_mul_right_dvd d) nd')
[GOAL]
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : succ k = m
d : 2 * (i + 2) ∣ n'
this : k ≤ 2
⊢ False
[PROOFSTEP]
rw [e] at this 
[GOAL]
case inr
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : succ k = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ False
[PROOFSTEP]
exact absurd this (by linarith)
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
this✝ : sqrt n' - k < sqrt n + 2 - k
m : ℕ
m2 : Prime m
ml : k < m
me : succ k = m
d : 2 * (i + 2) ∣ n'
this : 2 * i + 3 ≤ 2
⊢ ¬2 * i + 3 ≤ 2
[PROOFSTEP]
linarith
[GOAL]
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
[PROOFSTEP]
have pk : k ∣ n → Prime k :=
  by
  refine' fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) _⟩
  exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
⊢ k ∣ n → Prime k
[PROOFSTEP]
refine' fun dk => prime_def_minFac.2 ⟨k2, le_antisymm (minFac_le k0) _⟩
[GOAL]
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
dk : k ∣ n
⊢ k ≤ minFac k
[PROOFSTEP]
exact ih _ (minFac_prime (ne_of_gt k2)) (dvd_trans (minFac_dvd _) dk)
[GOAL]
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
⊢ MinSqFacProp n (if k ∣ n then if k ∣ n / k then some k else minSqFacAux (n / k) (k + 2) else minSqFacAux n (k + 2))
[PROOFSTEP]
split_ifs with dk dkk
[GOAL]
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : k ∣ n / k
⊢ MinSqFacProp n (some k)
[PROOFSTEP]
exact ⟨pk dk, (Nat.dvd_div_iff dk).1 dkk, fun p pp d => ih p pp (dvd_trans ⟨_, rfl⟩ d)⟩
[GOAL]
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
⊢ MinSqFacProp n (minSqFacAux (n / k) (k + 2))
[PROOFSTEP]
specialize IH (n / k) (div_dvd_of_dvd dk) dkk
[GOAL]
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
pk : k ∣ n → Prime k
dk : k ∣ n
dkk : ¬k ∣ n / k
IH : MinSqFacProp (n / k) (minSqFacAux (n / k) (k + 2))
⊢ MinSqFacProp n (minSqFacAux (n / k) (k + 2))
[PROOFSTEP]
exact minSqFacProp_div _ (pk dk) dk (mt (Nat.dvd_div_iff dk).2 dkk) IH
[GOAL]
case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
IH : ∀ (n' : ℕ), n' ∣ n → ¬k ∣ n' → MinSqFacProp n' (minSqFacAux n' (k + 2))
pk : k ∣ n → Prime k
dk : ¬k ∣ n
⊢ MinSqFacProp n (minSqFacAux n (k + 2))
[PROOFSTEP]
exact IH n (dvd_refl _) dk
[GOAL]
n : ℕ
⊢ MinSqFacProp n (minSqFac n)
[PROOFSTEP]
dsimp only [minSqFac]
[GOAL]
n : ℕ
⊢ MinSqFacProp n (if 2 ∣ n then if 2 ∣ n / 2 then some 2 else minSqFacAux (n / 2) 3 else minSqFacAux n 3)
[PROOFSTEP]
split_ifs with d2 d4
[GOAL]
case pos
n : ℕ
d2 : 2 ∣ n
d4 : 2 ∣ n / 2
⊢ MinSqFacProp n (some 2)
[PROOFSTEP]
exact ⟨prime_two, (dvd_div_iff d2).1 d4, fun p pp _ => pp.two_le⟩
[GOAL]
case neg
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
⊢ MinSqFacProp n (minSqFacAux (n / 2) 3)
[PROOFSTEP]
cases' Nat.eq_zero_or_pos n with n0 n0
[GOAL]
case neg.inl
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n = 0
⊢ MinSqFacProp n (minSqFacAux (n / 2) 3)
[PROOFSTEP]
subst n0
[GOAL]
case neg.inl
d2 : 2 ∣ 0
d4 : ¬2 ∣ 0 / 2
⊢ MinSqFacProp 0 (minSqFacAux (0 / 2) 3)
[PROOFSTEP]
cases d4 (by decide)
[GOAL]
d2 : 2 ∣ 0
d4 : ¬2 ∣ 0 / 2
⊢ 2 ∣ 0 / 2
[PROOFSTEP]
decide
[GOAL]
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ MinSqFacProp n (minSqFacAux (n / 2) 3)
[PROOFSTEP]
refine' minSqFacProp_div _ prime_two d2 (mt (dvd_div_iff d2).2 d4) _
[GOAL]
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ MinSqFacProp (n / 2) (minSqFacAux (n / 2) 3)
[PROOFSTEP]
refine' minSqFacAux_has_prop 3 (Nat.div_pos (le_of_dvd n0 d2) (by decide)) 0 rfl _
[GOAL]
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n / 2 → 3 ≤ m
[PROOFSTEP]
refine' fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le _)
[GOAL]
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n / 2
⊢ 2 ≠ p
[PROOFSTEP]
rintro rfl
[GOAL]
case neg.inr
n : ℕ
d2 : 2 ∣ n
d4 : ¬2 ∣ n / 2
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n / 2
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg
n : ℕ
d2 : ¬2 ∣ n
⊢ MinSqFacProp n (minSqFacAux n 3)
[PROOFSTEP]
cases' Nat.eq_zero_or_pos n with n0 n0
[GOAL]
case neg.inl
n : ℕ
d2 : ¬2 ∣ n
n0 : n = 0
⊢ MinSqFacProp n (minSqFacAux n 3)
[PROOFSTEP]
subst n0
[GOAL]
case neg.inl
d2 : ¬2 ∣ 0
⊢ MinSqFacProp 0 (minSqFacAux 0 3)
[PROOFSTEP]
cases d2 (by decide)
[GOAL]
d2 : ¬2 ∣ 0
⊢ 2 ∣ 0
[PROOFSTEP]
decide
[GOAL]
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ MinSqFacProp n (minSqFacAux n 3)
[PROOFSTEP]
refine' minSqFacAux_has_prop _ n0 0 rfl _
[GOAL]
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
⊢ ∀ (m : ℕ), Prime m → m ∣ n → 3 ≤ m
[PROOFSTEP]
refine' fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le _)
[GOAL]
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
p : ℕ
pp : Prime p
dp : p ∣ n
⊢ 2 ≠ p
[PROOFSTEP]
rintro rfl
[GOAL]
case neg.inr
n : ℕ
d2 : ¬2 ∣ n
n0 : n > 0
pp : Prime 2
dp : 2 ∣ n
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
n d : ℕ
h : minSqFac n = some d
⊢ Prime d
[PROOFSTEP]
have := minSqFac_has_prop n
[GOAL]
n d : ℕ
h : minSqFac n = some d
this : MinSqFacProp n (minSqFac n)
⊢ Prime d
[PROOFSTEP]
rw [h] at this 
[GOAL]
n d : ℕ
h : minSqFac n = some d
this : MinSqFacProp n (some d)
⊢ Prime d
[PROOFSTEP]
exact this.1
[GOAL]
n d : ℕ
h : minSqFac n = some d
⊢ d * d ∣ n
[PROOFSTEP]
have := minSqFac_has_prop n
[GOAL]
n d : ℕ
h : minSqFac n = some d
this : MinSqFacProp n (minSqFac n)
⊢ d * d ∣ n
[PROOFSTEP]
rw [h] at this 
[GOAL]
n d : ℕ
h : minSqFac n = some d
this : MinSqFacProp n (some d)
⊢ d * d ∣ n
[PROOFSTEP]
exact this.2.1
[GOAL]
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
⊢ d ≤ m
[PROOFSTEP]
have := minSqFac_has_prop n
[GOAL]
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : MinSqFacProp n (minSqFac n)
⊢ d ≤ m
[PROOFSTEP]
rw [h] at this 
[GOAL]
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : MinSqFacProp n (some d)
⊢ d ≤ m
[PROOFSTEP]
have fd := minFac_dvd m
[GOAL]
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : MinSqFacProp n (some d)
fd : minFac m ∣ m
⊢ d ≤ m
[PROOFSTEP]
exact
  le_trans (this.2.2 _ (minFac_prime <| ne_of_gt m2) (dvd_trans (mul_dvd_mul fd fd) md))
    (minFac_le <| lt_of_lt_of_le (by decide) m2)
[GOAL]
n d : ℕ
h : minSqFac n = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : MinSqFacProp n (some d)
fd : minFac m ∣ m
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ Squarefree n ↔ minSqFac n = none
[PROOFSTEP]
have := minSqFac_has_prop n
[GOAL]
n : ℕ
this : MinSqFacProp n (minSqFac n)
⊢ Squarefree n ↔ minSqFac n = none
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
this : MinSqFacProp n (minSqFac n)
⊢ Squarefree n → minSqFac n = none
[PROOFSTEP]
intro H
[GOAL]
case mpr
n : ℕ
this : MinSqFacProp n (minSqFac n)
⊢ minSqFac n = none → Squarefree n
[PROOFSTEP]
intro H
[GOAL]
case mp
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : Squarefree n
⊢ minSqFac n = none
[PROOFSTEP]
cases' e : n.minSqFac with d
[GOAL]
case mp.none
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : Squarefree n
e : minSqFac n = none
⊢ none = none
[PROOFSTEP]
rfl
[GOAL]
case mp.some
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : Squarefree n
d : ℕ
e : minSqFac n = some d
⊢ some d = none
[PROOFSTEP]
rw [e] at this 
[GOAL]
case mp.some
n : ℕ
H : Squarefree n
d : ℕ
this : MinSqFacProp n (some d)
e : minSqFac n = some d
⊢ some d = none
[PROOFSTEP]
cases squarefree_iff_prime_squarefree.1 H _ this.1 this.2.1
[GOAL]
case mpr
n : ℕ
this : MinSqFacProp n (minSqFac n)
H : minSqFac n = none
⊢ Squarefree n
[PROOFSTEP]
rwa [H] at this 
[GOAL]
⊢ Squarefree 2
[PROOFSTEP]
rw [squarefree_iff_nodup_factors]
[GOAL]
⊢ List.Nodup (factors 2)
[PROOFSTEP]
norm_num
[GOAL]
⊢ 2 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
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
[PROOFSTEP]
rw [(Finset.nodup _).ext ((Finset.nodup _).map_on _)]
[GOAL]
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
[PROOFSTEP]
intro a
[GOAL]
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
[PROOFSTEP]
simp only [Multiset.mem_filter, id.def, Multiset.mem_map, Finset.filter_val, ← Finset.mem_def, mem_divisors]
[GOAL]
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
[PROOFSTEP]
constructor
[GOAL]
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
[PROOFSTEP]
rintro ⟨⟨an, h0⟩, hsq⟩
[GOAL]
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
[PROOFSTEP]
use(UniqueFactorizationMonoid.normalizedFactors a).toFinset
[GOAL]
case h
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
[PROOFSTEP]
simp only [id.def, Finset.mem_powerset]
[GOAL]
case h
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
[PROOFSTEP]
rcases an with ⟨b, rfl⟩
[GOAL]
case h.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
[PROOFSTEP]
rw [mul_ne_zero_iff] at h0 
[GOAL]
case h.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
[PROOFSTEP]
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0.1] at hsq 
[GOAL]
case h.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
[PROOFSTEP]
rw [Multiset.toFinset_subset, Multiset.toFinset_val, hsq.dedup, ← associated_iff_eq, normalizedFactors_mul h0.1 h0.2]
[GOAL]
case h.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
[PROOFSTEP]
exact ⟨Multiset.subset_of_le (Multiset.le_add_right _ _), normalizedFactors_prod h0.1⟩
[GOAL]
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
[PROOFSTEP]
rintro ⟨s, hs, rfl⟩
[GOAL]
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)
[PROOFSTEP]
rw [Finset.mem_powerset, ← Finset.val_le_iff, Multiset.toFinset_val] at hs 
[GOAL]
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)
[PROOFSTEP]
have hs0 : s.val.prod ≠ 0 := by
  rw [Ne.def, Multiset.prod_eq_zero_iff]
  intro con
  apply not_irreducible_zero (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))
[GOAL]
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
⊢ Multiset.prod s.val ≠ 0
[PROOFSTEP]
rw [Ne.def, Multiset.prod_eq_zero_iff]
[GOAL]
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
⊢ ¬0 ∈ s.val
[PROOFSTEP]
intro con
[GOAL]
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ Multiset.dedup (normalizedFactors n)
con : 0 ∈ s.val
⊢ False
[PROOFSTEP]
apply not_irreducible_zero (irreducible_of_normalized_factor 0 (Multiset.mem_dedup.1 (Multiset.mem_of_le hs con)))
[GOAL]
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)
[PROOFSTEP]
rw [(normalizedFactors_prod h0).symm.dvd_iff_dvd_right]
[GOAL]
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)
[PROOFSTEP]
refine' ⟨⟨Multiset.prod_dvd_prod_of_le (le_trans hs (Multiset.dedup_le _)), h0⟩, _⟩
[GOAL]
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)
[PROOFSTEP]
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)
[GOAL]
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)
[PROOFSTEP]
rw [associated_eq_eq, Multiset.rel_eq] at h 
[GOAL]
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)
[PROOFSTEP]
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors hs0, h]
[GOAL]
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
[PROOFSTEP]
apply s.nodup
[GOAL]
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
[PROOFSTEP]
intro x hx y hy h
[GOAL]
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
[PROOFSTEP]
rw [← Finset.val_inj, ← Multiset.rel_eq, ← associated_eq_eq]
[GOAL]
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
[PROOFSTEP]
rw [← Finset.mem_def, Finset.mem_powerset] at hx hy 
[GOAL]
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
[PROOFSTEP]
apply UniqueFactorizationMonoid.factors_unique _ _ (associated_iff_eq.2 h)
[GOAL]
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
[PROOFSTEP]
intro z hz
[GOAL]
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
[PROOFSTEP]
apply irreducible_of_normalized_factor z
[GOAL]
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.123482
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
⊢ ℕ
[PROOFSTEP]
rw [← Multiset.mem_toFinset]
[GOAL]
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.123482)
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
⊢ ℕ
[PROOFSTEP]
apply hx hz
[GOAL]
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
[PROOFSTEP]
intro z hz
[GOAL]
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
[PROOFSTEP]
apply irreducible_of_normalized_factor z
[GOAL]
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.123723
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
⊢ ℕ
[PROOFSTEP]
rw [← Multiset.mem_toFinset]
[GOAL]
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.123723)
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
⊢ ℕ
[PROOFSTEP]
apply hy hz
[GOAL]
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ ∑ i in Finset.filter Squarefree (divisors n), f i =
    ∑ i in Finset.powerset (Multiset.toFinset (normalizedFactors n)), f (Multiset.prod i.val)
[PROOFSTEP]
rw [Finset.sum_eq_multiset_sum, divisors_filter_squarefree h0, Multiset.map_map, Finset.sum_eq_multiset_sum]
[GOAL]
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ Multiset.sum
      (Multiset.map ((fun i => f i) ∘ fun x => Multiset.prod x.val)
        (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val) =
    Multiset.sum
      (Multiset.map (fun i => f (Multiset.prod i.val)) (Finset.powerset (Multiset.toFinset (normalizedFactors n))).val)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
hn : 0 < n
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
classical
  -- Porting note: This line is not needed in Lean 3
set S := (Finset.range (n + 1)).filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2)
have hSne : S.Nonempty := by
  use 1
  have h1 : 0 < n ∧ ∃ x : ℕ, 1 = x ^ 2 := ⟨hn, ⟨1, (one_pow 2).symm⟩⟩
  simp [h1]
let s := Finset.max' S hSne
have hs : s ∈ S := Finset.max'_mem S hSne
simp only [Finset.mem_filter, Finset.mem_range] at hs 
obtain ⟨-, ⟨a, hsa⟩, ⟨b, hsb⟩⟩ := hs
rw [hsa] at hn 
obtain ⟨hlts, hlta⟩ := CanonicallyOrderedCommSemiring.mul_pos.mp hn
rw [hsb] at hsa hn hlts 
refine' ⟨a, b, hlta, (pow_pos_iff zero_lt_two).mp hlts, hsa.symm, _⟩
rintro x ⟨y, hy⟩
rw [Nat.isUnit_iff]
by_contra hx
refine'
  lt_le_antisymm _
    (Finset.le_max' S ((b * x) ^ 2) _)
      -- Porting note: these two goals were in the opposite order in Lean 3
· convert
    lt_mul_of_one_lt_right hlts
      (one_lt_pow 2 x zero_lt_two (one_lt_iff_ne_zero_and_ne_one.mpr ⟨fun h => by simp_all, hx⟩)) using
    1
  rw [mul_pow]
· simp_rw [hsa, Finset.mem_filter, Finset.mem_range]
  refine' ⟨lt_succ_iff.mpr (le_of_dvd hn _), _, ⟨b * x, rfl⟩⟩ <;> use y <;> rw [hy] <;> ring
[GOAL]
n : ℕ
hn : 0 < n
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
set S := (Finset.range (n + 1)).filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2)
[GOAL]
n : ℕ
hn : 0 < n
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
have hSne : S.Nonempty := by
  use 1
  have h1 : 0 < n ∧ ∃ x : ℕ, 1 = x ^ 2 := ⟨hn, ⟨1, (one_pow 2).symm⟩⟩
  simp [h1]
[GOAL]
n : ℕ
hn : 0 < n
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
⊢ Finset.Nonempty S
[PROOFSTEP]
use 1
[GOAL]
case h
n : ℕ
hn : 0 < n
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
⊢ 1 ∈ S
[PROOFSTEP]
have h1 : 0 < n ∧ ∃ x : ℕ, 1 = x ^ 2 := ⟨hn, ⟨1, (one_pow 2).symm⟩⟩
[GOAL]
case h
n : ℕ
hn : 0 < n
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
h1 : 0 < n ∧ ∃ x, 1 = x ^ 2
⊢ 1 ∈ S
[PROOFSTEP]
simp [h1]
[GOAL]
n : ℕ
hn : 0 < n
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
let s := Finset.max' S hSne
[GOAL]
n : ℕ
hn : 0 < n
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
have hs : s ∈ S := Finset.max'_mem S hSne
[GOAL]
n : ℕ
hn : 0 < n
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
hs : s ∈ S
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
simp only [Finset.mem_filter, Finset.mem_range] at hs 
[GOAL]
n : ℕ
hn : 0 < n
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
hs :
  Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne < n + 1 ∧
    Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne ∣ n ∧
      ∃ x, Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = x ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
obtain ⟨-, ⟨a, hsa⟩, ⟨b, hsb⟩⟩ := hs
[GOAL]
case intro.intro.intro.intro
n : ℕ
hn : 0 < n
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a : ℕ
hsa : n = Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne * a
b : ℕ
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
rw [hsa] at hn 
[GOAL]
case intro.intro.intro.intro
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a : ℕ
hn : 0 < Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne * a
hsa : n = Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne * a
b : ℕ
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
obtain ⟨hlts, hlta⟩ := CanonicallyOrderedCommSemiring.mul_pos.mp hn
[GOAL]
case intro.intro.intro.intro.intro
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a : ℕ
hn : 0 < Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne * a
hsa : n = Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne * a
b : ℕ
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne
hlta : 0 < a
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
rw [hsb] at hsa hn hlts 
[GOAL]
case intro.intro.intro.intro.intro
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
refine' ⟨a, b, hlta, (pow_pos_iff zero_lt_two).mp hlts, hsa.symm, _⟩
[GOAL]
case intro.intro.intro.intro.intro
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
⊢ Squarefree a
[PROOFSTEP]
rintro x ⟨y, hy⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
⊢ IsUnit x
[PROOFSTEP]
rw [Nat.isUnit_iff]
[GOAL]
case intro.intro.intro.intro.intro.intro
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
⊢ x = 1
[PROOFSTEP]
by_contra hx
[GOAL]
case intro.intro.intro.intro.intro.intro
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ False
[PROOFSTEP]
refine'
  lt_le_antisymm _
    (Finset.le_max' S ((b * x) ^ 2) _)
      -- Porting note: these two goals were in the opposite order in Lean 3
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_1
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ Finset.max' S (_ : ∃ x, x ∈ S) < (b * x) ^ 2
[PROOFSTEP]
convert
  lt_mul_of_one_lt_right hlts
    (one_lt_pow 2 x zero_lt_two (one_lt_iff_ne_zero_and_ne_one.mpr ⟨fun h => by simp_all, hx⟩)) using
  1
[GOAL]
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
h : x = 0
⊢ False
[PROOFSTEP]
simp_all
[GOAL]
case h.e'_4
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 = b ^ 2 * x ^ 2
[PROOFSTEP]
rw [mul_pow]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∈ S
[PROOFSTEP]
simp_rw [hsa, Finset.mem_filter, Finset.mem_range]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 < b ^ 2 * a + 1 ∧ (b * x) ^ 2 ∣ b ^ 2 * a ∧ ∃ x_1, (b * x) ^ 2 = x_1 ^ 2
[PROOFSTEP]
refine' ⟨lt_succ_iff.mpr (le_of_dvd hn _), _, ⟨b * x, rfl⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.refine'_1
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∣ b ^ 2 * a
[PROOFSTEP]
use y
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.refine'_2
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ (b * x) ^ 2 ∣ b ^ 2 * a
[PROOFSTEP]
use y
[GOAL]
case h
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * a = (b * x) ^ 2 * y
[PROOFSTEP]
rw [hy]
[GOAL]
case h
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * a = (b * x) ^ 2 * y
[PROOFSTEP]
rw [hy]
[GOAL]
case h
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * (x * x * y) = (b * x) ^ 2 * y
[PROOFSTEP]
ring
[GOAL]
case h
n : ℕ
S : Finset ℕ := Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))
hSne : Finset.Nonempty S
s : ℕ := Finset.max' S hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : Finset.max' (Finset.filter (fun s => s ∣ n ∧ ∃ x, s = x ^ 2) (Finset.range (n + 1))) hSne = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * (x * x * y) = (b * x) ^ 2 * y
[PROOFSTEP]
ring
[GOAL]
n : ℕ
h : 0 < n
⊢ ∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)
[PROOFSTEP]
obtain ⟨a₁, b₁, ha₁, hb₁, hab₁, hab₂⟩ := sq_mul_squarefree_of_pos h
[GOAL]
case intro.intro.intro.intro.intro
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ ∃ a b, (b + 1) ^ 2 * (a + 1) = n ∧ Squarefree (a + 1)
[PROOFSTEP]
refine' ⟨a₁.pred, b₁.pred, _, _⟩
[GOAL]
case intro.intro.intro.intro.intro.refine'_1
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ (pred b₁ + 1) ^ 2 * (pred a₁ + 1) = n
[PROOFSTEP]
simpa only [add_one, succ_pred_eq_of_pos, ha₁, hb₁]
[GOAL]
case intro.intro.intro.intro.intro.refine'_2
n : ℕ
h : 0 < n
a₁ b₁ : ℕ
ha₁ : 0 < a₁
hb₁ : 0 < b₁
hab₁ : b₁ ^ 2 * a₁ = n
hab₂ : Squarefree a₁
⊢ Squarefree (pred a₁ + 1)
[PROOFSTEP]
simpa only [add_one, succ_pred_eq_of_pos, ha₁, hb₁]
[GOAL]
n : ℕ
⊢ ∃ a b, b ^ 2 * a = n ∧ Squarefree a
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
⊢ ∃ a b, b ^ 2 * a = zero ∧ Squarefree a
[PROOFSTEP]
exact ⟨1, 0, by simp, squarefree_one⟩
[GOAL]
⊢ 0 ^ 2 * 1 = zero
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
⊢ ∃ a b, b ^ 2 * a = succ n ∧ Squarefree a
[PROOFSTEP]
obtain ⟨a, b, -, -, h₁, h₂⟩ := sq_mul_squarefree_of_pos (succ_pos n)
[GOAL]
case succ.intro.intro.intro.intro.intro
n a b : ℕ
h₁ : b ^ 2 * a = succ n
h₂ : Squarefree a
⊢ ∃ a b, b ^ 2 * a = succ n ∧ Squarefree a
[PROOFSTEP]
exact ⟨a, b, h₁, h₂⟩
[GOAL]
m n : ℕ
hmn : coprime m n
⊢ Squarefree (m * n) ↔ Squarefree m ∧ Squarefree n
[PROOFSTEP]
simp only [squarefree_iff_prime_squarefree, ← sq, ← forall_and]
[GOAL]
m n : ℕ
hmn : coprime m n
⊢ (∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m * n) ↔ ∀ (x : ℕ), Prime x → ¬x ^ 2 ∣ m ∧ ¬x ^ 2 ∣ n
[PROOFSTEP]
refine' ball_congr fun p hp => _
[GOAL]
m n : ℕ
hmn : coprime m n
p : ℕ
hp : Prime p
⊢ ¬p ^ 2 ∣ m * n ↔ ¬p ^ 2 ∣ m ∧ ¬p ^ 2 ∣ n
[PROOFSTEP]
simp only [hmn.isPrimePow_dvd_mul (hp.isPrimePow.pow two_ne_zero), not_or]
[GOAL]
n : ℕ
hn : Squarefree n
⊢ ∏ p in List.toFinset (factors n), p = n
[PROOFSTEP]
erw [List.prod_toFinset _ hn.nodup_factors, List.map_id, Nat.prod_factors hn.ne_zero]
