awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
f₁ f₂ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x_1 : ι
⊢ (update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i (f₁ + f₂) x_1 :
        (a : E x_1) → E₁ x_1)
      (x x_1) =
    update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i
      (HAdd.hAdd (α := E₁ i) (β := E₁ i) ((f₁ : (a : E i) → E₁ i) (x i) : E₁ i) ((f₂ : (a : E i) → E₁ i) (x i) : E₁ i))
      x_1

Tactic:
exact apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _

Premises used: Function.apply_update, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
f₁ f₂ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x_1 : ι
⊢ Eq.{wE₁ + 1} (α := E₁ x_1)
    ((update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i f₁ x_1 :
          (a : E x_1) → E₁ x_1)
        (x x_1) :
      E₁ x_1)
    (update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i ((f₁ : (a : E i) → E₁ i) (x i)) x_1 : E₁ x_1)

Tactic:
apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _

Premises used: Function.apply_update, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
f₁ f₂ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x_1 : ι
⊢ Eq.{wE₁ + 1} (α := E₁ x_1)
    ((update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i f₁ x_1 :
          (a : E x_1) → E₁ x_1)
        (x x_1) :
      E₁ x_1)
    (update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i ((f₁ : (a : E i) → E₁ i) (x i)) x_1 : E₁ x_1)

Tactic:
exact apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _

Premises used: Function.apply_update, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
f₁ f₂ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x_1 : ι
⊢ Eq.{wE₁ + 1} (α := E₁ x_1)
    ((update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i f₂ x_1 :
          (a : E x_1) → E₁ x_1)
        (x x_1) :
      E₁ x_1)
    (update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i ((f₂ : (a : E i) → E₁ i) (x i)) x_1 : E₁ x_1)

Tactic:
apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _

Premises used: Function.apply_update, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
f₁ f₂ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x_1 : ι
⊢ Eq.{wE₁ + 1} (α := E₁ x_1)
    ((update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i f₂ x_1 :
          (a : E x_1) → E₁ x_1)
        (x x_1) :
      E₁ x_1)
    (update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i ((f₂ : (a : E i) → E₁ i) (x i)) x_1 : E₁ x_1)

Tactic:
exact apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _

Premises used: Function.apply_update, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
a : 𝕜
f₀ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
h :
  ∀ (g : ContinuousMultilinearMap 𝕜 E₁ G) (x : (i : ι) → E i),
    Eq.{wG + 1} (α := G)
      ((((compContinuousLinearMapL (E := E) (E₁ := E₁)
                    (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i
                      (a • f₀)) :
                  (a : ContinuousMultilinearMap 𝕜 E₁ G) → ContinuousMultilinearMap 𝕜 E G)
                g :
              ContinuousMultilinearMap 𝕜 E G) :
            (a : (i : ι) → E i) → G)
          x :
        G)
      ((((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G) a
                    (compContinuousLinearMapL (E := E) (E₁ := E₁)
                      (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i
                        f₀)) :
                  (a : ContinuousMultilinearMap 𝕜 E₁ G) → ContinuousMultilinearMap 𝕜 E G)
                g :
              ContinuousMultilinearMap 𝕜 E G) :
            (a : (i : ι) → E i) → G)
          x :
        G)
⊢ compContinuousLinearMapL (E := E) (E₁ := E₁)
      (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (a • f₀)) =
    HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G) a
      (compContinuousLinearMapL (E := E) (E₁ := E₁)
        (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₀))

Tactic:
ext g x
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
a : 𝕜
f₀ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
h :
  ((g : (a : (i : ι) → E₁ i) → G) fun (j : ι) ↦
      (update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i (a • f₀) j :
          (a : E j) → E₁ j)
        (x j)) =
    HSMul.hSMul (β := G) a
      ((g : (a : (i : ι) → E₁ i) → G) fun (j : ι) ↦
          (update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i f₀ j :
              (a : E j) → E₁ j)
            (x j) :
        G)
⊢ Eq.{wG + 1} (α := G)
    ((((compContinuousLinearMapL (E := E) (E₁ := E₁)
                  (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i
                    (a • f₀)) :
                (a : ContinuousMultilinearMap 𝕜 E₁ G) → ContinuousMultilinearMap 𝕜 E G)
              g :
            ContinuousMultilinearMap 𝕜 E G) :
          (a : (i : ι) → E i) → G)
        x :
      G)
    ((((HSMul.hSMul (β := ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G) a
                  (compContinuousLinearMapL (E := E) (E₁ := E₁)
                    (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i
                      f₀)) :
                (a : ContinuousMultilinearMap 𝕜 E₁ G) → ContinuousMultilinearMap 𝕜 E G)
              g :
            ContinuousMultilinearMap 𝕜 E G) :
          (a : (i : ι) → E i) → G)
        x :
      G)

Tactic:
change (g fun j ↦ update f i (a • f₀) j <| x j) = a • g fun j ↦ update f i f₀ j (x j)

Premises used: Function.update, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
a : 𝕜
f₀ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
⊢ (g : (a : (i : ι) → E₁ i) → G)
      (update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i
        (HSMul.hSMul (β := E₁ i) a ((f₀ : (a : E i) → E₁ i) (x i) : E₁ i))) =
    HSMul.hSMul (β := G) a
      ((g : (a : (i : ι) → E₁ i) → G)
          (update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i ((f₀ : (a : E i) → E₁ i) (x i))) :
        G)

Tactic:
g.map_update_smul (fun j ↦ f j (x j)) i a (f₀ (x i))

