awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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:
apply A.symm.lipschitz

Premises used: ContinuousLinearEquiv.symm, 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'))
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 (α := (↑(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
-- 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
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')
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
⊢ LipschitzWith (β := E') (lipschitzExtensionConstant E' * K)
    ((⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E') ∘ g)

Tactic:
apply (LAsymm.comp hg).weaken

Premises used: LipschitzWith.weaken, LipschitzWith.comp
-- 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
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')
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
⊢ ‖(↑A.symm : ((↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) →L[ℝ] E')‖₊ *
      (‖(↑A : E' →L[ℝ] (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ)‖₊ * K) ≤
    lipschitzExtensionConstant E' * K

Tactic:
rw [lipschitzExtensionConstant, ← mul_assoc]

Premises used: mul_assoc, lipschitzExtensionConstant
-- 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
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 ≤
    (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:
mul_le_mul' (le_max_left _ _) le_rfl

Premises used: le_rfl, le_max_left, mul_le_mul'
-- 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
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 ≤
    (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:
exact mul_le_mul' (le_max_left _ _) le_rfl

Premises used: le_rfl, le_max_left, mul_le_mul'
-- 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
x : α
hx : x ∈ s
⊢ (A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) (f x) = g x

Tactic:
have : A (f x) = g x := gs hx
-- 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
x : α
hx : x ∈ s
this : (A : (a : E') → (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) (f x) = g x
⊢ f x = ((⇑A.symm : (a : (↑(Basis.ofVectorSpaceIndex ℝ E') : Type u_2) → ℝ) → E') ∘ g) x

Tactic:
simp only [(· ∘ ·), ← this, A.symm_apply_apply]

Premises used: Function.comp, ContinuousLinearEquiv.symm_apply_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 𝕜
inst_6 : FiniteDimensional 𝕜 E
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
inl : Subsingleton E → ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
inr : Nontrivial E → ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
⊢ ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
cases subsingleton_or_nontrivial E

Premises used: subsingleton_or_nontrivial
-- 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
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
h : Subsingleton E
⊢ ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
⟨1, zero_lt_one, AntilipschitzWith.of_subsingleton⟩

Premises used: AntilipschitzWith.of_subsingleton, zero_lt_one, And.intro, Exists.intro, OfNat.ofNat
-- 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
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
h : Subsingleton E
⊢ ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
exact ⟨1, zero_lt_one, AntilipschitzWith.of_subsingleton⟩
-- 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
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
h : Nontrivial E
⊢ Function.Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F)

Tactic:
rw [LinearMap.ker_eq_bot] at hf

Premises used: LinearMap.ker_eq_bot
-- 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
f : E →ₗ[𝕜] F
hf : f.ker = ⊥
h : Nontrivial E
hf₁ : Function.Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ Nontrivial E

Tactic:
rw [LinearMap.ker_eq_bot] at hf

Premises used: LinearMap.ker_eq_bot
-- 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
f : E →ₗ[𝕜] F
hf : Function.Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F)
h : Nontrivial E
e : ContinuousLinearEquiv.{u, u, v, w} (RingHom.id 𝕜) E ↥f.range :=
  LinearEquiv.toContinuousLinearEquiv (LinearEquiv.ofInjective f hf)
⊢ ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
⟨_, e.nnnorm_symm_pos, e.antilipschitz⟩

Premises used: ContinuousLinearEquiv.antilipschitz, And.intro, Exists.intro, ContinuousLinearEquiv.nnnorm_symm_pos
-- 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
f : E →ₗ[𝕜] F
hf : Function.Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F)
h : Nontrivial E
e : ContinuousLinearEquiv.{u, u, v, w} (RingHom.id 𝕜) E ↥f.range :=
  LinearEquiv.toContinuousLinearEquiv (LinearEquiv.ofInjective f hf)
⊢ ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
exact ⟨_, e.nnnorm_symm_pos, e.antilipschitz⟩
-- 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
f : E →ₗ[𝕜] F
mp :
  Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F) →
    ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
mpr :
  (∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)) →
    Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F)
⊢ Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F) ↔
    ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
constructor
-- 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
f : E →ₗ[𝕜] F
mp : f.ker = ⊥ → ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
⊢ Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F) →
    ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
rw [← LinearMap.ker_eq_bot]

Premises used: LinearMap.ker_eq_bot
-- 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
f : E →ₗ[𝕜] F
⊢ f.ker = ⊥ → ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
f.exists_antilipschitzWith

Premises used: LinearMap.exists_antilipschitzWith
-- 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
f : E →ₗ[𝕜] F
⊢ f.ker = ⊥ → ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)

Tactic:
exact f.exists_antilipschitzWith

Premises used: LinearMap.exists_antilipschitzWith
-- 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
f : E →ₗ[𝕜] F
K : ℝ≥0
H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
⊢ Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F)

Tactic:
H.injective

Premises used: AntilipschitzWith.injective
-- 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
f : E →ₗ[𝕜] F
K : ℝ≥0
H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f : (a : E) → F)
⊢ Injective.{v + 1, w + 1} (α := E) (β := F) (⇑f : (a : E) → F)

Tactic:
exact H.injective

Premises used: AntilipschitzWith.injective
-- 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
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := PE) (β := PF) (⇑f : (a : PE) → PF)
obtain :
  ∀ (K : ℝ≥0) (hK : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f.linear : (a : E) → F)),
    ∃ (K : ℝ≥0), AntilipschitzWith.{u_1, u_2} (α := PE) (β := PF) K (⇑f : (a : PE) → PF)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_1, u_2} (α := PE) (β := PF) K (⇑f : (a : PE) → PF)

Tactic:
obtain ⟨K, -, hK⟩ := f.linear.injective_iff_antilipschitz.mp (f.linear_injective_iff.mpr hf)

Premises used: Iff.mpr, AffineMap.linear_injective_iff, AffineMap.linear, Iff.mp, LinearMap.injective_iff_antilipschitz
-- 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
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := PE) (β := PF) (⇑f : (a : PE) → PF)
K : ℝ≥0
hK : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f.linear : (a : E) → F)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_1, u_2} (α := PE) (β := PF) K (⇑f : (a : PE) → PF)

Tactic:
⟨K, AntilipschitzWith.of_le_mul_dist fun x y ↦ ?_⟩

Premises used: AntilipschitzWith.of_le_mul_dist, Exists.intro
-- 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
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := PE) (β := PF) (⇑f : (a : PE) → PF)
K : ℝ≥0
hK : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑f.linear : (a : E) → F)
refine :
  ∀ (x y : PE), dist x y ≤ (↑K : ℝ) * dist.{u_2} (α := PF) ((f : (a : PE) → PF) x : PF) ((f : (a : PE) → PF) y : PF)
⊢ ∃ (K : ℝ≥0), AntilipschitzWith.{u_1, u_2} (α := PE) (β := PF) K (⇑f : (a : PE) → PF)

Tactic:
refine ⟨K, AntilipschitzWith.of_le_mul_dist fun x y ↦ ?_⟩