awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n_1 : ℕ
M : Fin n_1.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_1.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_1.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' : MultilinearMap R M₁ M₂
k n : ℕ
f : MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin n) ↦ M') M₂
s : Finset (Fin n)
hk : #s = k
z : M'
⊢ ∀ [inst_11 : DecidableEq (Fin k)] (m : (i : Fin k) → M') (i : Fin k) (x y : M'),
    ((f : (a : (i : Fin n) → M') → M₂) fun (j : Fin n) ↦
        if h : j ∈ s then
          update (β := fun (x : Fin k) ↦ M') m i (x + y)
            ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) j h))
        else z) =
      HAdd.hAdd (α := M₂) (β := M₂)
        ((f : (a : (i : Fin n) → M') → M₂) fun (j : Fin n) ↦
            if h : j ∈ s then
              update (β := fun (x : Fin k) ↦ M') m i x
                ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k)
                  (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) j h))
            else z :
          M₂)
        ((f : (a : (i : Fin n) → M') → M₂) fun (j : Fin n) ↦
            if h : j ∈ s then
              update (β := fun (x : Fin k) ↦ M') m i y
                ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k)
                  (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) j h))
            else z :
          M₂)

Tactic:
simp [dite_comp_equiv_update (s.orderIsoOfFin hk).symm]

Premises used: Finset.orderIsoOfFin, dite_comp_equiv_update, OrderIso.symm
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n_1 : ℕ
M : Fin n_1.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_1.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_1.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' : MultilinearMap R M₁ M₂
k n : ℕ
f : MultilinearMap.{uR, 0, v', v₂} R (fun (x : Fin n) ↦ M') M₂
s : Finset (Fin n)
hk : #s = k
z : M'
⊢ ∀ [inst_11 : DecidableEq (Fin k)] (m : (i : Fin k) → M') (i : Fin k) (c : R) (x : M'),
    ((f : (a : (i : Fin n) → M') → M₂) fun (j : Fin n) ↦
        if h : j ∈ s then
          update (β := fun (x : Fin k) ↦ M') m i (c • x)
            ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k) (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) j h))
        else z) =
      HSMul.hSMul (β := M₂) c
        ((f : (a : (i : Fin n) → M') → M₂) fun (j : Fin n) ↦
            if h : j ∈ s then
              update (β := fun (x : Fin k) ↦ M') m i x
                ((OrderIso.symm (s.orderIsoOfFin hk) : (a : ↥s) → Fin k)
                  (Subtype.mk (p := fun (x : Fin n) ↦ x ∈ s) j h))
            else z :
          M₂)

Tactic:
simp [dite_comp_equiv_update (s.orderIsoOfFin hk).symm]

Premises used: Finset.orderIsoOfFin, dite_comp_equiv_update, OrderIso.symm
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
x y : M 0
simp_rw :
  (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 (x + y)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) y m) : M₂)
simp_rw₁ :
  HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 x) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 y) : M₂) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) y m) : M₂)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) (x + y) m) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) y m) : M₂)

Tactic:
simp_rw [← update_cons_zero x m (x + y), f.map_update_add, update_cons_zero]

Premises used: MultilinearMap.map_update_add, Fin.update_cons_zero, HAdd.hAdd
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.succ
c : R
x : M 0
simp_rw :
  (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 (c • x)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
simp_rw₁ :
  HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (Fin.cons (α := M) x m) 0 x) : M₂) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) (c • x) m) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (Fin.cons (α := M) x m) : M₂)

Tactic:
simp_rw [← update_cons_zero x m (c • x), f.map_update_smul, update_cons_zero]

Premises used: MultilinearMap.map_update_smul, Fin.update_cons_zero, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
x y : M (last n)
simp_rw :
  (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) (x + y)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m y) : M₂)
simp_rw₁ :
  HAdd.hAdd (α := M₂) (β := M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) x) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) y) : M₂) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m y) : M₂)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m (x + y)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m y) : M₂)

Tactic:
simp_rw [← update_snoc_last x m (x + y), f.map_update_add, update_snoc_last]

