no goals
R : Type u_4
inst✝¹⁰ : Semiring R
M : Type u_3
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_2
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type ?u.42102
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type ?u.42132
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type ?u.42520
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
ι : Type u_1
ι' : Type ?u.42911
ι'' : Type ?u.42914
f✝ f' : AlternatingMap R M N ι
g g₂ : AlternatingMap R M N' ι
g' : AlternatingMap R M' N' ι
v : ι → M
v' : ι → M'
f : (ι → M) → N
h₁ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M), f (update m i (x + y)) = f (update m i x) + f (update m i y)
h₂ : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M), f (update m i (c • x)) = c • f (update m i x)
h₃ :
  ∀ (v : ι → M) (i j : ι),
    v i = v j →
      i ≠ j →
        MultilinearMap.toFun
            { toFun := f,
              map_add' :=
                (_ :
                  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M),
                    f (update m i (x + y)) = f (update m i x) + f (update m i y)),
              map_smul' :=
                (_ :
                  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M),
                    f (update m i (c • x)) = c • f (update m i x)) }
            v =
          0
⊢ ↑{
        toMultilinearMap :=
          { toFun := f,
            map_add' :=
              (_ :
                ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M),
                  f (update m i (x + y)) = f (update m i x) + f (update m i y)),
            map_smul' :=
              (_ :
                ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M),
                  f (update m i (c • x)) = c • f (update m i x)) },
        map_eq_zero_of_eq' := h₃ } =
    { toFun := f, map_add' := h₁, map_smul' := h₂ }
simp