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 𝕜
n : ℕ
⊢ IsOpen (X := E →L[𝕜] F)
    (⋃ (i : Finset E),
      ⋃ (_ : i.card = n),
        {x : E →L[𝕜] F |
          LinearIndependent.{v, u, w} 𝕜 (M := F) fun (x_1 : (↑(↑i : Set E) : Type v)) ↦
            ((↑x : E →ₗ[𝕜] F) : (a : E) → F) (↑x_1 : E)})

Tactic:
isOpen_biUnion fun t _ => ?_

Premises used: Set.Mem, isOpen_biUnion
-- 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 𝕜
n : ℕ
refine :
  ∀ (t : Finset E),
    Membership.mem (γ := Set (Finset E)) (fun (i : Finset E) ↦ i.card = n) t →
      IsOpen (X := E →L[𝕜] F)
        {x : E →L[𝕜] F |
          LinearIndependent.{v, u, w} 𝕜 (M := F) fun (x_1 : (↑(↑t : Set E) : Type v)) ↦
            ((↑x : E →ₗ[𝕜] F) : (a : E) → F) (↑x_1 : E)}
⊢ IsOpen (X := E →L[𝕜] F)
    (⋃ (i : Finset E),
      ⋃ (_ : i.card = n),
        {x : E →L[𝕜] F |
          LinearIndependent.{v, u, w} 𝕜 (M := F) fun (x_1 : (↑(↑i : Set E) : Type v)) ↦
            ((↑x : E →ₗ[𝕜] F) : (a : E) → F) (↑x_1 : E)})

Tactic:
refine isOpen_biUnion fun t _ => ?_

Premises used: isOpen_biUnion
-- 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 𝕜
n : ℕ
t : Finset E
h : Membership.mem (γ := Set (Finset E)) (fun (i : Finset E) ↦ i.card = n) t
⊢ Continuous[_, Pi.topologicalSpace] fun (f : E →L[𝕜] F) (x : (↑(↑t : Set E) : Type v)) ↦ (f : (a : E) → F) (↑x : E)

Tactic:
have : Continuous fun f : E →L[𝕜] F => fun x : (t : Set E) => f x :=
    continuous_pi fun x => (ContinuousLinearMap.apply 𝕜 F (x : E)).continuous
-- 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 𝕜
n : ℕ
t : Finset E
h : Membership.mem (γ := Set (Finset E)) (fun (i : Finset E) ↦ i.card = n) t
this :
  Continuous[_, Pi.topologicalSpace] fun (f : E →L[𝕜] F) (x : (↑(↑t : Set E) : Type v)) ↦ (f : (a : E) → F) (↑x : E)
⊢ IsOpen (X := E →L[𝕜] F)
    {x : E →L[𝕜] F |
      LinearIndependent.{v, u, w} 𝕜 (M := F) fun (x_1 : (↑(↑t : Set E) : Type v)) ↦
        ((↑x : E →ₗ[𝕜] F) : (a : E) → F) (↑x_1 : E)}

Tactic:
isOpen_setOf_linearIndependent.preimage this

Premises used: Set.Mem, setOf, Set.preimage, LinearIndependent, Function.Injective, IsOpen.preimage, isOpen_setOf_linearIndependent
-- 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 𝕜
n : ℕ
t : Finset E
h : Membership.mem (γ := Set (Finset E)) (fun (i : Finset E) ↦ i.card = n) t
this :
  Continuous[_, Pi.topologicalSpace] fun (f : E →L[𝕜] F) (x : (↑(↑t : Set E) : Type v)) ↦ (f : (a : E) → F) (↑x : E)
⊢ IsOpen (X := E →L[𝕜] F)
    {x : E →L[𝕜] F |
      LinearIndependent.{v, u, w} 𝕜 (M := F) fun (x_1 : (↑(↑t : Set E) : Type v)) ↦
        ((↑x : E →ₗ[𝕜] F) : (a : E) → F) (↑x_1 : E)}

Tactic:
exact isOpen_setOf_linearIndependent.preimage this

Premises used: IsOpen.preimage, isOpen_setOf_linearIndependent
-- 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 ι
inl : ∀ (h : IsEmpty ι), IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
inr : ∀ (i₀ : ι), IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
⊢ IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}

Tactic:
rcases isEmpty_or_nonempty ι with h | ⟨⟨i₀⟩⟩

Premises used: isEmpty_or_nonempty
-- 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 ι
h : IsEmpty ι
⊢ IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}

Tactic:
isOpen_discrete _

Premises used: isOpen_discrete
-- 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 ι
h : IsEmpty ι
⊢ IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}

Tactic:
exact isOpen_discrete _

Premises used: isOpen_discrete
-- 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 ι
i₀ : ι
inr :
  IsOpen[Pi.topologicalSpace]
    {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}
⊢ IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}

Tactic:
simp_rw [affineIndependent_iff_linearIndependent_vsub 𝕜 _ i₀]

