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.760748
k l n : ℕ
s : Finset (Fin n)
hk : Finset.card s = k
hl : Finset.card (sᶜ) = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
this :
  ↑(↑(LinearEquiv.symm (curryFinFinset R M₂ M' hk hl)) f) (Finset.piecewise s (fun x_1 => x) fun x => y) =
    ↑(↑f fun x_1 => x) fun x => y
⊢ (↑(↑f fun x_1 => x) fun i =>
      Finset.piecewise s (fun x_1 => x) (fun x => y) (↑(finSumEquivOfFinset hk hl) (Sum.inr i))) =
    ↑(↑f 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.760748
k l n : ℕ
s : Finset (Fin n)
hk : Finset.card s = k
hl : Finset.card (sᶜ) = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
⊢ (↑(↑f fun x_1 => x) fun i =>
      Finset.piecewise s (fun x_1 => x) (fun x => y) (↑(finSumEquivOfFinset hk hl) (Sum.inr i))) =
    ↑(↑f fun x_1 => x) fun x => y
have := curryFinFinset_symm_apply_piecewise_const hk hl f 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.760748
k l n : ℕ
s : Finset (Fin n)
hk : Finset.card s = k
hl : Finset.card (sᶜ) = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
this :
  (↑(↑f fun i => x) fun i =>
      Finset.piecewise s (fun x_1 => x) (fun x => y) (↑(finSumEquivOfFinset hk hl) (Sum.inr i))) =
    ↑(↑f fun i => x) fun x => y
⊢ (↑(↑f fun x_1 => x) fun i =>
      Finset.piecewise s (fun x_1 => x) (fun x => y) (↑(finSumEquivOfFinset hk hl) (Sum.inr i))) =
    ↑(↑f 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.760748
k l n : ℕ
s : Finset (Fin n)
hk : Finset.card s = k
hl : Finset.card (sᶜ) = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
this :
  ↑(↑(LinearEquiv.symm (curryFinFinset R M₂ M' hk hl)) f) (Finset.piecewise s (fun x_1 => x) fun x => y) =
    ↑(↑f fun x_1 => x) fun x => y
⊢ (↑(↑f fun x_1 => x) fun i =>
      Finset.piecewise s (fun x_1 => x) (fun x => y) (↑(finSumEquivOfFinset hk hl) (Sum.inr i))) =
    ↑(↑f fun x_1 => x) fun x => y
simp only [curryFinFinset_symm_apply, finSumEquivOfFinset_inl, Finset.orderEmbOfFin_mem,
Finset.piecewise_eq_of_mem, finSumEquivOfFinset_inr] at this
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.760748
k l n : ℕ
s : Finset (Fin n)
hk : Finset.card s = k
hl : Finset.card (sᶜ) = l
f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
x y : M'
this :
  (↑(↑f fun i => x) fun i =>
      Finset.piecewise s (fun x_1 => x) (fun x => y) (↑(finSumEquivOfFinset hk hl) (Sum.inr i))) =
    ↑(↑f fun i => x) fun x => y
⊢ (↑(↑f fun x_1 => x) fun i =>
      Finset.piecewise s (fun x_1 => x) (fun x => y) (↑(finSumEquivOfFinset hk hl) (Sum.inr i))) =
    ↑(↑f fun x_1 => x) fun x => y
exact this