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
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Finite ι
v : Basis ι 𝕜 E
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
⊢ ∃ 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 ι

Premises used: nonempty_fintype
-- 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 𝕜
ι : Type u_1
inst_6 : Finite ι
v : Basis ι 𝕜 E
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:
⟨max (Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊) 1,
      zero_lt_one.trans_le (le_max_right _ _), fun {u} M hu =>
      (v.opNNNorm_le M hu).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) zero_le⟩

Premises used: le_max_right, zero_le, NNNorm.nnnorm, Module.Basis.equivFunL, Fintype.card, zero_lt_one, mul_le_mul_of_nonneg_right, Max.max, LT.lt.trans_le, And.intro, Exists.intro, HSMul.hSMul, LE.le.trans, Module.Basis.opNNNorm_le, OfNat.ofNat, le_max_left, ContinuousLinearEquiv.toContinuousLinearMap
-- 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 𝕜
ι : Type u_1
inst_6 : Finite ι
v : Basis ι 𝕜 E
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:
exact
    ⟨max (Fintype.card ι • ‖v.equivFunL.toContinuousLinearMap‖₊) 1,
      zero_lt_one.trans_le (le_max_right _ _), fun {u} M hu =>
      (v.opNNNorm_le M hu).trans <| mul_le_mul_of_nonneg_right (le_max_left _ _) zero_le⟩
-- 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 𝕜
ι : Type u_1
inst_6 : Finite ι
v : Basis ι 𝕜 E
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
⊢ ∃ 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)

Premises used: Module.Basis.exists_opNNNorm_le
-- 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 𝕜
ι : 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

Tactic:
⟨C, hC, ?_⟩

Premises used: And.intro, Exists.intro, NNReal.toReal
-- 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 𝕜
ι : 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
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
⊢ ∃ 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:
refine ⟨C, hC, ?_⟩
-- 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 𝕜
ι : 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
u : E →L[𝕜] F
M : ℝ
hM : 0 ≤ M
H : ∀ (i : ι), norm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
⊢ ‖u‖ ≤ (↑C : ℝ) * M

Tactic:
simpa using h ⟨M, hM⟩ H

Premises used: Subtype.mk
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
inst_7 : SecondCountableTopology F
d : ℕ := finrank 𝕜 E
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq.{u, v, u} (𝕜 := 𝕜) (E := E) (F := Fin d → 𝕜) ⋯
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
  ContinuousLinearEquiv.trans (M₂ := (Fin d → 𝕜) →L[𝕜] F)
    (ContinuousLinearEquiv.arrowCongr.{u, v, u, w, w} (𝕜 := 𝕜) (E := E) (F := Fin d → 𝕜) (G := F) (H := F) e₁ 1)
    (ContinuousLinearEquiv.piRing (Fin d))
⊢ SecondCountableTopology (E →L[𝕜] F)

Tactic:
e₂.toHomeomorph.secondCountableTopology

Premises used: Homeomorph.secondCountableTopology, ContinuousLinearEquiv.toHomeomorph
-- 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
inst_7 : SecondCountableTopology F
d : ℕ := finrank 𝕜 E
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq.{u, v, u} (𝕜 := 𝕜) (E := E) (F := Fin d → 𝕜) ⋯
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
  ContinuousLinearEquiv.trans (M₂ := (Fin d → 𝕜) →L[𝕜] F)
    (ContinuousLinearEquiv.arrowCongr.{u, v, u, w, w} (𝕜 := 𝕜) (E := E) (F := Fin d → 𝕜) (G := F) (H := F) e₁ 1)
    (ContinuousLinearEquiv.piRing (Fin d))
⊢ SecondCountableTopology (E →L[𝕜] F)

Tactic:
exact e₂.toHomeomorph.secondCountableTopology

Premises used: Homeomorph.secondCountableTopology, ContinuousLinearEquiv.toHomeomorph
-- 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 𝕜
P : Type u_1
inst_4 : MetricSpace P
inst_5 : NormedAddTorsor E P
s : AffineSubspace 𝕜 P
inst_6 : FiniteDimensional.{u, v} 𝕜 ↥s.direction
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑s : Set P)

Tactic:
s.isClosed_direction_iff.mp s.direction.closed_of_finiteDimensional

Premises used: Submodule.closed_of_finiteDimensional, Iff.mp, AffineSubspace.direction, AffineSubspace.isClosed_direction_iff
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
⊢ F.FG

Tactic:
have hF : F.FG := ⟨s, rfl⟩
-- 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 𝕜
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
⊢ FiniteDimensional.{u, v} 𝕜 ↥F

Tactic:
haveI : FiniteDimensional 𝕜 F := .of_fg hF
-- 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 𝕜
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
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)

Tactic:
have Fclosed : IsClosed (F : Set E) := Submodule.closed_of_finiteDimensional _
-- 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 𝕜
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)
contrapose! : ∀ (h : ∀ (x : E), x ∈ F), FiniteDimensional 𝕜 E
⊢ ∃ (x : E), x ∉ F

Tactic:
contrapose! h
-- 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 𝕜
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
h₁ : ∀ (x : E), Membership.mem (γ := Submodule 𝕜 E) ⊤ x ↔ x ∈ F
⊢ ⊤ = F

Tactic:
ext x
-- 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 𝕜
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
x : E
⊢ Membership.mem (γ := Submodule 𝕜 E) ⊤ x ↔ x ∈ F

Tactic:
simp [h]
-- 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 𝕜
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

Tactic:
have : (⊤ : Submodule 𝕜 E) = F := by
      ext x
      simp [h]
-- 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 𝕜
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
⊢ Submodule.FG.{u, v} (R := 𝕜) (M := E) ⊤