Premises used: affineIndependent_iff_linearIndependent_vsub
-- 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 ι
i₀ : ι
ι' : Type (max 0 u_1) := { x : ι // x ≠ i₀ }
inr :
  ∀ (val : Fintype ι),
    IsOpen[Pi.topologicalSpace]
      {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}
⊢ IsOpen[Pi.topologicalSpace]
    {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}

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 ι
i₀ : ι
ι' : Type (max 0 u_1) := { x : ι // x ≠ i₀ }
val : Fintype ι
inr :
  ∀ (this : Fintype ι'),
    IsOpen[Pi.topologicalSpace]
      {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}
⊢ IsOpen[Pi.topologicalSpace]
    {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}

Tactic:
haveI : Fintype ι' := Subtype.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 ι
i₀ : ι
ι' : Type (max 0 u_1) := { x : ι // x ≠ i₀ }
val : Fintype ι
this : Fintype ι'
inr :
  IsOpen[Pi.topologicalSpace]
    (preimage (β := (i : ι') → E) (fun (p : ι → E) (i : ι') ↦ p (↑i : ι) -ᵥ p i₀) {p : ι' → E | LinearIndependent 𝕜 p})
⊢ IsOpen[Pi.topologicalSpace]
    {p : ι → E | LinearIndependent.{u_1, u, v} 𝕜 (M := E) fun (i : { x : ι // x ≠ i₀ }) ↦ p (↑i : ι) -ᵥ p i₀}

Tactic:
convert_to
      IsOpen ((fun (p : ι → E) (i : ι') ↦ p i -ᵥ p i₀) ⁻¹' {p : ι' → E | LinearIndependent 𝕜 p})

Premises used: setOf, VSub.vsub, Set.preimage, LinearIndependent, IsOpen, Subtype.val
-- 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 ι
i₀ : ι
ι' : Type (max 0 u_1) := { x : ι // x ≠ i₀ }
val : Fintype ι
this : Fintype ι'
⊢ Continuous[Pi.topologicalSpace, Pi.topologicalSpace] fun (p : ι → E) (i : ι') ↦ p (↑i : ι) -ᵥ p i₀

Tactic:
fun_prop
-- 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 ι
i₀ : ι
ι' : Type (max 0 u_1) := { x : ι // x ≠ i₀ }
val : Fintype ι
this : Fintype ι'
⊢ IsOpen[Pi.topologicalSpace]
    (preimage (β := (i : ι') → E) (fun (p : ι → E) (i : ι') ↦ p (↑i : ι) -ᵥ p i₀) {p : ι' → E | LinearIndependent 𝕜 p})

Tactic:
exact isOpen_setOf_linearIndependent.preimage (by fun_prop)

Premises used: IsOpen.preimage, isOpen_setOf_linearIndependent
-- 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 ι
inl : ∀ (h : IsEmpty ι), IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
inr inr₁ : ∀ (i₀ : ι), IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}
⊢ IsOpen[Pi.topologicalSpace] {p : ι → E | AffineIndependent 𝕜 p}

Tactic:
classical
  rcases isEmpty_or_nonempty ι with h | ⟨⟨i₀⟩⟩
  · exact isOpen_discrete _
  · simp_rw [affineIndependent_iff_linearIndependent_vsub 𝕜 _ i₀]
    let ι' := { x // x ≠ i₀ }
    cases nonempty_fintype ι
    haveI : Fintype ι' := Subtype.fintype _
    convert_to
      IsOpen ((fun (p : ι → E) (i : ι') ↦ p i -ᵥ p i₀) ⁻¹' {p : ι' → E | LinearIndependent 𝕜 p})
    exact isOpen_setOf_linearIndependent.preimage (by fun_prop)

Premises used: isEmpty_or_nonempty, nonempty_fintype, isOpen_discrete, IsOpen.preimage, isOpen_setOf_linearIndependent
-- 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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
set :
  let φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜);
  nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) ≤ Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) ≤
    Fintype.card ι • nnnorm (E := E →L[𝕜] ι → 𝕜) (↑v.equivFunL : E →L[𝕜] ι → 𝕜) * M * ‖e‖₊

Tactic:
set φ := v.equivFunL.toContinuousLinearMap

Premises used: Module.Basis.equivFunL, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
rw rw₁ : nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) = nnnorm.{w} (E := F) ((u : (a : E) → F) e : F)
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) =
    nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F)

Tactic:
rw [v.sum_equivFun]

Premises used: Module.Basis.sum_equivFun
-- 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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F) =
    nnnorm.{w} (E := F)
      (∑ i : ι,
        HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))

Tactic:
simp only [equivFun_apply, map_sum, map_smul]

Premises used: map_sum, Module.Basis.equivFun_apply, map_smul
-- 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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ nnnorm.{w} (E := F)
      (∑ i : ι,
        HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F)) ≤
    ∑ i : ι,
      ‖HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F)‖₊

Tactic:
nnnorm_sum_le _ _

Premises used: nnnorm_sum_le
-- 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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ Eq (α := ℝ≥0)
    (∑ i : ι,
      ‖HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F)‖₊)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))

Tactic:
simp only [nnnorm_smul]

Premises used: nnnorm_smul
-- 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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
h :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
⊢ LE.le (α := ℝ≥0)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M)

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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M

Tactic:
apply hu
-- 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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
rw rw₁ :
  Eq (α := ℝ≥0) (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M)
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M)
⊢ ∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M =
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)) * M

