-- Mathlib/Analysis/Normed/Field/Lemmas.lean
lemma NormedField.completeSpace_iff_isComplete_closedBall {K : Type*} [NormedField K] :
    CompleteSpace K ↔ IsComplete (Metric.closedBall 0 1 : Set K)

Proof state:
case mpr.inr.intro.mk.intro
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n => ‖u n‖)
kpos : 0 ≤ k
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨x, hx⟩ := NormedField.exists_lt_norm K k

Result:
case mpr.inr.intro.mk.intro.intro
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n => ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Proof state:
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n => ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 => x_1 / x) ∘ u)
⊢ ∀ (n : ℕ), ((fun x_1 => x_1 / x) ∘ u) n ∈ Metric.closedBall 0 1

Tactic:
intro

Result:
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n => ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 => x_1 / x) ∘ u)
n✝ : ℕ
⊢ ((fun x_1 => x_1 / x) ∘ u) n✝ ∈ Metric.closedBall 0 1

Proof state:
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n => ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 => x_1 / x) ∘ u)
hb : ∀ (n : ℕ), ((fun x_1 => x_1 / x) ∘ u) n ∈ Metric.closedBall 0 1
a : K
ha' : Tendsto ((fun x_1 => x_1 / x) ∘ u) atTop (𝓝 a)
⊢ x ≠ 0

Tactic:
contrapose! hx

Result:
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n => ‖u n‖)
kpos : 0 ≤ k
x : K
hu' : CauchySeq ((fun x_1 => x_1 / x) ∘ u)
hb : ∀ (n : ℕ), ((fun x_1 => x_1 / x) ∘ u) n ∈ Metric.closedBall 0 1
a : K
ha' : Tendsto ((fun x_1 => x_1 / x) ∘ u) atTop (𝓝 a)
hx : x = 0
⊢ ‖x‖ ≤ k

Proof state:
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n => ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 => x_1 / x) ∘ u)
n✝ : ℕ
⊢ ‖u n✝‖ / ‖x‖ ≤ 1

Tactic:
rw [div_le_one (kpos.trans_lt hx)]

Result:
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n => ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 => x_1 / x) ∘ u)
n✝ : ℕ
⊢ ‖u n✝‖ ≤ ‖x‖

Proof state:
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n => ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 => x_1 / x) ∘ u)
n✝ : ℕ
⊢ ((fun x_1 => x_1 / x) ∘ u) n✝ ∈ Metric.closedBall 0 1

Tactic:
simp only [Function.comp_apply, Metric.mem_closedBall, dist_zero_right, norm_div]

Result:
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n => ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 => x_1 / x) ∘ u)
n✝ : ℕ
⊢ ‖u n✝‖ / ‖x‖ ≤ 1

Proof state:
K : Type u_4
inst✝ : NormedField K
⊢ CompleteSpace K ↔ IsComplete (Metric.closedBall 0 1)

Tactic:
constructor <;> intro h

Result:
case mp
K : Type u_4
inst✝ : NormedField K
h : CompleteSpace K
⊢ IsComplete (Metric.closedBall 0 1)

case mpr
K : Type u_4
inst✝ : NormedField K
h : IsComplete (Metric.closedBall 0 1)
⊢ CompleteSpace K