awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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
⊢ curryMid (Ei := Ei) p (uncurryMid (Ei := Ei) p f) = f
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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
⊢ uncurry0 𝕜 G ((f : (a : (i : Fin 0) → G) → G') x) = f
have 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')
Tactic: ext m
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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
⊢ norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') x : G') = ‖f‖
have obtain : norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') 0 : G') = ‖f‖
Tactic: obtain rfl : x = 0 := Subsingleton.elim _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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‖
have refine : ‖f‖ ≤ norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') 0 : G')
Tactic: refine le_antisymm (by simpa using f.le_opNorm 0) ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (hypothesis)
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‖ ≤ norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') 0 : G')
have this : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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
⊢ enorm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') x : G') = ‖f‖ₑ
have simp_rw : ENNReal.ofReal (norm.{wG'} (E := G') ((f : (a : (i : Fin 0) → G) → G') x : G')) = ENNReal.ofReal ‖f‖
Tactic: simp_rw [← ofReal_norm, fin0_apply_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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'
⊢ (f + g).currySum = f.currySum + g.currySum
have 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')
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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'
⊢ (c • f).currySum = HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) f.currySum
have 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')
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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'
⊢ f.currySum.uncurrySum = f
have H : ∀ (m : (i : ι ⊕ ι') → G),
  Eq.{wG' + 1} (α := G') ((f.currySum.uncurrySum : (a : (i : ι ⊕ ι') → G) → G') m : G')
    ((f : (a : (i : ι ⊕ ι') → G) → G') m : G')
Tactic: ext m
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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')
have 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')
Tactic: refine (curryFinFinset_symm_apply_piecewise_const hk hl _ _ _).symm.trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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')
    ((((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')
have 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')
Tactic: rw [LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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)
⊢ (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)
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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 : ι
⊢ (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
have 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
Tactic: rcases eq_or_ne i j with rfl | hij
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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
⊢ (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
have 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
Tactic: rcases eq_or_ne i j with rfl | hij
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (hypothesis)
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 : ι
⊢ ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (x + y) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (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 (some j) x none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x (some i)).2 i :
        F)
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) y none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) y (some i)).2 i :
        F)
have B₁ : ∀ (z : G × ((i : ι) → E 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: have B z : (fun i ↦ (Function.update v (some j) z (some i)).2 i) =
            Function.update (fun (i : ι) ↦ (v i).2 i) j (z.2 j) := by
          ext i
          rcases eq_or_ne i j with rfl | hij
          · simp
          · simp [hij]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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 : ι
⊢ ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (x + y) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (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 (some j) x none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) x (some i)).2 i :
        F)
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) y none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) y (some i)).2 i :
        F)
have have : ∀ (z : G × ((i : ι) → E 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: classical
        have B z : (fun i ↦ (Function.update v (some j) z (some i)).2 i) =
            Function.update (fun (i : ι) ↦ (v i).2 i) j (z.2 j) := by
          ext i
          rcases eq_or_ne i j with rfl | hij
          · simp
          · simp [hij]
        simp [B]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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 ι
c : 𝕜
x : G × ((i : ι) → E i)
j : ι
z : G × ((i : ι) → E 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)
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Curry (goal)
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 ι
c : 𝕜
x : G × ((i : ι) → E i)
j : ι
z : G × ((i : ι) → E i)
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
have 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
Tactic: rcases eq_or_ne i j with rfl | hij
Cleared hypotheses: j