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