Theorem: continuousMultilinearCurryLeftEquiv_curryLeft (ForML/IndexDeriv.lean)

State before:
ι : Type u_1
𝕜 : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
g : ContinuousMultilinearMap 𝕜 M₁ F
⊢ (continuousMultilinearCurryLeftEquiv 𝕜 M₁ F) (ContinuousMultilinearMap.curryLeft g) = g
Tactic:
ext x
State after:
case H
ι : Type u_1
𝕜 : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
g : ContinuousMultilinearMap 𝕜 M₁ F
x : (i : Fin (Nat.succ n)) → M₁ i
⊢ ((continuousMultilinearCurryLeftEquiv 𝕜 M₁ F) (ContinuousMultilinearMap.curryLeft g)) x = g x

State before:
case H
ι : Type u_1
𝕜 : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
g : ContinuousMultilinearMap 𝕜 M₁ F
x : (i : Fin (Nat.succ n)) → M₁ i
⊢ ((continuousMultilinearCurryLeftEquiv 𝕜 M₁ F) (ContinuousMultilinearMap.curryLeft g)) x = g x
Tactic:
simp
State after:
no goals