Premises used: MultilinearMap.map_update_add, HAdd.hAdd, Fin.update_snoc_last
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
c : R
x : M (last n)
simp_rw :
  (f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) (c • x)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
simp_rw₁ :
  HSMul.hSMul (β := M₂) c
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (update (β := M) (snoc (α := M) m x) (last n) x) : M₂) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m (c • x)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (snoc (α := M) m x) : M₂)

Tactic:
simp_rw [← update_snoc_last x m (c • x), f.map_update_smul, update_snoc_last]

Premises used: MultilinearMap.map_update_smul, Fin.update_snoc_last, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
p : Fin (n + 1)
m : (i : Fin n) → M (p.succAbove i)
x y : M p
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) (x + y) m) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) x m) : M₂)
      ((f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) y m) : M₂)

Tactic:
simpa using f.map_update_add (p.insertNth 0 m) p x y

Premises used: MultilinearMap.map_update_add, Fin.insertNth, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M₂
inst_3 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_4 : Module R M₂
f : MultilinearMap R M M₂
p : Fin (n + 1)
m : (i : Fin n) → M (p.succAbove i)
c : R
x : M p
⊢ (f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) (c • x) m) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : Fin n.succ) → M i) → M₂) (p.insertNth (α := M) x m) : M₂)

Tactic:
simpa using f.map_update_smul (p.insertNth 0 m) p c x

