-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorPower.Pairing (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
this :
  ∀ (x : DecidableEq (Fin n)) (f : Fin n → Module.Dual R M) (φ : Module.Dual R M) (i j : Fin n) (v : Fin n → M),
    Eq.{u_1 + 1} (α := R) ((Function.update (β := fun (a : Fin n) ↦ Module.Dual R M) f i φ j : (a : M) → R) (v j) : R)
      (Function.update (β := fun (j : Fin n) ↦ R) (fun (j : Fin n) ↦ (f j : (a : M) → R) (v j)) i
          ((φ : (a : M) → R) (v i)) j :
        R)
inst_3 : DecidableEq (Fin n)
f : (i : Fin n) → Module.Dual R M
i : Fin n
φ₁ φ₂ : Module.Dual R M
v : (i : Fin n) → M
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin n) ↦ M)
            ((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
              (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                (MultilinearMap.mkPiRing R (Fin n) 1)
                (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i (φ₁ + φ₂))))
            (tprod R (s := fun (i : Fin n) ↦ M)) :
          (a : (i : Fin n) → M) → R)
        v :
      R)
    ((LinearMap.compMultilinearMap (M₁ := fun (i : Fin n) ↦ M)
            (HAdd.hAdd (α := Module.Dual R (⨂[R]^n M)) (β := Module.Dual R (⨂[R]^n M))
              ((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                    (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
                  (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                    (MultilinearMap.mkPiRing R (Fin n) 1)
                    (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ₁)) :
                (⨂[R] (i : Fin n), M) →ₗ[R] R)
              ((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                    (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
                  (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                    (MultilinearMap.mkPiRing R (Fin n) 1)
                    (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ₂)) :
                (⨂[R] (i : Fin n), M) →ₗ[R] R))
            (tprod R (s := fun (i : Fin n) ↦ M)) :
          (a : (i : Fin n) → M) → R)
        v :
      R)
have H : (((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
            (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
          (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
            (MultilinearMap.mkPiRing R (Fin n) 1)
            (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i (φ₁ + φ₂))) :
        (⨂[R] (i : Fin n), M) →ₗ[R] R) :
      (a : ⨂[R] (i : Fin n), M) → R)
    ((tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) =
  HAdd.hAdd (α := R) (β := R)
    ((((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
              (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                (MultilinearMap.mkPiRing R (Fin n) 1)
                (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ₁)) :
            (⨂[R] (i : Fin n), M) →ₗ[R] R) :
          (a : ⨂[R] (i : Fin n), M) → R)
        ((tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) :
      R)
    ((((PiTensorProduct.lift (s := fun (x : Fin n) ↦ M) :
                (a : MultilinearMap R (fun (x : Fin n) ↦ M) R) → (⨂[R] (i : Fin n), M) →ₗ[R] R)
              (MultilinearMap.compLinearMap (M₁ := fun (x : Fin n) ↦ M) (M₁' := fun (x : Fin n) ↦ R)
                (MultilinearMap.mkPiRing R (Fin n) 1)
                (Function.update (β := fun (x : Fin n) ↦ Module.Dual R M) f i φ₂)) :
            (⨂[R] (i : Fin n), M) →ₗ[R] R) :
          (a : ⨂[R] (i : Fin n), M) → R)
        ((tprod R (s := fun (i : Fin n) ↦ M) : (a : (i : Fin n) → M) → ⨂[R] (i : Fin n), M) v : ⨂[R] (i : Fin n), M) :
      R)
Tactic: dsimp