-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem FiniteDimensional.of_isCompact_closedBall₀ {r : ℝ} (rpos : 0 < r)
    (h : IsCompact (Metric.closedBall (0 : E) r)) : FiniteDimensional 𝕜 E

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
⊢ False

Tactic:
let g := fun n : ℕ => c • f n

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
g : ℕ → E := fun n => c • f n
⊢ False

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
g : ℕ → E := fun n => c • f n
A : ∀ (n : ℕ), g n ∈ closedBall 0 r
⊢ False

Tactic:
obtain ⟨x : E, _ : x ∈ Metric.closedBall (0 : E) r, φ : ℕ → ℕ, φmono : StrictMono φ,
  φlim : Tendsto (g ∘ φ) atTop (𝓝 x)⟩ := h.tendsto_subseq A

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
g : ℕ → E := fun n => c • f n
A : ∀ (n : ℕ), g n ∈ closedBall 0 r
x : E
left✝ : x ∈ closedBall 0 r
φ : ℕ → ℕ
φmono : StrictMono φ
φlim : Tendsto (g ∘ φ) atTop (𝓝 x)
⊢ False

Proof state:
case h₂
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
g : ℕ → E := fun n => c • f n
n : ℕ
⊢ ‖f n‖ ≤ R

Tactic:
apply fle

Result:
no goals

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
g : ℕ → E := fun n => c • f n
n : ℕ
⊢ r / R * R = r

Tactic:
field_simp [(zero_lt_one.trans Rgt).ne']

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
g : ℕ → E := fun n => c • f n
A : ∀ (n : ℕ), g n ∈ closedBall 0 r
x : E
left✝ : x ∈ closedBall 0 r
φ : ℕ → ℕ
φmono : StrictMono φ
φlim : Tendsto (g ∘ φ) atTop (𝓝 x)
B : CauchySeq (g ∘ φ)
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist ((g ∘ φ) n) ((g ∘ φ) N) < ‖c‖
⊢ False

Tactic:
apply lt_irrefl ‖c‖

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
g : ℕ → E := fun n => c • f n
A : ∀ (n : ℕ), g n ∈ closedBall 0 r
x : E
left✝ : x ∈ closedBall 0 r
φ : ℕ → ℕ
φmono : StrictMono φ
φlim : Tendsto (g ∘ φ) atTop (𝓝 x)
B : CauchySeq (g ∘ φ)
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist ((g ∘ φ) n) ((g ∘ φ) N) < ‖c‖
⊢ ‖c‖ < ‖c‖

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
g : ℕ → E := fun n => c • f n
A : ∀ (n : ℕ), g n ∈ closedBall 0 r
x : E
left✝ : x ∈ closedBall 0 r
φ : ℕ → ℕ
φmono : StrictMono φ
φlim : Tendsto (g ∘ φ) atTop (𝓝 x)
B : CauchySeq (g ∘ φ)
N : ℕ
hN : ∀ (n : ℕ), N ≤ n → dist ((g ∘ φ) n) ((g ∘ φ) N) < ‖c‖
⊢ ‖c‖ < ‖c‖

Tactic:
calc
  ‖c‖ ≤ dist (g (φ (N + 1))) (g (φ N)) := by
    conv_lhs => rw [← mul_one ‖c‖]
    simp only [g, dist_eq_norm, ← smul_sub, norm_smul]
    gcongr
    apply lef (ne_of_gt _)
    exact φmono (Nat.lt_succ_self N)
  _ < ‖c‖ := hN (N + 1) (Nat.le_succ N)

Result:
no goals

Proof state:
case h₁
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
g : ℕ → E := fun n => c • f n
n : ℕ
⊢ ‖c‖ ≤ r / R

Tactic:
exact hc.2.le

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
g : ℕ → E := fun n => c • f n
A : ∀ (n : ℕ), g n ∈ closedBall 0 r
x : E
left✝ : x ∈ closedBall 0 r
φ : ℕ → ℕ
φmono : StrictMono φ
φlim : Tendsto (g ∘ φ) atTop (𝓝 x)
⊢ False

Tactic:
have B : CauchySeq (g ∘ φ) := φlim.cauchySeq

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
r : ℝ
rpos : 0 < r
h : IsCompact (closedBall 0 r)
hfin : ¬FiniteDimensional 𝕜 E
R : ℝ
f : ℕ → E
Rgt : 1 < R
fle : ∀ (n : ℕ), ‖f n‖ ≤ R
lef : Pairwise fun m n => 1 ≤ ‖f m - f n‖
rRpos : 0 < r / R
c : 𝕜
hc : 0 < ‖c‖ ∧ ‖c‖ < r / R
g : ℕ → E := fun n => c • f n
A : ∀ (n : ℕ), g n ∈ closedBall 0 r
x : E
left✝ : x ∈ closedBall 0 r
φ : ℕ → ℕ
φmono : StrictMono φ
φlim : Tendsto (g ∘ φ) atTop (𝓝 x)
B : CauchySeq (g ∘ φ)
⊢ False