awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
inl : Subsingleton E → ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
⊢ ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
have inr : Nontrivial E → ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
Tactic: cases subsingleton_or_nontrivial E
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
h : Nontrivial E
⊢ ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
have hf₁ : Function.Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F)
Tactic: rw [LinearMap.ker_eq_bot] at hf
Cleared hypotheses: hf, h
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
⊢ Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F) ↔
    ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
have mp : Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F) →
  ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
Tactic: constructor
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
mp :
  Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F) →
    ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
⊢ Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F) ↔
    ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
have mpr : (∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)) →
  Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F)
Tactic: constructor
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
⊢ Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F) →
    ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
have mp : f.ker = ⊥ → ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
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
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
PE : Type u_1
PF : Type u_2
inst_6 : MetricSpace PE
inst_7 : NormedAddTorsor E PE
inst_8 : MetricSpace PF
inst_9 : NormedAddTorsor F PF
inst_10 : FiniteDimensional 𝕜 E
f : PE →ᵃ[𝕜] PF
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := PE) (β := PF) (⇑f : (a : PE) → PF)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_1, u_2} (α := PE) (β := PF) K (⇑f : (a : PE) → PF)
have obtain : ∀ (K : ℝ≥0) (hK : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f.linear : (a : E) → F)),
  ∃ (K : ℝ≥0), AntilipschitzWith.{u_1, u_2} (α := PE) (β := PF) K (⇑f : (a : PE) → PF)
Tactic: obtain ⟨K, -, hK⟩ := f.linear.injective_iff_antilipschitz.mp (f.linear_injective_iff.mpr 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 𝕜
PE : Type u_1
PF : Type u_2
inst_6 : MetricSpace PE
inst_7 : NormedAddTorsor E PE
inst_8 : MetricSpace PF
inst_9 : NormedAddTorsor F PF
inst_10 : FiniteDimensional 𝕜 E
f : PE →ᵃ[𝕜] PF
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := PE) (β := PF) (⇑f : (a : PE) → PF)
K : ℝ≥0
hK : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f.linear : (a : E) → F)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_1, u_2} (α := PE) (β := PF) K (⇑f : (a : PE) → PF)
have refine : ∀ (x y : PE), dist x y ≤ (↑K : ℝ) * dist.{u_2} (α := PF) ((f : (a : PE) → PF) x : PF) ((f : (a : PE) → PF) y : PF)
Tactic: refine ⟨K, AntilipschitzWith.of_le_mul_dist fun x y ↦ ?_⟩
-- 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 𝕜
PE : Type u_1
PF : Type u_2
inst_6 : MetricSpace PE
inst_7 : NormedAddTorsor E PE
inst_8 : MetricSpace PF
inst_9 : NormedAddTorsor F PF
inst_10 : FiniteDimensional 𝕜 E
f : PE →ᵃ[𝕜] PF
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := PE) (β := PF) (⇑f : (a : PE) → PF)
K : ℝ≥0
hK : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f.linear : (a : E) → F)
x y : PE
⊢ dist x y ≤ (↑K : ℝ) * dist.{u_2} (α := PF) ((f : (a : PE) → PF) x : PF) ((f : (a : PE) → PF) y : PF)
have rw : ‖x -ᵥ y‖ ≤ (↑K : ℝ) * norm.{w} (E := F) ((f.linear : (a : E) → F) (x -ᵥ y) : F)
Tactic: rw [dist_eq_norm_vsub E, dist_eq_norm_vsub F, ← f.linearMap_vsub]
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
⊢ IsOpen (X := E →L[𝕜] F) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
have rw : ∀ (x : E →L[𝕜] F),
  Membership.mem (γ := Set (E →L[𝕜] F)) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
      x →
    ∀ᶠ (y : E →L[𝕜] F) in 𝓝 x,
      Membership.mem (γ := Set (E →L[𝕜] F))
        {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)} y
Tactic: rw [isOpen_iff_eventually]
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ :
  Membership.mem (γ := Set (E →L[𝕜] F)) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
    φ₀
⊢ ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀,
    Membership.mem (γ := Set (E →L[𝕜] F))
      {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)} y
have rcases : ∀ (K : ℝ≥0) (K_pos : K > 0) (H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ₀ : E →ₗ[𝕜] F) : (a : E) → F)),
  ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀,
    Membership.mem (γ := Set (E →L[𝕜] F))
      {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)} y
Tactic: rcases φ₀.injective_iff_antilipschitz.mp hφ₀ with ⟨K, K_pos, H⟩
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ :
  Membership.mem (γ := Set (E →L[𝕜] F)) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
    φ₀
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ₀ : E →ₗ[𝕜] F) : (a : E) → F)
⊢ ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀,
    Membership.mem (γ := Set (E →L[𝕜] F))
      {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)} y
have this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
Tactic: have : ∀ᶠ φ in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹ := eventually_nnnorm_sub_lt _ <| inv_pos_of_pos K_pos
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ :
  Membership.mem (γ := Set (E →L[𝕜] F)) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
    φ₀
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ₀ : E →ₗ[𝕜] F) : (a : E) → F)
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
⊢ ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀,
    Membership.mem (γ := Set (E →L[𝕜] F))
      {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)} y