Tactic:
rw [← this] at hF
-- 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 𝕜
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
hF₁ : Submodule.FG.{u, v} (R := 𝕜) (M := E) ⊤
⊢ FiniteDimensional.{u, v} 𝕜 ↥F

Tactic:
rw [← this] at hF
-- 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 𝕜
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
hF₁ : Submodule.FG.{u, v} (R := 𝕜) (M := E) ⊤
this₁ : FiniteDimensional.{u, v} 𝕜 ↥F
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)

Tactic:
rw [← this] at hF
-- 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 𝕜
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
hF₁ : Submodule.FG.{u, v} (R := 𝕜) (M := E) ⊤
this₁ : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed₁ : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
⊢ ∀ (x : E), x ∈ F

Tactic:
rw [← this] at hF
-- 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 𝕜
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
hF₁ : Submodule.FG.{u, v} (R := 𝕜) (M := E) ⊤
this₁ : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed₁ : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
h₁ : ∀ (x : E), x ∈ F
⊢ ⊤ = F

Tactic:
rw [← this] at hF
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : Submodule.FG.{u, v} (R := 𝕜) (M := E) ⊤
this_1 : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
h : ∀ (x : E), x ∈ F
this : ⊤ = F
⊢ FiniteDimensional 𝕜 E

Tactic:
.of_fg_top hF

Premises used: Module.Finite.of_fg_top
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 (↑s : Set E)
hF : Submodule.FG.{u, v} (R := 𝕜) (M := E) ⊤
this_1 : FiniteDimensional.{u, v} 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑F : Set E)
h : ∀ (x : E), x ∈ F
this : ⊤ = F
⊢ FiniteDimensional 𝕜 E

Tactic:
exact .of_fg_top hF
-- 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 𝕜
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

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
-- 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 𝕜
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 ∈ F, 1 ≤ ‖x - y‖

Tactic:
riesz_lemma_of_norm_lt hc hR Fclosed this

Premises used: Set.Mem, riesz_lemma_of_norm_lt
-- 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 𝕜
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
obtain : ∀ (x : E) (xR : ‖x‖ ≤ R) (hx : ∀ y ∈ F, 1 ≤ ‖x - y‖), ∃ (x : E), ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖
⊢ ∃ (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

Premises used: riesz_lemma_of_norm_lt
-- 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 𝕜
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
rw : 1 ≤ ‖-(y - x)‖
⊢ 1 ≤ ‖y - x‖

Tactic:
rw [← norm_neg]

Premises used: norm_neg
-- 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 𝕜
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)‖

Tactic:
simpa using hx y hy
-- 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 𝕜
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 ∈ 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
-- 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 𝕜
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‖
hx' : ∀ y ∈ F, 1 ≤ ‖y - x‖
⊢ ∃ (x : E), ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖

Tactic:
⟨x, xR, fun y hy => hx' _ (Submodule.subset_span hy)⟩

Premises used: And.intro, Exists.intro, Submodule.subset_span
-- 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 𝕜
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‖
hx' : ∀ y ∈ F, 1 ≤ ‖y - x‖
⊢ ∃ (x : E), ‖x‖ ≤ R ∧ ∀ y ∈ s, 1 ≤ ‖y - x‖

Tactic:
exact ⟨x, xR, fun y hy => hx' _ (Submodule.subset_span hy)⟩
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
symm : ∀ (a b : E), 1 ≤ ‖a - b‖ → 1 ≤ ‖b - a‖
⊢ Std.Symm fun (x y : E) ↦ 1 ≤ ‖x - y‖

Tactic:
constructor
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
x y : E
hxy : 1 ≤ ‖x - y‖
symm : 1 ≤ ‖-(y - x)‖
⊢ 1 ≤ ‖y - x‖

Tactic:
rw [← norm_neg]

Premises used: norm_neg
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
x y : E
hxy : 1 ≤ ‖x - y‖
⊢ 1 ≤ ‖-(y - x)‖

Tactic:
simpa
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
⊢ 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
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
this : Std.Symm fun (x y : E) ↦ 1 ≤ ‖x - y‖
exists_seq_of_forall_finset_exists' : ∀ (s : Finset E), (∀ x ∈ s, ‖x‖ ≤ R) → ∃ (y : E), ‖y‖ ≤ R ∧ ∀ x ∈ s, 1 ≤ ‖x - y‖
⊢ ∃ (f : ℕ → E), (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ Pairwise fun (m n : ℕ) ↦ 1 ≤ ‖f m - f n‖

Tactic:
apply
    exists_seq_of_forall_finset_exists' (fun x : E => ‖x‖ ≤ R) fun (x : E) (y : E) => 1 ≤ ‖x - y‖

Premises used: Norm.norm, HSub.hSub, LE.le, OfNat.ofNat, exists_seq_of_forall_finset_exists'
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
this : Std.Symm fun (x y : E) ↦ 1 ≤ ‖x - y‖
s : Finset E
⊢ ∃ (y : E), ‖y‖ ≤ R ∧ ∀ x ∈ s, 1 ≤ ‖x - y‖

Tactic:
exists_norm_le_le_norm_sub_of_finset hc hR h s

Premises used: exists_norm_le_le_norm_sub_of_finset
-- 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 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
h : ¬FiniteDimensional 𝕜 E
this : Std.Symm fun (x y : E) ↦ 1 ≤ ‖x - y‖
s : Finset E
⊢ ∃ (y : E), ‖y‖ ≤ R ∧ ∀ x ∈ s, 1 ≤ ‖x - y‖

Tactic:
exact exists_norm_le_le_norm_sub_of_finset hc hR h s

Premises used: exists_norm_le_le_norm_sub_of_finset