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 : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
c : 𝕜
x : G
⊢ (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') (c • x) : ContinuousMultilinearMap 𝕜 E G') :
        (a : (i : ι) → E i) → G')
      m =
    HSMul.hSMul (α := 𝕜) (β := G') ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      ((((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
            (a : (i : ι) → E i) → G')
          m :
        G')

Tactic:
simp only [ContinuousMultilinearMap.smul_apply, map_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, ContinuousMultilinearMap.smul_apply, map_smul
-- 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 →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
x : G
rw :
  norm.{wG'} (E := G')
      (({
              toFun := fun (x : G) ↦
                (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
                    (a : (i : ι) → E i) → G')
                  m,
              map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' } :
            (a : G) → G')
          x :
        G') ≤
    ‖f‖ * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ norm.{wG'} (E := G')
      (({
              toFun := fun (x : G) ↦
                (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
                    (a : (i : ι) → E i) → G')
                  m,
              map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' } :
            (a : G) → G')
          x :
        G') ≤
    (‖f‖ * ∏ i : ι, ‖m i‖) * ‖x‖

Tactic:
rw [mul_right_comm]

Premises used: mul_right_comm
-- 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 →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
x : G
⊢ norm.{wG'} (E := G')
      (({
              toFun := fun (x : G) ↦
                (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
                    (a : (i : ι) → E i) → G')
                  m,
              map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' } :
            (a : G) → G')
          x :
        G') ≤
    ‖f‖ * ‖x‖ * ∏ i : ι, ‖m i‖

Tactic:
(f x).le_of_opNorm_le (f.le_opNorm x) _

Premises used: ContinuousLinearMap.le_opNorm, ContinuousMultilinearMap.le_of_opNorm_le
-- 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 →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
x : G
⊢ norm.{wG'} (E := G')
      (({
              toFun := fun (x : G) ↦
                (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
                    (a : (i : ι) → E i) → G')
                  m,
              map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' } :
            (a : G) → G')
          x :
        G') ≤
    ‖f‖ * ‖x‖ * ∏ i : ι, ‖m i‖

Tactic:
exact (f x).le_of_opNorm_le (f.le_opNorm x) _

Premises used: ContinuousLinearMap.le_opNorm, ContinuousMultilinearMap.le_of_opNorm_le
-- 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 →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
inst_11 : DecidableEq ι
m : (i : ι) → E i
i : ι
x y : E i
x_1 : G
⊢ Eq.{wG' + 1} (α := G')
    ((LinearMap.mkContinuous
            {
              toFun := fun (x_2 : G) ↦
                (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_2 : ContinuousMultilinearMap 𝕜 E G') :
                    (a : (i : ι) → E i) → G')
                  (update (β := E) m i (x + y)),
              map_add' := ⋯, map_smul' := ⋯ }
            (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i (x + y) i_1‖) ⋯ :
          (a : G) → G')
        x_1 :
      G')
    ((HAdd.hAdd (α := G →L[𝕜] G')
            (LinearMap.mkContinuous
              {
                toFun := fun (x_2 : G) ↦
                  (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_2 : ContinuousMultilinearMap 𝕜 E G') :
                      (a : (i : ι) → E i) → G')
                    (update (β := E) m i x),
                map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' }
              (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯)
            (LinearMap.mkContinuous
              {
                toFun := fun (x : G) ↦
                  (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
                      (a : (i : ι) → E i) → G')
                    (update (β := E) m i y),
                map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' }
              (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i y i_1‖) ⋯) :
          (a : G) → G')
        x_1 :
      G')

Tactic:
simp only [add_apply, ContinuousMultilinearMap.map_update_add, LinearMap.coe_mk,
          LinearMap.mkContinuous_apply, AddHom.coe_mk]

Premises used: LinearMap.coe_mk, LinearMap.mkContinuous_apply, ContinuousMultilinearMap.map_update_add, ContinuousLinearMap.add_apply, AddHom.coe_mk
-- 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 →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
inst_11 : DecidableEq ι
m : (i : ι) → E i
i : ι
c : 𝕜
x : E i
h :
  ∀ (x_1 : G),
    Eq.{wG' + 1} (α := G')
      ((LinearMap.mkContinuous
              {
                toFun := fun (x_2 : G) ↦
                  (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_2 : ContinuousMultilinearMap 𝕜 E G') :
                      (a : (i : ι) → E i) → G')
                    (update (β := E) m i (c • x)),
                map_add' := ⋯, map_smul' := ⋯ }
              (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i (c • x) i_1‖) ⋯ :
            (a : G) → G')
          x_1 :
        G')
      ((HSMul.hSMul (β := G →L[𝕜] G') c
              (LinearMap.mkContinuous
                {
                  toFun := fun (x_2 : G) ↦
                    (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_2 : ContinuousMultilinearMap 𝕜 E G') :
                        (a : (i : ι) → E i) → G')
                      (update (β := E) m i x),
                  map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' }
                (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯) :
            (a : G) → G')
          x_1 :
        G')
⊢ LinearMap.mkContinuous
      {
        toFun := fun (x_1 : G) ↦
          (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_1 : ContinuousMultilinearMap 𝕜 E G') :
              (a : (i : ι) → E i) → G')
            (update (β := E) m i (c • x)),
        map_add' := ⋯, map_smul' := ⋯ }
      (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i (c • x) i_1‖) ⋯ =
    HSMul.hSMul (β := G →L[𝕜] G') c
      (LinearMap.mkContinuous
        {
          toFun := fun (x_1 : G) ↦
            (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_1 : ContinuousMultilinearMap 𝕜 E G') :
                (a : (i : ι) → E i) → G')
              (update (β := E) m i x),
          map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' }
        (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯)

Tactic:
ext1
-- 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 →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
inst_11 : DecidableEq ι
m : (i : ι) → E i
i : ι
c : 𝕜
x : E i
x_1 : G
⊢ Eq.{wG' + 1} (α := G')
    ((LinearMap.mkContinuous
            {
              toFun := fun (x_2 : G) ↦
                (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_2 : ContinuousMultilinearMap 𝕜 E G') :
                    (a : (i : ι) → E i) → G')
                  (update (β := E) m i (c • x)),
              map_add' := ⋯, map_smul' := ⋯ }
            (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i (c • x) i_1‖) ⋯ :
          (a : G) → G')
        x_1 :
      G')
    ((HSMul.hSMul (β := G →L[𝕜] G') c
            (LinearMap.mkContinuous
              {
                toFun := fun (x_2 : G) ↦
                  (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x_2 : ContinuousMultilinearMap 𝕜 E G') :
                      (a : (i : ι) → E i) → G')
                    (update (β := E) m i x),
                map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' }
              (‖f‖ * ∏ i_1 : ι, ‖update (β := E) m i x i_1‖) ⋯) :
          (a : G) → G')
        x_1 :
      G')

Tactic:
simp only [coe_smul', ContinuousMultilinearMap.map_update_smul, LinearMap.coe_mk,
          LinearMap.mkContinuous_apply, Pi.smul_apply, AddHom.coe_mk]

Premises used: LinearMap.coe_mk, LinearMap.mkContinuous_apply, ContinuousLinearMap.coe_smul', ContinuousMultilinearMap.map_update_smul, AddHom.coe_mk, Pi.smul_apply
-- 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 →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
⊢ 0 ≤ ‖f‖ * ∏ i : ι, ‖m i‖

Tactic:
positivity
-- 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 →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
m : (i : ι) → E i
⊢ norm (E := G →L[𝕜] G')
      (LinearMap.mkContinuous
        {
          toFun := fun (x : G) ↦
            (((f : (a : G) → ContinuousMultilinearMap 𝕜 E G') x : ContinuousMultilinearMap 𝕜 E G') :
                (a : (i : ι) → E i) → G')
              m,
          map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] G' }
        (‖f‖ * ∏ i : ι, ‖m i‖) ⋯) ≤
    ‖f‖ * ∏ i : ι, ‖m i‖

Tactic:
exact LinearMap.mkContinuous_norm_le _ (by positivity) _

Premises used: LinearMap.mkContinuous_norm_le
-- 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
⊢ ∀ [inst : DecidableEq ι] (m : (i : ι) → E i) (i : ι) (x_1 y : E i),
    (((f : (a : (i : ι) → E i) → G →L[𝕜] G') (update (β := E) m i (x_1 + y)) : G →L[𝕜] G') : (a : G) → G') x =
      HAdd.hAdd (α := G') (β := G')
        ((((f : (a : (i : ι) → E i) → G →L[𝕜] G') (update (β := E) m i x_1) : G →L[𝕜] G') : (a : G) → G') x : G')
        ((((f : (a : (i : ι) → E i) → G →L[𝕜] G') (update (β := E) m i y) : G →L[𝕜] G') : (a : G) → G') x : 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 ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
⊢ ∀ [inst : DecidableEq ι] (m : (i : ι) → E i) (i : ι) (c : 𝕜) (x_1 : E i),
    (((f : (a : (i : ι) → E i) → G →L[𝕜] G') (update (β := E) m i (c • x_1)) : G →L[𝕜] G') : (a : G) → G') x =
      HSMul.hSMul (β := G') c
        ((((f : (a : (i : ι) → E i) → G →L[𝕜] G') (update (β := E) m i x_1) : G →L[𝕜] G') : (a : G) → G') x : 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 ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x y : G
H :
  ∀ (x_1 : (i : ι) → E i),
    Eq.{wG' + 1} (α := G')
      ((MultilinearMap.mk (M₁ := E)
              (fun (m : (i : ι) → E i) ↦
                (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') (x + y))
              ⋯ ⋯ :
            (a : (i : ι) → E i) → G')
          x_1 :
        G')
      ((HAdd.hAdd (α := MultilinearMap 𝕜 E G')
              (MultilinearMap.mk (M₁ := E)
                (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x) ⋯
                ⋯)
              (MultilinearMap.mk (M₁ := E)
                (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') y) ⋯
                ⋯) :
            (a : (i : ι) → E i) → G')
          x_1 :
        G')
⊢ MultilinearMap.mk (M₁ := E)
      (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') (x + y)) ⋯ ⋯ =
    HAdd.hAdd (α := MultilinearMap 𝕜 E G')
      (MultilinearMap.mk (M₁ := E)
        (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x) ⋯ ⋯)
      (MultilinearMap.mk (M₁ := E)
        (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') y) ⋯ ⋯)

Tactic:
ext1
-- 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 y : G
x_1 : (i : ι) → E i
⊢ Eq.{wG' + 1} (α := G')
    ((MultilinearMap.mk (M₁ := E)
            (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') (x + y))
            ⋯ ⋯ :
          (a : (i : ι) → E i) → G')
        x_1 :
      G')
    ((HAdd.hAdd (α := MultilinearMap 𝕜 E G')
            (MultilinearMap.mk (M₁ := E)
              (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x) ⋯
              ⋯)
            (MultilinearMap.mk (M₁ := E)
              (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') y) ⋯
              ⋯) :
          (a : (i : ι) → E i) → 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 ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
c : 𝕜
x : G
H :
  ∀ (x_1 : (i : ι) → E i),
    Eq.{wG' + 1} (α := G')
      ((MultilinearMap.mk (M₁ := E)
              (fun (m : (i : ι) → E i) ↦
                (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') (c • x))
              ⋯ ⋯ :
            (a : (i : ι) → E i) → G')
          x_1 :
        G')
      ((HSMul.hSMul (α := 𝕜) (β := MultilinearMap 𝕜 E G') ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
              (MultilinearMap.mk (M₁ := E)
                (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x) ⋯
                ⋯) :
            (a : (i : ι) → E i) → G')
          x_1 :
        G')
⊢ MultilinearMap.mk (M₁ := E)
      (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') (c • x)) ⋯ ⋯ =
    HSMul.hSMul (α := 𝕜) (β := MultilinearMap 𝕜 E G') ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (MultilinearMap.mk (M₁ := E)
        (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x) ⋯ ⋯)

Tactic:
ext1
-- 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')
c : 𝕜
x : G
x_1 : (i : ι) → E i
⊢ Eq.{wG' + 1} (α := G')
    ((MultilinearMap.mk (M₁ := E)
            (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') (c • x))
            ⋯ ⋯ :
          (a : (i : ι) → E i) → G')
        x_1 :
      G')
    ((HSMul.hSMul (α := 𝕜) (β := MultilinearMap 𝕜 E G') ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            (MultilinearMap.mk (M₁ := E)
              (fun (m : (i : ι) → E i) ↦ (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x) ⋯
              ⋯) :
          (a : (i : ι) → E i) → 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 ι
f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')
x : G
m : (i : ι) → E i
rw :
  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‖
⊢ norm.{wG'} (E := G')
      (((({
                    toFun := fun (x : G) ↦
                      MultilinearMap.mk (M₁ := E)
                        (fun (m : (i : ι) → E i) ↦
                          (((f : (a : (i : ι) → E i) → G →L[𝕜] G') m : G →L[𝕜] G') : (a : G) → G') x)
                        ⋯ ⋯,
                    map_add' := ⋯, map_smul' := ⋯ : G →ₗ[𝕜] MultilinearMap 𝕜 E G' } :
                  (a : G) → MultilinearMap 𝕜 E G')
                x :
              MultilinearMap 𝕜 E G') :
            (a : (i : ι) → E i) → G')
          m :
        G') ≤
    ‖f‖ * ‖x‖ * ∏ i : ι, ‖m i‖

Tactic:
rw [LinearMap.coe_mk, AddHom.coe_mk, MultilinearMap.coe_mk, mul_right_comm]

Premises used: LinearMap.coe_mk, MultilinearMap.coe_mk, mul_right_comm, AddHom.coe_mk