-- Mathlib/Analysis/Normed/Field/ProperSpace.lean
/-- A weakly locally compact normed field is proper.
This is a specialization of `ProperSpace.of_locallyCompactSpace`
which holds for `NormedSpace`s but requires more imports. -/
lemma ProperSpace.of_nontriviallyNormedField_of_weaklyLocallyCompactSpace
    (𝕜 : Type*) [NontriviallyNormedField 𝕜] [WeaklyLocallyCompactSpace 𝕜] :
    ProperSpace 𝕜

Proof state:
case h.e'_3
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
⊢ closedBall 0 (‖c‖ ^ n * r) = c ^ n • closedBall 0 r

Tactic:
ext

Result:
case h.e'_3.h
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
x✝ : 𝕜
⊢ x✝ ∈ closedBall 0 (‖c‖ ^ n * r) ↔ x✝ ∈ c ^ n • closedBall 0 r

Proof state:
case h.e'_3.h
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
x✝ : 𝕜
⊢ x✝ ∈ closedBall 0 (‖c‖ ^ n * r) ↔ x✝ ∈ c ^ n • closedBall 0 r

Tactic:
simp only [mem_closedBall, dist_zero_right, Set.mem_smul_set_iff_inv_smul_mem₀ this,
  smul_eq_mul, norm_mul, norm_inv, norm_pow,
  inv_mul_le_iff₀ (by simpa only [norm_pow] using norm_pos_iff.mpr this)]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ IsCompact (closedBall 0 (‖c‖ ^ n * r))

Tactic:
have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_lt] at hc

Result:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
⊢ IsCompact (closedBall 0 (‖c‖ ^ n * r))

Proof state:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
x✝ : 𝕜
⊢ 0 < ?m.5604

Tactic:
simpa only [norm_pow] using norm_pos_iff.mpr this

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
⊢ ProperSpace 𝕜

Tactic:
rcases exists_isCompact_closedBall (0 : 𝕜) with ⟨r, rpos, hr⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
⊢ ProperSpace 𝕜

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
⊢ ProperSpace 𝕜

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
⊢ ProperSpace 𝕜

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
hC : ∀ (n : ℕ), IsCompact (closedBall 0 (‖c‖ ^ n * r))
⊢ ProperSpace 𝕜

Tactic:
have hTop : Tendsto (fun n ↦ ‖c‖^n * r) atTop atTop :=
  Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
hC : ∀ (n : ℕ), IsCompact (closedBall 0 (‖c‖ ^ n * r))
hTop : Tendsto (fun n => ‖c‖ ^ n * r) atTop atTop
⊢ ProperSpace 𝕜

Proof state:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
h : c = 0
⊢ False

Tactic:
simp [h, zero_le_one.not_lt] at hc

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
⊢ ProperSpace 𝕜

Tactic:
have hC n : IsCompact (closedBall (0 : 𝕜) (‖c‖^n * r)) := by
  have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_lt] at hc
  convert hr.smul (c ^ n)
  ext
  simp only [mem_closedBall, dist_zero_right, Set.mem_smul_set_iff_inv_smul_mem₀ this,
    smul_eq_mul, norm_mul, norm_inv, norm_pow,
    inv_mul_le_iff₀ (by simpa only [norm_pow] using norm_pos_iff.mpr this)]

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
hC : ∀ (n : ℕ), IsCompact (closedBall 0 (‖c‖ ^ n * r))
⊢ ProperSpace 𝕜

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
hC : ∀ (n : ℕ), IsCompact (closedBall 0 (‖c‖ ^ n * r))
hTop : Tendsto (fun n => ‖c‖ ^ n * r) atTop atTop
⊢ ProperSpace 𝕜

Tactic:
exact .of_seq_closedBall hTop (Eventually.of_forall hC)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
⊢ IsCompact (closedBall 0 (‖c‖ ^ n * r))

Tactic:
convert hr.smul (c ^ n)

Result:
case h.e'_3
𝕜 : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : WeaklyLocallyCompactSpace 𝕜
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
this : c ^ n ≠ 0
⊢ closedBall 0 (‖c‖ ^ n * r) = c ^ n • closedBall 0 r