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)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : Equiv.{u_1 + 1, uι + 1} α (↑s : Type uι)
inst_9 : DecidablePred fun (x : ι) ↦ x ∈ s
z : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)
⊢ ∀ [inst_10 : DecidableEq α] (m : (i : α) → (i : ι) → M₁ i) (i : α) (c : R) (x : (i : ι) → M₁ i),
    ((((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                  MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
              z :
            MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
          (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
        fun (i_1 : { a : ι // a ∈ s }) ↦
        update (β := fun (x : α) ↦ (i : ι) → M₁ i) m i (c • x) ((e.symm : (a : (↑s : Type uι)) → α) i_1) (↑i_1 : ι)) =
      HSMul.hSMul (β := M₂) c
        ((((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                    (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                      MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                  z :
                MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
              (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
            fun (i_1 : { a : ι // a ∈ s }) ↦
            update (β := fun (x : α) ↦ (i : ι) → M₁ i) m i x ((e.symm : (a : (↑s : Type uι)) → α) i_1) (↑i_1 : ι) :
          M₂)

Tactic:
classical simp [iteratedFDeriv_aux]

Premises used: MultilinearMap.iteratedFDeriv_aux
-- 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)
α : Type u_1
f : MultilinearMap R M₁ M₂
s : Set ι
e : Equiv.{u_1 + 1, uι + 1} α (↑s : Type uι)
inst_9 : DecidablePred fun (x : ι) ↦ x ∈ s
inst_10 : DecidableEq { a : ι // a ∉ s }
m : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)
i : { a : ι // a ∉ s }
c : R
x : M₁ (↑i : ι)
x_1 : (i : α) → (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂)
    ((mk (M₁ := fun (x : α) ↦ (i : ι) → M₁ i)
            (fun (v : (i : α) → (i : ι) → M₁ i) ↦
              (((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                        (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                          MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                      (update (β := fun (i : { a : ι // a ∉ s }) ↦ M₁ (↑i : ι)) m i (c • x)) :
                    MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
                  (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
                fun (i : { a : ι // a ∈ s }) ↦ v ((e.symm : (a : (↑s : Type uι)) → α) i) (↑i : ι))
            ⋯ ⋯ :
          (a : (i : α) → (i : ι) → M₁ i) → M₂)
        x_1 :
      M₂)
    ((HSMul.hSMul (β := MultilinearMap R (fun (x : α) ↦ (i : ι) → M₁ i) M₂) c
            (mk (M₁ := fun (x : α) ↦ (i : ι) → M₁ i)
              (fun (v : (i : α) → (i : ι) → M₁ i) ↦
                (((f.domDomRestrictₗ (M₁ := M₁) fun (i : ι) ↦ i ∈ s :
                          (a : (i : { a : ι // a ∉ s }) → M₁ (↑i : ι)) →
                            MultilinearMap R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂)
                        (update (β := fun (i : { a : ι // a ∉ s }) ↦ M₁ (↑i : ι)) m i x) :
                      MultilinearMap.{uR, uι, v₁, v₂} R (fun (i : { a : ι // a ∈ s }) ↦ M₁ (↑i : ι)) M₂) :
                    (a : (i : { a : ι // a ∈ s }) → M₁ (↑i : ι)) → M₂)
                  fun (i : { a : ι // a ∈ s }) ↦ v ((e.symm : (a : (↑s : Type uι)) → α) i) (↑i : ι))
              ⋯ ⋯) :
          (a : (i : α) → (i : ι) → M₁ i) → M₂)
        x_1 :
      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)
e : (i : ι) → LinearEquiv.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
x : MultilinearMap R M₁' M₂
H :
  ∀ (x_1 : (i : ι) → M₁' i),
    Eq.{v₂ + 1} (α := M₂)
      ((((compLinearMapₗ (M₁ := M₁') (M₁' := M₁) fun (x : ι) ↦ (↑(e x).symm : M₁' x →ₗ[R] M₁ x) :
                  (a : MultilinearMap R M₁ M₂) → MultilinearMap R M₁' M₂)
                (AddHom.toFun
                  (LinearMap.toAddHom
                    (compLinearMapₗ (M₁ := M₁) (M₁' := M₁') fun (x : ι) ↦ (↑(e x) : M₁ x →ₗ[R] M₁' x)))
                  x) :
              MultilinearMap R M₁' M₂) :
            (a : (i : ι) → M₁' i) → M₂)
          x_1 :
        M₂)
      ((x : (a : (i : ι) → M₁' i) → M₂) x_1 : M₂)
⊢ (compLinearMapₗ (M₁ := M₁') (M₁' := M₁) fun (x : ι) ↦ (↑(e x).symm : M₁' x →ₗ[R] M₁ x) :
        (a : MultilinearMap R M₁ M₂) → MultilinearMap R M₁' M₂)
      (AddHom.toFun
        (LinearMap.toAddHom (compLinearMapₗ (M₁ := M₁) (M₁' := M₁') fun (x : ι) ↦ (↑(e x) : M₁ x →ₗ[R] M₁' x))) x) =
    x

Tactic:
ext
-- 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)
e : (i : ι) → LinearEquiv.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
x : MultilinearMap R M₁' M₂
x_1 : (i : ι) → M₁' i
⊢ Eq.{v₂ + 1} (α := M₂)
    ((((compLinearMapₗ (M₁ := M₁') (M₁' := M₁) fun (x : ι) ↦ (↑(e x).symm : M₁' x →ₗ[R] M₁ x) :
                (a : MultilinearMap R M₁ M₂) → MultilinearMap R M₁' M₂)
              (AddHom.toFun
                (LinearMap.toAddHom (compLinearMapₗ (M₁ := M₁) (M₁' := M₁') fun (x : ι) ↦ (↑(e x) : M₁ x →ₗ[R] M₁' x)))
                x) :
            MultilinearMap R M₁' M₂) :
          (a : (i : ι) → M₁' i) → M₂)
        x_1 :
      M₂)
    ((x : (a : (i : ι) → M₁' i) → M₂) x_1 : 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)
e : (i : ι) → LinearEquiv.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
x : MultilinearMap R M₁ M₂
H :
  ∀ (x_1 : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂)
      ((AddHom.toFun (M := MultilinearMap R M₁' M₂)
              (LinearMap.toAddHom (compLinearMapₗ (M₁ := M₁) (M₁' := M₁') fun (x : ι) ↦ (↑(e x) : M₁ x →ₗ[R] M₁' x)))
              ((compLinearMapₗ (M₁ := M₁') (M₁' := M₁) fun (x : ι) ↦ (↑(e x).symm : M₁' x →ₗ[R] M₁ x) :
                  (a : MultilinearMap R M₁ M₂) → MultilinearMap R M₁' M₂)
                x) :
            (a : (i : ι) → M₁ i) → M₂)
          x_1 :
        M₂)
      ((x : (a : (i : ι) → M₁ i) → M₂) x_1 : M₂)
⊢ AddHom.toFun (M := MultilinearMap R M₁' M₂)
      (LinearMap.toAddHom (compLinearMapₗ (M₁ := M₁) (M₁' := M₁') fun (x : ι) ↦ (↑(e x) : M₁ x →ₗ[R] M₁' x)))
      ((compLinearMapₗ (M₁ := M₁') (M₁' := M₁) fun (x : ι) ↦ (↑(e x).symm : M₁' x →ₗ[R] M₁ x) :
          (a : MultilinearMap R M₁ M₂) → MultilinearMap R M₁' M₂)
        x) =
    x

Tactic:
ext
-- 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)
e : (i : ι) → LinearEquiv.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
x : MultilinearMap R M₁ M₂
x_1 : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂)
    ((AddHom.toFun (M := MultilinearMap R M₁' M₂)
            (LinearMap.toAddHom (compLinearMapₗ (M₁ := M₁) (M₁' := M₁') fun (x : ι) ↦ (↑(e x) : M₁ x →ₗ[R] M₁' x)))
            ((compLinearMapₗ (M₁ := M₁') (M₁' := M₁) fun (x : ι) ↦ (↑(e x).symm : M₁' x →ₗ[R] M₁ x) :
                (a : MultilinearMap R M₁ M₂) → MultilinearMap R M₁' M₂)
              x) :
          (a : (i : ι) → M₁ i) → M₂)
        x_1 :
      M₂)
    ((x : (a : (i : ι) → M₁ i) → M₂) x_1 : 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_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)
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
                      (f₁ + f₂)) :
                  (a : MultilinearMap R M₁' M₂) → MultilinearMap R M₁ M₂)
                g :
              MultilinearMap R M₁ M₂) :
            (a : (i : ι) → M₁ i) → M₂)
          x :
        M₂)
      ((((HAdd.hAdd (α := MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂)
                    (compLinearMapₗ (M₁ := M₁) (M₁' := M₁')
                      (update (β := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) f i f₁))
                    (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 (f₁ + f₂)) =
    HAdd.hAdd (α := MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂)
      (compLinearMapₗ (M₁ := M₁) (M₁' := M₁')
        (update (β := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) f i f₁))
      (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 : ι
f₁ 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 (f₁ + f₂) j :
          (a : M₁ j) → M₁' j)
        (x j)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((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₂)
      ((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
                    (f₁ + f₂)) :
                (a : MultilinearMap R M₁' M₂) → MultilinearMap R M₁ M₂)
              g :
            MultilinearMap R M₁ M₂) :
          (a : (i : ι) → M₁ i) → M₂)
        x :
      M₂)
    ((((HAdd.hAdd (α := MultilinearMap R M₁' M₂ →ₗ[R] MultilinearMap R M₁ M₂)
                  (compLinearMapₗ (M₁ := M₁) (M₁' := M₁')
                    (update (β := fun (i : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)) f i f₁))
                  (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 (f₁ + f₂) j <| x j) =
        (g fun j ↦ update f i f₁ j <| x j) + g fun j ↦ update f i f₂ j (x j)

Premises used: Function.update, HAdd.hAdd, 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 : ι
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)
⊢ (g : (a : (i : ι) → M₁' i) → M₂)
      (update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i
        (HAdd.hAdd (α := M₁' i) (β := M₁' i) ((f₁ : (a : M₁ i) → M₁' i) (x i) : M₁' i)
          ((f₂ : (a : M₁ i) → M₁' i) (x i) : M₁' i))) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((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₂)
      ((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_add (fun j ↦ f j (x j)) i (f₁ (x i)) (f₂ (x i))

Premises used: MultilinearMap.map_update_add, 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 : ι
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)
h :
  ∀ (j : ι),
    (update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i (f₁ + f₂) j :
          (a : M₁ j) → M₁' j)
        (x j) =
      update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i
        (HAdd.hAdd (α := M₁' i) (β := M₁' i) ((f₁ : (a : M₁ i) → M₁' i) (x i) : M₁' i)
          ((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)
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 (f₁ + f₂) j :
          (a : M₁ j) → M₁' j)
        (x j)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((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₂)
      ((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_add (fun j ↦ f j (x j)) i (f₁ (x i)) (f₂ (x i)) with j j j

Premises used: MultilinearMap.map_update_add, 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 : ι
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 : ι
⊢ (update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i (f₁ + f₂) j :
        (a : M₁ j) → M₁' j)
      (x j) =
    update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i
      (HAdd.hAdd (α := M₁' i) (β := M₁' i) ((f₁ : (a : M₁ i) → M₁' i) (x i) : M₁' i)
        ((f₂ : (a : M₁ i) → M₁' i) (x i) : M₁' i))
      j

Tactic:
Function.apply_update c f i (f₁ + f₂) j

Premises used: Function.apply_update, HAdd.hAdd
-- 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 : ι
⊢ (update (β := fun (a : ι) ↦ LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ a) (M₁' a)) f i (f₁ + f₂) j :
        (a : M₁ j) → M₁' j)
      (x j) =
    update (β := M₁') (fun (j : ι) ↦ (f j : (a : M₁ j) → M₁' j) (x j)) i
      (HAdd.hAdd (α := M₁' i) (β := M₁' i) ((f₁ : (a : M₁ i) → M₁' i) (x i) : M₁' i)
        ((f₂ : (a : M₁ i) → M₁' i) (x i) : M₁' i))
      j

Tactic:
exact Function.apply_update c f i (f₁ + f₂) j

Premises used: Function.apply_update, HAdd.hAdd