awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
m : (i : ι) → E i
apply :
  norm (E := G →L[𝕜] G') ((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') * ‖x‖ ≤ (‖f‖ * ∏ i : ι, ‖m i‖) * ‖x‖
⊢ norm.{wG'} (E := G') ((((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x : G') ≤
    (‖f‖ * ∏ i : ι, ‖m i‖) * ‖x‖

Tactic:
apply ((f m).le_opNorm x).trans

Premises used: ContinuousLinearMap.le_opNorm, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
m : (i : ι) → E i
hbc : norm (E := G →L[𝕜] G') ((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') ≤ ‖f‖ * ∏ i : ι, ‖m i‖
⊢ norm (E := G →L[𝕜] G') ((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') * ‖x‖ ≤ (‖f‖ * ∏ i : ι, ‖m i‖) * ‖x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
m : (i : ι) → E i
⊢ norm (E := G →L[𝕜] G') ((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') ≤ ‖f‖ * ∏ i : ι, ‖m i‖

Tactic:
apply f.le_opNorm

Premises used: ContinuousMultilinearMap.le_opNorm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : SeminormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
inst_7 : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
⊢ f.flipMultilinear (E := E).flipLinear (E := E) = f

Tactic:
rfl

Premises used: MultilinearMap.mkContinuous, ContinuousMultilinearMap.flipLinear, MultilinearMap.mkContinuousLinear, LinearMap.mkContinuous, rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : SeminormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
⊢ f.flipLinear (E := E).flipMultilinear (E := E) = f

Tactic:
rfl

Premises used: ContinuousLinearMap.flipMultilinear, MultilinearMap.mkContinuous, LinearMap.mkContinuous, rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
f g : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
H :
  ∀ (x : (i : ι) → E i) (x_1 : G),
    Eq.{wG' + 1} (α := G')
      (((((f + g).flipMultilinear (E := E) : (a : (i : ι) → E i) → G →L[𝕜] G') x : G →L[𝕜] G') : (a : G) → G') x_1 : G')
      ((((f.flipMultilinear (E := E) + g.flipMultilinear (E := E) : (a : (i : ι) → E i) → G →L[𝕜] G') x : G →L[𝕜] G') :
            (a : G) → G')
          x_1 :
        G')
⊢ (f + g).flipMultilinear (E := E) = f.flipMultilinear (E := E) + g.flipMultilinear (E := E)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
f g : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
x : (i : ι) → E i
x_1 : G
⊢ Eq.{wG' + 1} (α := G')
    (((((f + g).flipMultilinear (E := E) : (a : (i : ι) → E i) → G →L[𝕜] G') x : G →L[𝕜] G') : (a : G) → G') x_1 : G')
    ((((f.flipMultilinear (E := E) + g.flipMultilinear (E := E) : (a : (i : ι) → E i) → G →L[𝕜] G') x : G →L[𝕜] G') :
          (a : G) → G')
        x_1 :
      G')

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
c : 𝕜
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
H :
  ∀ (x : (i : ι) → E i) (x_1 : G),
    Eq.{wG' + 1} (α := G')
      (((((c • f).flipMultilinear (E := E) : (a : (i : ι) → E i) → G →L[𝕜] G') x : G →L[𝕜] G') : (a : G) → G') x_1 : G')
      ((((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (f.flipMultilinear (E := E)) :
                  (a : (i : ι) → E i) → G →L[𝕜] G')
                x :
              G →L[𝕜] G') :
            (a : G) → G')
          x_1 :
        G')
⊢ (c • f).flipMultilinear (E := E) =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (f.flipMultilinear (E := E))

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
c : 𝕜
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
x : (i : ι) → E i
x_1 : G
⊢ Eq.{wG' + 1} (α := G')
    (((((c • f).flipMultilinear (E := E) : (a : (i : ι) → E i) → G →L[𝕜] G') x : G →L[𝕜] G') : (a : G) → G') x_1 : G')
    ((((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (f.flipMultilinear (E := E)) :
                (a : (i : ι) → E i) → G →L[𝕜] G')
              x :
            G →L[𝕜] G') :
          (a : G) → G')
        x_1 :
      G')

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : SeminormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
inst_7 : Fintype ι
⊢ Eq (α := (a : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') → ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G'))
    (⇑(flipMultilinearEquiv 𝕜 E G G') :
      (a : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G') → ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G'))
    (flipMultilinear (E := E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : SeminormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
inst_7 : Fintype ι
⊢ Eq (α := (a : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')) → G →L[𝕜] ContinuousMultilinearMap 𝕜 E G')
    (⇑(ContinuousLinearEquiv.symm (flipMultilinearEquiv 𝕜 E G G')) :
      (a : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')) → G →L[𝕜] ContinuousMultilinearMap 𝕜 E G')
    (flipLinear (E := E))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : SeminormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : SeminormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
inst_7 : Fintype ι
g : G →ₗᵢ[𝕜] G'
f : ContinuousMultilinearMap 𝕜 E G
⊢ ‖g.toContinuousLinearMap.compContinuousMultilinearMap (M₁ := E) f‖ = ‖f‖

Tactic:
simp only [ContinuousLinearMap.compContinuousMultilinearMap_coe,
    LinearIsometry.coe_toContinuousLinearMap, LinearIsometry.norm_map,
    ContinuousMultilinearMap.norm_def, Function.comp_apply]

Premises used: LinearIsometry.norm_map, LinearIsometry.coe_toContinuousLinearMap, ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, ContinuousMultilinearMap.norm_def
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
⊢ 0 ≤ ‖g‖ * ∏ i : ι, ‖f i‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
m : (i : ι) → E i
hbc :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) univ i →
      norm.{wE₁} (E := E₁ i) ((f i : (a : E i) → E₁ i) (m i) : E₁ i) ≤ ‖f i‖ * ‖m i‖
⊢ ‖g‖ * ∏ i : ι, norm.{wE₁} (E := E₁ i) ((f i : (a : E i) → E₁ i) (m i) : E₁ i) ≤ ‖g‖ * ∏ i : ι, ‖f i‖ * ‖m i‖

Tactic:
gcongr with i
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
m : (i : ι) → E i
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ norm.{wE₁} (E := E₁ i) ((f i : (a : E i) → E₁ i) (m i) : E₁ i) ≤ ‖f i‖ * ‖m i‖

Tactic:
(f i).le_opNorm (m i)

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
m : (i : ι) → E i
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ norm.{wE₁} (E := E₁ i) ((f i : (a : E i) → E₁ i) (m i) : E₁ i) ≤ ‖f i‖ * ‖m i‖

Tactic:
exact (f i).le_opNorm (m i)

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
m : (i : ι) → E i
rw : ‖g‖ * HMul.hMul (α := ℝ) (∏ x : ι, ‖f x‖) (∏ x : ι, ‖m x‖) = (‖g‖ * ∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖
rw₁ rw₂ :
  ‖g‖ * HMul.hMul (α := ℝ) (∏ x : ι, ‖f x‖) (∏ x : ι, ‖m x‖) =
    ‖g‖ * HMul.hMul (α := ℝ) (∏ i : ι, ‖f i‖) (∏ i : ι, ‖m i‖)
⊢ ‖g‖ * ∏ i : ι, ‖f i‖ * ‖m i‖ = (‖g‖ * ∏ i : ι, ‖f i‖) * ∏ i : ι, ‖m i‖

Tactic:
rw [prod_mul_distrib, mul_assoc]

Premises used: Finset.prod_mul_distrib, mul_assoc
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometry.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
⊢ norm (E := ContinuousMultilinearMap 𝕜 E G)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toContinuousLinearMap) ≤
    ‖g‖

Tactic:
opNorm_le_bound (norm_nonneg _) fun m => ?_

Premises used: ContinuousMultilinearMap.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometry.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
refine :
  ∀ (m : (i : ι) → E i),
    norm.{wG} (E := G)
        ((g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toContinuousLinearMap :
              (a : (i : ι) → E i) → G)
            m :
          G) ≤
      ‖g‖ * ∏ i : ι, ‖m i‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 E G)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toContinuousLinearMap) ≤
    ‖g‖

Tactic:
refine opNorm_le_bound (norm_nonneg _) fun m => ?_

Premises used: ContinuousMultilinearMap.opNorm_le_bound, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometry.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
m : (i : ι) → E i
apply :
  ‖g‖ *
      ∏ i : ι,
        norm.{wE₁} (E := E₁ i)
          ((((fun (i : ι) ↦
                      ((↑((fun (i : ι) ↦ (f i).toContinuousLinearMap) i) :
                          LinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) :
                        LinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)))
                    i :
                  LinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) :
                (a : E i) → E₁ i)
              (m i) :
            E₁ i) ≤
    ‖g‖ * ∏ i : ι, ‖m i‖
⊢ norm.{wG} (E := G)
      ((g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toContinuousLinearMap :
            (a : (i : ι) → E i) → G)
          m :
        G) ≤
    ‖g‖ * ∏ i : ι, ‖m i‖

Tactic:
apply (g.le_opNorm _).trans _

Premises used: ContinuousMultilinearMap.le_opNorm, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometry.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
m : (i : ι) → E i
⊢ ‖g‖ *
      ∏ i : ι,
        norm.{wE₁} (E := E₁ i)
          ((((fun (i : ι) ↦
                      ((↑((fun (i : ι) ↦ (f i).toContinuousLinearMap) i) :
                          LinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) :
                        LinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)))
                    i :
                  LinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) :
                (a : E i) → E₁ i)
              (m i) :
            E₁ i) ≤
    ‖g‖ * ∏ i : ι, ‖m i‖

Tactic:
simp only [ContinuousLinearMap.coe_coe, LinearIsometry.coe_toContinuousLinearMap,
    LinearIsometry.norm_map, le_rfl]

Premises used: LinearIsometry.norm_map, le_rfl, LinearIsometry.coe_toContinuousLinearMap, ContinuousLinearMap.coe_coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometryEquiv.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
apply :
  ‖g‖ ≤
    norm (E := ContinuousMultilinearMap 𝕜 E G)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toLinearIsometry.toContinuousLinearMap)
⊢ norm (E := ContinuousMultilinearMap 𝕜 E G)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i)) =
    ‖g‖

Tactic:
apply le_antisymm (g.norm_compContinuous_linearIsometry_le fun i => (f i).toLinearIsometry)

Premises used: LinearIsometryEquiv.toLinearIsometry, ContinuousMultilinearMap.norm_compContinuous_linearIsometry_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometryEquiv.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
H :
  ∀ (m : (i : ι) → E₁ i),
    Eq.{wG + 1} (α := G) ((g : (a : (i : ι) → E₁ i) → G) m : G)
      ((compContinuousLinearMap (M₁ := E₁) (M₁' := E)
              (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦
                (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i))
              fun (i : ι) ↦ (↑(↑(f i).symm : E₁ i ≃L[𝕜] E i) : E₁ i →L[𝕜] E i) :
            (a : (i : ι) → E₁ i) → G)
          m :
        G)
⊢ g =
    compContinuousLinearMap (M₁ := E₁) (M₁' := E)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i))
      fun (i : ι) ↦ (↑(↑(f i).symm : E₁ i ≃L[𝕜] E i) : E₁ i →L[𝕜] E i)

Tactic:
ext1 m
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometryEquiv.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
m : (i : ι) → E₁ i
⊢ Eq.{wG + 1} (α := G) ((g : (a : (i : ι) → E₁ i) → G) m : G)
    ((compContinuousLinearMap (M₁ := E₁) (M₁' := E)
            (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦
              (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i))
            fun (i : ι) ↦ (↑(↑(f i).symm : E₁ i ≃L[𝕜] E i) : E₁ i →L[𝕜] E i) :
          (a : (i : ι) → E₁ i) → G)
        m :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometryEquiv.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
⊢ g =
    compContinuousLinearMap (M₁ := E₁) (M₁' := E)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i))
      fun (i : ι) ↦ (↑(↑(f i).symm : E₁ i ≃L[𝕜] E i) : E₁ i →L[𝕜] E i)

Tactic:
have : g = (g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)).compContinuousLinearMap
      fun i => ((f i).symm : E₁ i →L[𝕜] E i) := by
    ext1 m
    simp