-- Module: Mathlib.LinearAlgebra.TensorPower.Pairing
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
H :
  ∀ (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)
⊢ (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 (φ₁ + φ₂))) =
    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)

Tactic:
ext v