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_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)

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]
-- 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_1 : 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 :
  ∀ (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)
⊢ ((((B_1 : (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_1 : (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_1 : (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)

Tactic:
simp [B]
-- 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 j (x + y) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v 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 j x none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v j x (some i)).2 i :
        F)
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v j y none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v j y (some i)).2 i :
        F)

Tactic:
match j with
      | none => simp
      | some j =>
        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]
-- 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 ι
c : 𝕜
x : G × ((i : ι) → E i)
⊢ ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v none (c • x) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v none (c • x) (some i)).2 i) =
    HSMul.hSMul (β := F) c
      ((((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)

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 ι
c : 𝕜
x : 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 ι
c : 𝕜
x : 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 ι
c : 𝕜
x 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 ι
c : 𝕜
x : 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]
-- 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 ι
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)

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]
-- 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_1 : 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 : ι
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)
⊢ ((((B_1 : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v (some j) (c • x) (some i)).2 i) =
    HSMul.hSMul (β := F) c
      ((((B_1 : (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)

Tactic:
simp [B]
-- 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 ι
c : 𝕜
x : G × ((i : ι) → E i)
⊢ ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
            (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v j (c • x) none).1 :
          ContinuousMultilinearMap 𝕜 E F) :
        (a : (i : ι) → E i) → F)
      fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v j (c • x) (some i)).2 i) =
    HSMul.hSMul (β := F) c
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F)
                (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v j x none).1 :
              ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (update (β := fun (x : Option ι) ↦ G × ((i : ι) → E i)) v j x (some i)).2 i :
        F)

Tactic:
match j with
      | none => simp
      | some j =>
        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]
-- 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 : 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_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
simp :
  norm.{u_1} (E := F)
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (b (some i)).2 i :
        F) ≤
    ‖B‖ * (‖b none‖ * ∏ i : ι, ‖b (some i)‖)
⊢ norm.{u_1} (E := F)
      ((MultilinearMap.mk (M₁ := fun (x : Option ι) ↦ G × ((i : ι) → E i))
              (fun (p : (i : Option ι) → G × ((i : ι) → E i)) ↦
                (((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (p none).1 : ContinuousMultilinearMap 𝕜 E F) :
                    (a : (i : ι) → E i) → F)
                  fun (i : ι) ↦ (p (some i)).2 i)
              ⋯ ⋯ :
            (a : (i : Option ι) → G × ((i : ι) → E i)) → F)
          b :
        F) ≤
    ‖B‖ * ∏ i : Option ι, ‖b i‖

Tactic:
simp only [MultilinearMap.coe_mk, Fintype.prod_option]

Premises used: Fintype.prod_option, MultilinearMap.coe_mk
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : 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_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
apply :
  norm (E := ContinuousMultilinearMap 𝕜 E F)
        ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) *
      ∏ i : ι, ‖(b (some i)).2 i‖ ≤
    ‖B‖ * (‖b none‖ * ∏ i : ι, ‖b (some i)‖)
⊢ norm.{u_1} (E := F)
      ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) :
            (a : (i : ι) → E i) → F)
          fun (i : ι) ↦ (b (some i)).2 i :
        F) ≤
    ‖B‖ * (‖b none‖ * ∏ i : ι, ‖b (some i)‖)

Tactic:
apply (ContinuousMultilinearMap.le_opNorm _ _).trans

Premises used: ContinuousMultilinearMap.le_opNorm, LE.le.trans
-- 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 : 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_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
rw :
  norm (E := ContinuousMultilinearMap 𝕜 E F)
        ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) *
      ∏ i : ι, ‖(b (some i)).2 i‖ ≤
    ‖B‖ * ‖b none‖ * ∏ i : ι, ‖b (some i)‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 E F)
        ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) *
      ∏ i : ι, ‖(b (some i)).2 i‖ ≤
    ‖B‖ * (‖b none‖ * ∏ i : ι, ‖b (some i)‖)

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- 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 : 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_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
h₁ :
  norm (E := ContinuousMultilinearMap 𝕜 E F)
      ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) ≤
    ‖B‖ * ‖b none‖
h₂ : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → ‖(b (some i)).2 i‖ ≤ ‖b (some i)‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 E F)
        ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) *
      ∏ i : ι, ‖(b (some i)).2 i‖ ≤
    ‖B‖ * ‖b none‖ * ∏ i : ι, ‖b (some i)‖

Tactic:
gcongr with 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 : 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_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
h₁ : ‖B‖ * ‖(b none).1‖ ≤ ‖B‖ * ‖b none‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 E F)
      ((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) (b none).1 : ContinuousMultilinearMap 𝕜 E F) ≤
    ‖B‖ * ‖b none‖

Tactic:
apply (B.le_opNorm _).trans

Premises used: ContinuousLinearMap.le_opNorm, LE.le.trans