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

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)⁻¹
⊢ ∑ x : ι, ‖g x - f x‖ < (↑K)⁻¹

Tactic:
exact hg

Result:
no goals

Proof state:
case 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)) = ⊥
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥

Tactic:
rcases LinearMap.exists_antilipschitzWith _ hf with ⟨K, K0, hK⟩

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))
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥

Proof state:
case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
hf : LinearIndependent 𝕜 f
val✝ : Fintype ι
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g

Tactic:
simp only [Fintype.linearIndependent_iff'] at hf ⊢

Result:
case 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)) = ⊥
⊢ ∀ᶠ (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‖ < ((fun a => ↑a) K)⁻¹
⊢ LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥

Tactic:
replace hg : ∑ i, ‖g i - f i‖₊ < K⁻¹ := by
  rw [← NNReal.coe_lt_coe]
  push_cast
  exact hg

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⁻¹
⊢ LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥

Proof state:
case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
hf : LinearIndependent 𝕜 f
val✝ : Fintype ι
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g

Tactic:
classical
simp only [Fintype.linearIndependent_iff'] at hf ⊢
rcases LinearMap.exists_antilipschitzWith _ hf with ⟨K, K0, hK⟩
have : Tendsto (fun g : ι → E => ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 <| ∑ i, ‖f i - f i‖) :=
  tendsto_finset_sum _ fun i _ =>
    Tendsto.norm <| ((continuous_apply i).tendsto _).sub tendsto_const_nhds
simp only [sub_self, norm_zero, Finset.sum_const_zero] at this
refine (this.eventually (gt_mem_nhds <| inv_pos.2 K0)).mono fun g hg => ?_
replace hg : ∑ i, ‖g i - f i‖₊ < K⁻¹ := by
  rw [← NNReal.coe_lt_coe]
  push_cast
  exact hg
rw [LinearMap.ker_eq_bot]
refine (hK.add_sub_lipschitzWith (LipschitzWith.of_dist_le_mul fun v u => ?_) hg).injective
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]
refine norm_sum_le_of_le _ fun i _ => ?_
rw [norm_smul, mul_comm]
gcongr
exact norm_le_pi_norm (v - u) i

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
hf : LinearIndependent 𝕜 f
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g

Tactic:
cases nonempty_fintype ι

Result:
case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
hf : LinearIndependent 𝕜 f
val✝ : Fintype ι
⊢ ∀ᶠ (g : ι → E) 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))
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥

Tactic:
have : Tendsto (fun g : ι → E => ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 <| ∑ i, ‖f i - f i‖) :=
  tendsto_finset_sum _ fun i _ =>
    Tendsto.norm <| ((continuous_apply i).tendsto _).sub tendsto_const_nhds

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) (𝓝 (∑ i : ι, ‖f i - f i‖))
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (g i)) = ⊥