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 𝕜
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
⊢ Eq (α := (a : PF) → PE) (⇑f.toHomeomorphOfFiniteDimensional.symm : (a : PF) → PE) (⇑f.symm : (a : PF) → PE)

Tactic:
rfl

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

Tactic:
⟨‖fL‖₊, LipschitzWith.of_dist_le_mul fun x y ↦ ?_⟩

Premises used: NNNorm.nnnorm, Exists.intro, LipschitzWith.of_dist_le_mul
-- 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 𝕜
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
refine :
  ∀ (x y : PE), dist.{u_2} (α := PF) ((f : (a : PE) → PF) x : PF) ((f : (a : PE) → PF) y : PF) ≤ (↑‖fL‖₊ : ℝ) * dist x y
⊢ ∃ (K : ℝ≥0), LipschitzWith.{u_1, u_2} (α := PE) (β := PF) K (⇑f : (a : PE) → PF)

Tactic:
refine ⟨‖fL‖₊, LipschitzWith.of_dist_le_mul fun x y ↦ ?_⟩
-- 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 𝕜
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
rw : norm.{w} (E := F) ((f.linear : (a : E) → F) (x -ᵥ y) : F) ≤ (↑‖fL‖₊ : ℝ) * ‖x -ᵥ y‖
⊢ dist.{u_2} (α := PF) ((f : (a : PE) → PF) x : PF) ((f : (a : PE) → PF) y : PF) ≤ (↑‖fL‖₊ : ℝ) * dist x y

Tactic:
rw [NormedAddTorsor.dist_eq_norm', NormedAddTorsor.dist_eq_norm', ← f.linearMap_vsub]

Premises used: AffineMap.linearMap_vsub, NormedAddTorsor.dist_eq_norm'
-- 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 𝕜
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
⊢ norm.{w} (E := F) ((f.linear : (a : E) → F) (x -ᵥ y) : F) ≤ (↑‖fL‖₊ : ℝ) * ‖x -ᵥ y‖

Tactic:
fL.le_opNorm _

Premises used: ContinuousLinearMap.le_opNorm, 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 𝕜
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
⊢ norm.{w} (E := F) ((f.linear : (a : E) → F) (x -ᵥ y) : F) ≤ (↑‖fL‖₊ : ℝ) * ‖x -ᵥ y‖

Tactic:
exact fL.le_opNorm _

Premises used: ContinuousLinearMap.le_opNorm
-- 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 𝕜
change :
  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) ↦ f.det

Tactic:
change Continuous fun f : E →L[𝕜] E => LinearMap.det (f : E →ₗ[𝕜] E)

Premises used: Continuous, ContinuousLinearMap.toLinearMap, LinearMap.det, DFunLike.coe
-- 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 𝕜
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)
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)
⊢ 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)

Premises used: 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 𝕜
h : ∃ (s : Finset E), Nonempty (Basis (↥s) 𝕜 E)
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)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)

Tactic:
rcases h with ⟨s, ⟨b⟩⟩
-- 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 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
⊢ FiniteDimensional 𝕜 E

Tactic:
haveI : FiniteDimensional 𝕜 E := b.finiteDimensional_of_finite
-- 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 𝕜
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)

Tactic:
simp_rw [LinearMap.det_eq_det_toMatrix_of_finset b]

Premises used: LinearMap.det_eq_det_toMatrix_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 𝕜
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))

Tactic:
Continuous.matrix_det ?_

Premises used: Continuous.matrix_det
-- 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 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
this : FiniteDimensional 𝕜 E
pos :
  Continuous[_, instTopologicalSpaceMatrix] fun (f : E →L[𝕜] E) ↦
    (LinearMap.toMatrix b b : (a : E →ₗ[𝕜] E) → Matrix (↥s) (↥s) 𝕜) (↑f : E →ₗ[𝕜] 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))

Tactic:
refine Continuous.matrix_det ?_

Premises used: Continuous.matrix_det
-- 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 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous[_, instTopologicalSpaceMatrix] fun (f : E →L[𝕜] E) ↦
    (LinearMap.toMatrix b b : (a : E →ₗ[𝕜] E) → Matrix (↥s) (↥s) 𝕜) (↑f : E →ₗ[𝕜] E)