Premises used: ContinuousMultilinearMap.map_update_smul, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
a : 𝕜
f₀ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
h :
  ∀ (x_1 : ι),
    (update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i (a • f₀) x_1 :
          (a : E x_1) → E₁ x_1)
        (x x_1) =
      update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i
        (HSMul.hSMul (β := E₁ i) a ((f₀ : (a : E i) → E₁ i) (x i) : E₁ i)) x_1
h₁ :
  ∀ (x_1 : ι),
    Eq.{wE₁ + 1} (α := E₁ x_1)
      ((update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i f₀ x_1 :
            (a : E x_1) → E₁ x_1)
          (x x_1) :
        E₁ x_1)
      (update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i ((f₀ : (a : E i) → E₁ i) (x i)) x_1 : E₁ x_1)
⊢ ((g : (a : (i : ι) → E₁ i) → G) fun (j : ι) ↦
      (update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i (a • f₀) j :
          (a : E j) → E₁ j)
        (x j)) =
    HSMul.hSMul (β := G) a
      ((g : (a : (i : ι) → E₁ i) → G) fun (j : ι) ↦
          (update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i f₀ j :
              (a : E j) → E₁ j)
            (x j) :
        G)

Tactic:
convert! g.map_update_smul (fun j ↦ f j (x j)) i a (f₀ (x i))

Premises used: ContinuousMultilinearMap.map_update_smul, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
a : 𝕜
f₀ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x_1 : ι
⊢ (update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i (a • f₀) x_1 :
        (a : E x_1) → E₁ x_1)
      (x x_1) =
    update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i
      (HSMul.hSMul (β := E₁ i) a ((f₀ : (a : E i) → E₁ i) (x i) : E₁ i)) x_1

Tactic:
apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _

Premises used: Function.apply_update, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
a : 𝕜
f₀ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x_1 : ι
⊢ (update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i (a • f₀) x_1 :
        (a : E x_1) → E₁ x_1)
      (x x_1) =
    update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i
      (HSMul.hSMul (β := E₁ i) a ((f₀ : (a : E i) → E₁ i) (x i) : E₁ i)) x_1

Tactic:
exact apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _

Premises used: Function.apply_update, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
a : 𝕜
f₀ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x_1 : ι
⊢ Eq.{wE₁ + 1} (α := E₁ x_1)
    ((update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i f₀ x_1 :
          (a : E x_1) → E₁ x_1)
        (x x_1) :
      E₁ x_1)
    (update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i ((f₀ : (a : E i) → E₁ i) (x i)) x_1 : E₁ x_1)

Tactic:
apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _

Premises used: Function.apply_update, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
inst_11 : DecidableEq ι
f : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
i : ι
a : 𝕜
f₀ : ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
x : (i : ι) → E i
x_1 : ι
⊢ Eq.{wE₁ + 1} (α := E₁ x_1)
    ((update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) f i f₀ x_1 :
          (a : E x_1) → E₁ x_1)
        (x x_1) :
      E₁ x_1)
    (update (β := E₁) (fun (j : ι) ↦ (f j : (a : E j) → E₁ j) (x j)) i ((f₀ : (a : E i) → E₁ i) (x i)) x_1 : E₁ x_1)

Tactic:
exact apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _

Premises used: Function.apply_update, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
f : (i : ι) → (fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) i
rw :
  norm (E := ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
      ((compContinuousLinearMapMultilinear 𝕜 E E₁ G :
            (a : (i : ι) → (fun (i : ι) ↦ E i →L[𝕜] E₁ i) i) →
              ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
          f :
        ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G) ≤
    ∏ i : ι, ‖f i‖
⊢ norm (E := ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
      ((compContinuousLinearMapMultilinear 𝕜 E E₁ G :
            (a : (i : ι) → (fun (i : ι) ↦ E i →L[𝕜] E₁ i) i) →
              ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
          f :
        ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G) ≤
    HMul.hMul (α := ℝ) 1 (∏ i : ι, ‖f i‖)

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst : Fintype ι'
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → SeminormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_4 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_5 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_6 : SeminormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
inst_8 : SeminormedAddCommGroup G'
inst_9 : NormedSpace 𝕜 G'
inst_10 : Fintype ι
f : (i : ι) → (fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) i
⊢ norm (E := ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
      ((compContinuousLinearMapMultilinear 𝕜 E E₁ G :
            (a : (i : ι) → (fun (i : ι) ↦ E i →L[𝕜] E₁ i) i) →
              ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
          f :
        ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G) ≤
    ∏ i : ι, ‖f i‖

Tactic:
apply norm_compContinuousLinearMapL_le

Premises used: ContinuousMultilinearMap.norm_compContinuousLinearMapL_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
E₁ : ι → Type wE₁
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → SeminormedAddCommGroup (E i)
inst_2 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst_4 : (i : ι) → NormedSpace.{u, wE₁} 𝕜 (E₁ i)
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : ContinuousMultilinearMap 𝕜 E₁ G
g dg : (i : ι) → ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
v : (i : ι) → E i
⊢ Eq.{wG + 1} (α := G)
    ((((f.fderivCompContinuousLinearMap (E := E) (E₁ := E₁) g :
                (a : (i : ι) → E i →L[𝕜] E₁ i) → ContinuousMultilinearMap 𝕜 E G)
              dg :
            ContinuousMultilinearMap 𝕜 E G) :
          (a : (i : ι) → E i) → G)
        v :
      G)
    (∑ i : ι,
        (f : (a : (i : ι) → E₁ i) → G) fun (j : ι) ↦
          (update (β := fun (a : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E a) (E₁ a)) g i (dg i) j :
              (a : E j) → E₁ j)
            (v j) :
      G)

Tactic:
simp [fderivCompContinuousLinearMap]

Premises used: ContinuousMultilinearMap.fderivCompContinuousLinearMap