-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace 𝕜
ι : Type u_1
inst_4 : Finite ι
f : ι → E
hf : LinearIndependent 𝕜 f
val : Fintype ι
intro :
  ∀
    (hf :
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (f i)))
        ⊥),
    ∀ᶠ (g : ι → E) in 𝓝 f,
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (g i)))
        ⊥
intro₁ :
  ∀
    (hf :
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (f i)))
        ⊥)
    (K : ℝ≥0) (K0 : K > 0)
    (hK :
      AntilipschitzWith (α := (i : ι) → 𝕜) (β := E) K
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (f i)) :
          (a : (i : ι) → 𝕜) → E)),
    ∀ᶠ (g : ι → E) in 𝓝 f,
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (g i)))
        ⊥
intro₂ :
  ∀
    (hf :
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (f i)))
        ⊥)
    (K : ℝ≥0) (K0 : K > 0)
    (hK :
      AntilipschitzWith (α := (i : ι) → 𝕜) (β := E) K
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (f i)) :
          (a : (i : ι) → 𝕜) → E))
    (this : Tendsto (β := ℝ) (fun (g : ι → E) ↦ ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 (∑ i : ι, ‖f i - f i‖))),
    ∀ᶠ (g : ι → E) in 𝓝 f,
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (g i)))
        ⊥
intro₃ :
  ∀
    (hf :
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (f i)))
        ⊥)
    (K : ℝ≥0) (K0 : K > 0)
    (hK :
      AntilipschitzWith (α := (i : ι) → 𝕜) (β := E) K
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (f i)) :
          (a : (i : ι) → 𝕜) → E))
    (this : Tendsto (β := ℝ) (fun (g : ι → E) ↦ ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)),
    ∀ᶠ (g : ι → E) in 𝓝 f,
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (g i)))
        ⊥
intro₄ :
  ∀
    (hf :
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (f i)))
        ⊥)
    (K : ℝ≥0) (K0 : K > 0)
    (hK :
      AntilipschitzWith (α := (i : ι) → 𝕜) (β := E) K
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (f i)) :
          (a : (i : ι) → 𝕜) → E))
    (this : Tendsto (β := ℝ) (fun (g : ι → E) ↦ ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)) (g : ι → E)
    (hg : ∑ i : ι, ‖g i - f i‖ < (↑K : ℝ)⁻¹),
    Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
      (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
        ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
          LinearMap.smulRight LinearMap.id (g i)))
      ⊥
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g
have intro₅ : ∀
  (hf :
    Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
      (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
        ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
          LinearMap.smulRight LinearMap.id (f i)))
      ⊥)
  (K : ℝ≥0) (K0 : K > 0)
  (hK :
    AntilipschitzWith (α := (i : ι) → 𝕜) (β := E) K
      (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (f i)) :
        (a : (i : ι) → 𝕜) → E))
  (this : Tendsto (β := ℝ) (fun (g : ι → E) ↦ ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)) (g : ι → E)
  (hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹),
  Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
      ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
        LinearMap.smulRight LinearMap.id (g i)))
    ⊥
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_finsetSum _ 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
Cleared hypotheses: hf