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'_1 f f' : MultilinearMap R M₁ M₂
inst_11 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : 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 (c • x)) =
    HSMul.hSMul (β := M₂) c
      ((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))

Tactic:
simp [smul_add]

Premises used: smul_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 f' : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
⊢ (f + f' : (a : (i : ι) → M₁ i) → M₂) m =
    HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂) ((f' : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
rfl

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

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 : 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₂
inst_11 : DecidableEq ι
x : (i : ι) → M₁ i
x_1 : ι
c : R
x_2 : M₁ x_1
⊢ (fun (x : (i : ι) → M₁ i) ↦ (0 : M₂)) (update (β := M₁) x x_1 (c • x_2)) =
    HSMul.hSMul (β := M₂) c ((fun (x : (i : ι) → M₁ i) ↦ (0 : M₂)) (update (β := M₁) x x_1 x_2))

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₂
m : (i : ι) → M₁ i
⊢ Eq.{v₂ + 1} (α := M₂) ((0 : (a : (i : ι) → M₁ i) → M₂) m : M₂) (0 : M₂)

Tactic:
rfl

Premises used: 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 : DistribSMul S M₂
inst_12 : SMulCommClass R S M₂
c : S
f : MultilinearMap R M₁ M₂
inst_13 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ (fun (m : (i : ι) → M₁ i) ↦ HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂))
      (update (β := M₁) m i (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : ι) → M₁ i) ↦ HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂))
        (update (β := M₁) m i x))
      ((fun (m : (i : ι) → M₁ i) ↦ HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂))
        (update (β := M₁) m i y))

Tactic:
simp [smul_add]

Premises used: smul_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' : MultilinearMap R M₁ M₂
inst_11 : DistribSMul S M₂
inst_12 : SMulCommClass R S M₂
c : S
f : MultilinearMap R M₁ M₂
inst_13 : DecidableEq ι
l : (i : ι) → M₁ i
i : ι
x : R
d : M₁ i
⊢ (fun (m : (i : ι) → M₁ i) ↦ HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂))
      (update (β := M₁) l i (x • d)) =
    HSMul.hSMul (β := M₂) x
      ((fun (m : (i : ι) → M₁ i) ↦ HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂))
        (update (β := M₁) l i d))

Tactic:
simp [← smul_comm x c (_ : M₂)]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : 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 : DistribSMul S M₂
inst_6 : SMulCommClass R S M₂
f : MultilinearMap R M₁ M₂
c : S
m : (i : ι) → M₁ i
⊢ (c • f : (a : (i : ι) → M₁ i) → M₂) m = HSMul.hSMul (β := M₂) c ((f : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : 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 : DistribSMul S M₂
inst_6 : SMulCommClass R S M₂
c : S
f : MultilinearMap R M₁ M₂
⊢ (⇑(c • f) : (a : (i : ι) → M₁ i) → M₂) =
    HSMul.hSMul (β := (a : (i : ι) → M₁ i) → M₂) c (⇑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₂
α : Type u_1
f : α → MultilinearMap R M₁ M₂
s : Finset α
⊢ Eq (α := (a : (i : ι) → M₁ i) → M₂) (⇑(∑ a ∈ s, f a) : (a : (i : ι) → M₁ i) → M₂)
    (∑ a ∈ s, (⇑(f a) : (a : (i : ι) → M₁ i) → M₂))

Tactic:
map_sum coeAddMonoidHom f s

Premises used: MultilinearMap.coeAddMonoidHom, map_sum
-- 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₂
α : Type u_1
f : α → MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
s : Finset α
⊢ Eq.{v₂ + 1} (α := M₂) ((∑ a ∈ s, f a : (a : (i : ι) → M₁ i) → M₂) m : M₂)
    (∑ a ∈ s, (f a : (a : (i : ι) → M₁ i) → M₂) m : M₂)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : 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₂
inst_11 : 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:
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 : 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₂
inst_11 : 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 (α := R) (β := M₂) ((RingHom.id R : (a : R) → R) c : R)
      ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x) : 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 : 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₂
g : MultilinearMap R M₁ M₃
inst_11 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (x + y)),
      (g : (a : (i : ι) → M₁ i) → M₃) (update (β := M₁) m i (x + y))) =
    HAdd.hAdd (α := M₂ × M₃) (β := M₂ × M₃)
      (((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x),
          (g : (a : (i : ι) → M₁ i) → M₃) (update (β := M₁) m i x)) :
        M₂ × M₃)
      (((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i y),
          (g : (a : (i : ι) → M₁ i) → M₃) (update (β := M₁) m i y)) :
        M₂ × M₃)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : 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₂
