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'
c : 𝕜
f : ContinuousMultilinearMap 𝕜 (fun (x : ι ⊕ ι') ↦ G) G'
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')

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

Tactic:
ext m
-- 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
⊢ Eq.{wG' + 1} (α := G') ((f.currySum.uncurrySum : (a : (i : ι ⊕ ι') → G) → G') m : G')
    ((f : (a : (i : ι ⊕ ι') → G) → G') m : G')

Tactic:
congr_arg f (Sum.elim_comp_inl_inr m)

Premises used: congr_arg, Sum.elim_comp_inl_inr, DFunLike.coe
-- 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
⊢ Eq.{wG' + 1} (α := G') ((f.currySum.uncurrySum : (a : (i : ι ⊕ ι') → G) → G') m : G')
    ((f : (a : (i : ι ⊕ ι') → G) → G') m : G')

Tactic:
exact congr_arg f (Sum.elim_comp_inl_inr m)

Premises used: congr_arg, Sum.elim_comp_inl_inr, DFunLike.coe
-- 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')
⊢ ‖f.uncurrySum‖ ≤ ‖f‖

Tactic:
MultilinearMap.mkContinuous_norm_le _ (norm_nonneg f) _

Premises used: ContinuousMultilinearMap.uncurrySum, 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 (x : ι) ↦ G) (ContinuousMultilinearMap.{u, v', wG, wG'} 𝕜 (fun (x : ι') ↦ G) G')
⊢ ‖f.uncurrySum‖ ≤ ‖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 : ℕ
G : Type wG
G' : Type wG'
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace 𝕜 G
inst_3 : NormedAddCommGroup G'
inst_4 : NormedSpace 𝕜 G'
k l : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G'
mk : Fin k → G
ml : Fin l → G
⊢ Eq.{wG' + 1} (α := G')
    ((((((curryFinFinset 𝕜 G G' hk hl :
                      (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) G') →
                        ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                          (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G'))
                    f :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                    (ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin l) ↦ G) G')) :
                (a : (i : Fin k) → G) → ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G')
              mk :
            ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin l) ↦ G) G') :
          (a : (i : Fin l) → G) → G')
        ml :
      G')
    ((f : (a : (i : Fin n) → G) → G') fun (i : Fin n) ↦
        Sum.elim mk ml (((finSumEquivOfFinset hk hl).symm : (a : Fin n) → Fin k ⊕ Fin l) i) :
      G')

Tactic:
rfl

Premises used: rfl, Sum.elim
-- 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'
k l : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f :
  ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G) (ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin l) ↦ G) G')
m : Fin n → G
⊢ Eq.{wG' + 1} (α := G')
    ((((LinearIsometryEquiv.symm (curryFinFinset 𝕜 G G' hk hl) :
                (a :
                    ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                      (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G')) →
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) G')
              f :
            ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G') :
          (a : (i : Fin n) → G) → G')
        m :
      G')
    (((f : (a : (i : Fin k) → G) → ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G') fun (i : Fin k) ↦
            m ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inl i)) :
          (a : (i : Fin l) → G) → G')
        fun (i : Fin l) ↦ m ((finSumEquivOfFinset hk hl : (a : Fin k ⊕ Fin l) → Fin n) (Sum.inr i)) :
      G')

Tactic:
rfl

Premises used: rfl, Sum.elim
-- 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'
k l : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f :
  ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G) (ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin l) ↦ G) G')
x y : G
⊢ Eq.{wG' + 1} (α := G')
    ((((LinearIsometryEquiv.symm (curryFinFinset 𝕜 G G' hk hl) :
                (a :
                    ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                      (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G')) →
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) G')
              f :
            ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G') :
          (a : (i : Fin n) → G) → G')
        (s.piecewise (π := fun (i : Fin n) ↦ G) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      G')
    (((f : (a : (i : Fin k) → G) → ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G') fun (x_1 : Fin k) ↦ x :
          (a : (i : Fin l) → G) → G')
        fun (x : Fin l) ↦ y :
      G')

Tactic:
MultilinearMap.curryFinFinset_symm_apply_piecewise_const hk hl _ x y

Premises used: MultilinearMap.curryFinFinset_symm_apply_piecewise_const
-- 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'
k l : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f :
  ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G) (ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin l) ↦ G) G')
x : G
⊢ Eq.{wG' + 1} (α := G')
    ((((LinearIsometryEquiv.symm (curryFinFinset 𝕜 G G' hk hl) :
                (a :
                    ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                      (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G')) →
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) G')
              f :
            ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G') :
          (a : (i : Fin n) → G) → G')
        fun (x_1 : Fin n) ↦ x :
      G')
    (((f : (a : (i : Fin k) → G) → ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G') fun (x_1 : Fin k) ↦ x :
          (a : (i : Fin l) → G) → G')
        fun (x_1 : Fin l) ↦ 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'
k l : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G'
x y : G
⊢ Eq.{wG' + 1} (α := G')
    (((((curryFinFinset 𝕜 G G' hk hl :
                    (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) G') →
                      ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                        (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G'))
                  f :
                ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                  (ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin l) ↦ G) G')) :
              (a : (i : Fin k) → G) → ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G')
            fun (x_1 : Fin k) ↦ x :
          (a : (i : Fin l) → G) → G')
        fun (x : Fin l) ↦ y :
      G')
    ((f : (a : (i : Fin n) → G) → G')
        (s.piecewise (π := fun (i : Fin n) ↦ G) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      G')

Tactic:
(curryFinFinset_symm_apply_piecewise_const hk hl _ _ _).symm.trans ?_

Premises used: ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const, Eq.symm, Eq.trans
-- 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'
k l : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G'
x y : G
refine :
  Eq.{wG' + 1} (α := G')
    ((((LinearIsometryEquiv.symm (curryFinFinset 𝕜 G G' hk hl) :
                (a :
                    ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                      (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G')) →
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) G')
              ((curryFinFinset 𝕜 G G' hk hl :
                  (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) G') →
                    ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                      (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G'))
                f) :
            ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G') :
          (a : (i : Fin n) → G) → G')
        (s.piecewise (π := fun (i : Fin n) ↦ G) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      G')
    ((f : (a : (i : Fin n) → G) → G')
        (s.piecewise (π := fun (i : Fin n) ↦ G) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      G')
⊢ Eq.{wG' + 1} (α := G')
    (((((curryFinFinset 𝕜 G G' hk hl :
                    (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) G') →
                      ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                        (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G'))
                  f :
                ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                  (ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin l) ↦ G) G')) :
              (a : (i : Fin k) → G) → ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G')
            fun (x_1 : Fin k) ↦ x :
          (a : (i : Fin l) → G) → G')
        fun (x : Fin l) ↦ y :
      G')
    ((f : (a : (i : Fin n) → G) → G')
        (s.piecewise (π := fun (i : Fin n) ↦ G) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      G')

Tactic:
refine (curryFinFinset_symm_apply_piecewise_const hk hl _ _ _).symm.trans ?_

Premises used: ContinuousMultilinearMap.curryFinFinset_symm_apply_piecewise_const, Eq.symm, Eq.trans
-- 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'
k l : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G'
x y : G
rw rw₁ :
  Eq.{wG' + 1} (α := G')
    ((f : (a : (i : Fin n) → G) → G')
        (s.piecewise (π := fun (i : Fin n) ↦ G) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      G')
    ((f : (a : (i : Fin n) → G) → G')
        (s.piecewise (π := fun (i : Fin n) ↦ G) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      G')
⊢ Eq.{wG' + 1} (α := G')
    ((((LinearIsometryEquiv.symm (curryFinFinset 𝕜 G G' hk hl) :
                (a :
                    ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                      (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G')) →
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) G')
              ((curryFinFinset 𝕜 G G' hk hl :
                  (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ G) G') →
                    ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ G)
                      (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ G) G'))
                f) :
            ContinuousMultilinearMap.{u, 0, wG, wG'} 𝕜 (fun (i : Fin n) ↦ G) G') :
          (a : (i : Fin n) → G) → G')
        (s.piecewise (π := fun (i : Fin n) ↦ G) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      G')
    ((f : (a : (i : Fin n) → G) → G')
        (s.piecewise (π := fun (i : Fin n) ↦ G) (fun (x_1 : Fin n) ↦ x) fun (x : Fin n) ↦ y) :
      G')

Tactic:
rw [LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_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_1 : Type wG
G' : Type wG'
inst_1 : Fintype ι
inst_2 : Fintype ι'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : (i : ι) → NormedAddCommGroup (E i)
inst_5 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_6 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_7 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_8 : NormedAddCommGroup G_1
inst_9 : NormedSpace 𝕜 G_1
inst_10 : NormedAddCommGroup G'
inst_11 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace 𝕜 F
inst_14 : NormedAddCommGroup G
inst_15 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : (i : Option ι) → G × ((i : ι) → E i)
j : Option ι
x y : G × ((i : ι) → E i)
⊢ ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v none (x + y) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v none (x + y) (some i)).2 i) =
    HAdd.hAdd (α := F) (β := F)
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v none x none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v none x (some i)).2 i :
        F)
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v none y none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v none y (some i)).2 i :
        F)

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_1 : Type wG
G' : Type wG'
inst_1 : Fintype ι
inst_2 : Fintype ι'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : (i : ι) → NormedAddCommGroup (E i)
inst_5 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_6 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_7 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_8 : NormedAddCommGroup G_1
inst_9 : NormedSpace 𝕜 G_1
inst_10 : NormedAddCommGroup G'
inst_11 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace 𝕜 F
inst_14 : NormedAddCommGroup G
inst_15 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : (i : Option ι) → G × ((i : ι) → E i)
j_1 : Option ι
x y : G × ((i : ι) → E i)
j : ι
z : G × ((i : ι) → E i)
h :
  ∀ (i : ι),
    (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i =
      update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j) i
⊢ (fun (i : ι) ↦ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i) =
    update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j)

Tactic:
ext i
-- 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_1 : Type wG
G' : Type wG'
inst_1 : Fintype ι
inst_2 : Fintype ι'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : (i : ι) → NormedAddCommGroup (E i)
inst_5 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_6 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_7 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_8 : NormedAddCommGroup G_1
inst_9 : NormedSpace 𝕜 G_1
inst_10 : NormedAddCommGroup G'
inst_11 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace 𝕜 F
inst_14 : NormedAddCommGroup G
inst_15 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : (i : Option ι) → G × ((i : ι) → E i)
j_1 : Option ι
x y : G × ((i : ι) → E i)
j : ι
z : G × ((i : ι) → E i)
i : ι
h :
  (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some i) z (some i)).2 i =
    update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) i (z.2 i) i
h₁ :
  ∀ (hij : i ≠ j),
    (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i =
      update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j) i
⊢ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i =
    update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j) i

Tactic:
rcases eq_or_ne i j with rfl | hij

Premises used: eq_or_ne, 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_1 : Type wG
G' : Type wG'
inst_1 : Fintype ι
inst_2 : Fintype ι'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : (i : ι) → NormedAddCommGroup (E i)
inst_5 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_6 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_7 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_8 : NormedAddCommGroup G_1
inst_9 : NormedSpace 𝕜 G_1
inst_10 : NormedAddCommGroup G'
inst_11 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace 𝕜 F
inst_14 : NormedAddCommGroup G
inst_15 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : (i : Option ι) → G × ((i : ι) → E i)
j : Option ι
x y z : G × ((i : ι) → E i)
i : ι
⊢ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some i) z (some i)).2 i =
    update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) i (z.2 i) i

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_1 : Type wG
G' : Type wG'
inst_1 : Fintype ι
inst_2 : Fintype ι'
inst_3 : NontriviallyNormedField 𝕜
inst_4 : (i : ι) → NormedAddCommGroup (E i)
inst_5 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_6 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_7 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_8 : NormedAddCommGroup G_1
inst_9 : NormedSpace 𝕜 G_1
inst_10 : NormedAddCommGroup G'
inst_11 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_12 : NormedAddCommGroup F
inst_13 : NormedSpace 𝕜 F
inst_14 : NormedAddCommGroup G
inst_15 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
inst : DecidableEq (Option ι)
v : (i : Option ι) → G × ((i : ι) → E i)
j_1 : Option ι
x y : G × ((i : ι) → E i)
j : ι
z : G × ((i : ι) → E i)
i : ι
hij : i ≠ j
⊢ (update (β := fun (a : Option ι) ↦ G × ((i : ι) → E i)) v (some j) z (some i)).2 i =
    update (β := E) (fun (i : ι) ↦ (v (some i)).2 i) j (z.2 j) i

Tactic:
simp [hij]