[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]


[GOAL]
n : ℕ
⊢ fib (n + 2) = fib n + fib (n + 1)
[PROOFSTEP]
simp [fib, Function.iterate_succ_apply']
[GOAL]
n : ℕ
⊢ fib n ≤ fib (n + 1)
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ fib zero ≤ fib (zero + 1)
[PROOFSTEP]
simp [fib_add_two]
[GOAL]
case succ
n✝ : ℕ
⊢ fib (succ n✝) ≤ fib (succ n✝ + 1)
[PROOFSTEP]
simp [fib_add_two]
[GOAL]
n : ℕ
n_pos : 0 < n
⊢ 0 < fib 1
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ fib (n + 2) - fib (n + 1) = fib n
[PROOFSTEP]
rw [fib_add_two, add_tsub_cancel_right]
[GOAL]
n : ℕ
hn : 2 ≤ n
⊢ fib n < fib (n + 1)
[PROOFSTEP]
rcases exists_add_of_le hn with ⟨n, rfl⟩
[GOAL]
case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ fib (2 + n) < fib (2 + n + 1)
[PROOFSTEP]
rw [← tsub_pos_iff_lt, add_comm 2, fib_add_two_sub_fib_add_one]
[GOAL]
case intro
n : ℕ
hn : 2 ≤ 2 + n
⊢ 0 < fib (n + 1)
[PROOFSTEP]
apply fib_pos (succ_pos n)
[GOAL]
⊢ StrictMono fun n => fib (n + 2)
[PROOFSTEP]
refine' strictMono_nat_of_lt_succ fun n => _
[GOAL]
n : ℕ
⊢ fib (n + 2) < fib (n + 1 + 2)
[PROOFSTEP]
rw [add_right_comm]
[GOAL]
n : ℕ
⊢ fib (n + 2) < fib (n + 2 + 1)
[PROOFSTEP]
exact fib_lt_fib_succ (self_le_add_left _ _)
[GOAL]
n : ℕ
five_le_n : 5 ≤ n
⊢ n ≤ fib n
[PROOFSTEP]
induction' five_le_n with n five_le_n IH
[GOAL]
case refl
n : ℕ
⊢ 5 ≤ fib 5
[PROOFSTEP]
rfl
[GOAL]
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ succ n ≤ fib (succ n)
[PROOFSTEP]
rw [succ_le_iff]
[GOAL]
case step
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ n < fib (succ n)
[PROOFSTEP]
calc
  n ≤ fib n := IH
  _ < fib (n + 1) := fib_lt_fib_succ (le_trans (by decide) five_le_n)
[GOAL]
n✝ n : ℕ
five_le_n : Nat.le 5 n
IH : n ≤ fib n
⊢ 2 ≤ 5
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ coprime (fib n) (fib (n + 1))
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ coprime (fib zero) (fib (zero + 1))
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib (succ n + 1))
[PROOFSTEP]
rw [fib_add_two]
[GOAL]
case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib n + fib (n + 1))
[PROOFSTEP]
simp only [coprime_add_self_right]
[GOAL]
case succ
n : ℕ
ih : coprime (fib n) (fib (n + 1))
⊢ coprime (fib (succ n)) (fib n)
[PROOFSTEP]
simp [coprime, ih.symm]
[GOAL]
m n : ℕ
⊢ fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
[PROOFSTEP]
induction' n with n ih generalizing m
[GOAL]
case zero
m✝ m : ℕ
⊢ fib (m + zero + 1) = fib m * fib zero + fib (m + 1) * fib (zero + 1)
[PROOFSTEP]
simp
[GOAL]
case succ
m✝ n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
[PROOFSTEP]
intros
[GOAL]
case succ
m✝ n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
[PROOFSTEP]
specialize ih (m + 1)
[GOAL]
case succ
m✝ n m : ℕ
ih : fib (m + 1 + n + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
[PROOFSTEP]
rw [add_assoc m 1 n, add_comm 1 n] at ih
[GOAL]
case succ
m✝ n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + succ n + 1) = fib m * fib (succ n) + fib (m + 1) * fib (succ n + 1)
[PROOFSTEP]
simp only [fib_add_two, ih]
[GOAL]
case succ
m✝ n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + 1) * fib n + (fib m + fib (m + 1)) * fib (n + 1) = fib m * fib (succ n) + fib (m + 1) * (fib n + fib (n + 1))
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ fib (2 * n) = fib n * (2 * fib (n + 1) - fib n)
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ fib (2 * zero) = fib zero * (2 * fib (zero + 1) - fib zero)
[PROOFSTEP]
simp
[GOAL]
case succ
n✝ : ℕ
⊢ fib (2 * succ n✝) = fib (succ n✝) * (2 * fib (succ n✝ + 1) - fib (succ n✝))
[PROOFSTEP]
rw [Nat.succ_eq_add_one, two_mul, ← add_assoc, fib_add, fib_add_two, two_mul]
[GOAL]
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) =
    fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + (fib n✝ + fib (n✝ + 1)) - fib (n✝ + 1))
