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 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
e₁ :
  nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) =
    nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F)
e₂ :
  nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F) =
    nnnorm.{w} (E := F)
      (∑ i : ι,
        HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
e₃ :
  Eq (α := ℝ≥0)
    (∑ i : ι,
      ‖HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F)‖₊)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
e₄ :
  LE.le (α := ℝ≥0)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M)
e₅ :
  ∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M =
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)) * M
e₆ : (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)) * M ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) ≤ Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
have e₇ : Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
Tactic: calc
      ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
      _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]
      _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _
      _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
      _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
        gcongr
        calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
      _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_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 : Finite ι
v : Basis ι 𝕜 E
⊢ ∃ C > 0,
    ∀ {u : E →L[𝕜] F} (M : ℝ≥0),
      (∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M) → ‖u‖₊ ≤ C * M
have intro : ∀ (val : Fintype ι),
  ∃ C > 0,
    ∀ {u : E →L[𝕜] F} (M : ℝ≥0),
      (∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M) → ‖u‖₊ ≤ C * M
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
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Finite ι
v : Basis ι 𝕜 E
⊢ ∃ C > 0,
    ∀ {u : E →L[𝕜] F} {M : ℝ},
      0 ≤ M → (∀ (i : ι), norm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M) → ‖u‖ ≤ C * M
have obtain : ∀ (C : ℝ≥0) (hC : C > 0)
  (h :
    ∀ {u : E →L[𝕜] F} (M : ℝ≥0),
      (∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M) → ‖u‖₊ ≤ C * M),
  ∃ C > 0,
    ∀ {u : E →L[𝕜] F} {M : ℝ},
      0 ≤ M → (∀ (i : ι), norm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M) → ‖u‖ ≤ C * M
Tactic: obtain ⟨C, hC, h⟩ := v.exists_opNNNorm_le (F := F)
-- 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 : Finite ι
v : Basis ι 𝕜 E
C : ℝ≥0
hC : C > 0
h :
  ∀ {u : E →L[𝕜] F} (M : ℝ≥0),
    (∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M) → ‖u‖₊ ≤ C * M
⊢ ∃ C > 0,
    ∀ {u : E →L[𝕜] F} {M : ℝ},
      0 ≤ M → (∀ (i : ι), norm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M) → ‖u‖ ≤ C * M
have refine : ∀ {u : E →L[𝕜] F} {M : ℝ},
  0 ≤ M → (∀ (i : ι), norm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M) → ‖u‖ ≤ (↑C : ℝ) * M
