awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
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'
p : Fin (n + 1)
f : Ei p →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G
⊢ ‖ContinuousLinearMap.uncurryMid (Ei := Ei) p f‖ ≤ ‖f‖

Tactic:
MultilinearMap.mkContinuous_norm_le _ (norm_nonneg f) _

Premises used: MultilinearMap.mkContinuous_norm_le, ContinuousLinearMap.uncurryMid, 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'
p : Fin (n + 1)
f : Ei p →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G
⊢ ‖ContinuousLinearMap.uncurryMid (Ei := Ei) p 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
p : Fin (n + 1)
f : ContinuousMultilinearMap 𝕜 Ei G
⊢ ‖curryMid (Ei := Ei) p f‖ = ‖f‖

Tactic:
(ContinuousMultilinearMap.curryMidEquiv 𝕜 Ei G p).norm_map f

Premises used: ContinuousMultilinearMap.curryMid, LinearIsometryEquiv.norm_map, ContinuousMultilinearMap.curryMidEquiv, 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
p : Fin (n + 1)
f : Ei p →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei (p.succAbove i)) G
⊢ ‖uncurryMid (Ei := Ei) p f‖ = ‖f‖

Tactic:
(ContinuousMultilinearMap.curryMidEquiv 𝕜 Ei G p).symm.norm_map f

Premises used: LinearIsometryEquiv.symm, LinearIsometryEquiv.norm_map, ContinuousMultilinearMap.curryMidEquiv, MultilinearMap.mkContinuous, ContinuousLinearMap.uncurryMid
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : NormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
x : G'
m : Fin 0 → G
⊢ (uncurry0 𝕜 G x : (a : (i : Fin 0) → G) → G') m = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
⊢ f.curry0 = (f : (a : (i : Fin 0) → G) → G') 0

Tactic:
rfl

Premises used: rfl, ContinuousMultilinearMap.curry0
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
x : Fin 0 → G
H :
  ∀ (m : (i : Fin 0) → G),
    Eq.{wG' + 1} (α := G')
      (((uncurry0 𝕜 G ((f : (a : (i : Fin 0) → G) → G') x) :
              ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin 0) ↦ G) G') :
            (a : (i : Fin 0) → G) → G')
          m :
        G')
      ((f : (a : (i : Fin 0) → G) → G') m : G')
⊢ uncurry0 𝕜 G ((f : (a : (i : Fin 0) → G) → G') x) = f

Tactic:
ext m
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
x m : (i : Fin 0) → G
⊢ Eq.{wG' + 1} (α := G')
    (((uncurry0 𝕜 G ((f : (a : (i : Fin 0) → G) → G') x) :
            ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin 0) ↦ G) G') :
          (a : (i : Fin 0) → G) → G')
        m :
      G')
    ((f : (a : (i : Fin 0) → G) → G') m : G')

Tactic:
simp [Subsingleton.elim x m]

Premises used: Subsingleton.elim
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
⊢ uncurry0 𝕜 G f.curry0 = f

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : NormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
x : G'
⊢ curry0 (uncurry0 𝕜 G x) = x

Tactic:
rfl

Premises used: rfl, ContinuousMultilinearMap.curry0
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : NormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
x : G'
⊢ norm (E := ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin 0) ↦ G) G') (uncurry0 𝕜 G x) = ‖x‖

Tactic:
norm_constOfIsEmpty _ _ _

Premises used: ContinuousMultilinearMap.uncurry0, ContinuousMultilinearMap.norm_constOfIsEmpty
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
x : Fin 0 → G
⊢ x = 0

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
x : Fin 0 → G
obtain : norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') 0 : G') = ‖f‖
⊢ norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') x : G') = ‖f‖

Tactic:
obtain rfl : x = 0 := Subsingleton.elim _ _

Premises used: Subsingleton.elim, rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
⊢ norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') 0 : G') ≤ ‖f‖

Tactic:
simpa using f.le_opNorm 0

Premises used: ContinuousMultilinearMap.le_opNorm, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
refine : ‖f‖ ≤ norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') 0 : G')
⊢ norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') 0 : G') = ‖f‖

Tactic:
refine le_antisymm (by simpa using f.le_opNorm 0) ?_

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
m : (i : Fin 0) → G
⊢ norm.{wG'} (E := G') ((uncurry0 𝕜 G f.curry0 : (a : (i : Fin 0) → G) → G') m : G') ≤ ‖f.curry0‖ * ∏ i : Fin 0, ‖m i‖

Tactic:
simp [-ContinuousMultilinearMap.apply_zero_uncurry0]

Premises used: ContinuousMultilinearMap.apply_zero_uncurry0
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
⊢ norm (E := ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin 0) ↦ G) G') (uncurry0 𝕜 G f.curry0) ≤ ‖f.curry0‖

Tactic:
have : ‖ContinuousMultilinearMap.uncurry0 𝕜 G f.curry0‖ ≤ ‖f.curry0‖ :=
    ContinuousMultilinearMap.opNorm_le_bound (norm_nonneg _) fun m => by
      simp [-ContinuousMultilinearMap.apply_zero_uncurry0]
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
this :
  norm (E := ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin 0) ↦ G) G') (uncurry0 𝕜 G f.curry0) ≤ ‖f.curry0‖
⊢ ‖f‖ ≤ norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') 0 : G')

Tactic:
simpa [-Matrix.zero_empty] using this

Premises used: Matrix.zero_empty
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
x : Fin 0 → G
simp_rw : ENNReal.ofReal (norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') x : G')) = ENNReal.ofReal ‖f‖
⊢ enorm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') x : G') = ‖f‖ₑ

Tactic:
simp_rw [← ofReal_norm, fin0_apply_norm]

Premises used: ofReal_norm, ContinuousMultilinearMap.fin0_apply_norm
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
⊢ ‖f.curry0‖ = ‖f‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 0) ↦ G) G'
⊢ Eq.{wG' + 1} (α := G')
    ((continuousMultilinearCurryFin0 𝕜 G G' : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ G) G') → G') f : G')
    ((f : (a : (i : Fin 0) → G) → G') 0 : G')

Tactic:
rfl

Premises used: rfl, ContinuousMultilinearMap.curry0
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : NormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
x : G'
⊢ Eq (α := ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin 0) ↦ G) G')
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 G G') :
          (a : G') → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ G) G')
        x :
      ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin 0) ↦ G) G')
    (uncurry0 𝕜 G x : ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin 0) ↦ G) G')

