awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G
h :
  ∀ (m : Ei 0) (x : (i : Fin n) → Ei i.succ),
    Eq.{wG + 1} (α := G)
      ((((f.uncurryLeft (Ei := Ei).curryLeft (Ei := Ei) :
                  (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G)
                m :
              ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
            (a : (i : Fin n) → Ei i.succ) → G)
          x :
        G)
      ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
              ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
            (a : (i : Fin n) → Ei i.succ) → G)
          x :
        G)
⊢ f.uncurryLeft (Ei := Ei).curryLeft (Ei := Ei) = f

Tactic:
ext m x
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
⊢ f.curryLeft (Ei := Ei).uncurryLeft (Ei := Ei) = f

Tactic:
ContinuousMultilinearMap.toMultilinearMap_injective <| f.toMultilinearMap.uncurry_curryLeft

Premises used: MultilinearMap.uncurry_curryLeft, ContinuousMultilinearMap.toMultilinearMap, ContinuousMultilinearMap.toMultilinearMap_injective
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
⊢ ‖f.curryLeft (Ei := Ei)‖ ≤ ‖f‖

Tactic:
MultilinearMap.mkContinuousLinear_norm_le _ (norm_nonneg f) _

Premises used: MultilinearMap.mkContinuousLinear_norm_le, ContinuousMultilinearMap.curryLeft, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
⊢ ‖f.curryLeft (Ei := Ei)‖ ≤ ‖f‖

Tactic:
exact MultilinearMap.mkContinuousLinear_norm_le _ (norm_nonneg f) _

Premises used: MultilinearMap.mkContinuousLinear_norm_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : Ei 0 →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G
⊢ ‖f.uncurryLeft (Ei := Ei)‖ ≤ ‖f‖

Tactic:
MultilinearMap.mkContinuous_norm_le _ (norm_nonneg f) _

Premises used: ContinuousLinearMap.uncurryLeft, MultilinearMap.mkContinuous_norm_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : Ei 0 →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G
⊢ ‖f.uncurryLeft (Ei := Ei)‖ ≤ ‖f‖

Tactic:
exact MultilinearMap.mkContinuous_norm_le _ (norm_nonneg f) _

Premises used: MultilinearMap.mkContinuous_norm_le, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
x : Ei 0
v : (i : Fin n) → Ei i.succ
⊢ Eq.{wG + 1} (α := G)
    ((((((continuousMultilinearCurryLeftEquiv 𝕜 Ei G :
                      (a : ContinuousMultilinearMap 𝕜 Ei G) →
                        Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G)
                    f :
                  Ei 0 →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
                (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G)
              x :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        v :
      G)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) (Fin.cons (α := Ei) x v) : G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G
v : (i : Fin n.succ) → Ei i
⊢ Eq.{wG + 1} (α := G)
    ((((LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 Ei G) :
                (a : Ei 0 →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) →
                  ContinuousMultilinearMap 𝕜 Ei G)
              f :
            ContinuousMultilinearMap 𝕜 Ei G) :
          (a : (i : Fin n.succ) → Ei i) → G)
        v :
      G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) (v 0) :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        (tail (α := Ei) v) :
      G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
⊢ ‖f.curryLeft (Ei := Ei)‖ = ‖f‖

Tactic:
(continuousMultilinearCurryLeftEquiv 𝕜 Ei G).norm_map f

Premises used: LinearIsometryEquiv.norm_map, ContinuousMultilinearMap.curryLeft, continuousMultilinearCurryLeftEquiv, MultilinearMap.mkContinuousLinear, LinearMap.mkContinuous
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G
⊢ ‖f.uncurryLeft (Ei := Ei)‖ = ‖f‖

Tactic:
(continuousMultilinearCurryLeftEquiv 𝕜 Ei G).symm.norm_map f

Premises used: ContinuousLinearMap.uncurryLeft, LinearIsometryEquiv.symm, LinearIsometryEquiv.norm_map, MultilinearMap.mkContinuous, continuousMultilinearCurryLeftEquiv
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f :
  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
    (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
m : (i : Fin n.succ) → Ei i
⊢ Eq.{wG + 1} (α := G) ((f.uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) m : G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) m) :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        (m (last n)) :
      G)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
inst_11 : DecidableEq (Fin n)
m : (i : Fin n) → Ei i.castSucc
i : Fin n
x y : Ei i.castSucc
h :
  ∀ (x_1 : Ei (last n)),
    Eq.{wG + 1} (α := G)
      ((LinearMap.mkContinuous
              ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                  (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
                (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (x + y)))
              (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (x + y) i_1‖) ⋯ :
            (a : Ei (last n)) → G)
          x_1 :
        G)
      ((HAdd.hAdd (α := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
              (LinearMap.mkContinuous
                ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                    (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
                  (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x))
                (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x i_1‖) ⋯)
              (LinearMap.mkContinuous
                ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                    (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
                  (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i y))
                (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i y i_1‖) ⋯) :
            (a : Ei (last n)) → G)
          x_1 :
        G)
⊢ LinearMap.mkContinuous
      ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
        (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (x + y)))
      (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (x + y) i_1‖) ⋯ =
    HAdd.hAdd (α := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
      (LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x))
        (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x i_1‖) ⋯)
      (LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i y))
        (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i y i_1‖) ⋯)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
