-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
inst_11 : Fintype ι
inst_12 : DecidableEq ι
a b : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N'
H :
  ∀ (x : ι → M),
    Eq.{u_6 + 1} (α := N')
      ((let __src : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N' :=
              ∑ σ : Perm ι,
                HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ (a + b));
            {
              toFun :=
                (⇑(∑ σ : Perm ι,
                      HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ)
                        (domDomCongr σ (a + b))) :
                  (a : (i : ι) → M) → N'),
              map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ } :
            (a : ι → M) → N')
          x :
        N')
      ((HAdd.hAdd (α := M [⋀^ι]→ₗ[R] N')
              (let __src : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N' :=
                ∑ σ : Perm ι,
                  HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ a);
              {
                toFun :=
                  (⇑(∑ σ : Perm ι,
                        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ)
                          (domDomCongr σ a)) :
                    (a : (i : ι) → M) → N'),
                map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→ₗ[R] N' })
              (let __src : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N' :=
                ∑ σ : Perm ι,
                  HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ b);
              {
                toFun :=
                  (⇑(∑ σ : Perm ι,
                        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ)
                          (domDomCongr σ b)) :
                    (a : (i : ι) → M) → N'),
                map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→ₗ[R] N' }) :
            (a : ι → M) → N')
          x :
        N')
⊢ (let __src : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N' :=
      ∑ σ : Perm ι,
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ (a + b));
    {
      toFun :=
        (⇑(∑ σ : Perm ι,
              HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ (a + b))) :
          (a : (i : ι) → M) → N'),
      map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ }) =
    HAdd.hAdd (α := M [⋀^ι]→ₗ[R] N')
      (let __src : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N' :=
        ∑ σ : Perm ι, HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ a);
      {
        toFun :=
          (⇑(∑ σ : Perm ι,
                HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ a)) :
            (a : (i : ι) → M) → N'),
        map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→ₗ[R] N' })
      (let __src : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N' :=
        ∑ σ : Perm ι, HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ b);
      {
        toFun :=
          (⇑(∑ σ : Perm ι,
                HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm ι →* ℤˣ) : (a : Perm ι) → ℤˣ) σ : ℤˣ) (domDomCongr σ b)) :
            (a : (i : ι) → M) → N'),
        map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := ⋯ : M [⋀^ι]→ₗ[R] N' })

Tactic:
ext