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
n p : ℕ
pp : Prime p
k x : ℕ
⊢ x ∈ properDivisors (p ^ k) ↔ ∃ j x_1, x = p ^ j
rw [mem_properDivisors, Nat.dvd_prime_pow pp, ← exists_and_right]
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
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
simp only [exists_prop, and_assoc]
case h
n p : ℕ
pp : Prime p
k x : ℕ
⊢ ∀ (a : ℕ), a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
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
apply exists_congr
case h
n p : ℕ
pp : Prime p
k x a : ℕ
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
case h
n p : ℕ
pp : Prime p
k x : ℕ
⊢ ∀ (a : ℕ), a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
intro a
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

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
case h
n p : ℕ
pp : Prime p
k x a : ℕ
⊢ a ≤ k ∧ x = p ^ a ∧ x < p ^ k ↔ a < k ∧ x = p ^ a
constructor <;> intro h
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
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
rcases h with ⟨_h_left, rfl, h_right⟩
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
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
rw [pow_lt_pow_iff pp.one_lt] at h_right
no goals
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
exact ⟨h_right, by rfl⟩
no goals
n p : ℕ
pp : Prime p
k a : ℕ
_h_left : a ≤ k
h_right : a < k
⊢ p ^ a = p ^ a
rfl
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
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
rcases h with ⟨h_left, rfl⟩
case h.mpr.intro
n p : ℕ
pp : Prime p
k a : ℕ
h_left : a < k
⊢ a ≤ k ∧ p ^ a = p ^ a ∧ a < k
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
rw [pow_lt_pow_iff pp.one_lt]
no goals
case h.mpr.intro
n p : ℕ
pp : Prime p
k a : ℕ
h_left : a < k
⊢ a ≤ k ∧ p ^ a = p ^ a ∧ a < k
simp [h_left, le_of_lt]