g : MultilinearMap R M₁ M₃
inst_11 : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ ((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i (c • x)),
      (g : (a : (i : ι) → M₁ i) → M₃) (update (β := M₁) m i (c • x))) =
    HSMul.hSMul (β := M₂ × M₃) c
      (((f : (a : (i : ι) → M₁ i) → M₂) (update (β := M₁) m i x),
          (g : (a : (i : ι) → M₁ i) → M₃) (update (β := M₁) m i x)) :
        M₂ × M₃)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Multilinear.Basic
Goal:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst : 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 : Subsingleton ι
i : ι
f : M₂ →ₗ[R] M₃
inst_12 : DecidableEq ι
m : (i : ι) → M₂
i_1 : ι
x y : M₂
⊢ (f : (a : M₂) → M₃) (update (β := fun (x : ι) ↦ M₂) m i_1 (x + y) i) =
    HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : M₂) → M₃) (update (β := fun (x : ι) ↦ M₂) m i_1 x i) : M₃)
      ((f : (a : M₂) → M₃) (update (β := fun (x : ι) ↦ M₂) m i_1 y i) : M₃)

Tactic:
simp [update_eq_const_of_subsingleton]

Premises used: Function.update_eq_const_of_subsingleton
-- 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 : Subsingleton ι
i : ι
f : M₂ →ₗ[R] M₃
inst_12 : DecidableEq ι
m : (i : ι) → M₂
i_1 : ι
c : R
x : M₂
⊢ (f : (a : M₂) → M₃) (update (β := fun (x : ι) ↦ M₂) m i_1 (c • x) i) =
    HSMul.hSMul (β := M₃) c ((f : (a : M₂) → M₃) (update (β := fun (x : ι) ↦ M₂) m i_1 x i) : M₃)

Tactic:
simp [update_eq_const_of_subsingleton]

Premises used: Function.update_eq_const_of_subsingleton
-- 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 : Subsingleton ι
i : ι
f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃
x y : M₂
⊢ ((f : (a : (i : ι) → M₂) → M₃) fun (x_1 : ι) ↦ x + y) =
    HAdd.hAdd (α := M₃) (β := M₃) ((f : (a : (i : ι) → M₂) → M₃) fun (x_1 : ι) ↦ x : M₃)
      ((f : (a : (i : ι) → M₂) → M₃) fun (x : ι) ↦ y : M₃)

Tactic:
simpa [update_eq_const_of_subsingleton] using f.map_update_add 0 i x y

Premises used: MultilinearMap.map_update_add, Function.update_eq_const_of_subsingleton, 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 : Subsingleton ι
i : ι
f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃
c : R
x : M₂
⊢ ((f : (a : (i : ι) → M₂) → M₃) fun (x_1 : ι) ↦ c • x) =
    HSMul.hSMul (α := R) (β := M₃) ((RingHom.id R : (a : R) → R) c : R)
      ((f : (a : (i : ι) → M₂) → M₃) fun (x_1 : ι) ↦ x : M₃)

Tactic:
simpa [update_eq_const_of_subsingleton] using f.map_update_smul 0 i c x

