R : Type u
ι : Type u'
n✝ : ℕ
M : Fin (Nat.succ n✝) → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin (Nat.succ n✝)) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin (Nat.succ n✝)) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
ι' : Type ?u.776425
k l n : ℕ
s : Finset (Fin n)
hk : Finset.card s = k
hl : Finset.card (sᶜ) = l
f : MultilinearMap R (fun x => M') M₂
x y : M'
⊢ (↑(↑(↑(curryFinFinset R M₂ M' hk hl) f) fun x_1 => x) fun x => y) = ↑f (Finset.piecewise s (fun x_1 => x) fun x => y)
R : Type u
ι : Type u'
n✝ : ℕ
M : Fin (Nat.succ n✝) → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin (Nat.succ n✝)) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin (Nat.succ n✝)) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
ι' : Type ?u.776425
k l n : ℕ
s : Finset (Fin n)
hk : Finset.card s = k
hl : Finset.card (sᶜ) = l
f : MultilinearMap R (fun x => M') M₂
x y : M'
⊢ (↑f fun i => Sum.elim (fun x_1 => x) (fun x => y) (↑(finSumEquivOfFinset hk hl).symm i)) =
    ↑f (Finset.piecewise s (fun x_1 => x) fun x => y)
rw [← curryFinFinset_apply]
no goals
R : Type u
ι : Type u'
n✝ : ℕ
M : Fin (Nat.succ n✝) → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : Fin (Nat.succ n✝)) → AddCommMonoid (M i)
inst✝⁴ : AddCommMonoid M'
inst✝³ : AddCommMonoid M₂
inst✝² : (i : Fin (Nat.succ n✝)) → Module R (M i)
inst✝¹ : Module R M'
inst✝ : Module R M₂
ι' : Type ?u.776425
k l n : ℕ
s : Finset (Fin n)
hk : Finset.card s = k
hl : Finset.card (sᶜ) = l
f : MultilinearMap R (fun x => M') M₂
x y : M'
⊢ (↑(↑(↑(curryFinFinset R M₂ M' hk hl) f) fun x_1 => x) fun x => y) = ↑f (Finset.piecewise s (fun x_1 => x) fun x => y)
apply curryFinFinset_apply_const