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 𝕜
h : ¬FiniteDimensional 𝕜 E
⊢ ∃ (c : 𝕜), 1 < ‖c‖

Tactic:
NormedField.exists_one_lt_norm 𝕜

Premises used: NormedField.exists_one_lt_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 𝕜
h : ¬FiniteDimensional 𝕜 E
obtain :
  ∀ (c : 𝕜) (hc : 1 < ‖c‖),
    ∃ (R : ℝ) (f : ℕ → E), 1 < R ∧ (∀ (n : ℕ), ‖f n‖ ≤ R) ∧ 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:
obtain ⟨c, hc⟩ : ∃ c : 𝕜, 1 < ‖c‖ := NormedField.exists_one_lt_norm 𝕜

Premises used: NormedField.exists_one_lt_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 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
linarith : ‖c‖ + 1 ≤ ‖c‖ → -1 + (‖c‖ + 1 - ‖c‖) = 0
⊢ ‖c‖ < ‖c‖ + 1

Tactic:
linarith
-- 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 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
⊢ ‖c‖ < ‖c‖ + 1

Tactic:
have A : ‖c‖ < ‖c‖ + 1 := by linarith
-- 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 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
A : ‖c‖ < ‖c‖ + 1
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‖
⊢ ∃ (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⟩

Premises used: exists_seq_norm_le_one_le_norm_sub'
-- 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 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
A : ‖c‖ < ‖c‖ + 1
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:
⟨‖c‖ + 1, f, hc.trans A, hf.1, hf.2⟩

Premises used: Norm.norm, And.right, And.left, HAdd.hAdd, And.intro, Exists.intro, LT.lt.trans, OfNat.ofNat
-- 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 𝕜
h : ¬FiniteDimensional 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
A : ‖c‖ < ‖c‖ + 1
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:
exact ⟨‖c‖ + 1, f, hc.trans A, hf.1, hf.2⟩
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
V : Type u_1
inst_2 : NormedAddCommGroup V
inst_3 : Module 𝕜 V
inst_4 : ContinuousSMul 𝕜 V
r : ℝ
rpos : 0 < r
h : IsCompact.{u_1} (X := V) (closedBall 0 r)
⊢ FiniteDimensional 𝕜 V

Tactic:
.of_totallyBounded_nhds_zero 𝕜 (Metric.closedBall_mem_nhds 0 rpos) h.totallyBounded

Premises used: Metric.closedBall_mem_nhds, FiniteDimensional.of_totallyBounded_nhds_zero, IsCompact.totallyBounded, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
V : Type u_1
inst_2 : NormedAddCommGroup V
inst_3 : Module 𝕜 V
inst_4 : ContinuousSMul 𝕜 V
r : ℝ
rpos : 0 < r
c : V
h : IsCompact (closedBall c r)
⊢ IsCompact.{u_1} (X := V) (closedBall 0 r)

Tactic:
simpa using h.vadd (-c)

Premises used: IsCompact.vadd, Neg.neg
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
rcases : ∀ (r : ℝ) (rpos : 0 < r) (hr : IsCompact.{u_2} (X := E) (closedBall 0 r)), ProperSpace E
⊢ ProperSpace E

Tactic:
rcases exists_isCompact_closedBall (0 : E) with ⟨r, rpos, hr⟩

Premises used: Metric.exists_isCompact_closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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)
rcases : ∀ (c : 𝕜) (hc : 1 < ‖c‖), ProperSpace E
⊢ ProperSpace E

Tactic:
rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩

Premises used: NormedField.exists_one_lt_norm
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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 : ℕ
h : c = 0
⊢ False

Tactic:
simp [h, zero_le_one.not_gt] at hc

Premises used: zero_le_one, LE.le.not_gt
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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 : ℕ
⊢ c ^ n ≠ 0

Tactic:
have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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 : ℕ
this : c ^ n ≠ 0
⊢ IsCompact.{u_2} (X := E) (closedBall 0 (‖c‖ ^ n * r))

Tactic:
simpa [_root_.smul_closedBall' this] using hr.smul (c ^ n)

Premises used: smul_closedBall', HPow.hPow, IsCompact.smul
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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))

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)
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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))
⊢ 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)
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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))
hTop : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c‖ ^ n * r) atTop atTop
⊢ ProperSpace E

Tactic:
.of_seq_closedBall hTop (Eventually.of_forall hC)

Premises used: ProperSpace.of_seq_closedBall, Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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))
hTop : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ‖c‖ ^ n * r) atTop atTop
⊢ ProperSpace E

Tactic:
exact .of_seq_closedBall hTop (Eventually.of_forall hC)
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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), v ≠ 0