inst_11 : DecidableEq (Fin n)
m : (i : Fin n) → Ei i.castSucc
i : Fin n
x y : Ei i.castSucc
x_1 : Ei (last n)
⊢ Eq.{wG + 1} (α := G)
    ((LinearMap.mkContinuous
            ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
              (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (x + y)))
            (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (x + y) i_1‖) ⋯ :
          (a : Ei (last n)) → G)
        x_1 :
      G)
    ((HAdd.hAdd (α := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
            (LinearMap.mkContinuous
              ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                  (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
                (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x))
              (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x i_1‖) ⋯)
            (LinearMap.mkContinuous
              ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                  (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
                (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i y))
              (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i y i_1‖) ⋯) :
          (a : Ei (last n)) → G)
        x_1 :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
inst_11 : DecidableEq (Fin n)
m : (i : Fin n) → Ei i.castSucc
i : Fin n
c : 𝕜
x : Ei i.castSucc
h :
  ∀ (x_1 : Ei (last n)),
    Eq.{wG + 1} (α := G)
      ((LinearMap.mkContinuous
              ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                  (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
                (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (c • x)))
              (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (c • x) i_1‖) ⋯ :
            (a : Ei (last n)) → G)
          x_1 :
        G)
      ((HSMul.hSMul (β := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) c
              (LinearMap.mkContinuous
                ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                    (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
                  (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x))
                (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x i_1‖) ⋯) :
            (a : Ei (last n)) → G)
          x_1 :
        G)
⊢ LinearMap.mkContinuous
      ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
        (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (c • x)))
      (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (c • x) i_1‖) ⋯ =
    HSMul.hSMul (β := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) c
      (LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x))
        (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x i_1‖) ⋯)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
inst_11 : DecidableEq (Fin n)
m : (i : Fin n) → Ei i.castSucc
i : Fin n
c : 𝕜
x : Ei i.castSucc
x_1 : Ei (last n)
⊢ Eq.{wG + 1} (α := G)
    ((LinearMap.mkContinuous
            ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
              (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (c • x)))
            (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i (c • x) i_1‖) ⋯ :
          (a : Ei (last n)) → G)
        x_1 :
      G)
    ((HSMul.hSMul (β := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) c
            (LinearMap.mkContinuous
              ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) :
                  (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
                (update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x))
              (‖f‖ * ∏ i_1 : Fin n, ‖update (β := fun (i : Fin n) ↦ Ei i.castSucc) m i x i_1‖) ⋯) :
          (a : Ei (last n)) → G)
        x_1 :
      G)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
f' : MultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
  (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :=
  MultilinearMap.mk (M₁ := fun (i : Fin n) ↦ Ei i.castSucc)
    (fun (m : (i : Fin n) → Ei i.castSucc) ↦
      LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          m)
        (‖f‖ * ∏ i : Fin n, ‖m i‖) ⋯)
    ⋯ ⋯
m : (i : Fin n) → Ei i.castSucc
simp :
  norm (E := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
      (LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          m)
        (‖f‖ * ∏ i : Fin n, ‖m i‖) ⋯) ≤
    ‖f‖ * ∏ i : Fin n, ‖m i‖
⊢ norm (E := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
      ((f' : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
        ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) ≤
    ‖f‖ * ∏ i : Fin n, ‖m i‖

Tactic:
simp only [f', MultilinearMap.coe_mk]

Premises used: MultilinearMap.coe_mk
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
f' : MultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
  (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :=
  MultilinearMap.mk (M₁ := fun (i : Fin n) ↦ Ei i.castSucc)
    (fun (m : (i : Fin n) → Ei i.castSucc) ↦
      LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          m)
        (‖f‖ * ∏ i : Fin n, ‖m i‖) ⋯)
    ⋯ ⋯
m : (i : Fin n) → Ei i.castSucc
⊢ 0 ≤ ‖f‖ * ∏ i : Fin n, ‖m i‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 Ei G
f' : MultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
  (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :=
  MultilinearMap.mk (M₁ := fun (i : Fin n) ↦ Ei i.castSucc)
    (fun (m : (i : Fin n) → Ei i.castSucc) ↦
      LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          m)
        (‖f‖ * ∏ i : Fin n, ‖m i‖) ⋯)
    ⋯ ⋯
m : (i : Fin n) → Ei i.castSucc
⊢ norm (E := ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
      (LinearMap.mkContinuous
        ((f.toMultilinearMap (M₁ := Ei).curryRight (M := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →ₗ[𝕜] G)
          m)
        (‖f‖ * ∏ i : Fin n, ‖m i‖) ⋯) ≤
    ‖f‖ * ∏ i : Fin n, ‖m i‖

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

Premises used: LinearMap.mkContinuous_norm_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
⊢ Eq.{wG + 1} (α := G)
    ((((f.curryRight (Ei := Ei) : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) m :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      G)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) (snoc (α := Ei) m x) : G)

Tactic:
rfl

Premises used: rfl