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 f' g : MultilinearMap R M₁ M₂
toFun : ((i : ι) → M₁ i) → M₂
map_update_add' :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun (update (β := M₁) m i (x + y)) = toFun (update (β := M₁) m i x) + toFun (update (β := M₁) m i y)
map_update_smul' :
  ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun (update (β := M₁) m i (c • x)) = c • toFun (update (β := M₁) m i x)
h :
  Eq (α := (a : (i : ι) → M₁ i) → M₂)
    ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁))
      (MultilinearMap.mk (M₁ := M₁) toFun map_update_add' map_update_smul'))
    ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁)) g)
mk :
  ∀ (toFun_1 : ((i : ι) → M₁ i) → M₂)
    (map_update_add'_1 :
      ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
        toFun_1 (update (β := M₁) m i (x + y)) = toFun_1 (update (β := M₁) m i x) + toFun_1 (update (β := M₁) m i y))
    (map_update_smul'_1 :
      ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
        toFun_1 (update (β := M₁) m i (c • x)) = c • toFun_1 (update (β := M₁) m i x))
    (h :
      Eq (α := (a : (i : ι) → M₁ i) → M₂)
        ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁))
          (MultilinearMap.mk (M₁ := M₁) toFun map_update_add' map_update_smul'))
        ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁))
          (MultilinearMap.mk (M₁ := M₁) toFun_1 map_update_add'_1 map_update_smul'_1))),
    MultilinearMap.mk (M₁ := M₁) toFun map_update_add' map_update_smul' =
      MultilinearMap.mk (M₁ := M₁) toFun_1 map_update_add'_1 map_update_smul'_1
⊢ MultilinearMap.mk (M₁ := M₁) toFun map_update_add' map_update_smul' = g

Tactic:
cases g
-- 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 f' : MultilinearMap R M₁ M₂
toFun : ((i : ι) → M₁ i) → M₂
map_update_add' :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun (update (β := M₁) m i (x + y)) = toFun (update (β := M₁) m i x) + toFun (update (β := M₁) m i y)
map_update_smul' :
  ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun (update (β := M₁) m i (c • x)) = c • toFun (update (β := M₁) m i x)
toFun_1 : ((i : ι) → M₁ i) → M₂
map_update_add'_1 :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun_1 (update (β := M₁) m i (x + y)) = toFun_1 (update (β := M₁) m i x) + toFun_1 (update (β := M₁) m i y)
map_update_smul'_1 :
  ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun_1 (update (β := M₁) m i (c • x)) = c • toFun_1 (update (β := M₁) m i x)
h :
  Eq (α := (a : (i : ι) → M₁ i) → M₂)
    ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁))
      (MultilinearMap.mk (M₁ := M₁) toFun map_update_add' map_update_smul'))
    ((fun (f : MultilinearMap R M₁ M₂) ↦ f.toFun (M₁ := M₁))
      (MultilinearMap.mk (M₁ := M₁) toFun_1 map_update_add'_1 map_update_smul'_1))
mk :
  ∀
    (map_update_add'_2 :
      ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
        toFun (update (β := M₁) m i (x + y)) = toFun (update (β := M₁) m i x) + toFun (update (β := M₁) m i y))
    (map_update_smul'_2 :
      ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
        toFun (update (β := M₁) m i (c • x)) = c • toFun (update (β := M₁) m i x)),
    MultilinearMap.mk (M₁ := M₁) toFun map_update_add' map_update_smul' =
      MultilinearMap.mk (M₁ := M₁) toFun map_update_add'_2 map_update_smul'_2
⊢ MultilinearMap.mk (M₁ := M₁) toFun map_update_add' map_update_smul' =
    MultilinearMap.mk (M₁ := M₁) toFun_1 map_update_add'_1 map_update_smul'_1

Tactic:
cases h
-- 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 f' : MultilinearMap R M₁ M₂
toFun : ((i : ι) → M₁ i) → M₂
map_update_add' :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun (update (β := M₁) m i (x + y)) = toFun (update (β := M₁) m i x) + toFun (update (β := M₁) m i y)
map_update_smul' :
  ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun (update (β := M₁) m i (c • x)) = c • toFun (update (β := M₁) m i x)
