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 :
  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
    (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
H :
  ∀ (m : (i : Fin n) → Ei i.castSucc) (x : Ei (last n)),
    Eq.{wG + 1} (α := G)
      ((((f.uncurryRight (Ei := Ei).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) → 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.uncurryRight (Ei := Ei).curryRight (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 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
    (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
m : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
H :
  Eq.{wG + 1} (α := G) ((f.uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) (snoc (α := Ei) m x) : 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) :
          (a : Ei (last n)) → G)
        x :
      G)
H₁ :
  Eq.{wG + 1} (α := G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) (snoc (α := Ei) m x)) :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        (snoc (α := Ei) m x (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) :
          (a : Ei (last n)) → G)
        x :
      G)
H₂ :
  Eq.{wG + 1} (α := G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) (snoc (α := Ei) m x)) :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        x :
      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) :
          (a : Ei (last n)) → G)
        x :
      G)
H₃ H₄ :
  Eq.{wG + 1} (α := 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) :
          (a : Ei (last n)) → G)
        x :
      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) :
          (a : Ei (last n)) → G)
        x :
      G)
⊢ Eq.{wG + 1} (α := G)
    ((((f.uncurryRight (Ei := Ei).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) → 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)

Tactic:
rw [ContinuousMultilinearMap.curryRight_apply, ContinuousMultilinearMap.uncurryRight_apply,
    snoc_last, init_snoc]

Premises used: ContinuousMultilinearMap.uncurryRight_apply, ContinuousMultilinearMap.curryRight_apply, Fin.init_snoc, Fin.snoc_last
-- 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
H :
  ∀ (m : (i : Fin n.succ) → Ei i),
    Eq.{wG + 1} (α := G) ((f.curryRight (Ei := Ei).uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) m : G)
      ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)
⊢ f.curryRight (Ei := Ei).uncurryRight (Ei := Ei) = f

Tactic:
ext m
-- 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.succ) → Ei i
H :
  Eq.{wG + 1} (α := G)
    ((((f.curryRight (Ei := Ei) : (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)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)
H₁ :
  Eq.{wG + 1} (α := G) ((f : (a : (i : Fin n.succ) → Ei i) → G) (snoc (α := Ei) (init (α := Ei) m) (m (last n))) : G)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)
H₂ H₃ :
  Eq.{wG + 1} (α := G) ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G) ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)
⊢ Eq.{wG + 1} (α := G) ((f.curryRight (Ei := Ei).uncurryRight (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) m : G)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) m : G)

Tactic:
rw [uncurryRight_apply, curryRight_apply, snoc_init_self]

Premises used: ContinuousMultilinearMap.uncurryRight_apply, Fin.snoc_init_self, ContinuousMultilinearMap.curryRight_apply
-- 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
⊢ norm (E :=
      ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
        (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G))
      (MultilinearMap.mkContinuous (E := fun (i : Fin n) ↦ Ei i.castSucc)
        (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‖) ⋯)
          ⋯ ⋯)
        ‖f‖ ⋯) ≤
    ‖f‖

Tactic:
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
ι : 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
⊢ norm (E :=
      ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
        (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G))
      (MultilinearMap.mkContinuous (E := fun (i : Fin n) ↦ Ei i.castSucc)
        (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‖) ⋯)
          ⋯ ⋯)
        ‖f‖ ⋯) ≤
    ‖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
ι : 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 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
    (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
⊢ norm (E := ContinuousMultilinearMap 𝕜 Ei G)
      (MultilinearMap.mkContinuous (E := Ei)
        ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin n) ↦ Ei i.castSucc) (ContinuousLinearMap.coeLM 𝕜)
              (f.toMultilinearMap (M₁ := fun (i : Fin n) ↦ Ei i.castSucc))).uncurryRight
          (M := Ei))
        ‖f‖ ⋯) ≤
    ‖f‖

Tactic:
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
ι : 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 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
    (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
⊢ norm (E := ContinuousMultilinearMap 𝕜 Ei G)
      (MultilinearMap.mkContinuous (E := Ei)
        ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin n) ↦ Ei i.castSucc) (ContinuousLinearMap.coeLM 𝕜)
              (f.toMultilinearMap (M₁ := fun (i : Fin n) ↦ Ei i.castSucc))).uncurryRight
          (M := Ei))
        ‖f‖ ⋯) ≤
    ‖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
v : (i : Fin n) → Ei i.castSucc
x : Ei (last n)
⊢ Eq.{wG + 1} (α := G)
    ((((((continuousMultilinearCurryRightEquiv 𝕜 Ei G :
                      (a : ContinuousMultilinearMap 𝕜 Ei G) →
                        ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc) (Ei (last n) →L[𝕜] G))
                    f :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
                    (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)) :
                (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G)
              v :
            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) v x) : 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 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc)
    (ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G)