Tactic:
exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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
obtain : ∀ (v : V) (hv : v ≠ 0), LocallyCompactSpace 𝕜
⊢ LocallyCompactSpace 𝕜

Tactic:
obtain ⟨v, hv⟩ : ∃ v : V, v ≠ 0 := exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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
⊢ IsClosedEmbedding L

Tactic:
have : IsClosedEmbedding L := isClosedEmbedding_smul_left hv
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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
this : IsClosedEmbedding L
⊢ LocallyCompactSpace 𝕜

Tactic:
apply IsClosedEmbedding.locallyCompactSpace this

Premises used: Topology.IsClosedEmbedding.locallyCompactSpace
-- 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 𝕜
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

Tactic:
⟨fun h y ↦ (apply 𝕜 F y).continuous.continuousAt.comp_continuousWithinAt h, fun h ↦ ?_⟩

Premises used: Continuous.continuousAt, ContinuousLinearMap.continuous, ContinuousLinearMap.apply, Iff.intro, ContinuousAt.comp_continuousWithinAt, DFunLike.coe
-- 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 𝕜
X : Type u_1
inst_6 : TopologicalSpace X
inst_7 : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
x : X
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
⊢ ContinuousWithinAt f s x ↔ ∀ (y : E), ContinuousWithinAt.{u_1, w} (Y := F) (fun (q : X) ↦ (f q : (a : E) → F) y) s x

Tactic:
refine ⟨fun h y ↦ (apply 𝕜 F y).continuous.continuousAt.comp_continuousWithinAt h, fun h ↦ ?_⟩
-- 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 𝕜
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)))
rw :
  ContinuousWithinAt.{u_1, w} (Y := Fin (finrank 𝕜 E) → F)
    ((⇑e.toHomeomorph : (a : E →L[𝕜] F) → Fin (finrank 𝕜 E) → F) ∘ f) s x
⊢ ContinuousWithinAt f s x

Tactic:
rw [e.toHomeomorph.isInducing.continuousWithinAt_iff]

Premises used: Homeomorph.isInducing, ContinuousLinearEquiv.toHomeomorph, Topology.IsInducing.continuousWithinAt_iff
-- 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 𝕜
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.{u_1, w} (Y := Fin (finrank 𝕜 E) → F)
    ((⇑e.toHomeomorph : (a : E →L[𝕜] F) → Fin (finrank 𝕜 E) → F) ∘ f) s x

Tactic:
continuousWithinAt_pi.mpr fun i ↦ h _

Premises used: Iff.mpr, ContinuousLinearEquiv.symm, LinearMap.single, ContinuousLinearMap.toLinearMap, Module.finrank_fin_fun, continuousWithinAt_pi, OfNat.ofNat, Eq.symm, ContinuousLinearEquiv.ofFinrankEq, DFunLike.coe, 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 𝕜
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.{u_1, w} (Y := Fin (finrank 𝕜 E) → F)
    ((⇑e.toHomeomorph : (a : E →L[𝕜] F) → Fin (finrank 𝕜 E) → F) ∘ f) s x

Tactic:
exact continuousWithinAt_pi.mpr fun i ↦ h _

Premises used: Iff.mpr, continuousWithinAt_pi
-- 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 𝕜
X : Type u_1
inst_6 : TopologicalSpace X
inst_7 : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
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
⊢ ContinuousOn f s ↔ ∀ (y : E), ContinuousOn.{u_1, w} (Y := F) (fun (x : X) ↦ (f x : (a : E) → F) y) s

Tactic:
simp_rw [ContinuousOn, continuousWithinAt_clm_apply, imp_forall_iff]

