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
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)
x y : PE
rw : ‖x -ᵥ y‖ ≤ (↑K : ℝ) * norm.{w} (E := F) ((f.linear : (a : E) → F) (x -ᵥ y) : F)
⊢ dist x y ≤ (↑K : ℝ) * dist.{u_2} (α := PF) ((f : (a : PE) → PF) x : PF) ((f : (a : PE) → PF) y : PF)

Tactic:
rw [dist_eq_norm_vsub E, dist_eq_norm_vsub F, ← f.linearMap_vsub]

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

Tactic:
ZeroHomClass.bound_of_antilipschitz f.linear hK (x -ᵥ y)

Premises used: VSub.vsub, ZeroHomClass.bound_of_antilipschitz, AffineMap.linear
-- 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)
x y : PE
⊢ ‖x -ᵥ y‖ ≤ (↑K : ℝ) * norm.{w} (E := F) ((f.linear : (a : E) → F) (x -ᵥ y) : F)

Tactic:
exact ZeroHomClass.bound_of_antilipschitz f.linear hK (x -ᵥ y)

Premises used: VSub.vsub, ZeroHomClass.bound_of_antilipschitz, AffineMap.linear
-- 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
rw :
  ∀ (x : E →L[𝕜] F),
    Membership.mem (γ := Set (E →L[𝕜] F))
        {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)} x →
      ∀ᶠ (y : E →L[𝕜] F) in 𝓝 x,
        Membership.mem (γ := Set (E →L[𝕜] F))
          {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)} y
⊢ IsOpen (X := E →L[𝕜] F) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}

Tactic:
rw [isOpen_iff_eventually]

Premises used: isOpen_iff_eventually
-- 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
φ₀ : E →L[𝕜] F
hφ₀ :
  Membership.mem (γ := Set (E →L[𝕜] F)) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
    φ₀
rcases :
  ∀ (K : ℝ≥0) (K_pos : K > 0) (H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ₀ : E →ₗ[𝕜] F) : (a : E) → F)),
    ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀,
      Membership.mem (γ := Set (E →L[𝕜] F))
        {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)} y
⊢ ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀,
    Membership.mem (γ := Set (E →L[𝕜] F))
      {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)} y

Tactic:
rcases φ₀.injective_iff_antilipschitz.mp hφ₀ with ⟨K, K_pos, H⟩

Premises used: ContinuousLinearMap.toLinearMap, 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ :
  Membership.mem (γ := Set (E →L[𝕜] F)) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
    φ₀
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ₀ : E →ₗ[𝕜] F) : (a : E) → F)
⊢ ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹

Tactic:
have : ∀ᶠ φ in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹ := eventually_nnnorm_sub_lt _ <| inv_pos_of_pos K_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
φ₀ : E →L[𝕜] F
hφ₀ :
  Membership.mem (γ := Set (E →L[𝕜] F)) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
    φ₀
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ₀ : E →ₗ[𝕜] F) : (a : E) → F)
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
h : ∀ (φ : E →L[𝕜] F) (hφ : ‖φ - φ₀‖₊ < K⁻¹), Injective.{v + 1, w + 1} (α := E) (β := F) (⇑φ : (a : E) → F)
⊢ ∀ᶠ (y : E →L[𝕜] F) in 𝓝 φ₀,
    Membership.mem (γ := Set (E →L[𝕜] F))
      {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)} y

Tactic:
filter_upwards [this] with φ 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ :
  Membership.mem (γ := Set (E →L[𝕜] F)) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
    φ₀
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ₀ : E →ₗ[𝕜] F) : (a : E) → F)
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
φ : E →L[𝕜] F
hφ : ‖φ - φ₀‖₊ < K⁻¹
h : ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ : E →ₗ[𝕜] F) : (a : E) → F)
⊢ Injective.{v + 1, w + 1} (α := E) (β := F) (⇑φ : (a : E) → F)

Tactic:
apply φ.injective_iff_antilipschitz.mpr

