[GOAL]
n : ℕ
h : n ≠ 0
⊢ filter (fun x => x ∣ n) (range (succ n)) = divisors n
[PROOFSTEP]
ext
[GOAL]
case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ filter (fun x => x ∣ n) (range (succ n)) ↔ a✝ ∈ divisors n
[PROOFSTEP]
simp only [divisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
[GOAL]
case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < succ n → 1 ≤ a✝
[PROOFSTEP]
exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)
[GOAL]
n : ℕ
h : n ≠ 0
⊢ filter (fun x => x ∣ n) (range n) = properDivisors n
[PROOFSTEP]
ext
[GOAL]
case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∈ filter (fun x => x ∣ n) (range n) ↔ a✝ ∈ properDivisors n
[PROOFSTEP]
simp only [properDivisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
[GOAL]
case a
n : ℕ
h : n ≠ 0
a✝ : ℕ
⊢ a✝ ∣ n → a✝ < n → 1 ≤ a✝
[PROOFSTEP]
exact fun ha _ => succ_le_iff.mpr (pos_of_dvd_of_pos ha h.bot_lt)
[GOAL]
n : ℕ
⊢ ¬n ∈ properDivisors n
[PROOFSTEP]
simp [properDivisors]
[GOAL]
n m : ℕ
⊢ n ∈ properDivisors m ↔ n ∣ m ∧ n < m
[PROOFSTEP]
rcases eq_or_ne m 0 with (rfl | hm)
[GOAL]
case inl
n : ℕ
⊢ n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0
[PROOFSTEP]
simp [properDivisors]
[GOAL]
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ properDivisors m ↔ n ∣ m ∧ n < m
[PROOFSTEP]
simp only [and_comm, ← filter_dvd_eq_properDivisors hm, mem_filter, mem_range]
[GOAL]
n : ℕ
h : n ≠ 0
⊢ insert n (properDivisors n) = divisors n
[PROOFSTEP]
rw [divisors, properDivisors, Ico_succ_right_eq_insert_Ico (one_le_iff_ne_zero.2 h), Finset.filter_insert,
  if_pos (dvd_refl n)]
[GOAL]
n : ℕ
h : n ≠ 0
⊢ cons n (properDivisors n) (_ : ¬n ∈ properDivisors n) = divisors n
[PROOFSTEP]
rw [cons_eq_insert, insert_self_properDivisors h]
[GOAL]
n m : ℕ
⊢ n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0
[PROOFSTEP]
rcases eq_or_ne m 0 with (rfl | hm)
[GOAL]
case inl
n : ℕ
⊢ n ∈ divisors 0 ↔ n ∣ 0 ∧ 0 ≠ 0
[PROOFSTEP]
simp [divisors]
[GOAL]
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∈ divisors m ↔ n ∣ m ∧ m ≠ 0
[PROOFSTEP]
simp only [hm, Ne.def, not_false_iff, and_true_iff, ← filter_dvd_eq_divisors hm, mem_filter, mem_range,
  and_iff_right_iff_imp, lt_succ_iff]
[GOAL]
case inr
n m : ℕ
hm : m ≠ 0
⊢ n ∣ m → n ≤ m
[PROOFSTEP]
exact le_of_dvd hm.bot_lt
[GOAL]
n : ℕ
⊢ 1 ∈ divisors n ↔ n ≠ 0
[PROOFSTEP]
simp
[GOAL]
n m : ℕ
h : n ∈ divisors m
⊢ n ∣ m
[PROOFSTEP]
cases m
[GOAL]
case zero
n : ℕ
h : n ∈ divisors zero
⊢ n ∣ zero
[PROOFSTEP]
apply dvd_zero
[GOAL]
case succ
n n✝ : ℕ
h : n ∈ divisors (succ n✝)
⊢ n ∣ succ n✝
[PROOFSTEP]
simp [mem_divisors.1 h]
[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ x ∈ divisorsAntidiagonal n ↔ x.fst * x.snd = n ∧ n ≠ 0
[PROOFSTEP]
simp only [divisorsAntidiagonal, Finset.mem_Ico, Ne.def, Finset.mem_filter, Finset.mem_product]
[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ ((1 ≤ x.fst ∧ x.fst < n + 1) ∧ 1 ≤ x.snd ∧ x.snd < n + 1) ∧ x.fst * x.snd = n ↔ x.fst * x.snd = n ∧ ¬n = 0
[PROOFSTEP]
rw [and_comm]
[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ x.fst * x.snd = n ∧ (1 ≤ x.fst ∧ x.fst < n + 1) ∧ 1 ≤ x.snd ∧ x.snd < n + 1 ↔ x.fst * x.snd = n ∧ ¬n = 0
[PROOFSTEP]
apply and_congr_right
[GOAL]
case h
n : ℕ
x : ℕ × ℕ
⊢ x.fst * x.snd = n → ((1 ≤ x.fst ∧ x.fst < n + 1) ∧ 1 ≤ x.snd ∧ x.snd < n + 1 ↔ ¬n = 0)
[PROOFSTEP]
rintro rfl
[GOAL]
case h
x : ℕ × ℕ
⊢ (1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1) ∧ 1 ≤ x.snd ∧ x.snd < x.fst * x.snd + 1 ↔ ¬x.fst * x.snd = 0
[PROOFSTEP]
constructor
[GOAL]
case h.mp
x : ℕ × ℕ
⊢ (1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1) ∧ 1 ≤ x.snd ∧ x.snd < x.fst * x.snd + 1 → ¬x.fst * x.snd = 0
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
x : ℕ × ℕ
⊢ ¬x.fst * x.snd = 0 → (1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1) ∧ 1 ≤ x.snd ∧ x.snd < x.fst * x.snd + 1
[PROOFSTEP]
intro h
[GOAL]
case h.mp
x : ℕ × ℕ
h : (1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1) ∧ 1 ≤ x.snd ∧ x.snd < x.fst * x.snd + 1
⊢ ¬x.fst * x.snd = 0
[PROOFSTEP]
contrapose! h
[GOAL]
case h.mp
x : ℕ × ℕ
h : x.fst * x.snd = 0
⊢ 1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1 → 1 ≤ x.snd → x.fst * x.snd + 1 ≤ x.snd
[PROOFSTEP]
simp [h]
[GOAL]
case h.mpr
x : ℕ × ℕ
h : ¬x.fst * x.snd = 0
⊢ (1 ≤ x.fst ∧ x.fst < x.fst * x.snd + 1) ∧ 1 ≤ x.snd ∧ x.snd < x.fst * x.snd + 1
[PROOFSTEP]
rw [Nat.lt_add_one_iff, Nat.lt_add_one_iff]
[GOAL]
case h.mpr
x : ℕ × ℕ
h : ¬x.fst * x.snd = 0
⊢ (1 ≤ x.fst ∧ x.fst ≤ x.fst * x.snd) ∧ 1 ≤ x.snd ∧ x.snd ≤ x.fst * x.snd
[PROOFSTEP]
rw [mul_eq_zero, not_or] at h
[GOAL]
case h.mpr
x : ℕ × ℕ
h : ¬x.fst = 0 ∧ ¬x.snd = 0
⊢ (1 ≤ x.fst ∧ x.fst ≤ x.fst * x.snd) ∧ 1 ≤ x.snd ∧ x.snd ≤ x.fst * x.snd
[PROOFSTEP]
simp only [succ_le_of_lt (Nat.pos_of_ne_zero h.1), succ_le_of_lt (Nat.pos_of_ne_zero h.2), true_and_iff]
[GOAL]
case h.mpr
x : ℕ × ℕ
h : ¬x.fst = 0 ∧ ¬x.snd = 0
⊢ x.fst ≤ x.fst * x.snd ∧ x.snd ≤ x.fst * x.snd
[PROOFSTEP]
exact ⟨le_mul_of_pos_right (Nat.pos_of_ne_zero h.2), le_mul_of_pos_left (Nat.pos_of_ne_zero h.1)⟩
[GOAL]
n m : ℕ
⊢ n ∈ divisors m → n ≤ m
[PROOFSTEP]
cases' m with m
[GOAL]
case zero
n : ℕ
⊢ n ∈ divisors zero → n ≤ zero
[PROOFSTEP]
simp
[GOAL]
case succ
n m : ℕ
⊢ n ∈ divisors (succ m) → n ≤ succ m
[PROOFSTEP]
simp only [mem_divisors, Nat.succ_ne_zero m, and_true_iff, Ne.def, not_false_iff]
[GOAL]
case succ
n m : ℕ
⊢ n ∣ succ m → n ≤ succ m
[PROOFSTEP]
exact Nat.le_of_dvd (Nat.succ_pos m)
[GOAL]
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
⊢ divisors m ⊆ properDivisors n
[PROOFSTEP]
apply Finset.subset_iff.2
[GOAL]
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
⊢ ∀ ⦃x : ℕ⦄, x ∈ divisors m → x ∈ properDivisors n
[PROOFSTEP]
intro x hx
[GOAL]
n m : ℕ
hzero : n ≠ 0
h : m ∣ n
hdiff : m ≠ n
x : ℕ
hx : x ∈ divisors m
⊢ x ∈ properDivisors n
[PROOFSTEP]
exact
  Nat.mem_properDivisors.2
    ⟨(Nat.mem_divisors.1 hx).1.trans h,
      lt_of_le_of_lt (divisor_le hx) (lt_of_le_of_ne (divisor_le (Nat.mem_divisors.2 ⟨h, hzero⟩)) hdiff)⟩
[GOAL]
n : ℕ
⊢ divisors 0 = ∅
[PROOFSTEP]
ext
[GOAL]
case a
n a✝ : ℕ
⊢ a✝ ∈ divisors 0 ↔ a✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ properDivisors 0 = ∅
[PROOFSTEP]
ext
[GOAL]
case a
n a✝ : ℕ
⊢ a✝ ∈ properDivisors 0 ↔ a✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ divisors 1 = {1}
[PROOFSTEP]
ext
[GOAL]
case a
n a✝ : ℕ
⊢ a✝ ∈ divisors 1 ↔ a✝ ∈ {1}
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ properDivisors 1 = ∅
[PROOFSTEP]
rw [properDivisors, Ico_self, filter_empty]
[GOAL]
n m : ℕ
h : m ∈ divisors n
⊢ 0 < m
[PROOFSTEP]
cases m
[GOAL]
case zero
n : ℕ
h : zero ∈ divisors n
⊢ 0 < zero
[PROOFSTEP]
rw [mem_divisors, zero_eq, zero_dvd_iff (a := n)] at h
[GOAL]
case zero
n : ℕ
h : n = 0 ∧ n ≠ 0
⊢ 0 < zero
[PROOFSTEP]
cases h.2 h.1
[GOAL]
case succ
n n✝ : ℕ
h : succ n✝ ∈ divisors n
⊢ 0 < succ n✝
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
n : ℕ
⊢ 1 ∈ properDivisors n ↔ 1 < n
[PROOFSTEP]
rw [mem_properDivisors, and_iff_right (one_dvd _)]
[GOAL]
n : ℕ
⊢ divisorsAntidiagonal 0 = ∅
[PROOFSTEP]
ext
[GOAL]
case a
n : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 0 ↔ a✝ ∈ ∅
[PROOFSTEP]
simp
[GOAL]
n : ℕ
⊢ divisorsAntidiagonal 1 = {(1, 1)}
[PROOFSTEP]
ext
[GOAL]
case a
n : ℕ
a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 1 ↔ a✝ ∈ {(1, 1)}
[PROOFSTEP]
simp [mul_eq_one, Prod.ext_iff]
[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ Prod.swap x ∈ divisorsAntidiagonal n ↔ x ∈ divisorsAntidiagonal n
[PROOFSTEP]
rw [mem_divisorsAntidiagonal, mem_divisorsAntidiagonal, mul_comm, Prod.swap]
[GOAL]
n : ℕ
x : ℕ × ℕ
⊢ x.snd * x.fst = n ∧ ¬n = 0 ↔ x ∈ divisorsAntidiagonal n
[PROOFSTEP]
rw [mem_divisorsAntidiagonal, mul_comm]
[GOAL]
n : ℕ
x : ℕ × ℕ
h : x ∈ divisorsAntidiagonal n
⊢ x.fst ∈ divisors n
[PROOFSTEP]
rw [mem_divisorsAntidiagonal] at h
[GOAL]
n : ℕ
x : ℕ × ℕ
h : x.fst * x.snd = n ∧ n ≠ 0
⊢ x.fst ∈ divisors n
[PROOFSTEP]
simp [Dvd.intro _ h.1, h.2]
[GOAL]
n : ℕ
x : ℕ × ℕ
h : x ∈ divisorsAntidiagonal n
⊢ x.snd ∈ divisors n
[PROOFSTEP]
rw [mem_divisorsAntidiagonal] at h
[GOAL]
n : ℕ
x : ℕ × ℕ
h : x.fst * x.snd = n ∧ n ≠ 0
⊢ x.snd ∈ divisors n
[PROOFSTEP]
simp [Dvd.intro_left _ h.1, h.2]
[GOAL]
n : ℕ
⊢ map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (divisorsAntidiagonal n) = divisorsAntidiagonal n
[PROOFSTEP]
rw [← coe_inj, coe_map, Equiv.coe_toEmbedding, Equiv.coe_prodComm, Set.image_swap_eq_preimage_swap]
[GOAL]
n : ℕ
⊢ Prod.swap ⁻¹' ↑(divisorsAntidiagonal n) = ↑(divisorsAntidiagonal n)
[PROOFSTEP]
ext
[GOAL]
case h
n : ℕ
x✝ : ℕ × ℕ
⊢ x✝ ∈ Prod.swap ⁻¹' ↑(divisorsAntidiagonal n) ↔ x✝ ∈ ↑(divisorsAntidiagonal n)
[PROOFSTEP]
exact swap_mem_divisorsAntidiagonal
[GOAL]
n : ℕ
⊢ image Prod.fst (divisorsAntidiagonal n) = divisors n
[PROOFSTEP]
ext
[GOAL]
case a
n a✝ : ℕ
⊢ a✝ ∈ image Prod.fst (divisorsAntidiagonal n) ↔ a✝ ∈ divisors n
[PROOFSTEP]
simp [Dvd.dvd, @eq_comm _ n (_ * _)]
[GOAL]
n : ℕ
⊢ image Prod.snd (divisorsAntidiagonal n) = divisors n
[PROOFSTEP]
rw [← map_swap_divisorsAntidiagonal, map_eq_image, image_image]
[GOAL]
n : ℕ
⊢ image (Prod.snd ∘ ↑(Equiv.toEmbedding (Equiv.prodComm ℕ ℕ))) (divisorsAntidiagonal n) = divisors n
[PROOFSTEP]
exact image_fst_divisorsAntidiagonal
[GOAL]
n : ℕ
⊢ map
      { toFun := fun d => (d, n / d),
        inj' :=
          (_ :
            ∀ (p₁ p₂ : ℕ),
              (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ →
                ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) }
      (divisors n) =
    divisorsAntidiagonal n
[PROOFSTEP]
ext ⟨d, nd⟩
[GOAL]
case a.mk
n d nd : ℕ
⊢ (d, nd) ∈
      map
        { toFun := fun d => (d, n / d),
          inj' :=
            (_ :
              ∀ (p₁ p₂ : ℕ),
                (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ →
                  ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) }
        (divisors n) ↔
    (d, nd) ∈ divisorsAntidiagonal n
[PROOFSTEP]
simp only [mem_map, mem_divisorsAntidiagonal, Function.Embedding.coeFn_mk, mem_divisors, Prod.ext_iff, exists_prop,
  and_left_comm, exists_eq_left]
[GOAL]
case a.mk
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0
[PROOFSTEP]
constructor
[GOAL]
case a.mk.mp
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0
[PROOFSTEP]
rintro ⟨⟨⟨k, rfl⟩, hn⟩, rfl⟩
[GOAL]
case a.mk.mp.intro.intro.intro
d k : ℕ
hn : d * k ≠ 0
⊢ d * (d * k / d) = d * k ∧ d * k ≠ 0
[PROOFSTEP]
rw [Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt]
[GOAL]
case a.mk.mp.intro.intro.intro
d k : ℕ
hn : d * k ≠ 0
⊢ d * k = d * k ∧ d * k ≠ 0
[PROOFSTEP]
exact ⟨rfl, hn⟩
[GOAL]
case a.mk.mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd
[PROOFSTEP]
rintro ⟨rfl, hn⟩
[GOAL]
case a.mk.mpr.intro
d nd : ℕ
hn : d * nd ≠ 0
⊢ (d ∣ d * nd ∧ d * nd ≠ 0) ∧ d * nd / d = nd
[PROOFSTEP]
exact ⟨⟨dvd_mul_right _ _, hn⟩, Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt⟩
[GOAL]
n : ℕ
⊢ map
      { toFun := fun d => (n / d, d),
        inj' :=
          (_ :
            ∀ (p₁ p₂ : ℕ),
              (fun d => (n / d, d)) p₁ = (fun d => (n / d, d)) p₂ →
                ((fun d => (n / d, d)) p₁).snd = ((fun d => (n / d, d)) p₂).snd) }
      (divisors n) =
    divisorsAntidiagonal n
[PROOFSTEP]
apply Finset.map_injective (Equiv.prodComm _ _).toEmbedding
[GOAL]
case a
n : ℕ
⊢ map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ))
      (map
        { toFun := fun d => (n / d, d),
          inj' :=
            (_ :
              ∀ (p₁ p₂ : ℕ),
                (fun d => (n / d, d)) p₁ = (fun d => (n / d, d)) p₂ →
                  ((fun d => (n / d, d)) p₁).snd = ((fun d => (n / d, d)) p₂).snd) }
        (divisors n)) =
    map (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) (divisorsAntidiagonal n)
[PROOFSTEP]
rw [map_swap_divisorsAntidiagonal, ← map_div_right_divisors, Finset.map_map]
[GOAL]
case a
n : ℕ
⊢ map
      (Function.Embedding.trans
        { toFun := fun d => (n / d, d),
          inj' :=
            (_ :
              ∀ (p₁ p₂ : ℕ),
                (fun d => (n / d, d)) p₁ = (fun d => (n / d, d)) p₂ →
                  ((fun d => (n / d, d)) p₁).snd = ((fun d => (n / d, d)) p₂).snd) }
        (Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)))
      (divisors n) =
    map
      { toFun := fun d => (d, n / d),
        inj' :=
          (_ :
            ∀ (p₁ p₂ : ℕ),
              (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ →
                ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) }
      (divisors n)
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ ∑ i in divisors n, i = ∑ i in properDivisors n, i + n
[PROOFSTEP]
rcases Decidable.eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
⊢ ∑ i in divisors 0, i = ∑ i in properDivisors 0, i + 0
[PROOFSTEP]
simp
[GOAL]
case inr
n : ℕ
hn : n ≠ 0
⊢ ∑ i in divisors n, i = ∑ i in properDivisors n, i + n
[PROOFSTEP]
rw [← cons_self_properDivisors hn, Finset.sum_cons, add_comm]
[GOAL]
n : ℕ
h : 0 < n
⊢ Perfect n ↔ ∑ i in divisors n, i = 2 * n
[PROOFSTEP]
rw [perfect_iff_sum_properDivisors h, sum_divisors_eq_sum_properDivisors_add_self, two_mul]
[GOAL]
n : ℕ
h : 0 < n
⊢ ∑ i in properDivisors n, i = n ↔ ∑ i in properDivisors n, i + n = n + n
[PROOFSTEP]
constructor
[GOAL]
case mp
n : ℕ
h : 0 < n
⊢ ∑ i in properDivisors n, i = n → ∑ i in properDivisors n, i + n = n + n
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : ℕ
h : 0 < n
⊢ ∑ i in properDivisors n, i + n = n + n → ∑ i in properDivisors n, i = n
[PROOFSTEP]
intro h
[GOAL]
case mp
n : ℕ
h✝ : 0 < n
h : ∑ i in properDivisors n, i = n
⊢ ∑ i in properDivisors n, i + n = n + n
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
n : ℕ
h✝ : 0 < n
h : ∑ i in properDivisors n, i + n = n + n
⊢ ∑ i in properDivisors n, i = n
[PROOFSTEP]
apply add_right_cancel h
[GOAL]
n p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ divisors (p ^ k) ↔ ∃ j x_1, x = p ^ j
[PROOFSTEP]
rw [mem_divisors, Nat.dvd_prime_pow pp, and_iff_left (ne_of_gt (pow_pos pp.pos k))]
[GOAL]
n p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ k_1, k_1 ≤ k ∧ x = p ^ k_1) ↔ ∃ j x_1, x = p ^ j
[PROOFSTEP]
simp
[GOAL]
n p : ℕ
pp : Prime p
⊢ Nat.divisors p = {1, p}
[PROOFSTEP]
ext
[GOAL]
case a
n p : ℕ
pp : Prime p
a✝ : ℕ
⊢ a✝ ∈ Nat.divisors p ↔ a✝ ∈ {1, p}
[PROOFSTEP]
rw [mem_divisors, dvd_prime pp, and_iff_left pp.ne_zero, Finset.mem_insert, Finset.mem_singleton]
[GOAL]
n p : ℕ
pp : Prime p
⊢ Nat.properDivisors p = {1}
[PROOFSTEP]
rw [← erase_insert properDivisors.not_self_mem, insert_self_properDivisors pp.ne_zero, pp.divisors, pair_comm,
  erase_insert fun con => pp.ne_one (mem_singleton.1 con)]
[GOAL]
n p : ℕ
pp : Prime p
k : ℕ
⊢ divisors (p ^ k) = map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (range (k + 1))
[PROOFSTEP]
ext a
[GOAL]
case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ divisors (p ^ k) ↔ a ∈ map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (range (k + 1))
[PROOFSTEP]
simp only [mem_divisors, mem_map, mem_range, lt_succ_iff, Function.Embedding.coeFn_mk, Nat.pow_eq,
  mem_divisors_prime_pow pp k]
[GOAL]
case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
[PROOFSTEP]
have := mem_divisors_prime_pow pp k (x := a)
[GOAL]
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∈ divisors (p ^ k) ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
[PROOFSTEP]
rw [mem_divisors] at this
[GOAL]
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
[PROOFSTEP]
rw [this]
[GOAL]
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ (∃ j x, a = p ^ j) ↔ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
[PROOFSTEP]
refine ⟨?_, ?_⟩
[GOAL]
case a.refine_1
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ (∃ j x, a = p ^ j) → ∃ a_2, a_2 ≤ k ∧ p ^ a_2 = a
[PROOFSTEP]
intro h
[GOAL]
case a.refine_1
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
h : ∃ j x, a = p ^ j
⊢ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
[PROOFSTEP]
rcases h with ⟨x, hx, hap⟩
[GOAL]
case a.refine_1.intro.intro
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
x : ℕ
hx : x ≤ k
hap : a = p ^ x
⊢ ∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a
[PROOFSTEP]
use x
[GOAL]
case h
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
x : ℕ
hx : x ≤ k
hap : a = p ^ x
⊢ x ≤ k ∧ p ^ x = a
[PROOFSTEP]
tauto
[GOAL]
case a.refine_2
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ p ^ k ≠ 0 ↔ ∃ j x, a = p ^ j
⊢ (∃ a_1, a_1 ≤ k ∧ p ^ a_1 = a) → ∃ j x, a = p ^ j
[PROOFSTEP]
tauto
[GOAL]
n : ℕ
s : Finset ℕ
hsub : s ⊆ properDivisors n
⊢ ∑ x in s, x = ∑ x in properDivisors n, x → s = properDivisors n
[PROOFSTEP]
cases n
[GOAL]
case zero
s : Finset ℕ
hsub : s ⊆ properDivisors zero
⊢ ∑ x in s, x = ∑ x in properDivisors zero, x → s = properDivisors zero
[PROOFSTEP]
rw [properDivisors_zero, subset_empty] at hsub
[GOAL]
case zero
s : Finset ℕ
hsub : s = ∅
⊢ ∑ x in s, x = ∑ x in properDivisors zero, x → s = properDivisors zero
[PROOFSTEP]
simp [hsub]
[GOAL]
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
⊢ ∑ x in s, x = ∑ x in properDivisors (succ n✝), x → s = properDivisors (succ n✝)
[PROOFSTEP]
classical
rw [← sum_sdiff hsub]
intro h
apply Subset.antisymm hsub
rw [← sdiff_eq_empty_iff_subset]
contrapose h
rw [← Ne.def, ← nonempty_iff_ne_empty] at h
apply ne_of_lt
rw [← zero_add (∑ x in s, x), ← add_assoc, add_zero]
apply add_lt_add_right
have hlt := sum_lt_sum_of_nonempty h fun x hx => pos_of_mem_properDivisors (sdiff_subset _ _ hx)
simp only [sum_const_zero] at hlt
apply hlt
[GOAL]
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
⊢ ∑ x in s, x = ∑ x in properDivisors (succ n✝), x → s = properDivisors (succ n✝)
[PROOFSTEP]
rw [← sum_sdiff hsub]
[GOAL]
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
⊢ ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x → s = properDivisors (succ n✝)
[PROOFSTEP]
intro h
[GOAL]
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
⊢ s = properDivisors (succ n✝)
[PROOFSTEP]
apply Subset.antisymm hsub
[GOAL]
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
⊢ properDivisors (succ n✝) ⊆ s
[PROOFSTEP]
rw [← sdiff_eq_empty_iff_subset]
[GOAL]
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
⊢ properDivisors (succ n✝) \ s = ∅
[PROOFSTEP]
contrapose h
[GOAL]
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : ¬properDivisors (succ n✝) \ s = ∅
⊢ ¬∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
[PROOFSTEP]
rw [← Ne.def, ← nonempty_iff_ne_empty] at h
[GOAL]
case succ
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ ¬∑ x in s, x = ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
[PROOFSTEP]
apply ne_of_lt
[GOAL]
case succ.h
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ ∑ x in s, x < ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
[PROOFSTEP]
rw [← zero_add (∑ x in s, x), ← add_assoc, add_zero]
[GOAL]
case succ.h
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ 0 + ∑ x in s, x < ∑ x in properDivisors (succ n✝) \ s, x + ∑ x in s, x
[PROOFSTEP]
apply add_lt_add_right
[GOAL]
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
⊢ 0 < ∑ x in properDivisors (succ n✝) \ s, x
[PROOFSTEP]
have hlt := sum_lt_sum_of_nonempty h fun x hx => pos_of_mem_properDivisors (sdiff_subset _ _ hx)
[GOAL]
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
hlt : ∑ i in properDivisors (succ n✝) \ s, 0 < ∑ i in properDivisors (succ n✝) \ s, i
⊢ 0 < ∑ x in properDivisors (succ n✝) \ s, x
[PROOFSTEP]
simp only [sum_const_zero] at hlt
[GOAL]
case succ.h.bc
s : Finset ℕ
n✝ : ℕ
hsub : s ⊆ properDivisors (succ n✝)
h : Finset.Nonempty (properDivisors (succ n✝) \ s)
hlt : 0 < ∑ i in properDivisors (succ n✝) \ s, i
⊢ 0 < ∑ x in properDivisors (succ n✝) \ s, x
[PROOFSTEP]
apply hlt
[GOAL]
n : ℕ
h : ∑ x in properDivisors n, x ∣ n
⊢ ∑ x in properDivisors n, x = 1 ∨ ∑ x in properDivisors n, x = n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
h : ∑ x in properDivisors zero, x ∣ zero
⊢ ∑ x in properDivisors zero, x = 1 ∨ ∑ x in properDivisors zero, x = zero
[PROOFSTEP]
simp
[GOAL]
case succ
n : ℕ
h : ∑ x in properDivisors (succ n), x ∣ succ n
⊢ ∑ x in properDivisors (succ n), x = 1 ∨ ∑ x in properDivisors (succ n), x = succ n
[PROOFSTEP]
cases' n with n
[GOAL]
case succ.zero
h : ∑ x in properDivisors (succ zero), x ∣ succ zero
⊢ ∑ x in properDivisors (succ zero), x = 1 ∨ ∑ x in properDivisors (succ zero), x = succ zero
[PROOFSTEP]
contrapose! h
[GOAL]
case succ.zero
h : ∑ x in properDivisors (succ zero), x ≠ 1 ∧ ∑ x in properDivisors (succ zero), x ≠ succ zero
⊢ ¬∑ x in properDivisors (succ zero), x ∣ succ zero
[PROOFSTEP]
simp
[GOAL]
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
⊢ ∑ x in properDivisors (succ (succ n)), x = 1 ∨ ∑ x in properDivisors (succ (succ n)), x = succ (succ n)
[PROOFSTEP]
rw [or_iff_not_imp_right]
[GOAL]
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
⊢ ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n) → ∑ x in properDivisors (succ (succ n)), x = 1
[PROOFSTEP]
intro ne_n
[GOAL]
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
⊢ ∑ x in properDivisors (succ (succ n)), x = 1
[PROOFSTEP]
have hlt : ∑ x in n.succ.succ.properDivisors, x < n.succ.succ := lt_of_le_of_ne (Nat.le_of_dvd (Nat.succ_pos _) h) ne_n
[GOAL]
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
hlt : ∑ x in properDivisors (succ (succ n)), x < succ (succ n)
⊢ ∑ x in properDivisors (succ (succ n)), x = 1
[PROOFSTEP]
symm
[GOAL]
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
hlt : ∑ x in properDivisors (succ (succ n)), x < succ (succ n)
⊢ 1 = ∑ x in properDivisors (succ (succ n)), x
[PROOFSTEP]
rw [← mem_singleton,
  eq_properDivisors_of_subset_of_sum_eq_sum (singleton_subset_iff.2 (mem_properDivisors.2 ⟨h, hlt⟩)) sum_singleton,
  mem_properDivisors]
[GOAL]
case succ.succ
n : ℕ
h : ∑ x in properDivisors (succ (succ n)), x ∣ succ (succ n)
ne_n : ¬∑ x in properDivisors (succ (succ n)), x = succ (succ n)
hlt : ∑ x in properDivisors (succ (succ n)), x < succ (succ n)
⊢ 1 ∣ succ (succ n) ∧ 1 < succ (succ n)
[PROOFSTEP]
refine' ⟨one_dvd _, Nat.succ_lt_succ (Nat.succ_pos _)⟩
[GOAL]
n : ℕ
α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x in Nat.properDivisors p, f x = f 1
[PROOFSTEP]
simp [h.properDivisors]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : CommMonoid α
p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x in Nat.divisors p, f x = f p * f 1
[PROOFSTEP]
rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]
[GOAL]
n : ℕ
⊢ properDivisors n = {1} ↔ Prime n
[PROOFSTEP]
refine ⟨?_, ?_⟩
[GOAL]
case refine_1
n : ℕ
⊢ properDivisors n = {1} → Prime n
[PROOFSTEP]
intro h
[GOAL]
case refine_1
n : ℕ
h : properDivisors n = {1}
⊢ Prime n
[PROOFSTEP]
refine' Nat.prime_def_lt''.mpr ⟨_, fun m hdvd => _⟩
[GOAL]
case refine_1.refine'_1
n : ℕ
h : properDivisors n = {1}
⊢ 2 ≤ n
[PROOFSTEP]
match n with
| 0 => contradiction
| 1 => contradiction
| Nat.succ (Nat.succ n) => simp [succ_le_succ]
[GOAL]
n : ℕ
h : properDivisors 0 = {1}
⊢ 2 ≤ 0
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
h : properDivisors 1 = {1}
⊢ 2 ≤ 1
[PROOFSTEP]
contradiction
[GOAL]
n✝ n : ℕ
h : properDivisors (succ (succ n)) = {1}
⊢ 2 ≤ succ (succ n)
[PROOFSTEP]
simp [succ_le_succ]
[GOAL]
case refine_1.refine'_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
⊢ m = 1 ∨ m = n
[PROOFSTEP]
rw [← mem_singleton, ← h, mem_properDivisors]
[GOAL]
case refine_1.refine'_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
⊢ m ∣ n ∧ m < n ∨ m = n
[PROOFSTEP]
have := Nat.le_of_dvd ?_ hdvd
[GOAL]
case refine_1.refine'_2.refine_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
this : m ≤ n
⊢ m ∣ n ∧ m < n ∨ m = n
[PROOFSTEP]
simp [hdvd, this]
[GOAL]
case refine_1.refine'_2.refine_2
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
this : m ≤ n
⊢ m < n ∨ m = n
[PROOFSTEP]
exact (le_iff_eq_or_lt.mp this).symm
[GOAL]
case refine_1.refine'_2.refine_1
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
⊢ 0 < n
[PROOFSTEP]
by_contra'
[GOAL]
case refine_1.refine'_2.refine_1
n : ℕ
h : properDivisors n = {1}
m : ℕ
hdvd : m ∣ n
this : n ≤ 0
⊢ False
[PROOFSTEP]
simp [nonpos_iff_eq_zero.mp this, this] at h
[GOAL]
case refine_2
n : ℕ
⊢ Prime n → properDivisors n = {1}
[PROOFSTEP]
exact fun h => Prime.properDivisors h
[GOAL]
n : ℕ
⊢ ∑ x in properDivisors n, x = 1 ↔ Prime n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
⊢ ∑ x in properDivisors zero, x = 1 ↔ Prime zero
[PROOFSTEP]
simp [Nat.not_prime_zero]
[GOAL]
case succ
n : ℕ
⊢ ∑ x in properDivisors (succ n), x = 1 ↔ Prime (succ n)
[PROOFSTEP]
cases n
[GOAL]
case succ.zero
⊢ ∑ x in properDivisors (succ zero), x = 1 ↔ Prime (succ zero)
[PROOFSTEP]
simp [Nat.not_prime_one]
[GOAL]
case succ.succ
n✝ : ℕ
⊢ ∑ x in properDivisors (succ (succ n✝)), x = 1 ↔ Prime (succ (succ n✝))
[PROOFSTEP]
rw [← properDivisors_eq_singleton_one_iff_prime]
[GOAL]
case succ.succ
n✝ : ℕ
⊢ ∑ x in properDivisors (succ (succ n✝)), x = 1 ↔ properDivisors (succ (succ n✝)) = {1}
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.symm ▸ sum_singleton⟩
[GOAL]
case succ.succ
n✝ : ℕ
h : ∑ x in properDivisors (succ (succ n✝)), x = 1
⊢ properDivisors (succ (succ n✝)) = {1}
[PROOFSTEP]
rw [@eq_comm (Finset ℕ) _ _]
[GOAL]
case succ.succ
n✝ : ℕ
h : ∑ x in properDivisors (succ (succ n✝)), x = 1
⊢ {1} = properDivisors (succ (succ n✝))
[PROOFSTEP]
apply
  eq_properDivisors_of_subset_of_sum_eq_sum
    (singleton_subset_iff.2 (one_mem_properDivisors_iff_one_lt.2 (succ_lt_succ (Nat.succ_pos _))))
    (Eq.trans sum_singleton h.symm)
[GOAL]
n p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ properDivisors (p ^ k) ↔ ∃ j x_1, x = p ^ j
[PROOFSTEP]
rw [mem_properDivisors, Nat.dvd_prime_pow pp, ← exists_and_right]
[GOAL]
n p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ x_1, (x_1 ≤ k ∧ x = p ^ x_1) ∧ x < p ^ k) ↔ ∃ j x_1, x = p ^ j
[PROOFSTEP]
simp only [exists_prop, and_assoc]
[GOAL]
n p : ℕ
pp : Prime p
k x : ℕ
⊢ (∃ x_1, x_1 ≤ k ∧ x = p ^ x_1 ∧ x < p ^ k) ↔ ∃ j, j < k ∧ x = p ^ j
[PROOFSTEP]
apply exists_congr
[GOAL]
case h
n p : ℕ
pp : Prime p
k x : ℕ
⊢ ∀ (a : ℕ), a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
[PROOFSTEP]
intro a
[GOAL]
case h
n p : ℕ
pp : Prime p
k x a : ℕ
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
[PROOFSTEP]
constructor
[GOAL]
case h.mp
n p : ℕ
pp : Prime p
k x a : ℕ
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k → a < k ∧ x = p ^ a
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
n p : ℕ
pp : Prime p
k x a : ℕ
⊢ a < k ∧ x = p ^ a → a ≤ k ∧ x = p ^ a ∧ x < p ^ k
[PROOFSTEP]
intro h
[GOAL]
case h.mp
n p : ℕ
pp : Prime p
k x a : ℕ
h : a ≤ k ∧ x = p ^ a ∧ x < p ^ k
⊢ a < k ∧ x = p ^ a
[PROOFSTEP]
rcases h with ⟨_h_left, rfl, h_right⟩
[GOAL]
case h.mp.intro.intro
n p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : p ^ a < p ^ k
⊢ a < k ∧ p ^ a = p ^ a
[PROOFSTEP]
rw [pow_lt_pow_iff pp.one_lt] at h_right
[GOAL]
case h.mp.intro.intro
n p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : a < k
⊢ a < k ∧ p ^ a = p ^ a
[PROOFSTEP]
exact ⟨h_right, by rfl⟩
[GOAL]
n p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : a < k
⊢ p ^ a = p ^ a
[PROOFSTEP]
rfl
[GOAL]
case h.mpr
n p : ℕ
pp : Prime p
k x a : ℕ
h : a < k ∧ x = p ^ a
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k
[PROOFSTEP]
rcases h with ⟨h_left, rfl⟩
[GOAL]
case h.mpr.intro
n p : ℕ
pp : Prime p
k a : ℕ
h_left : a < k
⊢ a ≤ k ∧ p ^ a = p ^ a ∧ p ^ a < p ^ k
[PROOFSTEP]
rw [pow_lt_pow_iff pp.one_lt]
[GOAL]
case h.mpr.intro
n p : ℕ
pp : Prime p
k a : ℕ
h_left : a < k
⊢ a ≤ k ∧ p ^ a = p ^ a ∧ a < k
[PROOFSTEP]
simp [h_left, le_of_lt]
[GOAL]
n p : ℕ
pp : Prime p
k : ℕ
⊢ properDivisors (p ^ k) = map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (range k)
[PROOFSTEP]
ext a
[GOAL]
case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∈ properDivisors (p ^ k) ↔ a ∈ map { toFun := Nat.pow p, inj' := (_ : Function.Injective fun n => p ^ n) } (range k)
[PROOFSTEP]
simp only [mem_properDivisors, Nat.isUnit_iff, mem_map, mem_range, Function.Embedding.coeFn_mk, pow_eq]
[GOAL]
case a
n p : ℕ
pp : Prime p
k a : ℕ
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
[PROOFSTEP]
have := mem_properDivisors_prime_pow pp k (x := a)
[GOAL]
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∈ properDivisors (p ^ k) ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
[PROOFSTEP]
rw [mem_properDivisors] at this
[GOAL]
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
⊢ a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
[PROOFSTEP]
rw [this]
[GOAL]
case a
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
⊢ (∃ j x, a = p ^ j) ↔ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
[PROOFSTEP]
refine ⟨?_, ?_⟩
[GOAL]
case a.refine_1
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
⊢ (∃ j x, a = p ^ j) → ∃ a_2, a_2 < k ∧ p ^ a_2 = a
[PROOFSTEP]
intro h
[GOAL]
case a.refine_1
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
h : ∃ j x, a = p ^ j
⊢ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
[PROOFSTEP]
rcases h with ⟨j, hj, hap⟩
[GOAL]
case a.refine_1.intro.intro
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
j : ℕ
hj : j < k
hap : a = p ^ j
⊢ ∃ a_1, a_1 < k ∧ p ^ a_1 = a
[PROOFSTEP]
use j
[GOAL]
case h
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
j : ℕ
hj : j < k
hap : a = p ^ j
⊢ j < k ∧ p ^ j = a
[PROOFSTEP]
tauto
[GOAL]
case a.refine_2
n p : ℕ
pp : Prime p
k a : ℕ
this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j x, a = p ^ j
⊢ (∃ a_1, a_1 < k ∧ p ^ a_1 = a) → ∃ j x, a = p ^ j
[PROOFSTEP]
tauto
[GOAL]
n : ℕ
α : Type u_1
inst✝ : CommMonoid α
k p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x in properDivisors (p ^ k), f x = ∏ x in range k, f (p ^ x)
[PROOFSTEP]
simp [h, properDivisors_prime_pow]
[GOAL]
n : ℕ
α : Type u_1
inst✝ : CommMonoid α
k p : ℕ
f : ℕ → α
h : Prime p
⊢ ∏ x in divisors (p ^ k), f x = ∏ x in range (k + 1), f (p ^ x)
[PROOFSTEP]
simp [h, divisors_prime_pow]
[GOAL]
n✝ : ℕ
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i in divisorsAntidiagonal n, f i.fst i.snd = ∏ i in divisors n, f i (n / i)
[PROOFSTEP]
rw [← map_div_right_divisors, Finset.prod_map]
[GOAL]
n✝ : ℕ
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x in divisors n,
      f
        (↑{ toFun := fun d => (d, n / d),
                inj' :=
                  (_ :
                    ∀ (p₁ p₂ : ℕ),
                      (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ →
                        ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) }
            x).fst
        (↑{ toFun := fun d => (d, n / d),
                inj' :=
                  (_ :
                    ∀ (p₁ p₂ : ℕ),
                      (fun d => (d, n / d)) p₁ = (fun d => (d, n / d)) p₂ →
                        ((fun d => (d, n / d)) p₁).fst = ((fun d => (d, n / d)) p₂).fst) }
            x).snd =
    ∏ i in divisors n, f i (n / i)
[PROOFSTEP]
rfl
[GOAL]
n✝ : ℕ
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ i in divisorsAntidiagonal n, f i.fst i.snd = ∏ i in divisors n, f (n / i) i
[PROOFSTEP]
rw [← map_swap_divisorsAntidiagonal, Finset.prod_map]
[GOAL]
n✝ : ℕ
M : Type u_1
inst✝ : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ x in divisorsAntidiagonal n,
      f (↑(Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) x).fst (↑(Equiv.toEmbedding (Equiv.prodComm ℕ ℕ)) x).snd =
    ∏ i in divisors n, f (n / i) i
[PROOFSTEP]
exact prod_divisorsAntidiagonal fun i j => f j i
[GOAL]
n✝ n : ℕ
⊢ List.toFinset (factors n) = filter Prime (divisors n)
[PROOFSTEP]
rcases n.eq_zero_or_pos with (rfl | hn)
[GOAL]
case inl
n : ℕ
⊢ List.toFinset (factors 0) = filter Prime (divisors 0)
[PROOFSTEP]
simp
[GOAL]
case inr
n✝ n : ℕ
hn : n > 0
⊢ List.toFinset (factors n) = filter Prime (divisors n)
[PROOFSTEP]
ext q
[GOAL]
case inr.a
n✝ n : ℕ
hn : n > 0
q : ℕ
⊢ q ∈ List.toFinset (factors n) ↔ q ∈ filter Prime (divisors n)
[PROOFSTEP]
simpa [hn, hn.ne', mem_factors] using and_comm
[GOAL]
n✝ n : ℕ
⊢ image (fun x => n / x) (divisors n) = divisors n
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n✝ n : ℕ
hn : n = 0
⊢ image (fun x => n / x) (divisors n) = divisors n
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
n✝ n : ℕ
hn : ¬n = 0
⊢ image (fun x => n / x) (divisors n) = divisors n
[PROOFSTEP]
ext a
[GOAL]
case neg.a
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ image (fun x => n / x) (divisors n) ↔ a ∈ divisors n
[PROOFSTEP]
constructor
[GOAL]
case neg.a.mp
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ image (fun x => n / x) (divisors n) → a ∈ divisors n
[PROOFSTEP]
rw [mem_image]
[GOAL]
case neg.a.mp
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ (∃ a_1, a_1 ∈ divisors n ∧ n / a_1 = a) → a ∈ divisors n
[PROOFSTEP]
rintro ⟨x, hx1, hx2⟩
[GOAL]
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∈ divisors n
hx2 : n / x = a
⊢ a ∈ divisors n
[PROOFSTEP]
rw [mem_divisors] at *
[GOAL]
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n ∧ n ≠ 0
[PROOFSTEP]
refine' ⟨_, hn⟩
[GOAL]
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ a ∣ n
[PROOFSTEP]
rw [← hx2]
[GOAL]
case neg.a.mp.intro.intro
n✝ n : ℕ
hn : ¬n = 0
a x : ℕ
hx1 : x ∣ n ∧ n ≠ 0
hx2 : n / x = a
⊢ n / x ∣ n
[PROOFSTEP]
exact div_dvd_of_dvd hx1.1
[GOAL]
case neg.a.mpr
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∈ divisors n → a ∈ image (fun x => n / x) (divisors n)
[PROOFSTEP]
rw [mem_divisors, mem_image]
[GOAL]
case neg.a.mpr
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
⊢ a ∣ n ∧ n ≠ 0 → ∃ a_2, a_2 ∈ divisors n ∧ n / a_2 = a
[PROOFSTEP]
rintro ⟨h1, -⟩
[GOAL]
case neg.a.mpr.intro
n✝ n : ℕ
hn : ¬n = 0
a : ℕ
h1 : a ∣ n
⊢ ∃ a_1, a_1 ∈ divisors n ∧ n / a_1 = a
[PROOFSTEP]
exact ⟨n / a, mem_divisors.mpr ⟨div_dvd_of_dvd h1, hn⟩, Nat.div_div_self h1 hn⟩
[GOAL]
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
⊢ ∏ d in divisors n, f (n / d) = Finset.prod (divisors n) f
[PROOFSTEP]
by_cases hn : n = 0
[GOAL]
case pos
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : n = 0
⊢ ∏ d in divisors n, f (n / d) = Finset.prod (divisors n) f
[PROOFSTEP]
simp [hn]
[GOAL]
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d in divisors n, f (n / d) = Finset.prod (divisors n) f
[PROOFSTEP]
rw [← prod_image]
[GOAL]
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ x in image (fun d => n / d) (divisors n), f x = Finset.prod (divisors n) f
[PROOFSTEP]
exact prod_congr (image_div_divisors_eq_divisors n) (by simp)
[GOAL]
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ (x : ℕ), x ∈ divisors n → f x = f x
[PROOFSTEP]
simp
[GOAL]
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∀ (x : ℕ), x ∈ divisors n → ∀ (y : ℕ), y ∈ divisors n → n / x = n / y → x = y
[PROOFSTEP]
intro x hx y hy h
[GOAL]
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ divisors n
y : ℕ
hy : y ∈ divisors n
h : n / x = n / y
⊢ x = y
[PROOFSTEP]
rw [mem_divisors] at hx hy
[GOAL]
case neg
n✝ : ℕ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∣ n ∧ n ≠ 0
y : ℕ
hy : y ∣ n ∧ n ≠ 0
h : n / x = n / y
⊢ x = y
[PROOFSTEP]
exact (div_eq_iff_eq_of_dvd_dvd hn hx.1 hy.1).mp h