-- Mathlib/NumberTheory/FactorisationProperties.lean
theorem Prime.deficient_pow  (h : Prime n) : Deficient (n ^ m)

Proof state:
case inr
n m : ℕ
h : Prime n
h✝ : m > 0
h1 : (n ^ m).properDivisors = image (fun x => n ^ x) (range m)
⊢ (n ^ m).Deficient

Tactic:
have h2 : ∑ i ∈ image (fun x => n ^ x) (range m), i = ∑ i ∈ range m, n^i := by
  rw [Finset.sum_image]
  rintro x _ y _
  apply pow_injective_of_not_isUnit h.not_unit <| Prime.ne_zero h

Result:
case inr
n m : ℕ
h : Prime n
h✝ : m > 0
h1 : (n ^ m).properDivisors = image (fun x => n ^ x) (range m)
h2 : ∑ i ∈ image (fun x => n ^ x) (range m), i = ∑ i ∈ range m, n ^ i
⊢ (n ^ m).Deficient

Proof state:
case a.intro.intro.intro
n m : ℕ
h : Prime n
h✝ : m > 0
t : ℕ
ht : t ≤ m
ha' : n ^ t < n ^ m
⊢ ∃ a < m, n ^ a = n ^ t

Tactic:
exact ⟨t, lt_of_le_of_ne ht (fun ht' ↦ lt_irrefl _ (ht' ▸ ha')), rfl⟩

Result:
no goals

Proof state:
case a.left
n m : ℕ
h : Prime n
h✝ : m > 0
a x : ℕ
hx : x < m
hy : n ^ x = a
⊢ ∃ k ≤ m, n ^ x = n ^ k

Tactic:
exact ⟨x, Nat.le_of_succ_le hx, rfl⟩

Result:
no goals

Proof state:
n m : ℕ
h : Prime n
⊢ (n ^ m).Deficient

Tactic:
rcases Nat.eq_zero_or_pos m with (rfl | _)

Result:
case inl
n : ℕ
h : Prime n
⊢ (n ^ 0).Deficient

case inr
n m : ℕ
h : Prime n
h✝ : m > 0
⊢ (n ^ m).Deficient

Proof state:
case inr
n m : ℕ
h : Prime n
h✝ : m > 0
h1 : (n ^ m).properDivisors = image (fun x => n ^ x) (range m)
h2 : ∑ i ∈ image (fun x => n ^ x) (range m), i = ∑ i ∈ range m, n ^ i
⊢ (n ^ m).Deficient

Tactic:
rw [Deficient, h1, h2]

Result:
case inr
n m : ℕ
h : Prime n
h✝ : m > 0
h1 : (n ^ m).properDivisors = image (fun x => n ^ x) (range m)
h2 : ∑ i ∈ image (fun x => n ^ x) (range m), i = ∑ i ∈ range m, n ^ i
⊢ ∑ i ∈ range m, n ^ i < n ^ m

Proof state:
case a.left
n m : ℕ
h : Prime n
h✝ : m > 0
a x : ℕ
hx : x < m
hy : n ^ x = a
⊢ a ∣ n ^ m

Tactic:
rw [← hy, dvd_prime_pow h]

Result:
case a.left
n m : ℕ
h : Prime n
h✝ : m > 0
a x : ℕ
hx : x < m
hy : n ^ x = a
⊢ ∃ k ≤ m, n ^ x = n ^ k

Proof state:
n m : ℕ
h : Prime n
h✝ : m > 0
h1 : (n ^ m).properDivisors = image (fun x => n ^ x) (range m)
⊢ ∑ i ∈ image (fun x => n ^ x) (range m), i = ∑ i ∈ range m, n ^ i

Tactic:
rw [Finset.sum_image]

Result:
n m : ℕ
h : Prime n
h✝ : m > 0
h1 : (n ^ m).properDivisors = image (fun x => n ^ x) (range m)
⊢ ∀ x ∈ range m, ∀ y ∈ range m, n ^ x = n ^ y → x = y

Proof state:
case inr
n m : ℕ
h : Prime n
h✝ : m > 0
h1 : (n ^ m).properDivisors = image (fun x => n ^ x) (range m)
h2 : ∑ i ∈ image (fun x => n ^ x) (range m), i = ∑ i ∈ range m, n ^ i
⊢ ∑ i ∈ range m, n ^ i < n ^ m

Tactic:
calc
  ∑ i ∈ range m, n ^ i
    = (n ^ m - 1) / (n - 1) := (Nat.geomSum_eq (Prime.two_le h) _)
  _ ≤ (n ^ m - 1) := Nat.div_le_self (n ^ m - 1) (n - 1)
  _ < n ^ m := sub_lt (pow_pos (Prime.pos h) m) (Nat.one_pos)

Result:
no goals

Proof state:
case a
n m : ℕ
h : Prime n
h✝ : m > 0
a : ℕ
⊢ a ∈ image (fun x => n ^ x) (range m) → a ∈ (n ^ m).properDivisors

Tactic:
simp only [mem_image, mem_range, mem_properDivisors, forall_exists_index, and_imp]

Result:
case a
n m : ℕ
h : Prime n
h✝ : m > 0
a : ℕ
⊢ ∀ x < m, n ^ x = a → a ∣ n ^ m ∧ a < n ^ m

Proof state:
n m : ℕ
h : Prime n
h✝ : m > 0
⊢ (n ^ m).properDivisors = image (fun x => n ^ x) (range m)

Tactic:
apply subset_antisymm <;> intro a

Result:
case a
n m : ℕ
h : Prime n
h✝ : m > 0
a : ℕ
⊢ a ∈ (n ^ m).properDivisors → a ∈ image (fun x => n ^ x) (range m)

case a
n m : ℕ
h : Prime n
h✝ : m > 0
a : ℕ
⊢ a ∈ image (fun x => n ^ x) (range m) → a ∈ (n ^ m).properDivisors

Proof state:
n m : ℕ
h : Prime n
h✝ : m > 0
h1 : (n ^ m).properDivisors = image (fun x => n ^ x) (range m)
⊢ ∀ x ∈ range m, ∀ y ∈ range m, n ^ x = n ^ y → x = y

Tactic:
rintro x _ y _

Result:
n m : ℕ
h : Prime n
h✝ : m > 0
h1 : (n ^ m).properDivisors = image (fun x => n ^ x) (range m)
x : ℕ
a✝¹ : x ∈ range m
y : ℕ
a✝ : y ∈ range m
⊢ n ^ x = n ^ y → x = y

Proof state:
n m : ℕ
h : Prime n
h✝ : m > 0
h1 : (n ^ m).properDivisors = image (fun x => n ^ x) (range m)
x : ℕ
a✝¹ : x ∈ range m
y : ℕ
a✝ : y ∈ range m
⊢ n ^ x = n ^ y → x = y

Tactic:
apply pow_injective_of_not_isUnit h.not_unit <| Prime.ne_zero h

Result:
no goals

Proof state:
case a
n m : ℕ
h : Prime n
h✝ : m > 0
a : ℕ
⊢ ∀ x < m, n ^ x = a → a ∣ n ^ m ∧ a < n ^ m

Tactic:
intro x hx hy

Result:
case a
n m : ℕ
h : Prime n
h✝ : m > 0
a x : ℕ
hx : x < m
hy : n ^ x = a
⊢ a ∣ n ^ m ∧ a < n ^ m

Proof state:
case a.right
n m : ℕ
h : Prime n
h✝ : m > 0
a x : ℕ
hx : x < m
hy : n ^ x = a
⊢ n ^ x < n ^ m

Tactic:
exact (Nat.pow_lt_pow_iff_right (Prime.two_le h)).mpr hx

Result:
no goals

Proof state:
case inl
n : ℕ
h : Prime n
⊢ (n ^ 0).Deficient

Tactic:
simpa using deficient_one

Result:
no goals

Proof state:
case a.right
n m : ℕ
h : Prime n
h✝ : m > 0
a x : ℕ
hx : x < m
hy : n ^ x = a
⊢ a < n ^ m

Tactic:
rw [← hy]

Result:
case a.right
n m : ℕ
h : Prime n
h✝ : m > 0
a x : ℕ
hx : x < m
hy : n ^ x = a
⊢ n ^ x < n ^ m

Proof state:
case a
n m : ℕ
h : Prime n
h✝ : m > 0
a : ℕ
⊢ (∃ k ≤ m, a = n ^ k) ∧ a < n ^ m → ∃ a_2 < m, n ^ a_2 = a

Tactic:
rintro ⟨⟨t, ht, rfl⟩, ha'⟩

Result:
case a.intro.intro.intro
n m : ℕ
h : Prime n
h✝ : m > 0
t : ℕ
ht : t ≤ m
ha' : n ^ t < n ^ m
⊢ ∃ a < m, n ^ a = n ^ t

Proof state:
case a
n m : ℕ
h : Prime n
h✝ : m > 0
a x : ℕ
hx : x < m
hy : n ^ x = a
⊢ a ∣ n ^ m ∧ a < n ^ m

Tactic:
constructor

Result:
case a.left
n m : ℕ
h : Prime n
h✝ : m > 0
a x : ℕ
hx : x < m
hy : n ^ x = a
⊢ a ∣ n ^ m

case a.right
n m : ℕ
h : Prime n
h✝ : m > 0
a x : ℕ
hx : x < m
hy : n ^ x = a
⊢ a < n ^ m

Proof state:
case a
n m : ℕ
h : Prime n
h✝ : m > 0
a : ℕ
⊢ a ∈ (n ^ m).properDivisors → a ∈ image (fun x => n ^ x) (range m)

Tactic:
simp only [mem_properDivisors, mem_image, mem_range, dvd_prime_pow h]

Result:
case a
n m : ℕ
h : Prime n
h✝ : m > 0
a : ℕ
⊢ (∃ k ≤ m, a = n ^ k) ∧ a < n ^ m → ∃ a_2 < m, n ^ a_2 = a