Premises used: MultilinearMap.map_update_smul, Function.update_eq_const_of_subsingleton, 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 : Subsingleton ι
i : ι
f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃
H :
  ∀ (x : (i : ι) → M₂),
    Eq.{v₃ + 1} (α := M₃)
      (((fun (f : M₂ →ₗ[R] M₃) ↦
                (mk (M₁ := fun (x : ι) ↦ M₂) (fun (x : (i : ι) → M₂) ↦ (f : (a : M₂) → M₃) (x i)) ⋯ ⋯ :
                  MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃))
              ((fun (f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃) ↦
                  ({ toFun := fun (x : M₂) ↦ (f : (a : (i : ι) → M₂) → M₃) fun (x_1 : ι) ↦ x, map_add' := ⋯,
                      map_smul' := ⋯ } :
                    M₂ →ₗ[R] M₃))
                f) :
            (a : (i : ι) → M₂) → M₃)
          x :
        M₃)
      ((f : (a : (i : ι) → M₂) → M₃) x : M₃)
⊢ (fun (f : M₂ →ₗ[R] M₃) ↦
        (mk (M₁ := fun (x : ι) ↦ M₂) (fun (x : (i : ι) → M₂) ↦ (f : (a : M₂) → M₃) (x i)) ⋯ ⋯ :
          MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃))
      ((fun (f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃) ↦
          ({ toFun := fun (x : M₂) ↦ (f : (a : (i : ι) → M₂) → M₃) fun (x_1 : ι) ↦ x, map_add' := ⋯, map_smul' := ⋯ } :
            M₂ →ₗ[R] M₃))
        f) =
    f

Tactic:
ext 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 : Subsingleton ι
i : ι
f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃
x : (i : ι) → M₂
⊢ Eq.{v₃ + 1} (α := M₃)
    (((fun (f : M₂ →ₗ[R] M₃) ↦
              (mk (M₁ := fun (x : ι) ↦ M₂) (fun (x : (i : ι) → M₂) ↦ (f : (a : M₂) → M₃) (x i)) ⋯ ⋯ :
                MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃))
            ((fun (f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃) ↦
                ({ toFun := fun (x : M₂) ↦ (f : (a : (i : ι) → M₂) → M₃) fun (x_1 : ι) ↦ x, map_add' := ⋯,
                    map_smul' := ⋯ } :
                  M₂ →ₗ[R] M₃))
              f) :
          (a : (i : ι) → M₂) → M₃)
        x :
      M₃)
    ((f : (a : (i : ι) → M₂) → M₃) x : M₃)

Tactic:
congr_arg f ?_

Premises used: MultilinearMap.congr_arg
-- 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 : Subsingleton ι
i : ι
f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃
x : (i : ι) → M₂
H : (fun (x_1 : ι) ↦ x i) = x
⊢ Eq.{v₃ + 1} (α := M₃)
    (((fun (f : M₂ →ₗ[R] M₃) ↦
              (mk (M₁ := fun (x : ι) ↦ M₂) (fun (x : (i : ι) → M₂) ↦ (f : (a : M₂) → M₃) (x i)) ⋯ ⋯ :
                MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃))
            ((fun (f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃) ↦
                ({ toFun := fun (x : M₂) ↦ (f : (a : (i : ι) → M₂) → M₃) fun (x_1 : ι) ↦ x, map_add' := ⋯,
                    map_smul' := ⋯ } :
                  M₂ →ₗ[R] M₃))
              f) :
          (a : (i : ι) → M₂) → M₃)
        x :
      M₃)
    ((f : (a : (i : ι) → M₂) → M₃) x : M₃)

Tactic:
refine congr_arg f ?_

Premises used: MultilinearMap.congr_arg
-- 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 : Subsingleton ι
i : ι
f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃
x : (i : ι) → M₂
⊢ (fun (x_1 : ι) ↦ x i) = x

Tactic:
(eq_const_of_subsingleton _ _).symm

Premises used: eq_const_of_subsingleton, Eq.symm
-- 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 : Subsingleton ι
i : ι
f : MultilinearMap.{uR, uι, v₂, v₃} R (fun (x : ι) ↦ M₂) M₃
x : (i : ι) → M₂
⊢ (fun (x_1 : ι) ↦ x i) = x

Tactic:
exact (eq_const_of_subsingleton _ _).symm

Premises used: eq_const_of_subsingleton, Eq.symm