awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
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
val : Fintype ι
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)))
      ⊥
have this₁ : Tendsto (β := ℝ) (fun (g : ι → E) ↦ ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
Tactic: simp only [sub_self, norm_zero, Finset.sum_const_zero] at this
Cleared hypotheses: this
-- 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
val : Fintype ι
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)))
      ⊥
have intro : ∀ (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: refine (this.eventually (gt_mem_nhds <| inv_pos.2 K0)).mono fun g hg => ?_
-- 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
val : Fintype ι
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 : ℝ)⁻¹
⊢ (↑(∑ i : ι, ‖g i - f i‖₊) : ℝ) < (↑K⁻¹ : ℝ)
have push_cast : ∑ x : ι, ‖g x - f x‖ < (↑K : ℝ)⁻¹
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
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
val : Fintype ι
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)))
    ⊥
have hg₁ : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
Tactic: replace hg : ∑ i, ‖g i - f i‖₊ < K⁻¹ := by
    rw [← NNReal.coe_lt_coe]
    push_cast
    exact hg
Cleared hypotheses: hg
-- 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
val : Fintype ι
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)))
    ⊥
have intro : Function.Injective (α := (i : ι) → 𝕜) (β := E)
  (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
        LinearMap.smulRight LinearMap.id (g i)) :
    (a : (i : ι) → 𝕜) → E)
Tactic: rw [LinearMap.ker_eq_bot]
-- 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
val : Fintype ι
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⁻¹
⊢ Function.Injective (α := (i : ι) → 𝕜) (β := E)
    (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
          LinearMap.smulRight LinearMap.id (g i)) :
      (a : (i : ι) → 𝕜) → E)
have intro : ∀ (v u : (i : ι) → 𝕜),
  dist
      (HSub.hSub (α := ((i : ι) → 𝕜) → E) (β := ((i : ι) → 𝕜) → E)
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (g i)) :
          (a : (i : ι) → 𝕜) → E)
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (f i)) :
          (a : (i : ι) → 𝕜) → E)
        v)
      (HSub.hSub (α := ((i : ι) → 𝕜) → E) (β := ((i : ι) → 𝕜) → E)
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (g i)) :
          (a : (i : ι) → 𝕜) → E)
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (f i)) :
          (a : (i : ι) → 𝕜) → E)
        u) ≤
    (↑(∑ i : ι, ‖g i - f i‖₊) : ℝ) * dist v u
Tactic: refine (hK.add_sub_lipschitzWith (LipschitzWith.of_dist_le_mul fun v u => ?_) hg).injective
-- 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
val : Fintype ι
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⁻¹
v u : (i : ι) → 𝕜
⊢ dist
      (HSub.hSub (α := ((i : ι) → 𝕜) → E) (β := ((i : ι) → 𝕜) → E)
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (g i)) :
          (a : (i : ι) → 𝕜) → E)
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (f i)) :
          (a : (i : ι) → 𝕜) → E)
        v)
      (HSub.hSub (α := ((i : ι) → 𝕜) → E) (β := ((i : ι) → 𝕜) → E)
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (g i)) :
          (a : (i : ι) → 𝕜) → E)
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (f i)) :
          (a : (i : ι) → 𝕜) → E)
        u) ≤
    (↑(∑ i : ι, ‖g i - f i‖₊) : ℝ) * dist v u
have intro : norm.{v} (E := E) (∑ x : ι, (v x - u x) • (g x - f x)) ≤ ∑ i : ι, ‖g i - f i‖ * ‖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]
-- 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
val : Fintype ι
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⁻¹
v u : (i : ι) → 𝕜
⊢ norm.{v} (E := E) (∑ x : ι, (v x - u x) • (g x - f x)) ≤ ∑ i : ι, ‖g i - f i‖ * ‖v - u‖
have intro : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → ‖(v i - u i) • (g i - f i)‖ ≤ ‖g i - f i‖ * ‖v - u‖
Tactic: refine norm_sum_le_of_le _ fun i _ => ?_
-- 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
val : Fintype ι
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⁻¹
v u : (i : ι) → 𝕜
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ‖(v i - u i) • (g i - f i)‖ ≤ ‖g i - f i‖ * ‖v - u‖
have intro : ‖g i - f i‖ * ‖v i - u i‖ ≤ ‖g i - f i‖ * ‖v - u‖
Tactic: rw [norm_smul, mul_comm]
-- 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
val : Fintype ι
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⁻¹
v u : (i : ι) → 𝕜
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ‖g i - f i‖ * ‖v i - u i‖ ≤ ‖g i - f i‖ * ‖v - u‖
have intro : ‖v i - u i‖ ≤ ‖v - u‖
Tactic: gcongr
-- 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 ι
⊢ ∀ᶠ (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)))
      ⊥),
  ∀ᶠ (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)))
      ⊥
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
-- 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)))
        ⊥
