-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem LinearIndependent.eventually {ι} [Finite ι] {f : ι → E}
    (hf : LinearIndependent 𝕜 f) : ∀ᶠ g in 𝓝 f, LinearIndependent 𝕜 g

Proof state:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
⊢ dist
      ((⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) -
          ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)))
        v)
      ((⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) -
          ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)))
        u) ≤
    ↑(∑ i : ι, ‖g i - f i‖₊) * dist v u

Tactic:
simp only [dist_eq_norm, LinearMap.lsum_apply, Pi.sub_apply, LinearMap.sum_apply,
  LinearMap.comp_apply, LinearMap.proj_apply, LinearMap.smulRight_apply, LinearMap.id_apply, ←
  Finset.sum_sub_distrib, ← smul_sub, ← sub_smul, NNReal.coe_sum, coe_nnnorm, Finset.sum_mul]

Result:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
⊢ ‖∑ x : ι, (v x - u x) • (g x - f x)‖ ≤ ∑ i : ι, ‖g i - f i‖ * ‖v - u‖

Proof state:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
⊢ Function.Injective ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i))

Tactic:
refine (hK.add_sub_lipschitzWith (LipschitzWith.of_dist_le_mul fun v u => ?_) hg).injective

Result:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
⊢ dist
      ((⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) -
          ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)))
        v)
      ((⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) -
          ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)))
        u) ≤
    ↑(∑ i : ι, ‖g i - f i‖₊) * dist v u

Proof state:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 (∑ i : ι, ‖f i - f i‖))
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥

Tactic:
simp only [sub_self, norm_zero, Finset.sum_const_zero] at this

Result:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥

Proof state:
case intro.intro.intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖g i - f i‖ * ‖v i - u i‖ ≤ ‖g i - f i‖ * ‖v - u‖

Tactic:
gcongr

Result:
case intro.intro.intro.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖v i - u i‖ ≤ ‖v - u‖

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖ < ((fun a => ↑a) K)⁻¹
⊢ ∑ i : ι, ‖g i - f i‖₊ < K⁻¹

Tactic:
rw [← NNReal.coe_lt_coe]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖ < ((fun a => ↑a) K)⁻¹
⊢ ↑(∑ i : ι, ‖g i - f i‖₊) < ↑K⁻¹