Premises used: MultilinearMap.map_update_smul, Fin.insertNth, OfNat.ofNat
-- 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' : MultilinearMap R M₁ M₂
inst_11 : (i : ι) → AddCommMonoid (M₁' i)
inst_12 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_13 : (i : ι) → AddCommMonoid (M₁'' i)
inst_14 : (i : ι) → Module.{uR, v₁''} R (M₁'' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
inst_15 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ ∀ (j : ι) (z : M₁ i),
    Eq.{v₁' + 1} (α := M₁' j) ((f j : (a : M₁ j) → M₁' j) (update (β := M₁) m i z j) : M₁' j)
      (update (β := M₁') (fun (k : ι) ↦ (f k : (a : M₁ k) → M₁' k) (m k)) i ((f i : (a : M₁ i) → M₁' i) z) j : M₁' j)

Tactic:
have : ∀ j z, f j (update m i z j) = update (fun k => f k (m k)) i (f i z) j := fun j z =>
      Function.apply_update (fun k => f k) _ _ _ _
-- 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' : MultilinearMap R M₁ M₂
inst_11 : (i : ι) → AddCommMonoid (M₁' i)
inst_12 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_13 : (i : ι) → AddCommMonoid (M₁'' i)
inst_14 : (i : ι) → Module.{uR, v₁''} R (M₁'' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
inst_15 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
this :
  ∀ (j : ι) (z : M₁ i),
    Eq.{v₁' + 1} (α := M₁' j) ((f j : (a : M₁ j) → M₁' j) (update (β := M₁) m i z j) : M₁' j)
      (update (β := M₁') (fun (k : ι) ↦ (f k : (a : M₁ k) → M₁' k) (m k)) i ((f i : (a : M₁ i) → M₁' i) z) j : M₁' j)
⊢ ((g : (a : (i : ι) → M₁' i) → M₂) fun (i_1 : ι) ↦
      (f i_1 : (a : M₁ i_1) → M₁' i_1) (update (β := M₁) m i (x + y) i_1)) =
    HAdd.hAdd (α := M₂) (β := M₂)
      ((g : (a : (i : ι) → M₁' i) → M₂) fun (i_1 : ι) ↦ (f i_1 : (a : M₁ i_1) → M₁' i_1) (update (β := M₁) m i x i_1) :
        M₂)
      ((g : (a : (i : ι) → M₁' i) → M₂) fun (i_1 : ι) ↦ (f i_1 : (a : M₁ i_1) → M₁' i_1) (update (β := M₁) m i y i_1) :
        M₂)

Tactic:
simp [this]
-- 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' : MultilinearMap R M₁ M₂
inst_11 : (i : ι) → AddCommMonoid (M₁' i)
inst_12 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_13 : (i : ι) → AddCommMonoid (M₁'' i)
inst_14 : (i : ι) → Module.{uR, v₁''} R (M₁'' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
inst_15 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ ∀ (j : ι) (z : M₁ i),
    Eq.{v₁' + 1} (α := M₁' j) ((f j : (a : M₁ j) → M₁' j) (update (β := M₁) m i z j) : M₁' j)
      (update (β := M₁') (fun (k : ι) ↦ (f k : (a : M₁ k) → M₁' k) (m k)) i ((f i : (a : M₁ i) → M₁' i) z) j : M₁' j)

Tactic:
have : ∀ j z, f j (update m i z j) = update (fun k => f k (m k)) i (f i z) j := fun j z =>
      Function.apply_update (fun k => f k) _ _ _ _
-- 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' : MultilinearMap R M₁ M₂
inst_11 : (i : ι) → AddCommMonoid (M₁' i)
inst_12 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_13 : (i : ι) → AddCommMonoid (M₁'' i)
inst_14 : (i : ι) → Module.{uR, v₁''} R (M₁'' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
inst_15 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
this :
  ∀ (j : ι) (z : M₁ i),
    Eq.{v₁' + 1} (α := M₁' j) ((f j : (a : M₁ j) → M₁' j) (update (β := M₁) m i z j) : M₁' j)
      (update (β := M₁') (fun (k : ι) ↦ (f k : (a : M₁ k) → M₁' k) (m k)) i ((f i : (a : M₁ i) → M₁' i) z) j : M₁' j)
⊢ ((g : (a : (i : ι) → M₁' i) → M₂) fun (i_1 : ι) ↦
      (f i_1 : (a : M₁ i_1) → M₁' i_1) (update (β := M₁) m i (c • x) i_1)) =
    HSMul.hSMul (β := M₂) c
      ((g : (a : (i : ι) → M₁' i) → M₂) fun (i_1 : ι) ↦ (f i_1 : (a : M₁ i_1) → M₁' i_1) (update (β := M₁) m i x i_1) :
        M₂)

Tactic:
simp [this]
-- 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 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → AddCommMonoid (M₁' i)
inst_6 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
m : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂) ((g.compLinearMap (M₁ := M₁) (M₁' := M₁') f : (a : (i : ι) → M₁ i) → M₂) m : M₂)
    ((g : (a : (i : ι) → M₁' i) → M₂) fun (i : ι) ↦ (f i : (a : M₁ i) → M₁' 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₁''
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 : (i : ι) → AddCommMonoid (M₁' i)
inst_6 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
inst_7 : (i : ι) → AddCommMonoid (M₁'' i)
inst_8 : (i : ι) → Module.{uR, v₁''} R (M₁'' i)
g : MultilinearMap R M₁'' M₂
f₁ : (i : ι) → LinearMap.{uR, uR, v₁', v₁''} (RingHom.id R) (M₁' i) (M₁'' i)
f₂ : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
⊢ (g.compLinearMap (M₁ := M₁') (M₁' := M₁'') f₁).compLinearMap (M₁ := M₁) (M₁' := M₁') f₂ =
    g.compLinearMap (M₁ := M₁) (M₁' := M₁'') fun (i : ι) ↦ f₁ i ∘ₗ f₂ i

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 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → AddCommMonoid (M₁' i)
inst_6 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
⊢ Eq (α := MultilinearMap R M₁ M₂) (compLinearMap (M₁ := M₁) (M₁' := M₁') 0 f) 0

Tactic:
ext fun _ => rfl

Premises used: MultilinearMap.ext, rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
ι : Type uι
M₁' : ι → Type v₁'
M₂ : Type v₂
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : (i : ι) → AddCommMonoid (M₁' i)
inst_4 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
g : MultilinearMap R M₁' M₂
⊢ (g.compLinearMap (M₁ := M₁') (M₁' := M₁') fun (x : ι) ↦ LinearMap.id) = g

Tactic:
ext fun _ => rfl

Premises used: MultilinearMap.ext, 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 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → AddCommMonoid (M₁' i)
inst_6 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
hf : ∀ (i : ι), Surjective.{v₁ + 1, v₁' + 1} (α := M₁ i) (β := M₁' i) (⇑(f i) : (a : M₁ i) → M₁' i)
g₁ g₂ : MultilinearMap R M₁' M₂
h :
  Eq (α := MultilinearMap R M₁ M₂) ((fun (g : MultilinearMap R M₁' M₂) ↦ g.compLinearMap (M₁ := M₁) (M₁' := M₁') f) g₁)
    ((fun (g : MultilinearMap R M₁' M₂) ↦ g.compLinearMap (M₁ := M₁) (M₁' := M₁') f) g₂)
x : (i : ι) → M₁' i
⊢ Eq.{v₂ + 1} (α := M₂) ((g₁ : (a : (i : ι) → M₁' i) → M₂) x : M₂) ((g₂ : (a : (i : ι) → M₁' i) → M₂) x : M₂)

Tactic:
simpa [fun i => surjInv_eq (hf i)]
      using MultilinearMap.ext_iff.mp h fun i => surjInv (hf i) (x i)

Premises used: Function.surjInv, Function.surjInv_eq, Iff.mp, MultilinearMap.ext_iff
-- 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 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → AddCommMonoid (M₁' i)
inst_6 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
f : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
hf : ∀ (i : ι), Surjective.{v₁ + 1, v₁' + 1} (α := M₁ i) (β := M₁' i) (⇑(f i) : (a : M₁ i) → M₁' i)
g₁ g₂ : MultilinearMap R M₁' M₂
⊢ g₁.compLinearMap (M₁ := M₁) (M₁' := M₁') f = g₂.compLinearMap (M₁ := M₁) (M₁' := M₁') f ↔ g₁ = g₂

Tactic:
(compLinearMap_injective _ hf).eq_iff

Premises used: MultilinearMap.compLinearMap_injective, Function.Injective.eq_iff
-- 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 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → AddCommMonoid (M₁' i)
inst_6 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → LinearEquiv.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
set :
  let f' : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) := fun (i : ι) ↦
    (↑(f i) : M₁ i →ₗ[R] M₁' i);
  g.compLinearMap (M₁ := M₁) (M₁' := M₁') f' = 0 ↔ g = 0
⊢ Eq (α := MultilinearMap R M₁ M₂) (g.compLinearMap (M₁ := M₁) (M₁' := M₁') fun (i : ι) ↦ (↑(f i) : M₁ i →ₗ[R] M₁' i))
      0 ↔
    g = 0

Tactic:
set f' := fun i => (f i : M₁ i →ₗ[R] M₁' i)

Premises used: LinearEquiv.toLinearMap
-- 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 : (i : ι) → Module.{uR, v₁} R (M₁ i)
inst_4 : Module R M₂
inst_5 : (i : ι) → AddCommMonoid (M₁' i)
inst_6 : (i : ι) → Module.{uR, v₁'} R (M₁' i)
g : MultilinearMap R M₁' M₂
f : (i : ι) → LinearEquiv.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i)
f' : (i : ι) → LinearMap.{uR, uR, v₁, v₁'} (RingHom.id R) (M₁ i) (M₁' i) := fun (i : ι) ↦ (↑(f i) : M₁ i →ₗ[R] M₁' i)
rw : g.compLinearMap (M₁ := M₁) (M₁' := M₁') f' = compLinearMap (M₁ := M₁) (M₁' := M₁') 0 f' ↔ g = 0
rw₁ rw₂ : g = 0 ↔ g = 0
⊢ g.compLinearMap (M₁ := M₁) (M₁' := M₁') f' = 0 ↔ g = 0

Tactic:
rw [← zero_compLinearMap f', compLinearMap_inj f' fun i => (f i).surjective]

Premises used: LinearEquiv.surjective, MultilinearMap.zero_compLinearMap, MultilinearMap.compLinearMap_inj