Premises used: Iff.mpr, ContinuousLinearMap.toLinearMap, 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 𝕜
inst_6 : FiniteDimensional 𝕜 E
φ₀ : E →L[𝕜] F
hφ₀ :
  Membership.mem (γ := Set (E →L[𝕜] F)) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
    φ₀
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ₀ : E →ₗ[𝕜] F) : (a : E) → F)
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
φ : E →L[𝕜] F
hφ : ‖φ - φ₀‖₊ < K⁻¹
⊢ ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ : E →ₗ[𝕜] F) : (a : E) → F)

Tactic:
⟨(K⁻¹ - ‖φ - φ₀‖₊)⁻¹, inv_pos_of_pos (tsub_pos_of_lt hφ),
    H.add_sub_lipschitzWith (φ - φ₀).lipschitz hφ⟩

Premises used: NNNorm.nnnorm, HSub.hSub, ContinuousLinearMap.lipschitz, inv_pos_of_pos, Inv.inv, And.intro, Exists.intro, AntilipschitzWith.add_sub_lipschitzWith, tsub_pos_of_lt
-- 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
φ₀ : E →L[𝕜] F
hφ₀ :
  Membership.mem (γ := Set (E →L[𝕜] F)) {L : E →L[𝕜] F | Injective.{v + 1, w + 1} (α := E) (β := F) (⇑L : (a : E) → F)}
    φ₀
K : ℝ≥0
K_pos : K > 0
H : AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ₀ : E →ₗ[𝕜] F) : (a : E) → F)
this : ∀ᶠ (φ : E →L[𝕜] F) in 𝓝 φ₀, ‖φ - φ₀‖₊ < K⁻¹
φ : E →L[𝕜] F
hφ : ‖φ - φ₀‖₊ < K⁻¹
⊢ ∃ K > 0, AntilipschitzWith.{v, w} (α := E) (β := F) K (⇑(↑φ : E →ₗ[𝕜] F) : (a : E) → F)

Tactic:
exact ⟨(K⁻¹ - ‖φ - φ₀‖₊)⁻¹, inv_pos_of_pos (tsub_pos_of_lt hφ),
    H.add_sub_lipschitzWith (φ - φ₀).lipschitz 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 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
⊢ Continuous[Pi.topologicalSpace, topologicalSpace]
    (⇑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜) ≪≫ₗ
          LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
      (a : ι → E) → (ι → 𝕜) →L[𝕜] E)

Tactic:
AddMonoidHomClass.continuous_of_bound
        (LinearMap.toContinuousLinearMap.toLinearMap.comp
            (LinearEquiv.piRing 𝕜 E ι 𝕜).symm.toLinearMap)
        (Fintype.card ι : ℝ) fun g ↦ ?_

