Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: 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✝ : ι
c✝ : R
x✝ : N (Sum.inl val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inl val✝) (c✝ • x✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inl val✝) (c✝ • x✝) (Sum.inr i')) =
    c✝ • (g fun i ↦ update m✝ (Sum.inl val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inl val✝) x✝ (Sum.inr i')

pp: 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✝ : ι'
c✝ : R
x✝ : N (Sum.inr val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inr val✝) (c✝ • x✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inr val✝) (c✝ • x✝) (Sum.inr i')) =
    c✝ • (g fun i ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inr i')

Tactic:
<;>

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✝ : ι
c✝ : R
x✝ : N (Sum.inl val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inl val✝) (c✝ • x✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inl val✝) (c✝ • x✝) (Sum.inr i')) =
    c✝ • (g fun i ↦ update m✝ (Sum.inl val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inl val✝) x✝ (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✝ : ι'
c✝ : R
x✝ : N (Sum.inr val✝)
⊢ ((g fun i ↦ update m✝ (Sum.inr val✝) (c✝ • x✝) (Sum.inl i)) fun i' ↦
      update m✝ (Sum.inr val✝) (c✝ • x✝) (Sum.inr i')) =
    c✝ • (g fun i ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inl i)) fun i' ↦ update m✝ (Sum.inr val✝) x✝ (Sum.inr i')