⊢ ∀ᶠ (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)),
  ∀ᶠ (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)))
      ⊥
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
-- 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
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
n : ℕ
⊢ IsOpen (X := E →L[𝕜] F) {f : E →L[𝕜] F | (↑n : Cardinal.{w}) ≤ (↑f : E →ₗ[𝕜] F).rank}
have simp : IsOpen (X := E →L[𝕜] F)
  (⋃ (i : Finset E),
    ⋃ (_ : i.card = n),
      {x : E →L[𝕜] F |
        LinearIndependent.{v, u, w} 𝕜 (M := F) fun (x_1 : (↑(↑i : Set E) : Type v)) ↦
          ((↑x : E →ₗ[𝕜] F) : (a : E) → F) (↑x_1 : E)})
Tactic: simp only [LinearMap.le_rank_iff_exists_linearIndependent_finset, setOf_exists, ← exists_prop]
-- 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
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
n : ℕ
⊢ IsOpen (X := E →L[𝕜] F)
    (⋃ (i : Finset E),
      ⋃ (_ : i.card = n),
        {x : E →L[𝕜] F |
          LinearIndependent.{v, u, w} 𝕜 (M := F) fun (x_1 : (↑(↑i : Set E) : Type v)) ↦
            ((↑x : E →ₗ[𝕜] F) : (a : E) → F) (↑x_1 : E)})
have refine : ∀ (t : Finset E),
  Membership.mem (γ := Set (Finset E)) (fun (i : Finset E) ↦ i.card = n) t →
    IsOpen (X := E →L[𝕜] F)
      {x : E →L[𝕜] F |
        LinearIndependent.{v, u, w} 𝕜 (M := F) fun (x_1 : (↑(↑t : Set E) : Type v)) ↦
          ((↑x : E →ₗ[𝕜] F) : (a : E) → F) (↑x_1 : E)}
Tactic: refine isOpen_biUnion fun t _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
n : ℕ
t : Finset E
h : Membership.mem (γ := Set (Finset E)) (fun (i : Finset E) ↦ i.card = n) t
⊢ IsOpen (X := E →L[𝕜] F)
    {x : E →L[𝕜] F |
      LinearIndependent.{v, u, w} 𝕜 (M := F) fun (x_1 : (↑(↑t : Set E) : Type v)) ↦
        ((↑x : E →ₗ[𝕜] F) : (a : E) → F) (↑x_1 : E)}
have this : Continuous[_, Pi.topologicalSpace] fun (f : E →L[𝕜] F) (x : (↑(↑t : Set E) : Type v)) ↦ (f : (a : E) → F) (↑x : E)
Tactic: have : Continuous fun f : E →L[𝕜] F => fun x : (t : Set E) => f x :=
    continuous_pi fun x => (ContinuousLinearMap.apply 𝕜 F (x : E)).continuous
-- 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 ι
⊢ IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
have inl : ∀ (h : IsEmpty ι), IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
Tactic: rcases isEmpty_or_nonempty ι with h | ⟨⟨i₀⟩⟩
-- 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 ι
inl : ∀ (h : IsEmpty ι), IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
⊢ IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
have inr : ∀ (i₀ : ι), IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
Tactic: rcases isEmpty_or_nonempty ι with h | ⟨⟨i₀⟩⟩
-- 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 ι
i₀ : ι
⊢ IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
have inr : IsOpen[Pi.topologicalSpace]
  {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}
Tactic: simp_rw [affineIndependent_iff_linearIndependent_vsub 𝕜 _ i₀]