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 𝕜
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
fL : E →L[𝕜] F :=
  ((LinearMap.toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) f.linear
⊢ ∃ (K : ℝ≥0), LipschitzWith.{u_1, u_2} (α := PE) (β := PF) K (⇑f : (a : PE) → PF)
have refine : ∀ (x y : PE), dist.{u_2} (α := PF) ((f : (a : PE) → PF) x : PF) ((f : (a : PE) → PF) y : PF) ≤ (↑‖fL‖₊ : ℝ) * dist x y
Tactic: refine ⟨‖fL‖₊, LipschitzWith.of_dist_le_mul 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
fL : E →L[𝕜] F :=
  ((LinearMap.toContinuousLinearMap : (E →ₗ[𝕜] F) ≃ₗ[𝕜] E →L[𝕜] F) : (a : E →ₗ[𝕜] F) → E →L[𝕜] F) f.linear
x y : PE
⊢ dist.{u_2} (α := PF) ((f : (a : PE) → PF) x : PF) ((f : (a : PE) → PF) y : PF) ≤ (↑‖fL‖₊ : ℝ) * dist x y
have rw : norm.{w} (E := F) ((f.linear : (a : E) → F) (x -ᵥ y) : F) ≤ (↑‖fL‖₊ : ℝ) * ‖x -ᵥ y‖
Tactic: rw [NormedAddTorsor.dist_eq_norm', NormedAddTorsor.dist_eq_norm', ← 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
inst_3 : CompleteSpace 𝕜
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦ f.det
have change : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
  (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
Tactic: change Continuous fun f : E →L[𝕜] E => LinearMap.det (f : E →ₗ[𝕜] E)
-- 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 𝕜
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
have pos : ∀ (h : ∃ (s : Finset E), Nonempty (Basis (↥s) 𝕜 E)),
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
Tactic: by_cases h : ∃ s : Finset E, Nonempty (Basis (↥s) 𝕜 E)
-- 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 𝕜
pos :
  ∀ (h : ∃ (s : Finset E), Nonempty (Basis (↥s) 𝕜 E)),
    Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
      (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
have neg : ∀ (h : ¬∃ (s : Finset E), Nonempty (Basis (↥s) 𝕜 E)),
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
Tactic: by_cases h : ∃ s : Finset E, Nonempty (Basis (↥s) 𝕜 E)
-- 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 : ∃ (s : Finset E), Nonempty (Basis (↥s) 𝕜 E)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
have pos : ∀ (s : Finset E) (b : Basis (↥s) 𝕜 E),
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
Tactic: rcases h with ⟨s, ⟨b⟩⟩
Cleared hypotheses: 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 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
have this : FiniteDimensional 𝕜 E
Tactic: haveI : FiniteDimensional 𝕜 E := b.finiteDimensional_of_finite
-- 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 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
have pos : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
  Matrix.det.{u, v} (n := ↥s) ((LinearMap.toMatrix b b : (a : E →ₗ[𝕜] E) → Matrix (↥s) (↥s) 𝕜) (↑f : E →ₗ[𝕜] E))
Tactic: simp_rw [LinearMap.det_eq_det_toMatrix_of_finset b]
-- 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 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    Matrix.det.{u, v} (n := ↥s) ((LinearMap.toMatrix b b : (a : E →ₗ[𝕜] E) → Matrix (↥s) (↥s) 𝕜) (↑f : E →ₗ[𝕜] E))
have pos : Continuous[_, instTopologicalSpaceMatrix] fun (f : E →L[𝕜] E) ↦
  (LinearMap.toMatrix b b : (a : E →ₗ[𝕜] E) → Matrix (↥s) (↥s) 𝕜) (↑f : E →ₗ[𝕜] E)
Tactic: refine Continuous.matrix_det ?_
-- 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 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
have pos : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
  Matrix.det.{u, v} (n := ↥s) ((LinearMap.toMatrix b b : (a : E →ₗ[𝕜] E) → Matrix (↥s) (↥s) 𝕜) (↑f : E →ₗ[𝕜] E))
Tactic: classical
    simp_rw [LinearMap.det_eq_det_toMatrix_of_finset b]
    refine Continuous.matrix_det ?_
    exact
      ((LinearMap.toMatrix b b).toLinearMap.comp
          (ContinuousLinearMap.coeLM 𝕜)).continuous_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 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
this : FiniteDimensional 𝕜 E
pos :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    Matrix.det.{u, v} (n := ↥s) ((LinearMap.toMatrix b b : (a : E →ₗ[𝕜] E) → Matrix (↥s) (↥s) 𝕜) (↑f : E →ₗ[𝕜] E))
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
have pos₁ : Continuous[_, instTopologicalSpaceMatrix] fun (f : E →L[𝕜] E) ↦
  (LinearMap.toMatrix b b : (a : E →ₗ[𝕜] E) → Matrix (↥s) (↥s) 𝕜) (↑f : E →ₗ[𝕜] E)
Tactic: classical
    simp_rw [LinearMap.det_eq_det_toMatrix_of_finset b]
    refine Continuous.matrix_det ?_
    exact
      ((LinearMap.toMatrix b b).toLinearMap.comp
          (ContinuousLinearMap.coeLM 𝕜)).continuous_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 𝕜
h : ¬∃ (s : Finset E), Nonempty (Basis (↥s) 𝕜 E)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)
have neg : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
  (if H : ∃ (s : Finset E), Nonempty (Basis (↥s) 𝕜 E) then LinearMap.detAux (Trunc.mk sorry.some) else 1 :
      (a : E →ₗ[𝕜] E) → 𝕜)
    (↑f : E →ₗ[𝕜] E)
Tactic: rw [LinearMap.det]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
E' : Type u_1
inst : NormedAddCommGroup E'
inst_1 : NormedSpace ℝ E'
inst_2 : FiniteDimensional ℝ E'
⊢ 0 < lipschitzExtensionConstant E'
have rw : LT.lt (α := ℝ≥0) 0
  (have A : E' ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_1) → ℝ :=
    LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'));
  max
    (‖(↑A.symm : ((↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_1) → ℝ) →L[ℝ] E')‖₊ *
      ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_1) → ℝ)‖₊)
    1)
Tactic: rw [lipschitzExtensionConstant]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace ℝ E'
inst_3 : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2)
A : E' ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
⊢ ∃ (g : α → E'), LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
have LA : LipschitzWith (α := E') (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
  ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊
  (⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
Tactic: have LA : LipschitzWith ‖A.toContinuousLinearMap‖₊ A := by apply A.lipschitz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace ℝ E'
inst_3 : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2)
A : E' ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA :
  LipschitzWith (α := E') (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊
    (⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
⊢ ∃ (g : α → E'), LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
have L : LipschitzOnWith (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
  (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K)
  ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) s
Tactic: have L : LipschitzOnWith (‖A.toContinuousLinearMap‖₊ * K) (A ∘ f) s :=
    LA.comp_lipschitzOnWith hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace ℝ E'
inst_3 : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2)
A : E' ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA :
  LipschitzWith (α := E') (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊
    (⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
L :
  LipschitzOnWith (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K)
    ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) s
⊢ ∃ (g : α → E'), LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
have obtain : ∀ (g : α → ι → ℝ) (hg : LipschitzWith (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K) g)
  (gs : EqOn ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) g s),
  ∃ (g : α → E'), LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
Tactic: obtain ⟨g, hg, gs⟩ :
    ∃ g : α → ι → ℝ, LipschitzWith (‖A.toContinuousLinearMap‖₊ * K) g ∧ EqOn (A ∘ f) g s :=
    L.extend_pi
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace ℝ E'
inst_3 : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2)
A : E' ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA :
  LipschitzWith (α := E') (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊
    (⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
L :
  LipschitzOnWith (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K)
    ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K) g
gs : EqOn ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) g s
⊢ ∃ (g : α → E'), LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
have refine_1 : LipschitzWith (β := E') (lipschitzExtensionConstant E' * K)
  ((⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E') ∘ g)
Tactic: refine ⟨A.symm ∘ g, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace ℝ E'
inst_3 : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2)
A : E' ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA :
  LipschitzWith (α := E') (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊
    (⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
L :
  LipschitzOnWith (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K)
    ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K) g
gs : EqOn ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) g s
refine_1 :
  LipschitzWith (β := E') (lipschitzExtensionConstant E' * K)
    ((⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E') ∘ g)
⊢ ∃ (g : α → E'), LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
have refine_2 : EqOn f ((⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E') ∘ g) s
Tactic: refine ⟨A.symm ∘ g, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace ℝ E'
inst_3 : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2)
A : E' ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA :
  LipschitzWith (α := E') (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊
    (⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
L :
  LipschitzOnWith (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K)
    ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K) g
gs : EqOn ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) g s
⊢ LipschitzWith (β := E') (lipschitzExtensionConstant E' * K)
    ((⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E') ∘ g)
have LAsymm : LipschitzWith (α := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) (β := E')
  ‖(↑A.symm : ((↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) →L[ℝ] E')‖₊
  (⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E')
Tactic: have LAsymm : LipschitzWith ‖A.symm.toContinuousLinearMap‖₊ A.symm := by
      apply A.symm.lipschitz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace ℝ E'
inst_3 : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2)
A : E' ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA :
  LipschitzWith (α := E') (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊
    (⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
L :
  LipschitzOnWith (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K)
    ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K) g
gs : EqOn ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) g s
LAsymm :
  LipschitzWith (α := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) (β := E')
    ‖(↑A.symm : ((↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) →L[ℝ] E')‖₊
    (⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E')
⊢ LipschitzWith (β := E') (lipschitzExtensionConstant E' * K)
    ((⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E') ∘ g)
have refine_1 : ‖(↑A.symm : ((↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) →L[ℝ] E')‖₊ *
    (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K) ≤
  lipschitzExtensionConstant E' * K
Tactic: apply (LAsymm.comp hg).weaken
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace ℝ E'
inst_3 : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2)
A : E' ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA :
  LipschitzWith (α := E') (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊
    (⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
L :
  LipschitzOnWith (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K)
    ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K) g
gs : EqOn ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) g s
LAsymm :
  LipschitzWith (α := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) (β := E')
    ‖(↑A.symm : ((↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) →L[ℝ] E')‖₊
    (⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E')
⊢ ‖(↑A.symm : ((↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) →L[ℝ] E')‖₊ *
      (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K) ≤
    lipschitzExtensionConstant E' * K
have refine_1 : ‖(↑A.symm : ((↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) →L[ℝ] E')‖₊ *
      ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ *
    K ≤
  (have A : E' ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ :=
      LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'));
    max
      (‖(↑A.symm : ((↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) →L[ℝ] E')‖₊ *
        ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊)
      1) *
    K
Tactic: rw [lipschitzExtensionConstant, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.FiniteDimension (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
E' : Type u_2
inst_1 : NormedAddCommGroup E'
inst_2 : NormedSpace ℝ E'
inst_3 : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2)
A : E' ≃L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA :
  LipschitzWith (α := E') (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    ‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊
    (⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
L :
  LipschitzOnWith (β := (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)
    (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K)
    ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K) g
gs : EqOn ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) g s
x : α
hx : x ∈ s
⊢ f x = ((⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E') ∘ g) x
have this : (A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) (f x) = g x
Tactic: have : A (f x) = g x := gs hx
-- 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 = ⊥
⊢ ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
have inl : Subsingleton E → ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
Tactic: cases subsingleton_or_nontrivial E