awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometryEquiv.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
⊢ g =
    compContinuousLinearMap (M₁ := E₁) (M₁' := E)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i))
      fun (i : ι) ↦ (↑(↑(f i).symm : E₁ i ≃L[𝕜] E i) : E₁ i →L[𝕜] E i)
have H : ∀ (m : (i : ι) → E₁ i),
  Eq.{wG + 1} (α := G) ((g : (a : (i : ι) → E₁ i) → G) m : G)
    ((compContinuousLinearMap (M₁ := E₁) (M₁' := E)
            (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦
              (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i))
            fun (i : ι) ↦ (↑(↑(f i).symm : E₁ i ≃L[𝕜] E i) : E₁ i →L[𝕜] E i) :
          (a : (i : ι) → E₁ i) → G)
        m :
      G)
Tactic: ext1 m
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (hypothesis)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometryEquiv.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
⊢ ‖g‖ ≤
    norm (E := ContinuousMultilinearMap 𝕜 E G)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toLinearIsometry.toContinuousLinearMap)
have this : g =
  compContinuousLinearMap (M₁ := E₁) (M₁' := E)
    (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i))
    fun (i : ι) ↦ (↑(↑(f i).symm : E₁ i ≃L[𝕜] E i) : E₁ i →L[𝕜] E i)
Tactic: have : g = (g.compContinuousLinearMap fun i => (f i : E i →L[𝕜] E₁ i)).compContinuousLinearMap
      fun i => ((f i).symm : E₁ i →L[𝕜] E i) := by
    ext1 m
    simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometryEquiv.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
this :
  g =
    compContinuousLinearMap (M₁ := E₁) (M₁' := E)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i))
      fun (i : ι) ↦ (↑(↑(f i).symm : E₁ i ≃L[𝕜] E i) : E₁ i →L[𝕜] E i)
| ‖g‖
have rw : norm (E := ContinuousMultilinearMap 𝕜 E₁ G)
  (compContinuousLinearMap (M₁ := E₁) (M₁' := E)
    (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i))
    fun (i : ι) ↦ (↑(↑(f i).symm : E₁ i ≃L[𝕜] E i) : E₁ i →L[𝕜] E i))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → LinearIsometryEquiv.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)
this :
  g =
    compContinuousLinearMap (M₁ := E₁) (M₁' := E)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i))
      fun (i : ι) ↦ (↑(↑(f i).symm : E₁ i ≃L[𝕜] E i) : E₁ i →L[𝕜] E i)
⊢ ‖g‖ ≤
    norm (E := ContinuousMultilinearMap 𝕜 E G)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toLinearIsometry.toContinuousLinearMap)
have conv_lhs : norm (E := ContinuousMultilinearMap 𝕜 E₁ G)
    (compContinuousLinearMap (M₁ := E₁) (M₁' := E)
      (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (↑(↑(f i) : E i ≃L[𝕜] E₁ i) : E i →L[𝕜] E₁ i))
      fun (i : ι) ↦ (↑(↑(f i).symm : E₁ i ≃L[𝕜] E i) : E₁ i →L[𝕜] E i)) ≤
  norm (E := ContinuousMultilinearMap 𝕜 E G)
    (g.compContinuousLinearMap (M₁ := E) (M₁' := E₁) fun (i : ι) ↦ (f i).toLinearIsometry.toContinuousLinearMap)
Tactic: conv_lhs => rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : 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.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
      (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (f₁ + f₂)) =
    g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
        (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₁) +
      g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
        (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₂)
have H : ∀ (x : (i : ι) → E i),
  Eq.{wG + 1} (α := G)
    ((g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
            (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i
              (f₁ + f₂)) :
          (a : (i : ι) → E i) → G)
        x :
      G)
    ((g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
              (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₁) +
            g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
              (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₂) :
          (a : (i : ι) → E i) → G)
        x :
      G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : 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)
x : (i : ι) → E i
⊢ Eq.{wG + 1} (α := G)
    ((g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
            (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i
              (f₁ + f₂)) :
          (a : (i : ι) → E i) → G)
        x :
      G)
    ((g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
              (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₁) +
            g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
              (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₂) :
          (a : (i : ι) → E i) → G)
        x :
      G)
have H : ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
    (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (f₁ + f₂) i_1 :
        (a : E i_1) → E₁ i_1)
      (x i_1)) =
  HAdd.hAdd (α := G) (β := G)
    ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
        (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₁ i_1 :
            (a : E i_1) → E₁ i_1)
          (x i_1) :
      G)
    ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
        (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₂ i_1 :
            (a : E i_1) → E₁ i_1)
          (x i_1) :
      G)
Tactic: simp only [compContinuousLinearMap_apply, add_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : 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)
x : (i : ι) → E i
⊢ ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
      (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (f₁ + f₂) i_1 :
          (a : E i_1) → E₁ i_1)
        (x i_1)) =
    HAdd.hAdd (α := G) (β := G)
      ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
          (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₁ i_1 :
              (a : E i_1) → E₁ i_1)
            (x i_1) :
        G)
      ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
          (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₂ i_1 :
              (a : E i_1) → E₁ i_1)
            (x i_1) :
        G)