Tactic:
((LinearMap.toMatrix b b).toLinearMap.comp
          (ContinuousLinearMap.coeLM 𝕜)).continuous_of_finiteDimensional

Premises used: LinearMap.comp, LinearEquiv.toLinearMap, ContinuousLinearMap.coeLM, LinearMap.continuous_of_finiteDimensional, LinearMap.toMatrix
-- 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 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous[_, instTopologicalSpaceMatrix] fun (f : E →L[𝕜] E) ↦
    (LinearMap.toMatrix b b : (a : E →ₗ[𝕜] E) → Matrix (↥s) (↥s) 𝕜) (↑f : E →ₗ[𝕜] E)

Tactic:
exact
      ((LinearMap.toMatrix b b).toLinearMap.comp
          (ContinuousLinearMap.coeLM 𝕜)).continuous_of_finiteDimensional

Premises used: LinearMap.comp, LinearEquiv.toLinearMap, ContinuousLinearMap.coeLM, LinearMap.continuous_of_finiteDimensional, LinearMap.toMatrix
-- 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 𝕜
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))
pos₁ :
  Continuous[_, instTopologicalSpaceMatrix] fun (f : E →L[𝕜] E) ↦
    (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)

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

Premises used: Continuous.matrix_det
-- 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 : ¬∃ (s : Finset E), Nonempty (Basis (↥s) 𝕜 E)
neg :
  Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (if H : ∃ (s : Finset E), Nonempty (Basis (↥s) 𝕜 E) then LinearMap.detAux (Trunc.mk ⋯.some) else 1 :
        (a : E →ₗ[𝕜] E) → 𝕜)
      (↑f : E →ₗ[𝕜] E)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑f : E →ₗ[𝕜] E)

Tactic:
rw [LinearMap.det]

Premises used: LinearMap.det
-- 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 : ¬∃ (s : Finset E), Nonempty (Basis (↥s) 𝕜 E)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (f : E →L[𝕜] E) ↦
    (if H : ∃ (s : Finset E), Nonempty (Basis (↥s) 𝕜 E) then LinearMap.detAux (Trunc.mk ⋯.some) else 1 :
        (a : E →ₗ[𝕜] E) → 𝕜)
      (↑f : E →ₗ[𝕜] E)

Tactic:
simpa only [h, MonoidHom.one_apply, dif_neg, not_false_iff] using continuous_const

Premises used: continuous_const, dif_neg, MonoidHom.one_apply, not_false_iff
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E' : Type u_1
inst : NormedAddCommGroup E'
inst_1 : NormedSpace ℝ E'
inst_2 : FiniteDimensional ℝ E'
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)
⊢ 0 < lipschitzExtensionConstant E'

Tactic:
rw [lipschitzExtensionConstant]

Premises used: lipschitzExtensionConstant
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E' : Type u_1
inst : NormedAddCommGroup E'
inst_1 : NormedSpace ℝ E'
inst_2 : FiniteDimensional ℝ E'
⊢ 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:
zero_lt_one.trans_le (le_max_right _ _)

Premises used: le_max_right, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
E' : Type u_1
inst : NormedAddCommGroup E'
inst_1 : NormedSpace ℝ E'
inst_2 : FiniteDimensional ℝ E'
⊢ 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:
exact zero_lt_one.trans_le (le_max_right _ _)

Premises used: le_max_right, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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'))
⊢ 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:
apply A.lipschitz

Premises used: ContinuousLinearEquiv.lipschitz
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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'))
⊢ 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
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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) → ℝ)
⊢ 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
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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 : α → ι → ℝ),
    LipschitzWith (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K) g ∧
      EqOn ((⇑A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) ∘ f) g s

Tactic:
L.extend_pi

Premises used: LipschitzOnWith.extend_pi
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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
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
⊢ ∃ (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

Premises used: LipschitzOnWith.extend_pi
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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

Tactic:
⟨A.symm ∘ g, ?_, ?_⟩

Premises used: ContinuousLinearEquiv.symm, Function.comp, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
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)
refine_2 : EqOn f ((⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E') ∘ g) s
⊢ ∃ (g : α → E'), LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s

Tactic:
refine ⟨A.symm ∘ g, ?_, ?_⟩