map_update_add'_1 :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    toFun (update (β := M₁) m i (x + y)) = toFun (update (β := M₁) m i x) + toFun (update (β := M₁) m i y)
map_update_smul'_1 :
  ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    toFun (update (β := M₁) m i (c • x)) = c • toFun (update (β := M₁) m i x)
⊢ mk (M₁ := M₁) toFun map_update_add' map_update_smul' = mk (M₁ := M₁) toFun map_update_add'_1 map_update_smul'_1

Tactic:
rfl
-- 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 : DecidableEq ι
f : ((i : ι) → M₁ i) → M₂
h₁ :
  ∀ (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    f (update (β := M₁) m i (x + y)) = f (update (β := M₁) m i x) + f (update (β := M₁) m i y)
h₂ :
  ∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (update (β := M₁) m i (c • x)) = c • f (update (β := M₁) m i x)
inst_12 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update (β := M₁) m i (x + y)) = f (update (β := M₁) m i x) + f (update (β := M₁) m i y)

Tactic:
h₁ m i x y
-- 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 : DecidableEq ι
f : ((i : ι) → M₁ i) → M₂
h₁ :
  ∀ (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    f (update (β := M₁) m i (x + y)) = f (update (β := M₁) m i x) + f (update (β := M₁) m i y)
h₂ :
  ∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (update (β := M₁) m i (c • x)) = c • f (update (β := M₁) m i x)
inst_12 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update (β := M₁) m i (x + y)) = f (update (β := M₁) m i x) + f (update (β := M₁) m i y)

Tactic:
convert! h₁ m i x y
-- 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 : DecidableEq ι
f : ((i : ι) → M₁ i) → M₂
h₁ :
  ∀ (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    f (update (β := M₁) m i (x + y)) = f (update (β := M₁) m i x) + f (update (β := M₁) m i y)
h₂ :
  ∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (update (β := M₁) m i (c • x)) = c • f (update (β := M₁) m i x)
inst_12 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ f (update (β := M₁) m i (c • x)) = c • f (update (β := M₁) m i x)

Tactic:
h₂ m i c 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 : 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 : DecidableEq ι
f : ((i : ι) → M₁ i) → M₂
h₁ :
  ∀ (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    f (update (β := M₁) m i (x + y)) = f (update (β := M₁) m i x) + f (update (β := M₁) m i y)
h₂ :
  ∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (update (β := M₁) m i (c • x)) = c • f (update (β := M₁) m i x)
inst_12 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ f (update (β := M₁) m i (c • x)) = c • f (update (β := M₁) m i x)

Tactic:
convert! h₂ m i c x
-- 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₂
⊢ f.toFun (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₂
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 : ((i : ι) → M₁ i) → M₂
h₁ :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    f (update (β := M₁) m i (x + y)) = f (update (β := M₁) m i x) + f (update (β := M₁) m i y)
h₂ :
  ∀ [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    f (update (β := M₁) m i (c • x)) = c • f (update (β := M₁) m i x)
⊢ (⇑(mk (M₁ := M₁) f h₁ h₂) : (a : (i : ι) → M₁ i) → M₂) = f

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 g : MultilinearMap R M₁ M₂
h : f = g
x : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂) ((g : (a : (i : ι) → M₁ i) → M₂) x : M₂)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- 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₂
x y : (i : ι) → M₁ i
h : x = y
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂) ((f : (a : (i : ι) → M₁ i) → M₂) y : M₂)

Tactic:
DFunLike.congr_arg f h

Premises used: DFunLike.congr_arg
-- 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₂
⊢ Injective (α := MultilinearMap R M₁ M₂) (β := (a : (i : ι) → M₁ i) → M₂)
    (DFunLike.coe (β := fun (x : (i : ι) → M₁ i) ↦ M₂))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- 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 g : MultilinearMap R M₁ M₂
⊢ Eq (α := (a : (i : ι) → M₁ i) → M₂) (⇑f : (a : (i : ι) → M₁ i) → M₂) (⇑g : (a : (i : ι) → M₁ i) → M₂) ↔ f = g

Tactic:
DFunLike.coe_fn_eq

Premises used: DFunLike.coe_fn_eq
-- 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 f' : MultilinearMap R M₁ M₂
H :
  ∀ (x : (i : ι) → M₁ i),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂) ((f' : (a : (i : ι) → M₁ i) → M₂) x : M₂)
⊢ f = f'

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- 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₂
h₁ :
  ∀ [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
    (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + y)) =
      HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
        ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)
h₂ :
  ∀ [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
    (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (c • x)) =
      HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
⊢ mk (M₁ := M₁) (⇑f : (a : (i : ι) → M₁ i) → M₂) h₁ h₂ = f

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₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + y)) =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y) : M₂)

