-- 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₂
f : M 0 →ₗ[R] MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂
m : (i : Fin n.succ) → M i
i : Fin n.succ
x y : M i
zero :
  ∀ (x y : M 0),
    (fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m 0 (x + y)) =
      HAdd.hAdd (α := M₂)
        ((fun (m : (i : Fin n.succ) → M i) ↦
            ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                    MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                  (a : (i : Fin n) → M i.succ) → M₂)
                (tail (α := M) m) :
              M₂))
          (update (β := M) m 0 x))
        ((fun (m : (i : Fin n.succ) → M i) ↦
            ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                    MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                  (a : (i : Fin n) → M i.succ) → M₂)
                (tail (α := M) m) :
              M₂))
          (update (β := M) m 0 y))
⊢ (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
              (a : (i : Fin n) → M i.succ) → M₂)
            (tail (α := M) m) :
          M₂))
      (update (β := M) m i (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m i x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m i y))
have succ : ∀ (i : Fin n) (x y : M i.succ),
  (fun (m : (i : Fin n.succ) → M i) ↦
        ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
              (a : (i : Fin n) → M i.succ) → M₂)
            (tail (α := M) m) :
          M₂))
      (update (β := M) m i.succ (x + y)) =
    HAdd.hAdd (α := M₂)
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m i.succ x))
      ((fun (m : (i : Fin n.succ) → M i) ↦
          ((((f : (a : M 0) → MultilinearMap R (fun (i : Fin n) ↦ M i.succ) M₂) (m 0) :
                  MultilinearMap.{uR, 0, v, v₂} R (fun (i : Fin n) ↦ M i.succ) M₂) :
                (a : (i : Fin n) → M i.succ) → M₂)
              (tail (α := M) m) :
            M₂))
        (update (β := M) m i.succ y))
Tactic: cases i using Fin.cases
Cleared hypotheses: i, x, y