-- 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.inl
K : Type u_4
inst✝ : NormedField K
h : IsComplete (Metric.closedBall 0 1)
h✝ : DiscreteTopology K
⊢ CompleteSpace K

Tactic:
rwa [completeSpace_iff_isComplete_univ,
     ← NormedDivisionRing.unitClosedBall_eq_univ_of_discrete]

Result:
no goals

Proof state:
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‖
hu' : CauchySeq ((fun x_1 => x_1 / x) ∘ u)
hb : ∀ (n : ℕ), ((fun x_1 => x_1 / x) ∘ u) n ∈ Metric.closedBall 0 1
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨a, -, ha'⟩ := cauchySeq_tendsto_of_isComplete h hb hu'

Result:
case mpr.inr.intro.mk.intro.intro.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‖
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)
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Proof state:
case mpr.inr.intro.mk.intro.intro.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‖
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_1 : ℕ), ((fun b => b * x) ∘ (fun x_2 => x_2 / x) ∘ u) x_1 = u x_1

Tactic:
simp [div_mul_cancel₀ _ hx']

Result:
no goals

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‖

Tactic:
exact hx.le.trans' (hk (by simp))

Result:
no goals

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

Tactic:
exact Metric.isClosed_closedBall.isComplete

Result:
no goals

Proof state:
case mpr.inr.intro.mk
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
⊢ CompleteSpace K

Tactic:
refine Metric.complete_of_cauchySeq_tendsto fun u hu ↦ ?_

Result:
case mpr.inr.intro.mk
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (𝓝 a)

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

Tactic:
rcases NormedField.discreteTopology_or_nontriviallyNormedField K with _|⟨_, rfl⟩

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

case mpr.inr.intro.mk
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
⊢ CompleteSpace 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✝‖ ∈ Set.range fun n => ‖u n‖

Tactic:
simp

Result:
no goals

Proof state:
case mpr.inr.intro.mk.intro.intro.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‖
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_1 : ℕ), ((fun b => b * x) ∘ (fun x_2 => x_2 / x) ∘ u) x_1 = u x_1

Tactic:
have hx' : x ≠ 0 := by
  contrapose! hx
  simp [hx, kpos]

Result:
case mpr.inr.intro.mk.intro.intro.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‖
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_1 : ℕ), ((fun b => b * x) ∘ (fun x_2 => x_2 / x) ∘ u) x_1 = u x_1

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‖)
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
have kpos : 0 ≤ k := (_root_.norm_nonneg (u 0)).trans (hk (by simp))

Result:
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)

Proof state:
case mpr.inr.intro.mk
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (Metric.closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
obtain ⟨k, hk⟩ := hu.norm_bddAbove

Result:
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‖)
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Proof state:
case mpr.inr.intro.mk.intro.intro.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‖
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)
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
refine ⟨a * x, (((continuous_mul_right x).tendsto a).comp ha').congr ?_⟩

Result:
case mpr.inr.intro.mk.intro.intro.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‖
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_1 : ℕ), ((fun b => b * x) ∘ (fun x_2 => x_2 / x) ∘ u) x_1 = u x_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‖)
⊢ ‖u 0‖ ∈ Set.range fun n => ‖u n‖

Tactic:
simp

Result:
no goals

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
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

Tactic:
simp [hx, kpos]

Result:
no goals