Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: 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✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin n.succ) → Module R (M i)
inst✝³ : Module R M'
inst✝² : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝¹ : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
⊢ ∀ [inst : DecidableEq (ι ⊕ ι')] (m : (i : ι ⊕ ι') → N i) (i : ι ⊕ ι') (x y : N i),
    ((g fun i_1 ↦ update m i (x + y) (Sum.inl i_1)) fun i' ↦ update m i (x + y) (Sum.inr i')) =
      ((g fun i_1 ↦ update m i x (Sum.inl i_1)) fun i' ↦ update m i x (Sum.inr i')) +
        (g fun i_1 ↦ update m i y (Sum.inl i_1)) fun i' ↦ update m i y (Sum.inr i')

Tactic:
rintro _ _ (_ | _) _ _

Goal state after:
case inl
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✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : Module R M'
inst✝³ : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝² : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst✝ : DecidableEq (ι ⊕ ι')
m✝ : (i : ι ⊕ ι') → N i
val✝ : ι
x✝ y✝ : N (Sum.inl val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inr i')) =
    ((g fun i ↦ update m✝ (Sum.inl val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inl val✝) x✝ (Sum.inr i')) +
      (g fun i ↦ update m✝ (Sum.inl val✝) y✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inl val✝) y✝ (Sum.inr i')

case inr
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✝⁸ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : Module R M'
inst✝³ : Module R M₂
N : ι ⊕ ι' → Type u_1
inst✝² : (i : ι ⊕ ι') → AddCommMonoid (N i)
inst✝¹ : (i : ι ⊕ ι') → Module R (N i)
g : MultilinearMap R (fun i ↦ N (Sum.inl i)) (MultilinearMap R (fun i ↦ N (Sum.inr i)) M₂)
this✝ : DecidableEq ι := Classical.decEq ι
this : DecidableEq ι' := Classical.decEq ι'
inst✝ : DecidableEq (ι ⊕ ι')
m✝ : (i : ι ⊕ ι') → N i
val✝ : ι'
x✝ y✝ : N (Sum.inr val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inr val✝) (x✝ + y✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inr val✝) (x✝ + y✝) (Sum.inr i')) =
    ((g fun i ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inr i')) +
      (g fun i ↦ update m✝ (Sum.inr val✝) y✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inr val✝) y✝ (Sum.inr i')