v : (i : Fin n.succ) → Ei i
⊢ Eq.{wG + 1} (α := G)
    ((((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv 𝕜 Ei G) :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.castSucc) (Ei (last n) →L[𝕜] G)) →
                  ContinuousMultilinearMap 𝕜 Ei G)
              f :
            ContinuousMultilinearMap 𝕜 Ei G) :
          (a : (i : Fin n.succ) → Ei i) → G)
        v :
      G)
    ((((f : (a : (i : Fin n) → Ei i.castSucc) → Ei (last n) →L[𝕜] G) (init (α := Ei) v) :
            ContinuousLinearMap.{u, u, wEi, wG} (RingHom.id 𝕜) (Ei (last n)) G) :
          (a : Ei (last n)) → G)
        (v (last n)) :
      G)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : NormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) (G →L[𝕜] G')
v : Fin (n + 1) → G
⊢ Eq.{wG' + 1} (α := G')
    ((((LinearIsometryEquiv.symm (continuousMultilinearCurryRightEquiv' 𝕜 n G G') :
                (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) (G →L[𝕜] G')) →
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin n.succ) ↦ G) G')
              f :
            ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n.succ) ↦ G) G') :
          (a : (i : Fin n.succ) → G) → G')
        v :
      G')
    ((((f : (a : (i : Fin n) → G) → G →L[𝕜] G') (init (α := fun (i : Fin (n + 1)) ↦ G) v) : G →L[𝕜] G') : (a : G) → G')
        (v (last n)) :
      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.curryRight (Ei := Ei)‖ = ‖f‖

Tactic:
(continuousMultilinearCurryRightEquiv 𝕜 Ei G).norm_map f

Premises used: LinearIsometryEquiv.norm_map, continuousMultilinearCurryRightEquiv, MultilinearMap.mkContinuous, ContinuousMultilinearMap.curryRight
-- 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)
⊢ ‖f.uncurryRight (Ei := Ei)‖ = ‖f‖

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

Premises used: LinearIsometryEquiv.symm, LinearIsometryEquiv.norm_map, continuousMultilinearCurryRightEquiv, MultilinearMap.mkContinuous, ContinuousMultilinearMap.uncurryRight
-- 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'
p : Fin (n + 1)
f : Ei p →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G
m : (i : Fin n.succ) → Ei i
⊢ norm.{wG} (E := G)
      ((LinearMap.uncurryMid (M := Ei) p
              (toMultilinearMapLinear (M₁ := fun (i : Fin n) ↦ Ei (p.succAbove i)) ∘ₗ
                (↑f : Ei p →ₗ[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G)) :
            (a : (i : Fin n.succ) → Ei i) → G)
          m :
        G) ≤
    ‖f‖ * ∏ i : Fin n.succ, ‖m i‖

Tactic:
ContinuousLinearMap.norm_map_removeNth_le f m

Premises used: ContinuousLinearMap.norm_map_removeNth_le
-- 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'
p : Fin (n + 1)
f : Ei p →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G
m : (i : Fin n.succ) → Ei i
⊢ norm.{wG} (E := G)
      ((LinearMap.uncurryMid (M := Ei) p
              (toMultilinearMapLinear (M₁ := fun (i : Fin n) ↦ Ei (p.succAbove i)) ∘ₗ
                (↑f : Ei p →ₗ[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G)) :
            (a : (i : Fin n.succ) → Ei i) → G)
          m :
        G) ≤
    ‖f‖ * ∏ i : Fin n.succ, ‖m i‖

Tactic:
exact ContinuousLinearMap.norm_map_removeNth_le f m

Premises used: ContinuousLinearMap.norm_map_removeNth_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
p : Fin (n + 1)
f : ContinuousMultilinearMap 𝕜 Ei G
x : Ei p
m : (i : Fin n) → Ei (p.succAbove i)
⊢ Eq.{wG + 1} (α := G)
    ((((curryMid (Ei := Ei) p f : (a : Ei p) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G) x :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G) :
          (a : (i : Fin n) → Ei (p.succAbove i)) → G)
        m :
      G)
    ((f : (a : (i : Fin n.succ) → Ei i) → G) (p.insertNth (α := Ei) x m) : 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
p : Fin (n + 1)
f : Ei p →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G
h :
  ∀ (x : Ei p) (x_1 : (i : Fin n) → Ei (p.succAbove i)),
    Eq.{wG + 1} (α := G)
      ((((curryMid (Ei := Ei) p (uncurryMid (Ei := Ei) p f) :
                  (a : Ei p) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G)
                x :
              ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G) :
            (a : (i : Fin n) → Ei (p.succAbove i)) → G)
          x_1 :
        G)
      ((((f : (a : Ei p) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G) x :
              ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G) :
            (a : (i : Fin n) → Ei (p.succAbove i)) → G)
          x_1 :
        G)
⊢ curryMid (Ei := Ei) p (uncurryMid (Ei := Ei) p f) = f

Tactic:
ext
-- 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
p : Fin (n + 1)
f : Ei p →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G
x : Ei p
x_1 : (i : Fin n) → Ei (p.succAbove i)
⊢ Eq.{wG + 1} (α := G)
    ((((curryMid (Ei := Ei) p (uncurryMid (Ei := Ei) p f) :
                (a : Ei p) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G)
              x :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G) :
          (a : (i : Fin n) → Ei (p.succAbove i)) → G)
        x_1 :
      G)
    ((((f : (a : Ei p) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G) x :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G) :
          (a : (i : Fin n) → Ei (p.succAbove i)) → G)
        x_1 :
      G)

Tactic:
simp
-- 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
p : Fin (n + 1)
f : ContinuousMultilinearMap 𝕜 Ei G
⊢ ContinuousLinearMap.uncurryMid (Ei := Ei) p (curryMid (Ei := Ei) p f) = f

Tactic:
ContinuousMultilinearMap.toMultilinearMap_injective <| f.toMultilinearMap.uncurryMid_curryMid p

Premises used: MultilinearMap.uncurryMid_curryMid, 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'
p : Fin (n + 1)
f : ContinuousMultilinearMap 𝕜 Ei G
⊢ ‖curryMid (Ei := Ei) p f‖ ≤ ‖f‖

Tactic:
MultilinearMap.mkContinuousLinear_norm_le _ (norm_nonneg f) _

Premises used: ContinuousMultilinearMap.curryMid, MultilinearMap.mkContinuousLinear_norm_le, norm_nonneg