have h₁ : ∀ (x_1 : ι),
  (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) 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: convert! g.map_update_add (fun j ↦ f j (x j)) i (f₁ (x i)) (f₂ (x i))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : 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)
x : (i : ι) → E i
h₁ :
  ∀ (x_1 : ι),
    (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) 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
⊢ ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
      (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (f₁ + f₂) i_1 :
          (a : E i_1) → E₁ i_1)
        (x i_1)) =
    HAdd.hAdd (α := G) (β := G)
      ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
          (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₁ i_1 :
              (a : E i_1) → E₁ i_1)
            (x i_1) :
        G)
      ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
          (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₂ i_1 :
              (a : E i_1) → E₁ i_1)
            (x i_1) :
        G)
have h₂ : ∀ (x_1 : ι),
  Eq.{wE₁ + 1} (α := E₁ x_1)
    ((update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) 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: convert! g.map_update_add (fun j ↦ f j (x j)) i (f₁ (x i)) (f₂ (x i))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : 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)
x : (i : ι) → E i
h₁ :
  ∀ (x_1 : ι),
    (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) 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
h₂ :
  ∀ (x_1 : ι),
    Eq.{wE₁ + 1} (α := E₁ x_1)
      ((update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) 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 (i_1 : ι) ↦
      (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (f₁ + f₂) i_1 :
          (a : E i_1) → E₁ i_1)
        (x i_1)) =
    HAdd.hAdd (α := G) (β := G)
      ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
          (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₁ i_1 :
              (a : E i_1) → E₁ i_1)
            (x i_1) :
        G)
      ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
          (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₂ i_1 :
              (a : E i_1) → E₁ i_1)
            (x i_1) :
        G)
have h₃ : ∀ (x_1 : ι),
  Eq.{wE₁ + 1} (α := E₁ x_1)
    ((update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) 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: convert! g.map_update_add (fun j ↦ f j (x j)) i (f₁ (x i)) (f₂ (x i))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : 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.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
      (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (a • f₀)) =
    a •
      g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
        (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₀)
have H : ∀ (x : (i : ι) → E i),
  Eq.{wG + 1} (α := G)
    ((g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
            (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (a • f₀)) :
          (a : (i : ι) → E i) → G)
        x :
      G)
    ((a •
            g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
              (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₀) :
          (a : (i : ι) → E i) → G)
        x :
      G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : 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)
x : (i : ι) → E i
⊢ Eq.{wG + 1} (α := G)
    ((g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
            (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (a • f₀)) :
          (a : (i : ι) → E i) → G)
        x :
      G)
    ((a •
            g.compContinuousLinearMap (M₁ := E) (M₁' := E₁)
              (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₀) :
          (a : (i : ι) → E i) → G)
        x :
      G)
have H : ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
    (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (a • f₀) i_1 :
        (a : E i_1) → E₁ i_1)
      (x i_1)) =
  HSMul.hSMul (β := G) a
    ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
        (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₀ i_1 :
            (a : E i_1) → E₁ i_1)
          (x i_1) :
      G)
Tactic: simp only [compContinuousLinearMap_apply, smul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : 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)
x : (i : ι) → E i
⊢ ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
      (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (a • f₀) i_1 :
          (a : E i_1) → E₁ i_1)
        (x i_1)) =
    HSMul.hSMul (β := G) a
      ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
          (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₀ i_1 :
              (a : E i_1) → E₁ i_1)
            (x i_1) :
        G)
have h₁ : ∀ (x_1 : ι),
  (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) 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: convert! g.map_update_smul (fun j ↦ f j (x j)) i a (f₀ (x i))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Multilinear.Basic (goal)
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 ι
g : ContinuousMultilinearMap 𝕜 E₁ G
h : 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)
x : (i : ι) → E i
h₁ :
  ∀ (x_1 : ι),
    (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) 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
⊢ ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
      (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i (a • f₀) i_1 :
          (a : E i_1) → E₁ i_1)
        (x i_1)) =
    HSMul.hSMul (β := G) a
      ((g : (a : (i : ι) → E₁ i) → G) fun (i_1 : ι) ↦
          (update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) f i f₀ i_1 :
              (a : E i_1) → E₁ i_1)
            (x i_1) :
        G)
have h₂ : ∀ (x_1 : ι),
  Eq.{wE₁ + 1} (α := E₁ x_1)
    ((update (β := fun (i : ι) ↦ ContinuousLinearMap.{u, u, wE, wE₁} (RingHom.id 𝕜) (E i) (E₁ i)) 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: convert! g.map_update_smul (fun j ↦ f j (x j)) i a (f₀ (x i))