case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ∃ k, ↑p ^ (-↑k) < ε
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
⊢ ∃ k, ↑p ^ (-↑k) < ε
obtain ⟨k, hk⟩ := exists_nat_gt ε⁻¹
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑p ^ (-↑k) < ε
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ∃ k, ↑p ^ (-↑k) < ε
use k
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < (↑p ^ (-↑k))⁻¹

p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 0 < ↑p
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑p ^ (-↑k) < ε
rw [← inv_lt_inv hε (_root_.zpow_pos_of_pos _ _)]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < ↑p ^ k
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < (↑p ^ (-↑k))⁻¹
rw [zpow_neg, inv_inv, zpow_ofNat]
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑k ≤ ↑p ^ k
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ε⁻¹ < ↑p ^ k
apply lt_of_lt_of_le hk
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ k ≤ p ^ k
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ ↑k ≤ ↑p ^ k
norm_cast
case intro.a
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ k < p ^ k
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ k ≤ p ^ k
apply le_of_lt
case intro.a.convert_2
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 1 < p
case intro.a
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ k < p ^ k
convert Nat.lt_pow_self _ _ using 1
no goals
case intro.a.convert_2
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 1 < p
exact hp.1.one_lt
no goals
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℝ
hε : 0 < ε
k : ℕ
hk : ε⁻¹ < ↑k
⊢ 0 < ↑p
exact_mod_cast hp.1.pos