-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
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'
⊢ (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' })
have 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' := sorry, map_update_smul' := sorry, map_eq_zero_of_eq' := sorry } :
          (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' := sorry, map_update_smul' := sorry, map_eq_zero_of_eq' := sorry : 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' := sorry, map_update_smul' := sorry, map_eq_zero_of_eq' := sorry : M [⋀^ι]→ₗ[R] N' }) :
          (a : ι → M) → N')
        x :
      N')
Tactic: ext