Tactic:
rfl

Premises used: ContinuousMultilinearMap.constOfIsEmpty, ContinuousMultilinearMap.uncurry0, rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : NormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
x : G'
v : Fin 0 → G
⊢ (((LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 G G') :
              (a : G') → ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ G) G')
            x :
          ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin 0) ↦ G) G') :
        (a : (i : Fin 0) → G) → G')
      v =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 1) ↦ G) G'
x : G
⊢ Eq.{wG' + 1} (α := G')
    ((((continuousMultilinearCurryFin1 𝕜 G G' : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ G) G') → G →L[𝕜] G')
              f :
            G →L[𝕜] G') :
          (a : G) → G')
        x :
      G')
    ((f : (a : (i : Fin 1) → G) → G') (snoc (α := fun (i : Fin 1) ↦ G) 0 x) : G')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
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 : G →L[𝕜] G'
v : Fin 1 → G
⊢ Eq.{wG' + 1} (α := G')
    ((((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 G G') :
                (a : G →L[𝕜] G') → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ G) G')
              f :
            ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin 1) ↦ G) G') :
          (a : (i : Fin 1) → G) → G')
        v :
      G')
    ((f : (a : G) → G') (v 0) : G')

Tactic:
rfl

Premises used: Fin.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
σ : ι ≃ ι'
f : ContinuousMultilinearMap.{u, v, wG, wG'} 𝕜 (fun (x : ι) ↦ G) G'
⊢ ‖domDomCongr σ f‖ = ‖f‖

Tactic:
simp only [norm_def, ← σ.prod_comp,
    (σ.arrowCongr (Equiv.refl G)).surjective.forall, domDomCongr_apply, Equiv.arrowCongr_apply,
    Equiv.coe_refl, comp_apply, Equiv.symm_apply_apply, id]

Premises used: Function.Surjective.forall, Equiv.arrowCongr_apply, Equiv.symm_apply_apply, Equiv.arrowCongr, id, ContinuousMultilinearMap.domDomCongr_apply, Equiv.prod_comp, Equiv.coe_refl, Function.comp_apply, Equiv.surjective, ContinuousMultilinearMap.norm_def, Equiv.refl
-- 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 (x : ι ⊕ ι') ↦ G) G'
m : (i : ι) → G
m' : (i : ι') → G
⊢ norm.{wG'} (E := G')
      ((((f.toMultilinearMap (M₁ := fun (x : ι ⊕ ι') ↦ G).currySum (N := fun (x : ι ⊕ ι') ↦ G) :
                  (a : (i : ι) → G) → MultilinearMap 𝕜 (fun (x : ι') ↦ G) G')
                m :
              MultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G') :
            (a : (i : ι') → G) → G')
          m' :
        G') ≤
    (‖f‖ * ∏ i : ι, ‖m i‖) * ∏ i : ι', ‖m' i‖

Tactic:
simpa [Fintype.prod_sum_type, mul_assoc] using f.le_opNorm (Sum.elim m m')

Premises used: mul_assoc, ContinuousMultilinearMap.le_opNorm, Fintype.prod_sum_type, Sum.elim
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun (x : ι ⊕ ι') ↦ G) G'
m : ι → G
m' : ι' → G
⊢ Eq.{wG' + 1} (α := G')
    ((((f.currySum : (a : (i : ι) → G) → ContinuousMultilinearMap 𝕜 (fun (x : ι') ↦ G) G') m :
            ContinuousMultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G') :
          (a : (i : ι') → G) → G')
        m' :
      G')
    ((f : (a : (i : ι ⊕ ι') → G) → G') (Sum.elim m m') : G')

Tactic:
rfl

Premises used: rfl, Sum.elim
-- 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 (x : ι) ↦ G) (ContinuousMultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G')
m : (i : ι ⊕ ι') → G
⊢ norm.{wG'} (E := G')
      (((LinearMap.compMultilinearMap (M₁ := fun (x : ι) ↦ G) (toMultilinearMapLinear (M₁ := fun (x : ι') ↦ G))
                  (f.toMultilinearMap (M₁ := fun (x : ι) ↦ G))).uncurrySum
              (N := fun (x : ι ⊕ ι') ↦ G) :
            (a : (i : ι ⊕ ι') → G) → G')
          m :
        G') ≤
    ‖f‖ * ∏ i : ι ⊕ ι', ‖m i‖

Tactic:
simpa [Fintype.prod_sum_type, mul_assoc] using
      (f (m ∘ Sum.inl)).le_of_opNorm_le (f.le_opNorm _) (m ∘ Sum.inr)

Premises used: mul_assoc, ContinuousMultilinearMap.le_opNorm, Function.comp, Sum.inr, ContinuousMultilinearMap.le_of_opNorm_le, Fintype.prod_sum_type
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
G : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
inst_5 : NormedAddCommGroup G'
inst_6 : NormedSpace 𝕜 G'
f : ContinuousMultilinearMap 𝕜 (fun (x : ι) ↦ G) (ContinuousMultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G')
m : ι ⊕ ι' → G
⊢ Eq.{wG' + 1} (α := G') ((f.uncurrySum : (a : (i : ι ⊕ ι') → G) → G') m : G')
    ((((f : (a : (i : ι) → G) → ContinuousMultilinearMap 𝕜 (fun (x : ι') ↦ G) G') (m ∘ Sum.inl) :
            ContinuousMultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G') :
          (a : (i : ι') → G) → G')
        (m ∘ Sum.inr) :
      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 g : ContinuousMultilinearMap 𝕜 (fun (x : ι ⊕ ι') ↦ G) G'
H :
  ∀ (x : (i : ι) → G) (x_1 : (i : ι') → G),
    Eq.{wG' + 1} (α := G')
      (((((f + g).currySum : (a : (i : ι) → G) → ContinuousMultilinearMap 𝕜 (fun (x : ι') ↦ G) G') x :
              ContinuousMultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G') :
            (a : (i : ι') → G) → G')
          x_1 :
        G')
      ((((f.currySum + g.currySum : (a : (i : ι) → G) → ContinuousMultilinearMap 𝕜 (fun (x : ι') ↦ G) G') x :
              ContinuousMultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G') :
            (a : (i : ι') → G) → G')
          x_1 :
        G')
⊢ (f + g).currySum = f.currySum + g.currySum

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 g : ContinuousMultilinearMap 𝕜 (fun (x : ι ⊕ ι') ↦ G) G'
x : (i : ι) → G
x_1 : (i : ι') → G
⊢ Eq.{wG' + 1} (α := G')
    (((((f + g).currySum : (a : (i : ι) → G) → ContinuousMultilinearMap 𝕜 (fun (x : ι') ↦ G) G') x :
            ContinuousMultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G') :
          (a : (i : ι') → G) → G')
        x_1 :
      G')
    ((((f.currySum + g.currySum : (a : (i : ι) → G) → ContinuousMultilinearMap 𝕜 (fun (x : ι') ↦ G) G') x :
            ContinuousMultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G') :
          (a : (i : ι') → G) → G')
        x_1 :
      G')

Tactic:
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'
c : 𝕜
f : ContinuousMultilinearMap 𝕜 (fun (x : ι ⊕ ι') ↦ G) G'
H :
  ∀ (x : (i : ι) → G) (x_1 : (i : ι') → G),
    Eq.{wG' + 1} (α := G')
      (((((c • f).currySum : (a : (i : ι) → G) → ContinuousMultilinearMap 𝕜 (fun (x : ι') ↦ G) G') x :
              ContinuousMultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G') :
            (a : (i : ι') → G) → G')
          x_1 :
        G')
      ((((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) f.currySum :
                  (a : (i : ι) → G) → ContinuousMultilinearMap 𝕜 (fun (x : ι') ↦ G) G')
                x :
              ContinuousMultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G') :
            (a : (i : ι') → G) → G')
          x_1 :
        G')
⊢ (c • f).currySum = HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) f.currySum

Tactic:
ext