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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_11 : DecidablePred P
z : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
x : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
a b : M₁ (↑i : ι)
repeat :
  (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (a + b)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) a) :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) b) :
        M₂)
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
      if h : P j then
        update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i (a + b) (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
      else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) x i b (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)

Tactic:
repeat (rw [domDomRestrict_aux])

Premises used: MultilinearMap.domDomRestrict_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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_11 : DecidablePred P
z : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
x : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
a b : M₁ (↑i : ι)
⊢ (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (a + b)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) a) :
        M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) b) :
        M₂)

Tactic:
simp only [MultilinearMap.map_update_add]

Premises used: MultilinearMap.map_update_add
-- 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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_11 : DecidablePred P
z_1 : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
z : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
c : R
a : M₁ (↑i : ι)
rw :
  (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (c • a)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
      if h : P j then
        update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i (c • a) (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
      else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)

Tactic:
rw [domDomRestrict_aux]

Premises used: MultilinearMap.domDomRestrict_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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_11 : DecidablePred P
z_1 : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
z : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
c : R
a : M₁ (↑i : ι)
rw :
  (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (c • a)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) a) :
        M₂)
⊢ (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (c • a)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)

Tactic:
rw [domDomRestrict_aux]

Premises used: MultilinearMap.domDomRestrict_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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_11 : DecidablePred P
z_1 : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
z : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
c : R
a : M₁ (↑i : ι)
repeat :
  (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (c • a)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) a) :
        M₂)
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
      if h : P j then
        update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i (c • a) (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
      else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)

Tactic:
repeat (rw [domDomRestrict_aux])

Premises used: MultilinearMap.domDomRestrict_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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_11 : DecidablePred P
z_1 : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
z : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
c : R
a : M₁ (↑i : ι)
⊢ (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (c • a)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) a) :
        M₂)

Tactic:
simp only [MultilinearMap.map_update_smul]

