case H.h
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₂
f : MultilinearMap R (fun i => M (↑castSucc i)) (M (last n) →ₗ[R] M₂)
m : (i : Fin n) → M (↑castSucc i)
x : M (last n)
⊢ ↑(↑(curryRight (uncurryRight f)) m) x = ↑(↑f m) x
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₂
f : MultilinearMap R (fun i => M (↑castSucc i)) (M (last n) →ₗ[R] M₂)
⊢ curryRight (uncurryRight f) = f
ext (m x)
case H.h
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₂
f : MultilinearMap R (fun i => M (↑castSucc i)) (M (last n) →ₗ[R] M₂)
m : (i : Fin n) → M (↑castSucc i)
x : M (last n)
⊢ ↑(↑f (init (snoc m x))) x = ↑(↑f m) x
case H.h
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₂
f : MultilinearMap R (fun i => M (↑castSucc i)) (M (last n) →ₗ[R] M₂)
m : (i : Fin n) → M (↑castSucc i)
x : M (last n)
⊢ ↑(↑(curryRight (uncurryRight f)) m) x = ↑(↑f m) x
simp only [snoc_last, MultilinearMap.curryRight_apply, MultilinearMap.uncurryRight_apply]
no goals
case H.h
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₂
f : MultilinearMap R (fun i => M (↑castSucc i)) (M (last n) →ₗ[R] M₂)
m : (i : Fin n) → M (↑castSucc i)
x : M (last n)
⊢ ↑(↑f (init (snoc m x))) x = ↑(↑f m) x
rw [init_snoc]