Tactic: refine ⟨C, hC, ?_⟩
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
⊢ ∃ (x : E), ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
have hF : F.FG
Tactic: have hF : F.FG := ⟨s, rfl⟩
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : F.FG
⊢ ∃ (x : E), ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
have this : FiniteDimensional.{u, v} 𝕜 ↥F
Tactic: haveI : FiniteDimensional 𝕜 F := .of_fg hF
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : F.FG
this : FiniteDimensional.{u, v} 𝕜 ↥F
⊢ ∃ (x : E), ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
have Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
Tactic: have Fclosed : IsClosed (F : Set E) := Submodule.closed_of_finiteDimensional _
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : F.FG
this : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
⊢ ∃ (x : E), x ∉ F
have contrapose! : ∀ (h : ∀ (x : E), x ∈ F), FiniteDimensional 𝕜 E
Tactic: contrapose! h
Cleared hypotheses: 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
inst_3 : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : F.FG
this : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
h : ∀ (x : E), x ∈ F
⊢ ⊤ = F
have h₁ : ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) ⊤ x ↔ x ∈ F
Tactic: ext x
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : F.FG
this : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
h : ∀ (x : E), x ∈ F
⊢ FiniteDimensional 𝕜 E
have this₁ : ⊤ = F
Tactic: have : (⊤ : Submodule 𝕜 E) = F := by
      ext x
      simp [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
inst_3 : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : F.FG
this_1 : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
h : ∀ (x : E), x ∈ F
this : ⊤ = F
⊢ FiniteDimensional 𝕜 E
have hF₁ : Submodule.FG.{u, v} (R := 𝕜) (M := E) ⊤
Tactic: rw [← this] at hF
Cleared hypotheses: hF, this_1, Fclosed, h, this
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : F.FG
this : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
⊢ ∃ (x : E), ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
have this₁ : ∃ (x : E), x ∉ F
Tactic: have : ∃ x, x ∉ F := by
    contrapose! h
    have : (⊤ : Submodule 𝕜 E) = F := by
      ext x
      simp [h]
    rw [← this] at hF
    exact .of_fg_top 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : F.FG
this_1 : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
this : ∃ (x : E), x ∉ F
⊢ ∃ (x : E), ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
have obtain : ∀ (x : E) (xR : ‖x‖ ≤ R) (hx : ∀ y ∈ F, 1 ≤ ‖x - y‖), ∃ (x : E), ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
Tactic: obtain ⟨x, xR, hx⟩ : ∃ x : E, ‖x‖ ≤ R ∧ ∀ y : E, y ∈ F → 1 ≤ ‖x - y‖ :=
    riesz_lemma_of_norm_lt hc hR Fclosed 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : F.FG
this_1 : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
this : ∃ (x : E), x ∉ F
x : E
xR : ‖x‖ ≤ R
hx : ∀ y ∈ F, 1 ≤ ‖x - y‖
y : E
hy : y ∈ F
⊢ 1 ≤ ‖y - x‖
have rw : 1 ≤ ‖-(y - x)‖
Tactic: rw [← norm_neg]
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : F.FG
this_1 : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
this : ∃ (x : E), x ∉ F
x : E
xR : ‖x‖ ≤ R
hx : ∀ y ∈ F, 1 ≤ ‖x - y‖
⊢ ∃ (x : E), ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
have hx' : ∀ y ∈ F, 1 ≤ ‖y - x‖
Tactic: have hx' : ∀ y : E, y ∈ F → 1 ≤ ‖y - x‖ := by
    intro y hy
    rw [← norm_neg]
    simpa using hx y hy
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
⊢ Std.Symm fun (x y : E) ↦ 1 ≤ ‖x - y‖
have symm : ∀ (a b : E), 1 ≤ ‖a - b‖ → 1 ≤ ‖b - a‖
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
inst_3 : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
x y : E
hxy : 1 ≤ ‖x - y‖
⊢ 1 ≤ ‖y - x‖
have symm : 1 ≤ ‖-(y - x)‖
Tactic: rw [← norm_neg]
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
⊢ ∃ (f : ℕ → E), (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun (m n : ℕ) ↦ 1 ≤ ‖f m - f n‖
have this : Std.Symm fun (x y : E) ↦ 1 ≤ ‖x - y‖
Tactic: have : Std.Symm fun x y : E => 1 ≤ ‖x - y‖ := by
    constructor
    intro x y hxy
    rw [← norm_neg]
    simpa
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
this : Std.Symm fun (x y : E) ↦ 1 ≤ ‖x - y‖
⊢ ∃ (f : ℕ → E), (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun (m n : ℕ) ↦ 1 ≤ ‖f m - f n‖
have exists_seq_of_forall_finset_exists' : ∀ (s : Finset E), (∀ x ∈ s, ‖x‖ ≤ R) → ∃ (y : E), ‖y‖ ≤ R ∧ ∀ x ∈ s, 1 ≤ ‖x - y‖
Tactic: apply
    exists_seq_of_forall_finset_exists' (fun x : E => ‖x‖ ≤ R) fun (x : E) (y : E) => 1 ≤ ‖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
inst_3 : CompleteSpace 𝕜
h : ¬FiniteDimensional 𝕜 E
⊢ ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun (m n : ℕ) ↦ 1 ≤ ‖f m - f n‖
have obtain : ∀ (c : 𝕜) (hc : 1 < ‖c‖),
  ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun (m n : ℕ) ↦ 1 ≤ ‖f m - f n‖
Tactic: obtain ⟨c, hc⟩ : ∃ c : 𝕜, 1 < ‖c‖ := NormedField.exists_one_lt_norm 𝕜
-- 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 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
⊢ ‖c‖ < ‖c‖ + 1
have linarith : ‖c‖ + 1 ≤ ‖c‖ → -1 + (‖c‖ + 1 - ‖c‖) = 0
Tactic: linarith
-- 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 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
⊢ ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun (m n : ℕ) ↦ 1 ≤ ‖f m - f n‖
have A : ‖c‖ < ‖c‖ + 1
Tactic: have A : ‖c‖ < ‖c‖ + 1 := by linarith
-- 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 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
A : ‖c‖ < ‖c‖ + 1
⊢ ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun (m n : ℕ) ↦ 1 ≤ ‖f m - f n‖
have rcases : ∀ (f : ℕ → E) (hf : (∀ (n : ℕ), ‖f n‖ ≤ ‖c‖ + 1) ∧ Pairwise fun (m n : ℕ) ↦ 1 ≤ ‖f m - f n‖),
  ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun (m n : ℕ) ↦ 1 ≤ ‖f m - f n‖
Tactic: rcases exists_seq_norm_le_one_le_norm_sub' hc A h with ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
⊢ ProperSpace E
have rcases : ∀ (r : ℝ) (rpos : 0 < r) (hr : IsCompact.{u_2} (X := E) (closedBall 0 r)), ProperSpace E
Tactic: rcases exists_isCompact_closedBall (0 : E) with ⟨r, rpos, hr⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_2} (X := E) (closedBall 0 r)
⊢ ProperSpace E
have rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ProperSpace E
Tactic: rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_2} (X := E) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ IsCompact.{u_2} (X := E) (closedBall 0 (‖c‖ ^ n * r))
have this : c ^ n ≠ 0
Tactic: have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_2} (X := E) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
⊢ ProperSpace E
have hC : ∀ (n : ℕ), IsCompact.{u_2} (X := E) (closedBall 0 (‖c‖ ^ n * r))
Tactic: have hC : ∀ n, IsCompact (closedBall (0 : E) (‖c‖ ^ n * r)) := fun n ↦ by
    have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc
    simpa [_root_.smul_closedBall' this] using hr.smul (c ^ n)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
r : ℝ
rpos : 0 < r
hr : IsCompact.{u_2} (X := E) (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
hC : ∀ (n : ℕ), IsCompact.{u_2} (X := E) (closedBall 0 (‖c‖ ^ n * r))
⊢ ProperSpace E
have hTop : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c‖ ^ n * r) atTop atTop
Tactic: have hTop : Tendsto (fun n ↦ ‖c‖ ^ n * r) atTop atTop :=
    Tendsto.atTop_mul_const rpos (tendsto_pow_atTop_atTop_of_one_lt hc)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
V : Type u_1
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : Nontrivial V
inst_7 : LocallyCompactSpace V
inst_8 : Module 𝕜 V
inst_9 : ContinuousSMul 𝕜 V
⊢ LocallyCompactSpace 𝕜
have obtain : ∀ (v : V) (hv : v ≠ 0), LocallyCompactSpace 𝕜
Tactic: obtain ⟨v, hv⟩ : ∃ v : V, v ≠ 0 := exists_ne 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
V : Type u_1
inst_2 : AddCommGroup V
inst_3 : TopologicalSpace V
inst_4 : IsTopologicalAddGroup V
inst_5 : T2Space V
inst_6 : Nontrivial V
inst_7 : LocallyCompactSpace V
inst_8 : Module 𝕜 V
inst_9 : ContinuousSMul 𝕜 V
v : V
hv : v ≠ 0
L : 𝕜 → V := fun (t : 𝕜) ↦ t • v
⊢ LocallyCompactSpace 𝕜
have this : IsClosedEmbedding L
Tactic: have : IsClosedEmbedding L := isClosedEmbedding_smul_left hv
-- 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 𝕜
X : Type u_1
inst_6 : TopologicalSpace X
inst_7 : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
x : X
⊢ ContinuousWithinAt f s x ↔ ∀ (y : E), ContinuousWithinAt.{u_1, w} (Y := F) (fun (q : X) ↦ (f q : (a : E) → F) y) s x
have refine : ∀ (h : ∀ (y : E), ContinuousWithinAt.{u_1, w} (Y := F) (fun (q : X) ↦ (f q : (a : E) → F) y) s x),
  ContinuousWithinAt f s x
Tactic: refine ⟨fun h y ↦ (apply 𝕜 F y).continuous.continuousAt.comp_continuousWithinAt h, fun 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 𝕜
X : Type u_1
inst_6 : TopologicalSpace X
inst_7 : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
x : X
h : ∀ (y : E), ContinuousWithinAt.{u_1, w} (Y := F) (fun (q : X) ↦ (f q : (a : E) → F) y) s x
e : (E →L[𝕜] F) ≃L[𝕜] Fin (finrank 𝕜 E) → F :=
  ContinuousLinearEquiv.trans (M₂ := (Fin (finrank 𝕜 E) → 𝕜) →L[𝕜] F)
    (ContinuousLinearEquiv.arrowCongr.{u, v, u, w, w} (𝕜 := 𝕜) (E := E) (F := Fin (finrank 𝕜 E) → 𝕜) (G := F) (H := F)
      (ContinuousLinearEquiv.ofFinrankEq.{u, v, u} (𝕜 := 𝕜) (E := E) (F := Fin (finrank 𝕜 E) → 𝕜) ⋯) 1)
    (ContinuousLinearEquiv.piRing (Fin (finrank 𝕜 E)))
⊢ ContinuousWithinAt f s x
have rw : ContinuousWithinAt.{u_1, w} (Y := Fin (finrank 𝕜 E) → F)
  ((⇑e.toHomeomorph : (a : E →L[𝕜] F) → Fin (finrank 𝕜 E) → F) ∘ f) s x
Tactic: rw [e.toHomeomorph.isInducing.continuousWithinAt_iff]
-- 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 𝕜
X : Type u_1
inst_6 : TopologicalSpace X
inst_7 : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
⊢ ContinuousOn f s ↔ ∀ (y : E), ContinuousOn.{u_1, w} (Y := F) (fun (x : X) ↦ (f x : (a : E) → F) y) s
have simp_rw : (∀ (x : X) (x_1 : E), x ∈ s → ContinuousWithinAt.{u_1, w} (Y := F) (fun (q : X) ↦ (f q : (a : E) → F) x_1) s x) ↔
  ∀ (y : E), ∀ x ∈ s, ContinuousWithinAt.{u_1, w} (Y := F) (fun (x : X) ↦ (f x : (a : E) → F) y) s x
Tactic: simp_rw [ContinuousOn, continuousWithinAt_clm_apply, imp_forall_iff]
-- 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 𝕜
X : Type u_1
inst_6 : TopologicalSpace X
inst_7 : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
x : X
⊢ ContinuousAt f x ↔ ∀ (y : E), ContinuousAt.{u_1, w} (Y := F) (fun (q : X) ↦ (f q : (a : E) → F) y) x
have simp_rw : ContinuousWithinAt f univ x ↔
  ∀ (y : E), ContinuousWithinAt.{u_1, w} (Y := F) (fun (q : X) ↦ (f q : (a : E) → F) y) univ x
Tactic: simp_rw [← continuousWithinAt_univ, continuousWithinAt_clm_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 𝕜
X : Type u_1
inst_6 : TopologicalSpace X
inst_7 : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
⊢ Continuous[inst_6, _] f ↔
    ∀ (y : E),
      Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ (f x : (a : E) → F) y
have simp_rw : ContinuousOn f univ ↔ ∀ (y : E), ContinuousOn.{u_1, w} (Y := F) (fun (x : X) ↦ (f x : (a : E) → F) y) univ
Tactic: simp_rw [← continuousOn_univ, continuousOn_clm_apply]