Premises used: continuousWithinAt_clm_apply, imp_forall_iff, ContinuousOn
-- 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 𝕜
X : Type u_1
inst_6 : TopologicalSpace X
inst_7 : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
⊢ (∀ (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:
forall_comm

Premises used: forall_comm
-- 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 𝕜
X : Type u_1
inst_6 : TopologicalSpace X
inst_7 : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
⊢ (∀ (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:
exact forall_comm

Premises used: forall_comm
-- 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 𝕜
X : Type u_1
inst_6 : TopologicalSpace X
inst_7 : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
x : X
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
⊢ ContinuousAt f x ↔ ∀ (y : E), ContinuousAt.{u_1, w} (Y := F) (fun (q : X) ↦ (f q : (a : E) → F) y) x

Tactic:
simp_rw [← continuousWithinAt_univ, continuousWithinAt_clm_apply]

Premises used: continuousWithinAt_univ, continuousWithinAt_clm_apply
-- 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 𝕜
X : Type u_1
inst_6 : TopologicalSpace X
inst_7 : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
simp_rw : ContinuousOn f univ ↔ ∀ (y : E), ContinuousOn.{u_1, w} (Y := F) (fun (x : X) ↦ (f x : (a : E) → F) y) univ
⊢ Continuous[inst_6, _] f ↔
    ∀ (y : E),
      Continuous[inst_6, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : X) ↦ (f x : (a : E) → F) y

Tactic:
simp_rw [← continuousOn_univ, continuousOn_clm_apply]

Premises used: continuousOn_univ, continuousOn_clm_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 : LocallyCompactSpace 𝕜
inst_4 : FiniteDimensional 𝕜 E
⊢ ProperSpace 𝕜

Tactic:
have : ProperSpace 𝕜 := .of_locallyCompactSpace 𝕜
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace 𝕜
inst_4 : FiniteDimensional 𝕜 E
this : ProperSpace 𝕜
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 :=
  ContinuousLinearEquiv.ofFinrankEq.{u, v, u} (𝕜 := 𝕜) (E := E) (F := Fin (finrank 𝕜 E) → 𝕜) ⋯
⊢ ProperSpace E

Tactic:
e.symm.antilipschitz.properSpace e.symm.continuous e.symm.surjective

Premises used: ContinuousLinearEquiv.antilipschitz, ContinuousLinearEquiv.symm, ContinuousLinearEquiv.surjective, AntilipschitzWith.properSpace, ContinuousLinearEquiv.continuous
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace 𝕜
inst_4 : FiniteDimensional 𝕜 E
this : ProperSpace 𝕜
e : E ≃L[𝕜] Fin (finrank 𝕜 E) → 𝕜 :=
  ContinuousLinearEquiv.ofFinrankEq.{u, v, u} (𝕜 := 𝕜) (E := E) (F := Fin (finrank 𝕜 E) → 𝕜) ⋯
⊢ ProperSpace E

Tactic:
exact e.symm.antilipschitz.properSpace e.symm.continuous e.symm.surjective

Premises used: ContinuousLinearEquiv.antilipschitz, ContinuousLinearEquiv.symm, ContinuousLinearEquiv.surjective, AntilipschitzWith.properSpace, ContinuousLinearEquiv.continuous
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
⊢ ProperSpace E

Tactic:
FiniteDimensional.proper ℝ E

Premises used: Real, FiniteDimensional.proper
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : LocallyCompactSpace E
S : Submodule 𝕜 E
⊢ Nontrivial E

Tactic:
nontriviality E
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : LocallyCompactSpace E
S : Submodule 𝕜 E
h : Nontrivial E
⊢ ProperSpace 𝕜

Tactic:
have : ProperSpace 𝕜 := .of_locallyCompact_module 𝕜 E
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : LocallyCompactSpace E
S : Submodule 𝕜 E
h : Nontrivial E
this : ProperSpace 𝕜
⊢ FiniteDimensional 𝕜 E

Tactic:
have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : LocallyCompactSpace E
S : Submodule 𝕜 E
h : Nontrivial E
this_1 : ProperSpace 𝕜
this : FiniteDimensional 𝕜 E
⊢ ProperSpace.{u_2} ↥S

Tactic:
FiniteDimensional.proper 𝕜 S

Premises used: Set.Mem, Membership.mem, Subtype, FiniteDimensional.proper
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : LocallyCompactSpace E
S : Submodule 𝕜 E
h : Nontrivial E
this_1 : ProperSpace 𝕜
this : FiniteDimensional 𝕜 E
⊢ ProperSpace.{u_2} ↥S

Tactic:
exact FiniteDimensional.proper 𝕜 S

Premises used: Membership.mem, Subtype, FiniteDimensional.proper
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
rcases :
  ∀ (y : E) (hys : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] sᶜ) (hyd : infDist x sᶜ = dist x y),
    ∃ y ∈ frontier s, infDist x sᶜ = dist x y
⊢ ∃ y ∈ frontier s, infDist x sᶜ = dist x y

Tactic:
rcases Metric.exists_mem_closure_infDist_eq_dist (nonempty_compl.2 hs) x with ⟨y, hys, hyd⟩

Premises used: Iff.mpr, Metric.exists_mem_closure_infDist_eq_dist, Set.nonempty_compl
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
x : E
s : Set E
hx : x ∈ s
hs : s ≠ univ
y : E
hys : y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] sᶜ
hyd : infDist x sᶜ = dist x y
⊢ y ∈ (interior s)ᶜ

Tactic:
rw [closure_compl] at hys

Premises used: closure_compl