Tactic:
rw [Finset.sum_mul]

Premises used: Finset.sum_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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
bc : ∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊)
⊢ (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)) * M ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M

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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ ∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) ≤
    Fintype.card ι • nnnorm (E := ι → 𝕜) ((φ : (a : E) → ι → 𝕜) e : ι → 𝕜)

Tactic:
Pi.sum_nnnorm_apply_le_nnnorm _

Premises used: Pi.sum_nnnorm_apply_le_nnnorm
-- 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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ Fintype.card ι • nnnorm (E := ι → 𝕜) ((φ : (a : E) → ι → 𝕜) e : ι → 𝕜) ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊)

Tactic:
nsmul_le_nsmul_right (φ.le_opNNNorm e) _

Premises used: nsmul_le_nsmul_right, ContinuousLinearMap.le_opNNNorm
-- 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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ ∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊)

Tactic:
calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _

Premises used: HMul.hMul, NNNorm.nnnorm, Fintype.card, nsmul_le_nsmul_right, Pi.sum_nnnorm_apply_le_nnnorm, ContinuousLinearMap.le_opNNNorm, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.FiniteDimension
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
E : Type v
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type w
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace 𝕜
ι : Type u_1
inst_6 : Fintype ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
⊢ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊

Tactic:
simp only [smul_mul_assoc, mul_right_comm]

Premises used: smul_mul_assoc, mul_right_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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ≥0
hu : ∀ (i : ι), nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
e : E
φ : E →L[𝕜] ι → 𝕜 := (↑v.equivFunL : E →L[𝕜] ι → 𝕜)
e₁ :
  nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) =
    nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F)
e₂ :
  nnnorm.{w} (E := F)
      ((u : (a : E) → F)
          (∑ i : ι,
            HSMul.hSMul.{u, v, v} (α := 𝕜) (β := E) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
              ((v : (a : ι) → E) i : E)) :
        F) =
    nnnorm.{w} (E := F)
      (∑ i : ι,
        HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
e₃ :
  Eq (α := ℝ≥0)
    (∑ i : ι,
      ‖HSMul.hSMul.{u, w, w} (α := 𝕜) (β := F) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)
          ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F)‖₊)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
e₄ :
  LE.le (α := ℝ≥0)
    (∑ i : ι,
      nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) *
        nnnorm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F))
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M)
e₅ :
  ∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜) * M =
    (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)) * M
e₆ : (∑ i : ι, nnnorm.{u} (E := 𝕜) ((v.equivFun : (a : E) → ι → 𝕜) e i : 𝕜)) * M ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M
e₇ : Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊
⊢ nnnorm.{w} (E := F) ((u : (a : E) → F) e : F) ≤ Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊

Tactic:
calc
      ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun]
      _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp only [equivFun_apply, map_sum, map_smul]
      _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _
      _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul]
      _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu
      _ = (∑ i, ‖v.equivFun e i‖₊) * M := by rw [Finset.sum_mul]
      _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) * M := by
        gcongr
        calc
          ∑ i, ‖v.equivFun e i‖₊ ≤ Fintype.card ι • ‖φ e‖₊ := Pi.sum_nnnorm_apply_le_nnnorm _
          _ ≤ Fintype.card ι • (‖φ‖₊ * ‖e‖₊) := nsmul_le_nsmul_right (φ.le_opNNNorm e) _
      _ = Fintype.card ι • ‖φ‖₊ * M * ‖e‖₊ := by simp only [smul_mul_assoc, mul_right_comm]

Premises used: nnnorm_sum_le, HMul.hMul, Finset.univ, NNNorm.nnnorm, Fintype.card, HSMul.hSMul, DFunLike.coe, Finset.sum, Module.Basis.equivFun
-- 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 ι
v : Basis ι 𝕜 E
u : E →L[𝕜] F
M : ℝ
hM : 0 ≤ M
hu : ∀ (i : ι), norm.{w} (E := F) ((u : (a : E) → F) ((v : (a : ι) → E) i : E) : F) ≤ M
⊢ ‖u‖ ≤ Fintype.card ι • norm (E := E →L[𝕜] ι → 𝕜) (↑v.equivFunL : E →L[𝕜] ι → 𝕜) * M

Tactic:
simpa using NNReal.coe_le_coe.mpr (v.opNNNorm_le ⟨M, hM⟩ hu)

Premises used: Iff.mpr, Subtype.mk, Module.Basis.opNNNorm_le, NNReal.coe_le_coe