Tactic:
f.map_update_add' m i x y

Premises used: MultilinearMap.map_update_add'
-- 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₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ (f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (c • x)) =
    HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : M₂)

Tactic:
f.map_update_smul' m i c x

Premises used: MultilinearMap.map_update_smul'
-- 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₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
⊢ HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0

Tactic:
simp
-- 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₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
⊢ HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0

Tactic:
have : (0 : R) • (0 : M₁ i) = 0 := by simp
-- 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₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
this : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0
rw : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (m i)) : M₂) (0 : M₂)
rw₁ : Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) (0 : M₂)
rw₂ :
  Eq.{v₂ + 1} (α := M₂)
    ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0)) : M₂)
    (0 : M₂)
rw₃ : HSMul.hSMul.{uR, v₂, v₂} (α := R) (β := M₂) 0 ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) = 0
rw₄ rw₅ : Eq.{v₂ + 1} (α := M₂) 0 0
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)

Tactic:
rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]

Premises used: MultilinearMap.map_update_smul, Function.update_eq_self, zero_smul
-- 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₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
have : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0
have₁ :
  ∀ (this : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)
have₂ : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0
have₃ have₄ :
  ∀ (this : HSMul.hSMul.{uR, v₁, v₁} (α := R) (β := M₁ i) 0 0 = 0),
    Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)

Tactic:
classical
    have : (0 : R) • (0 : M₁ i) = 0 := by simp
    rw [← update_eq_self i m, h, ← this, f.map_update_smul, zero_smul]

Premises used: zero_smul
-- 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₂
inst_5 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i 0) : M₂) (0 : M₂)

Tactic:
f.map_coord_zero i (update_self i 0 m)

Premises used: MultilinearMap.map_coord_zero, Function.update_self, OfNat.ofNat
-- 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₂
inst_5 : Nonempty ι
⊢ ∃ (i : ι), Membership.mem (γ := Set ι) Set.univ i

Tactic:
Set.exists_mem_of_nonempty ι

Premises used: Set.exists_mem_of_nonempty
-- 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₂
inst_5 : Nonempty ι
obtain :
  ∀ (i : ι),
    Membership.mem (γ := Set ι) Set.univ i → Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) 0 : M₂) (0 : M₂)
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) 0 : M₂) (0 : M₂)

Tactic:
obtain ⟨i, _⟩ : ∃ i : ι, i ∈ Set.univ := Set.exists_mem_of_nonempty ι

Premises used: Set.univ, Set.exists_mem_of_nonempty
-- 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₂
inst_5 : Nonempty ι
i : ι
h : Membership.mem (γ := Set ι) Set.univ i
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) 0 : M₂) (0 : M₂)

Tactic:
map_coord_zero f i rfl

Premises used: MultilinearMap.map_coord_zero, 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₂
inst_5 : Nonempty ι
i : ι
h : Membership.mem (γ := Set ι) Set.univ i
⊢ Eq.{v₂ + 1} (α := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) 0 : M₂) (0 : M₂)

Tactic:
exact map_coord_zero f i rfl

Premises used: MultilinearMap.map_coord_zero
-- 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'_1 f f' : MultilinearMap R M₁ M₂
inst_11 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ (fun (x : (i : ι) → M₁ i) ↦
        HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
          ((f' : (a : (i : ι) → M₁ i) → M₂) x : M₂))
      (update (β := M₁) m i (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (x : (i : ι) → M₁ i) ↦
          HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
            ((f' : (a : (i : ι) → M₁ i) → M₂) x : M₂))
        (update (β := M₁) m i x))
      ((fun (x : (i : ι) → M₁ i) ↦
          HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) x : M₂)
            ((f' : (a : (i : ι) → M₁ i) → M₂) x : M₂))
        (update (β := M₁) m i y))

Tactic:
simp [add_left_comm, add_assoc]

Premises used: add_left_comm, add_assoc