Premises used: LinearEquiv.symm, AddMonoidHomClass.continuous_of_bound, Fintype.card, Nat.cast, LinearMap.comp, LinearEquiv.toLinearMap, LinearEquiv.piRing, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
refine :
  ∀ (g : ι → E),
    norm (E := (ι → 𝕜) →L[𝕜] E)
        ((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                    ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                  (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
                (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
              (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
            g :
          (ι → 𝕜) →L[𝕜] E) ≤
      (↑(Fintype.card ι) : ℝ) * ‖g‖
⊢ Continuous[Pi.topologicalSpace, topologicalSpace]
    (⇑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜) ≪≫ₗ
          LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
      (a : ι → E) → (ι → 𝕜) →L[𝕜] E)

Tactic:
refine AddMonoidHomClass.continuous_of_bound
        (LinearMap.toContinuousLinearMap.toLinearMap.comp
            (LinearEquiv.piRing 𝕜 E ι 𝕜).symm.toLinearMap)
        (Fintype.card ι : ℝ) fun g ↦ ?_

Premises used: LinearEquiv.symm, AddMonoidHomClass.continuous_of_bound, Fintype.card, Nat.cast, LinearMap.comp, LinearEquiv.toLinearMap, LinearEquiv.piRing, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
rw :
  norm (E := (ι → 𝕜) →L[𝕜] E)
      ((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                  ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
              (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
            (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
          g :
        (ι → 𝕜) →L[𝕜] E) ≤
    Fintype.card ι • ‖g‖
⊢ norm (E := (ι → 𝕜) →L[𝕜] E)
      ((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                  ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
              (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
            (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
          g :
        (ι → 𝕜) →L[𝕜] E) ≤
    (↑(Fintype.card ι) : ℝ) * ‖g‖

Tactic:
rw [← nsmul_eq_mul]

Premises used: nsmul_eq_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 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
⊢ norm (E := (ι → 𝕜) →L[𝕜] E)
      ((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                  ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
              (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
            (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
          g :
        (ι → 𝕜) →L[𝕜] E) ≤
    Fintype.card ι • ‖g‖

Tactic:
opNorm_le_bound _ (nsmul_nonneg (norm_nonneg g) (Fintype.card ι)) fun t ↦ ?_

Premises used: Fintype.card, ContinuousLinearMap.opNorm_le_bound, nsmul_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
refine :
  ∀ (t : ι → 𝕜),
    norm.{v} (E := E)
        ((((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                          ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                        (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
                      (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
                    (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
                  g :
                (ι → 𝕜) →L[𝕜] E) :
              (a : ι → 𝕜) → E)
            t :
          E) ≤
      Fintype.card ι • ‖g‖ * ‖t‖
⊢ norm (E := (ι → 𝕜) →L[𝕜] E)
      ((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                  ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
              (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
            (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
          g :
        (ι → 𝕜) →L[𝕜] E) ≤
    Fintype.card ι • ‖g‖

Tactic:
refine opNorm_le_bound _ (nsmul_nonneg (norm_nonneg g) (Fintype.card ι)) fun t ↦ ?_

Premises used: Fintype.card, ContinuousLinearMap.opNorm_le_bound, nsmul_nonneg, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
simp_rw : norm.{v} (E := E) (∑ i : ι, t i • g i) ≤ Fintype.card ι • ‖g‖ * ‖t‖
⊢ norm.{v} (E := E)
      ((((((↑(LinearMap.toContinuousLinearMap (𝕜 := 𝕜) (E := ι → 𝕜) (F' := E)) :
                        ((ι → 𝕜) →ₗ[𝕜] E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) ∘ₗ
                      (↑(LinearEquiv.symm (LinearEquiv.piRing 𝕜 E ι 𝕜)) : (ι → E) →ₗ[𝕜] (ι → 𝕜) →ₗ[𝕜] E) :
                    (ι → E) →ₗ[𝕜] (ι → 𝕜) →L[𝕜] E) :
                  (a : ι → E) → (ι → 𝕜) →L[𝕜] E)
                g :
              (ι → 𝕜) →L[𝕜] E) :
            (a : ι → 𝕜) → E)
          t :
        E) ≤
    Fintype.card ι • ‖g‖ * ‖t‖

Tactic:
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply,
        LinearMap.coe_toContinuousLinearMap', LinearEquiv.piRing_symm_apply]

Premises used: LinearMap.coe_toContinuousLinearMap', LinearEquiv.piRing_symm_apply, LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_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 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
apply : ∑ i : ι, ‖t i • g i‖ ≤ Fintype.card ι • ‖g‖ * ‖t‖
⊢ norm.{v} (E := E) (∑ i : ι, t i • g i) ≤ Fintype.card ι • ‖g‖ * ‖t‖

Tactic:
apply le_trans (norm_sum_le _ _)

Premises used: norm_sum_le, le_trans
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
rw : ∑ i : ι, ‖t i • g i‖ ≤ Fintype.card ι • (‖g‖ * ‖t‖)
⊢ ∑ i : ι, ‖t i • g i‖ ≤ Fintype.card ι • ‖g‖ * ‖t‖

Tactic:
rw [smul_mul_assoc]

Premises used: smul_mul_assoc
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
⊢ ∑ i : ι, ‖t i • g i‖ ≤ Fintype.card ι • (‖g‖ * ‖t‖)

Tactic:
Finset.sum_le_card_nsmul _ _ _ fun i _ ↦ ?_

Premises used: Fintype.card, Finset.sum_le_card_nsmul
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
refine : ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → ‖t i • g i‖ ≤ ‖g‖ * ‖t‖
⊢ ∑ i : ι, ‖t i • g i‖ ≤ Fintype.card ι • (‖g‖ * ‖t‖)

Tactic:
refine Finset.sum_le_card_nsmul _ _ _ fun i _ ↦ ?_

Premises used: Finset.sum_le_card_nsmul
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
rw : ‖g i‖ * ‖t i‖ ≤ ‖g‖ * ‖t‖
⊢ ‖t i • g i‖ ≤ ‖g‖ * ‖t‖

Tactic:
rw [norm_smul, mul_comm]

Premises used: norm_smul, mul_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 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
h₁ : ‖g i‖ ≤ ‖g‖
h₂ : ‖t i‖ ≤ ‖t‖
⊢ ‖g i‖ * ‖t i‖ ≤ ‖g‖ * ‖t‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ‖g i‖ ≤ ‖g‖

Tactic:
apply norm_le_pi_norm

Premises used: norm_le_pi_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 𝕜
ι : Type u_1
inst_6 : Fintype ι
inst_7 : DecidableEq ι
g : ι → E
t : ι → 𝕜
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ‖t i‖ ≤ ‖t‖

Tactic:
apply norm_le_pi_norm

Premises used: norm_le_pi_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 𝕜
ι : Type u_1
inst_4 : Finite ι
f : ι → E
hf : LinearIndependent 𝕜 f
intro : ∀ (val : Fintype ι), ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace 𝕜
ι : Type u_1
inst_4 : Finite ι
f : ι → E
hf : LinearIndependent 𝕜 f
val : Fintype ι
intro :
  ∀
    (hf :
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (f i)))
        ⊥),
    ∀ᶠ (g : ι → E) in 𝓝 f,
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (g i)))
        ⊥
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g

Tactic:
simp only [Fintype.linearIndependent_iff'] at hf ⊢

Premises used: Fintype.linearIndependent_iff'
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace 𝕜
ι : Type u_1
inst_4 : Finite ι
f : ι → E
val : Fintype ι
hf :
  Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
    (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
      ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
        LinearMap.smulRight LinearMap.id (f i)))
    ⊥
intro :
  ∀ (K : ℝ≥0) (K0 : K > 0)
    (hK :
      AntilipschitzWith (α := (i : ι) → 𝕜) (β := E) K
        (⇑((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
              LinearMap.smulRight LinearMap.id (f i)) :
          (a : (i : ι) → 𝕜) → E)),
    ∀ᶠ (g : ι → E) in 𝓝 f,
      Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
        (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
          ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
            LinearMap.smulRight LinearMap.id (g i)))
        ⊥
⊢ ∀ᶠ (g : ι → E) in 𝓝 f,
    Eq (α := Submodule 𝕜 ((i : ι) → 𝕜))
      (LinearMap.ker (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
        ((LinearMap.lsum 𝕜 (fun (x : ι) ↦ 𝕜) ℕ : (a : (i : ι) → 𝕜 →ₗ[𝕜] E) → ((i : ι) → 𝕜) →ₗ[𝕜] E) fun (i : ι) ↦
          LinearMap.smulRight LinearMap.id (g i)))
      ⊥

Tactic:
rcases LinearMap.exists_antilipschitzWith _ hf with ⟨K, K0, hK⟩

Premises used: LinearMap.exists_antilipschitzWith