-- Lean 4 proof step from Mathlib.LinearAlgebra.Multilinear.Curry (goal)
Goal:
R : Type uR
S : Type uS
ι : Type uι
ι' : Type uι'
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst : CommSemiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid M₂
inst_4 : (i : Fin n.succ) → Module.{uR, v} R (M i)
inst_5 : Module R M'
inst_6 : Module R M₂
p : Fin (n + 1)
f : M p →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x y : M i
x₁ :
  ∀ (x y : M p),
    (fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
                (a : (i : Fin n) → M (p.succAbove i)) → M₂)
              (p.removeNth (α := M) m) :
            M₂))
        (update (β := M) m p (x + y)) =
      HAdd.hAdd (α := M₂)
        ((fun (m : (i : Fin n.succ) → M i) ↦
            ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                    MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
                  (a : (i : Fin n) → M (p.succAbove i)) → M₂)
                (p.removeNth (α := M) m) :
              M₂))
          (update (β := M) m p x))
        ((fun (m : (i : Fin n.succ) → M i) ↦
            ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                    MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
                  (a : (i : Fin n) → M (p.succAbove i)) → M₂)
                (p.removeNth (α := M) m) :
              M₂))
          (update (β := M) m p y))
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
              (a : (i : Fin n) → M (p.succAbove i)) → M₂)
            (p.removeNth (α := M) m) :
          M₂))
      (update (β := M) m i (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
                (a : (i : Fin n) → M (p.succAbove i)) → M₂)
              (p.removeNth (α := M) m) :
            M₂))
        (update (β := M) m i x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
                (a : (i : Fin n) → M (p.succAbove i)) → M₂)
              (p.removeNth (α := M) m) :
            M₂))
        (update (β := M) m i y))
have p₁ : ∀ (j : Fin n) (x y : M (p.succAbove j)),
  (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
              (a : (i : Fin n) → M (p.succAbove i)) → M₂)
            (p.removeNth (α := M) m) :
          M₂))
      (update (β := M) m (p.succAbove j) (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
                (a : (i : Fin n) → M (p.succAbove i)) → M₂)
              (p.removeNth (α := M) m) :
            M₂))
        (update (β := M) m (p.succAbove j) x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M p) → MultilinearMap R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) (m p) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M (p.succAbove i)) M₂) :
                (a : (i : Fin n) → M (p.succAbove i)) → M₂)
              (p.removeNth (α := M) m) :
            M₂))
        (update (β := M) m (p.succAbove j) y))
Tactic: cases i using Fin.succAboveCases p
Cleared hypotheses: i, x, y