[PROOFSTEP]
simp only [← add_assoc, add_tsub_cancel_right]
[GOAL]
case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) = fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + fib n✝)
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ fib (2 * n + 1) = fib (n + 1) ^ 2 + fib n ^ 2
[PROOFSTEP]
rw [two_mul, fib_add]
[GOAL]
n : ℕ
⊢ fib n * fib n + fib (n + 1) * fib (n + 1) = fib (n + 1) ^ 2 + fib n ^ 2
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ fib (2 * n + 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
[PROOFSTEP]
rw [fib_add_two, fib_two_mul, fib_two_mul_add_one]
  -- porting note: A bunch of issues similar to [this zulip thread](https://github.com/leanprover-community/mathlib4/pull/1576) with `zify`
[GOAL]
n : ℕ
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
[PROOFSTEP]
have : fib n ≤ 2 * fib (n + 1) := le_trans (fib_le_fib_succ) (mul_comm 2 _ ▸ le_mul_of_pos_right two_pos)
[GOAL]
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ fib n * (2 * fib (n + 1) - fib n) + (fib (n + 1) ^ 2 + fib n ^ 2) = fib (n + 1) * (2 * fib n + fib (n + 1))
[PROOFSTEP]
zify [this]
[GOAL]
n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ ↑(fib n) * (2 * ↑(fib (n + 1)) - ↑(fib n)) + (↑(fib (n + 1)) ^ 2 + ↑(fib n) ^ 2) =
    ↑(fib (n + 1)) * (2 * ↑(fib n) + ↑(fib (n + 1)))
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ fib (bit0 n) = fib n * (2 * fib (n + 1) - fib n)
[PROOFSTEP]
rw [bit0_eq_two_mul, fib_two_mul]
[GOAL]
n : ℕ
⊢ fib (bit1 n) = fib (n + 1) ^ 2 + fib n ^ 2
[PROOFSTEP]
rw [Nat.bit1_eq_succ_bit0, bit0_eq_two_mul, fib_two_mul_add_one]
[GOAL]
n : ℕ
⊢ fib (bit1 n + 1) = fib (n + 1) * (2 * fib n + fib (n + 1))
[PROOFSTEP]
rw [Nat.bit1_eq_succ_bit0, bit0_eq_two_mul, fib_two_mul_add_two]
[GOAL]
n : ℕ
⊢ fastFibAux (bit false n) =
    let p := fastFibAux n;
    (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2)
[PROOFSTEP]
rw [fastFibAux, binaryRec_eq]
[GOAL]
n : ℕ
⊢ (if false = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).snd *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).fst +
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).fst *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).snd -
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst),
        (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2)) =
    let p :=
      binaryRec (fib 0, fib 1)
        (fun b x p =>
          if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
          else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
        n;
    (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2)
[PROOFSTEP]
rfl
[GOAL]
case h
n : ℕ
⊢ (if false = true then
      ((fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2,
        (fib 0, fib 1).snd * (2 * (fib 0, fib 1).fst + (fib 0, fib 1).snd))
    else
      ((fib 0, fib 1).fst * (2 * (fib 0, fib 1).snd - (fib 0, fib 1).fst),
        (fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2)) =
    (fib 0, fib 1)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ fastFibAux (bit true n) =
    let p := fastFibAux n;
    (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
[PROOFSTEP]
rw [fastFibAux, binaryRec_eq]
[GOAL]
n : ℕ
⊢ (if true = true then
      ((binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2,
        (binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).snd *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).fst +
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd))
    else
      ((binaryRec (fib 0, fib 1)
              (fun b x p =>
                if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
              n).fst *
          (2 *
              (binaryRec (fib 0, fib 1)
                  (fun b x p =>
                    if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                    else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                  n).snd -
            (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst),
        (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).snd ^
            2 +
          (binaryRec (fib 0, fib 1)
                (fun b x p =>
                  if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
                  else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
                n).fst ^
            2)) =
    let p :=
      binaryRec (fib 0, fib 1)
        (fun b x p =>
          if b = true then (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
          else (p.fst * (2 * p.snd - p.fst), p.snd ^ 2 + p.fst ^ 2))
        n;
    (p.snd ^ 2 + p.fst ^ 2, p.snd * (2 * p.fst + p.snd))
[PROOFSTEP]
rfl
[GOAL]
case h
n : ℕ
⊢ (if false = true then
      ((fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2,
        (fib 0, fib 1).snd * (2 * (fib 0, fib 1).fst + (fib 0, fib 1).snd))
    else
      ((fib 0, fib 1).fst * (2 * (fib 0, fib 1).snd - (fib 0, fib 1).fst),
        (fib 0, fib 1).snd ^ 2 + (fib 0, fib 1).fst ^ 2)) =
    (fib 0, fib 1)
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ fastFibAux n = (fib n, fib (n + 1))
[PROOFSTEP]
apply Nat.binaryRec _ (fun b n' ih => _) n
[GOAL]
n : ℕ
⊢ fastFibAux 0 = (fib 0, fib (0 + 1))
[PROOFSTEP]
simp [fastFibAux]
[GOAL]
n : ℕ
⊢ ∀ (b : Bool) (n' : ℕ),
    fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
[PROOFSTEP]
intro b
[GOAL]
n : ℕ
b : Bool
⊢ ∀ (n' : ℕ), fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
[PROOFSTEP]
intro n'
[GOAL]
n : ℕ
b : Bool
n' : ℕ
⊢ fastFibAux n' = (fib n', fib (n' + 1)) → fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
[PROOFSTEP]
intro ih
[GOAL]
n : ℕ
b : Bool
n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fastFibAux (bit b n') = (fib (bit b n'), fib (bit b n' + 1))
[PROOFSTEP]
cases b
[GOAL]
case false
n n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fastFibAux (bit false n') = (fib (bit false n'), fib (bit false n' + 1))
[PROOFSTEP]
simp only [fast_fib_aux_bit_ff, fast_fib_aux_bit_tt, congr_arg Prod.fst ih, congr_arg Prod.snd ih, Prod.mk.inj_iff]
[GOAL]
case true
n n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fastFibAux (bit true n') = (fib (bit true n'), fib (bit true n' + 1))
[PROOFSTEP]
simp only [fast_fib_aux_bit_ff, fast_fib_aux_bit_tt, congr_arg Prod.fst ih, congr_arg Prod.snd ih, Prod.mk.inj_iff]
[GOAL]
case false
n n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fib n' * (2 * fib (n' + 1) - fib n') = fib (bit false n') ∧ fib (n' + 1) ^ 2 + fib n' ^ 2 = fib (bit false n' + 1)
[PROOFSTEP]
simp [bit, fib_bit0, fib_bit1, fib_bit0_succ, fib_bit1_succ]
[GOAL]
case true
n n' : ℕ
ih : fastFibAux n' = (fib n', fib (n' + 1))
⊢ fib (n' + 1) ^ 2 + fib n' ^ 2 = fib (bit true n') ∧ fib (n' + 1) * (2 * fib n' + fib (n' + 1)) = fib (bit true n' + 1)
[PROOFSTEP]
simp [bit, fib_bit0, fib_bit1, fib_bit0_succ, fib_bit1_succ]
[GOAL]
n : ℕ
⊢ fastFib n = fib n
[PROOFSTEP]
rw [fastFib, fast_fib_aux_eq]
[GOAL]
m n : ℕ
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
[PROOFSTEP]
cases' Nat.eq_zero_or_pos n with h h
[GOAL]
case inl
m n : ℕ
h : n = 0
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
[PROOFSTEP]
rw [h]
[GOAL]
case inl
m n : ℕ
h : n = 0
⊢ gcd (fib m) (fib (0 + m)) = gcd (fib m) (fib 0)
[PROOFSTEP]
simp
[GOAL]
case inr
m n : ℕ
h : n > 0
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
[PROOFSTEP]
replace h := Nat.succ_pred_eq_of_pos h
[GOAL]
case inr
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)
[PROOFSTEP]
rw [← h, succ_eq_add_one]
[GOAL]
case inr
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n + 1 + m)) = gcd (fib m) (fib (pred n + 1))
[PROOFSTEP]
calc
  gcd (fib m) (fib (n.pred + 1 + m)) = gcd (fib m) (fib n.pred * fib m + fib (n.pred + 1) * fib (m + 1)) :=
    by
    rw [← fib_add n.pred _]
    ring_nf
  _ = gcd (fib m) (fib (n.pred + 1) * fib (m + 1)) := by rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
  _ = gcd (fib m) (fib (n.pred + 1)) :=
    coprime.gcd_mul_right_cancel_right (fib (n.pred + 1)) (coprime.symm (fib_coprime_fib_succ m))
[GOAL]
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n + 1 + m)) = gcd (fib m) (fib (pred n) * fib m + fib (pred n + 1) * fib (m + 1))
[PROOFSTEP]
rw [← fib_add n.pred _]
[GOAL]
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n + 1 + m)) = gcd (fib m) (fib (pred n + m + 1))
[PROOFSTEP]
ring_nf
[GOAL]
m n : ℕ
h : succ (pred n) = n
⊢ gcd (fib m) (fib (pred n) * fib m + fib (pred n + 1) * fib (m + 1)) = gcd (fib m) (fib (pred n + 1) * fib (m + 1))
[PROOFSTEP]
rw [add_comm, gcd_add_mul_right_right (fib m) _ (fib n.pred)]
[GOAL]
m n : ℕ
⊢ gcd (fib m) (fib (n + 0 * m)) = gcd (fib m) (fib n)
[PROOFSTEP]
simp
[GOAL]
m n k : ℕ
⊢ gcd (fib m) (fib (n + (k + 1) * m)) = gcd (fib m) (fib n)
[PROOFSTEP]
rw [← gcd_fib_add_mul_self m n k, add_mul, ← add_assoc, one_mul, gcd_fib_add_self _ _]
[GOAL]
m n : ℕ
⊢ fib (gcd m n) = gcd (fib m) (fib n)
[PROOFSTEP]
induction m, n using Nat.gcd.induction with
| H0 => simp
| H1 m n _ h' =>
  rw [← gcd_rec m n] at h'
  conv_rhs => rw [← mod_add_div' n m]
  rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
[GOAL]
m n : ℕ
⊢ fib (gcd m n) = gcd (fib m) (fib n)
[PROOFSTEP]
induction m, n using Nat.gcd.induction with
| H0 => simp
| H1 m n _ h' =>
  rw [← gcd_rec m n] at h'
  conv_rhs => rw [← mod_add_div' n m]
  rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
[GOAL]
case H0
n✝ : ℕ
⊢ fib (gcd 0 n✝) = gcd (fib 0) (fib n✝)
[PROOFSTEP]

| H0 => simp
[GOAL]
case H0
n✝ : ℕ
⊢ fib (gcd 0 n✝) = gcd (fib 0) (fib n✝)
[PROOFSTEP]
simp
[GOAL]
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd (n % m) m) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib n)
[PROOFSTEP]

| H1 m n _ h' =>
  rw [← gcd_rec m n] at h'
  conv_rhs => rw [← mod_add_div' n m]
  rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
[GOAL]
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd (n % m) m) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib n)
[PROOFSTEP]
rw [← gcd_rec m n] at h'
[GOAL]
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib n)
[PROOFSTEP]
conv_rhs => rw [← mod_add_div' n m]
[GOAL]
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
| gcd (fib m) (fib n)
[PROOFSTEP]
rw [← mod_add_div' n m]
[GOAL]
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
| gcd (fib m) (fib n)
[PROOFSTEP]
rw [← mod_add_div' n m]
[GOAL]
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
| gcd (fib m) (fib n)
[PROOFSTEP]
rw [← mod_add_div' n m]
[GOAL]
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (gcd m n) = gcd (fib (n % m)) (fib m)
⊢ fib (gcd m n) = gcd (fib m) (fib (n % m + n / m * m))
[PROOFSTEP]
rwa [gcd_fib_add_mul_self m (n % m) (n / m), gcd_comm (fib m) _]
[GOAL]
m n : ℕ
h : m ∣ n
⊢ fib m ∣ fib n
[PROOFSTEP]
rwa [gcd_eq_left_iff_dvd, ← fib_gcd, gcd_eq_left_iff_dvd.mp]
[GOAL]
n : ℕ
h1 : fib (n + 1) = ∑ p in Finset.Nat.antidiagonal n, choose p.fst p.snd
h2 : fib (succ n + 1) = ∑ p in Finset.Nat.antidiagonal (succ n), choose p.fst p.snd
⊢ fib (succ (succ n) + 1) = ∑ p in Finset.Nat.antidiagonal (succ (succ n)), choose p.fst p.snd
[PROOFSTEP]
rw [fib_add_two, h1, h2, Finset.Nat.antidiagonal_succ_succ', Finset.Nat.antidiagonal_succ']
[GOAL]
n : ℕ
h1 : fib (n + 1) = ∑ p in Finset.Nat.antidiagonal n, choose p.fst p.snd
h2 : fib (succ n + 1) = ∑ p in Finset.Nat.antidiagonal (succ n), choose p.fst p.snd
⊢ ∑ p in Finset.Nat.antidiagonal n, choose p.fst p.snd +
      ∑ p in
        Finset.cons (n + 1, 0)
          (Finset.map (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := succ, inj' := succ_injective })
            (Finset.Nat.antidiagonal n))
          (_ :
            ¬(n + 1, 0) ∈
                Finset.map
                  (Function.Embedding.prodMap (Function.Embedding.refl ℕ) { toFun := succ, inj' := succ_injective })
                  (Finset.Nat.antidiagonal n)),
        choose p.fst p.snd =
    ∑ p in
      Finset.cons (0, n + 2)
        (Finset.cons (n + 2, 0)
          (Finset.map
            (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
              { toFun := succ, inj' := succ_injective })
            (Finset.Nat.antidiagonal n))
          (_ :
            ¬(n + 2, 0) ∈
                Finset.map
                  (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
                    { toFun := succ, inj' := succ_injective })
                  (Finset.Nat.antidiagonal n)))
        (_ :
          ¬(0, n + 2) ∈
              Finset.cons (n + 2, 0)
                (Finset.map
                  (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
                    { toFun := succ, inj' := succ_injective })
                  (Finset.Nat.antidiagonal n))
                (_ :
                  ¬(n + 2, 0) ∈
                      Finset.map
                        (Function.Embedding.prodMap { toFun := succ, inj' := succ_injective }
                          { toFun := succ, inj' := succ_injective })
                        (Finset.Nat.antidiagonal n))),
      choose p.fst p.snd
[PROOFSTEP]
simp [choose_succ_succ, Finset.sum_add_distrib, add_left_comm]
[GOAL]
n : ℕ
⊢ fib (n + 1) = ∑ k in Finset.range n, fib k + 1
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
⊢ fib (zero + 1) = ∑ k in Finset.range zero, fib k + 1
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
ih : fib (n + 1) = ∑ k in Finset.range n, fib k + 1
⊢ fib (succ n + 1) = ∑ k in Finset.range (succ n), fib k + 1
[PROOFSTEP]
calc
  fib (n + 2) = fib n + fib (n + 1) := fib_add_two
  _ = (fib n + ∑ k in Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
  _ = (∑ k in Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]
[GOAL]
n : ℕ
ih : fib (n + 1) = ∑ k in Finset.range n, fib k + 1
⊢ fib n + fib (n + 1) = fib n + ∑ k in Finset.range n, fib k + 1
[PROOFSTEP]
rw [ih, add_assoc]
[GOAL]
n : ℕ
ih : fib (n + 1) = ∑ k in Finset.range n, fib k + 1
⊢ fib n + ∑ k in Finset.range n, fib k + 1 = ∑ k in Finset.range (n + 1), fib k + 1
[PROOFSTEP]
simp [Finset.range_add_one]