have h : ∀ (φ : E →L[𝕜] F) (hφ : ‖φ - φ₀‖₊ < K⁻¹), Injective.{v + 1, w + 1} (α := E) (β := F) (⇑φ : (a : E) → F)
Tactic: filter_upwards [this] with φ hφ
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ :
  Membership.mem (γ := Set (E →L[𝕜] F)) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
    φ₀
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ₀ : E →ₗ[𝕜] F) : (a : E) → F)
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
φ : E →L[𝕜] F
hφ : ‖φ - φ₀‖₊ < K⁻¹
⊢ Injective.{v + 1, w + 1} (α := E) (β := F) (⇑φ : (a : E) → F)
have h : ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ : E →ₗ[𝕜] F) : (a : E) → F)
Tactic: apply φ.injective_iff_antilipschitz.mpr
-- 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 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
⊢ Continuous[Pi.topologicalSpace, topologicalSpace]
    (⇑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜) ≪≫ₗ
          LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
      (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
have refine : ∀ (g : ι → E),
  norm (E := (ι → 𝕜) →L[𝕜] E)
      ((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                  ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
              (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
            (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
          g :
        (ι → 𝕜) →L[𝕜] E) ≤
    (↑(Fintype.card ι) : ℝ) * ‖g‖
Tactic: refine AddMonoidHomClass.continuous_of_bound
        (LinearMap.toContinuousLinearMap.toLinearMap.comp
            (LinearEquiv.piRing 𝕜 E ι 𝕜).symm.toLinearMap)
        (Fintype.card ι : ℝ) fun g ↦ ?_
-- 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 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
⊢ norm (E := (ι → 𝕜) →L[𝕜] E)
      ((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                  ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
              (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
            (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
          g :
        (ι → 𝕜) →L[𝕜] E) ≤
    (↑(Fintype.card ι) : ℝ) * ‖g‖
have rw : norm (E := (ι → 𝕜) →L[𝕜] E)
    ((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) : ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
              (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
            (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
          (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
        g :
      (ι → 𝕜) →L[𝕜] E) ≤
  Fintype.card ι • ‖g‖
Tactic: rw [← nsmul_eq_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
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
⊢ norm (E := (ι → 𝕜) →L[𝕜] E)
      ((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                  ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
              (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
            (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
          g :
        (ι → 𝕜) →L[𝕜] E) ≤
    Fintype.card ι • ‖g‖
have refine : ∀ (t : ι → 𝕜),
  norm.{v} (E := E)
      ((((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                        ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                      (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
                    (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
                  (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
                g :
              (ι → 𝕜) →L[𝕜] E) :
            (a : ι → 𝕜) → E)
          t :
        E) ≤
    Fintype.card ι • ‖g‖ * ‖t‖
Tactic: refine opNorm_le_bound _ (nsmul_nonneg (norm_nonneg g) (Fintype.card ι)) fun t ↦ ?_
-- 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 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
⊢ norm.{v} (E := E)
      ((((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                        ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                      (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
                    (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
                  (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
                g :
              (ι → 𝕜) →L[𝕜] E) :
            (a : ι → 𝕜) → E)
          t :
        E) ≤
    Fintype.card ι • ‖g‖ * ‖t‖
have simp_rw : norm.{v} (E := E) (∑ i : ι, t i • g i) ≤ Fintype.card ι • ‖g‖ * ‖t‖
Tactic: simp_rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply,
        LinearMap.coe_toContinuousLinearMap', LinearEquiv.piRing_symm_apply]
-- 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 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
⊢ norm.{v} (E := E) (∑ i : ι, t i • g i) ≤ Fintype.card ι • ‖g‖ * ‖t‖
have apply : ∑ i : ι, ‖t i • g i‖ ≤ Fintype.card ι • ‖g‖ * ‖t‖
Tactic: apply le_trans (norm_sum_le _ _)
-- 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 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
⊢ ∑ i : ι, ‖t i • g i‖ ≤ Fintype.card ι • ‖g‖ * ‖t‖
have rw : ∑ i : ι, ‖t i • g i‖ ≤ Fintype.card ι • (‖g‖ * ‖t‖)
Tactic: rw [smul_mul_assoc]
-- 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 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
⊢ ∑ i : ι, ‖t i • g i‖ ≤ Fintype.card ι • (‖g‖ * ‖t‖)
have refine : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → ‖t i • g i‖ ≤ ‖g‖ * ‖t‖
Tactic: refine Finset.sum_le_card_nsmul _ _ _ 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
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ‖t i • g i‖ ≤ ‖g‖ * ‖t‖
have rw : ‖g i‖ * ‖t i‖ ≤ ‖g‖ * ‖t‖
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
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ‖g i‖ * ‖t i‖ ≤ ‖g‖ * ‖t‖
have h₁ : ‖g i‖ ≤ ‖g‖
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
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
h₁ : ‖g i‖ ≤ ‖g‖
⊢ ‖g i‖ * ‖t i‖ ≤ ‖g‖ * ‖t‖
have h₂ : ‖t i‖ ≤ ‖t‖
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
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g
have intro : ∀ (val : Fintype ι), ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g
Tactic: cases nonempty_fintype ι
-- 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: simp only [Fintype.linearIndependent_iff'] at hf ⊢
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
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)))
    ⊥
⊢ ∀ᶠ (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 : ∀ (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: rcases LinearMap.exists_antilipschitzWith _ hf with ⟨K, K0, hK⟩
-- 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)
⊢ ∀ᶠ (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) (𝓝 (∑ 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