Premises used: MultilinearMap.map_update_smul
-- 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 : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : ι) → AddCommMonoid (M₁ i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M'
inst_6 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R M'
f_1 f' f : MultilinearMap R M₁ M₂
P : ι → Prop
inst_11 : DecidablePred P
z_1 : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
inst_12 : DecidableEq { a : ι // P a }
z : (i : { a : ι // P a }) → M₁ (↑i : ι)
i : { a : ι // P a }
c : R
a : M₁ (↑i : ι)
repeat repeat₁ repeat₂ :
  (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (c • a)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)
repeat₃ repeat₄ :
  (f : (a : (i : ι) → M₁ i) → M₂)
      (update (β := M₁)
        (fun (j : ι) ↦
          if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
        (↑i : ι) (c • a)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂)
          (update (β := M₁)
            (fun (j : ι) ↦
              if h : P j then z (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
              else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h))
            (↑i : ι) a) :
        M₂)
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
      if h : P j then
        update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i (c • a) (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
      else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h)) =
    HSMul.hSMul (β := M₂) c
      ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
          if h : P j then
            update (β := fun (i : { a : ι // P a }) ↦ M₁ (↑i : ι)) z i a (Subtype.mk (p := fun (a : ι) ↦ P a) j h)
          else z_1 (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
        M₂)

Tactic:
classical
    repeat (rw [domDomRestrict_aux])
    simp only [MultilinearMap.map_update_smul]

Premises used: MultilinearMap.map_update_smul, MultilinearMap.domDomRestrict_aux
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
P : ι → Prop
inst_5 : DecidablePred P
x : (i : { a : ι // P a }) → M₁ (↑i : ι)
z : (i : { a : ι // ¬P a }) → M₁ (↑i : ι)
⊢ Eq.{v₂ + 1} (α := M₂) ((f.domDomRestrict (M₁ := M₁) P z : (a : (i : { a : ι // P a }) → M₁ (↑i : ι)) → M₂) x : M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) fun (j : ι) ↦
        if h : P j then x (Subtype.mk (p := fun (a : ι) ↦ P a) j h) else z (Subtype.mk (p := fun (a : ι) ↦ ¬P a) j h) :
      M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
f : MultilinearMap R M₁ M₂
x y : (i : ι) → M₁ i
unfold :
  Eq.{v₂ + 1} (α := M₂)
    ((∑ i : ι, f.toLinearMap (M₁ := M₁) x i ∘ₗ LinearMap.proj (φ := M₁) i : (a : (i : ι) → M₁ i) → M₂) y : M₂)
    (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)) : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f.linearDeriv (M₁ := M₁) x : (a : (i : ι) → M₁ i) → M₂) y : M₂)
    (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)) : M₂)

Tactic:
unfold linearDeriv

Premises used: MultilinearMap.linearDeriv
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
inst_5 : DecidableEq ι
inst_6 : Fintype ι
f : MultilinearMap R M₁ M₂
x y : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂)
    ((∑ i : ι, f.toLinearMap (M₁ := M₁) x i ∘ₗ LinearMap.proj (φ := M₁) i : (a : (i : ι) → M₁ i) → M₂) y : M₂)
    (∑ i : ι, (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) x i (y i)) : M₂)

Tactic:
simp only [LinearMap.coe_sum, LinearMap.coe_comp, LinearMap.coe_proj, Finset.sum_apply,
    Function.comp_apply, Function.eval, toLinearMap_apply]

Premises used: Finset.sum_apply, LinearMap.coe_proj, LinearMap.coe_sum, Function.eval, LinearMap.coe_comp, Function.comp_apply, MultilinearMap.toLinearMap_apply
-- 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 : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → AddCommMonoid (M₁' i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M'
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M'
g : M₂ →ₗ[R] M₃
f : MultilinearMap R M₁ M₂
inst_13 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ Function.comp (β := M₂) (⇑g : (a : M₂) → M₃) (⇑f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + y)) =
    HAdd.hAdd (α := M₃)
      (Function.comp (β := M₂) (⇑g : (a : M₂) → M₃) (⇑f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x))
      (Function.comp (β := M₂) (⇑g : (a : M₂) → M₃) (⇑f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y))

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 : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → AddCommMonoid (M₁' i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid M'
inst_7 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_8 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R M'
g : M₂ →ₗ[R] M₃
f : MultilinearMap R M₁ M₂
inst_13 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ Function.comp (β := M₂) (⇑g : (a : M₂) → M₃) (⇑f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (c • x)) =
    HSMul.hSMul (β := M₃) c
      (Function.comp (β := M₂) (⇑g : (a : M₂) → M₃) (⇑f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
g : M₂ →ₗ[R] M₃
f : MultilinearMap R M₁ M₂
⊢ Eq (α := (a : (i : ι) → M₁ i) → M₃) (⇑(g.compMultilinearMap (M₁ := M₁) f) : (a : (i : ι) → M₁ i) → M₃)
    (Function.comp (β := M₂) (⇑g : (a : M₂) → M₃) (⇑f : (a : (i : ι) → M₁ i) → M₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
g : M₂ →ₗ[R] M₃
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
⊢ Eq.{v₃ + 1} (α := M₃) ((g.compMultilinearMap (M₁ := M₁) f : (a : (i : ι) → M₁ i) → M₃) m : M₃)
    ((g : (a : M₂) → M₃) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) : M₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst : Semiring 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₂
⊢ compMultilinearMap (M₁ := M₁) id f = f

Tactic:
rfl

Premises used: LinearMap.compMultilinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid M₄
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : Module R M₂
inst_7 : Module R M₃
inst_8 : Module R M₄
g : M₃ →ₗ[R] M₄
g' : M₂ →ₗ[R] M₃
f : MultilinearMap R M₁ M₂
⊢ (g ∘ₗ g').compMultilinearMap (M₁ := M₁) f = g.compMultilinearMap (M₁ := M₁) (g'.compMultilinearMap (M₁ := M₁) f)

Tactic:
rfl

Premises used: LinearMap.compMultilinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : (i : ι) → AddCommMonoid (M₁' i)
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_6 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_7 : Module R M₂
inst_8 : Module R M₃
g : M₂ →ₗ[R] M₃
f : MultilinearMap R M₁ M₂
f' : (i : ι) → LinearMap.{uR, uR, v₁', v₁} (RingHom.id R) (M₁' i) (M₁ i)
⊢ g.compMultilinearMap (M₁ := M₁') (f.compLinearMap (M₁ := M₁') (M₁' := M₁) f') =
    (g.compMultilinearMap (M₁ := M₁) f).compLinearMap (M₁ := M₁') (M₁' := M₁) f'

Tactic:
rfl

Premises used: MultilinearMap.compLinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
g : M₂ →ₗ[R] M₃
⊢ Eq (α := MultilinearMap R M₁ M₃) (g.compMultilinearMap (M₁ := M₁) 0) 0

Tactic:
MultilinearMap.ext fun _ => map_zero g

Premises used: map_zero, MultilinearMap.ext
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
f : MultilinearMap R M₁ M₂
⊢ Eq (α := MultilinearMap R M₁ M₃) (compMultilinearMap (M₁ := M₁) 0 f) 0

Tactic:
rfl

Premises used: LinearMap.compMultilinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
g : M₂ →ₗ[R] M₃
f₁ f₂ : MultilinearMap R M₁ M₂
⊢ g.compMultilinearMap (M₁ := M₁) (f₁ + f₂) = g.compMultilinearMap (M₁ := M₁) f₁ + g.compMultilinearMap (M₁ := M₁) f₂

Tactic:
MultilinearMap.ext fun _ => map_add g _ _

Premises used: map_add, MultilinearMap.ext, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M₁ i)
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_5 : Module R M₂
inst_6 : Module R M₃
g₁ g₂ : M₂ →ₗ[R] M₃
f : MultilinearMap R M₁ M₂
⊢ (g₁ + g₂).compMultilinearMap (M₁ := M₁) f = g₁.compMultilinearMap (M₁ := M₁) f + g₂.compMultilinearMap (M₁ := M₁) f

Tactic:
rfl

Premises used: LinearMap.compMultilinearMap, rfl