awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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)
⊢ Tendsto (β := ℝ) (fun (g : ι → E) ↦ ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 (∑ i : ι, ‖f i - f i‖))

Tactic:
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
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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‖))
⊢ Tendsto (β := ℝ) (fun (g : ι → E) ↦ ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)

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

Premises used: sub_self, norm_zero, Finset.sum_const_zero
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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)))
      ⊥

Tactic:
(this.eventually (gt_mem_nhds <| inv_pos.2 K0)).mono fun g hg => ?_

Premises used: Iff.mpr, gt_mem_nhds, inv_pos, Filter.Eventually.mono, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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)
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)))
      ⊥
⊢ ∀ᶠ (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:
refine (this.eventually (gt_mem_nhds <| inv_pos.2 K0)).mono fun g hg => ?_

Premises used: Iff.mpr, gt_mem_nhds, inv_pos, Filter.Eventually.mono, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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 : ℝ)⁻¹
push_cast : ∑ x : ι, ‖g x - f x‖ < (↑K : ℝ)⁻¹
⊢ (↑(∑ i : ι, ‖g i - f i‖₊) : ℝ) < (↑K⁻¹ : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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 : ℝ)⁻¹
⊢ ∑ x : ι, ‖g x - f x‖ < (↑K : ℝ)⁻¹

Tactic:
hg

Premises used: NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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 : ℝ)⁻¹
⊢ ∑ x : ι, ‖g x - f x‖ < (↑K : ℝ)⁻¹

Tactic:
exact hg
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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⁻¹

Tactic:
replace hg : ∑ i, ‖g i - f i‖₊ < K⁻¹ := by
    rw [← NNReal.coe_lt_coe]
    push_cast
    exact hg
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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⁻¹
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)
⊢ 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:
rw [LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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)

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

Premises used: AntilipschitzWith.injective, LipschitzWith.of_dist_le_mul, AntilipschitzWith.add_sub_lipschitzWith
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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⁻¹
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
⊢ 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:
refine (hK.add_sub_lipschitzWith (LipschitzWith.of_dist_le_mul fun v u => ?_) hg).injective

Premises used: AntilipschitzWith.injective, LipschitzWith.of_dist_le_mul, AntilipschitzWith.add_sub_lipschitzWith
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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 : ι) → 𝕜
intro : norm.{v} (E := E) (∑ x : ι, (v x - u x) • (g x - f x)) ≤ ∑ i : ι, ‖g i - f i‖ * ‖v - u‖
⊢ 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:
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]

Premises used: dist_eq_norm, LinearMap.id_apply, LinearMap.smulRight_apply, LinearMap.lsum_apply, LinearMap.proj_apply, sub_smul, LinearMap.comp_apply, NNReal.coe_sum, smul_sub, Finset.sum_sub_distrib, coe_nnnorm, LinearMap.sum_apply, Finset.sum_mul, Pi.sub_apply
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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‖

Tactic:
norm_sum_le_of_le _ fun i _ => ?_

Premises used: norm_sum_le_of_le
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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 : ι) → 𝕜
intro : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → ‖(v i - u i) • (g i - f i)‖ ≤ ‖g i - f i‖ * ‖v - u‖
⊢ norm.{v} (E := E) (∑ x : ι, (v x - u x) • (g x - f x)) ≤ ∑ i : ι, ‖g i - f i‖ * ‖v - u‖

Tactic:
refine norm_sum_le_of_le _ fun i _ => ?_

Premises used: norm_sum_le_of_le
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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
intro : ‖g i - f i‖ * ‖v i - u i‖ ≤ ‖g i - f i‖ * ‖v - u‖
⊢ ‖(v i - u i) • (g i - f i)‖ ≤ ‖g i - f i‖ * ‖v - u‖

Tactic:
rw [norm_smul, mul_comm]

Premises used: norm_smul, mul_comm
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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
intro : ‖v i - u i‖ ≤ ‖v - u‖
⊢ ‖g i - f i‖ * ‖v i - u i‖ ≤ ‖g i - f i‖ * ‖v - u‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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‖ ≤ ‖v - u‖

Tactic:
exact norm_le_pi_norm (v - u) i

Premises used: HSub.hSub, norm_le_pi_norm
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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] {f : ι → E | LinearIndependent 𝕜 f}

Tactic:
isOpen_iff_mem_nhds.2 fun _ => LinearIndependent.eventually

Premises used: Iff.mpr, LinearIndependent.eventually, isOpen_iff_mem_nhds
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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 : ℕ
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)})
⊢ IsOpen (X := E →L[𝕜] F) {f : E →L[𝕜] F | (↑n : Cardinal.{w}) ≤ (↑f : E →ₗ[𝕜] F).rank}

Tactic:
simp only [LinearMap.le_rank_iff_exists_linearIndependent_finset, setOf_exists, ← exists_prop]

Premises used: Set.setOf_exists, exists_prop, LinearMap.le_rank_iff_exists_linearIndependent_finset