awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
f₁ f₂ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) → M₁' i :=
  fun (i : ι) (f : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) ↦ (f : (a : M₁ i) → M₁' i) (x i)
j : ι
⊢ Eq.{v₁' + 1} (α := M₁' j)
    ((update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i f₁ j :
          (a : M₁ j) → M₁' j)
        (x j) :
      M₁' j)
    (update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i ((f₁ : (a : M₁ i) → M₁' i) (x i)) j : M₁' j)

Tactic:
Function.apply_update c f i f₁ j

Premises used: Function.apply_update
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
f₁ f₂ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) → M₁' i :=
  fun (i : ι) (f : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) ↦ (f : (a : M₁ i) → M₁' i) (x i)
j : ι
⊢ Eq.{v₁' + 1} (α := M₁' j)
    ((update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i f₁ j :
          (a : M₁ j) → M₁' j)
        (x j) :
      M₁' j)
    (update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i ((f₁ : (a : M₁ i) → M₁' i) (x i)) j : M₁' j)

Tactic:
exact Function.apply_update c f i f₁ j

Premises used: Function.apply_update
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
f₁ f₂ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) → M₁' i :=
  fun (i : ι) (f : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) ↦ (f : (a : M₁ i) → M₁' i) (x i)
j : ι
⊢ Eq.{v₁' + 1} (α := M₁' j)
    ((update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i f₂ j :
          (a : M₁ j) → M₁' j)
        (x j) :
      M₁' j)
    (update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i ((f₂ : (a : M₁ i) → M₁' i) (x i)) j : M₁' j)

Tactic:
Function.apply_update c f i f₂ j

Premises used: Function.apply_update
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
f₁ f₂ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) → M₁' i :=
  fun (i : ι) (f : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) ↦ (f : (a : M₁ i) → M₁' i) (x i)
j : ι
⊢ Eq.{v₁' + 1} (α := M₁' j)
    ((update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i f₂ j :
          (a : M₁ j) → M₁' j)
        (x j) :
      M₁' j)
    (update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i ((f₂ : (a : M₁ i) → M₁' i) (x i)) j : M₁' j)

Tactic:
exact Function.apply_update c f i f₂ j

Premises used: Function.apply_update
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
a : R
f₀ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
h :
  ∀ (g : MultilinearMap R M₁' M₂) (x : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂)
      ((((compLinearMapₗ (M₁ := M₁) (M₁' := M₁')
                    (update (β := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) f i
                      (a • f₀)) :
                  (a : MultilinearMap R M₁' M₂) → MultilinearMap R M₁ M₂)
                g :
              MultilinearMap R M₁ M₂) :
            (a : (i : ι) → M₁ i) → M₂)
          x :
        M₂)
      ((((HSMul.hSMul (β := MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂) a
                    (compLinearMapₗ (M₁ := M₁) (M₁' := M₁')
                      (update (β := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) f i f₀)) :
                  (a : MultilinearMap R M₁' M₂) → MultilinearMap R M₁ M₂)
                g :
              MultilinearMap R M₁ M₂) :
            (a : (i : ι) → M₁ i) → M₂)
          x :
        M₂)
⊢ compLinearMapₗ (M₁ := M₁) (M₁' := M₁')
      (update (β := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) f i (a • f₀)) =
    HSMul.hSMul (β := MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂) a
      (compLinearMapₗ (M₁ := M₁) (M₁' := M₁')
        (update (β := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) f i f₀))

Tactic:
ext g x
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
a : R
f₀ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
h :
  ((g : (a : (i : ι) → M₁' i) → M₂) fun (j : ι) ↦
      (update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i (a • f₀) j :
          (a : M₁ j) → M₁' j)
        (x j)) =
    HSMul.hSMul (β := M₂) a
      ((g : (a : (i : ι) → M₁' i) → M₂) fun (j : ι) ↦
          (update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i f₀ j :
              (a : M₁ j) → M₁' j)
            (x j) :
        M₂)
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((compLinearMapₗ (M₁ := M₁) (M₁' := M₁')
                  (update (β := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) f i (a • f₀)) :
                (a : MultilinearMap R M₁' M₂) → MultilinearMap R M₁ M₂)
              g :
            MultilinearMap R M₁ M₂) :
          (a : (i : ι) → M₁ i) → M₂)
        x :
      M₂)
    ((((HSMul.hSMul (β := MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂) a
                  (compLinearMapₗ (M₁ := M₁) (M₁' := M₁')
                    (update (β := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) f i f₀)) :
                (a : MultilinearMap R M₁' M₂) → MultilinearMap R M₁ M₂)
              g :
            MultilinearMap R M₁ M₂) :
          (a : (i : ι) → M₁ i) → M₂)
        x :
      M₂)

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.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
a : R
f₀ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) → M₁' i :=
  fun (i : ι) (f : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) ↦ (f : (a : M₁ i) → M₁' i) (x i)
⊢ (g : (a : (i : ι) → M₁' i) → M₂)
      (update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i
        (HSMul.hSMul (β := M₁' i) a ((f₀ : (a : M₁ i) → M₁' i) (x i) : M₁' i))) =
    HSMul.hSMul (β := M₂) a
      ((g : (a : (i : ι) → M₁' i) → M₂)
          (update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i ((f₀ : (a : M₁ i) → M₁' i) (x i))) :
        M₂)

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

Premises used: MultilinearMap.map_update_smul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
a : R
f₀ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) → M₁' i :=
  fun (i : ι) (f : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) ↦ (f : (a : M₁ i) → M₁' i) (x i)
h :
  ∀ (j : ι),
    (update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i (a • f₀) j :
          (a : M₁ j) → M₁' j)
        (x j) =
      update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i
        (HSMul.hSMul (β := M₁' i) a ((f₀ : (a : M₁ i) → M₁' i) (x i) : M₁' i)) j
h₁ :
  ∀ (j : ι),
    Eq.{v₁' + 1} (α := M₁' j)
      ((update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i f₀ j :
            (a : M₁ j) → M₁' j)
          (x j) :
        M₁' j)
      (update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i ((f₀ : (a : M₁ i) → M₁' i) (x i)) j : M₁' j)
⊢ ((g : (a : (i : ι) → M₁' i) → M₂) fun (j : ι) ↦
      (update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i (a • f₀) j :
          (a : M₁ j) → M₁' j)
        (x j)) =
    HSMul.hSMul (β := M₂) a
      ((g : (a : (i : ι) → M₁' i) → M₂) fun (j : ι) ↦
          (update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i f₀ j :
              (a : M₁ j) → M₁' j)
            (x j) :
        M₂)

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

Premises used: MultilinearMap.map_update_smul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
a : R
f₀ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) → M₁' i :=
  fun (i : ι) (f : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) ↦ (f : (a : M₁ i) → M₁' i) (x i)
j : ι
⊢ (update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i (a • f₀) j :
        (a : M₁ j) → M₁' j)
      (x j) =
    update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i
      (HSMul.hSMul (β := M₁' i) a ((f₀ : (a : M₁ i) → M₁' i) (x i) : M₁' i)) j

Tactic:
Function.apply_update c f i (a • f₀) j

Premises used: Function.apply_update, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
a : R
f₀ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) → M₁' i :=
  fun (i : ι) (f : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) ↦ (f : (a : M₁ i) → M₁' i) (x i)
j : ι
⊢ (update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i (a • f₀) j :
        (a : M₁ j) → M₁' j)
      (x j) =
    update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i
      (HSMul.hSMul (β := M₁' i) a ((f₀ : (a : M₁ i) → M₁' i) (x i) : M₁' i)) j

Tactic:
exact Function.apply_update c f i (a • f₀) j

Premises used: Function.apply_update, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
a : R
f₀ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) → M₁' i :=
  fun (i : ι) (f : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) ↦ (f : (a : M₁ i) → M₁' i) (x i)
j : ι
⊢ Eq.{v₁' + 1} (α := M₁' j)
    ((update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i f₀ j :
          (a : M₁ j) → M₁' j)
        (x j) :
      M₁' j)
    (update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i ((f₀ : (a : M₁ i) → M₁' i) (x i)) j : M₁' j)

Tactic:
Function.apply_update c f i f₀ j

Premises used: Function.apply_update
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f_1 f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
i : ι
a : R
f₀ : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) → M₁' i :=
  fun (i : ι) (f : LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) ↦ (f : (a : M₁ i) → M₁' i) (x i)
j : ι
⊢ Eq.{v₁' + 1} (α := M₁' j)
    ((update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i f₀ j :
          (a : M₁ j) → M₁' j)
        (x j) :
      M₁' j)
    (update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i ((f₀ : (a : M₁ i) → M₁' i) (x i)) j : M₁' j)

Tactic:
exact Function.apply_update c f i f₀ j

Premises used: Function.apply_update
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
⊢ ∀ (x y : MultilinearMap R M₁' M₂),
    LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) (M₂ :=
        MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂)
        ((LinearMap.applyₗ :
            (a : MultilinearMap R M₁' M₂) →
              (MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂) →ₗ[R] MultilinearMap R M₁ M₂)
          (x + y))
        (compLinearMapMultilinear (M₁ := M₁) (M₁' := M₁')) =
      HAdd.hAdd (α :=
        MultilinearMap R (fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i))
          (MultilinearMap R M₁ M₂))
        (LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i))
          (M₂ := MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂)
          ((LinearMap.applyₗ :
              (a : MultilinearMap R M₁' M₂) →
                (MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂) →ₗ[R] MultilinearMap R M₁ M₂)
            x)
          (compLinearMapMultilinear (M₁ := M₁) (M₁' := M₁')))
        (LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i))
          (M₂ := MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂)
          ((LinearMap.applyₗ :
              (a : MultilinearMap R M₁' M₂) →
                (MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂) →ₗ[R] MultilinearMap R M₁ M₂)
            y)
          (compLinearMapMultilinear (M₁ := M₁) (M₁' := M₁')))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
f f' : MultilinearMap R M₁ M₂
inst_7 : (i : ι) → AddCommMonoid (M₁' i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
⊢ ∀ (m : R) (x : MultilinearMap R M₁' M₂),
    LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) (M₂ :=
        MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂)
        ((LinearMap.applyₗ :
            (a : MultilinearMap R M₁' M₂) →
              (MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂) →ₗ[R] MultilinearMap R M₁ M₂)
          (m • x))
        (compLinearMapMultilinear (M₁ := M₁) (M₁' := M₁')) =
      HSMul.hSMul (α := R) (β :=
        MultilinearMap R (fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i))
          (MultilinearMap R M₁ M₂))
        ((RingHom.id R : (a : R) → R) m : R)
        (LinearMap.compMultilinearMap (M₁ := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i))
          (M₂ := MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂)
          ((LinearMap.applyₗ :
              (a : MultilinearMap R M₁' M₂) →
                (MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂) →ₗ[R] MultilinearMap R M₁ M₂)
            x)
          (compLinearMapMultilinear (M₁ := M₁) (M₁' := M₁')))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
f : MultilinearMap R M₁ M₂
inst_5 : DecidableEq ι
c : ι → R
m : (i : ι) → M₁ i
s : Finset ι
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (Finset.piecewise (π := M₁) ∅ (fun (i : ι) ↦ c i • m i) m) =
    HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) (∏ i ∈ ∅, c i) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
simp