Theorem: ContinuousMultilinearMap.curryLeft_compContinuousLinearMap (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)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
⊢ curryLeft (compContinuousLinearMap g f) =
    ContinuousLinearMap.comp (compContinuousLinearMapL fun i => f (Fin.succ i))
      (ContinuousLinearMap.comp (curryLeft g) (f 0))
Tactic:
ext u m
State after:
case h.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)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ ((curryLeft (compContinuousLinearMap g f)) u) m =
    ((ContinuousLinearMap.comp (compContinuousLinearMapL fun i => f (Fin.succ i))
          (ContinuousLinearMap.comp (curryLeft g) (f 0)))
        u)
      m

State before:
case h.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)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ ((curryLeft (compContinuousLinearMap g f)) u) m =
    ((ContinuousLinearMap.comp (compContinuousLinearMapL fun i => f (Fin.succ i))
          (ContinuousLinearMap.comp (curryLeft g) (f 0)))
        u)
      m
Tactic:
simp
State after:
case h.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)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ (g fun i => (f i) (Fin.cons u m i)) = g (Fin.cons ((f 0) u) fun i => (f (Fin.succ i)) (m i))

State before:
case h.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)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ (g fun i => (f i) (Fin.cons u m i)) = g (Fin.cons ((f 0) u) fun i => (f (Fin.succ i)) (m i))
Tactic:
congr
State after:
case h.H.h.e_6.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)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ (fun i => (f i) (Fin.cons u m i)) = Fin.cons ((f 0) u) fun i => (f (Fin.succ i)) (m i)

State before:
case h.H.h.e_6.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)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ (fun i => (f i) (Fin.cons u m i)) = Fin.cons ((f 0) u) fun i => (f (Fin.succ i)) (m i)
Tactic:
ext i
State after:
case h.H.h.e_6.h.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)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
i : Fin (n + 1)
⊢ (f i) (Fin.cons u m i) = Fin.cons ((f 0) u) (fun i => (f (Fin.succ i)) (m i)) i

State before:
case h.H.h.e_6.h.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)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
i : Fin (n + 1)
⊢ (f i) (Fin.cons u m i) = Fin.cons ((f 0) u) (fun i => (f (Fin.succ i)) (m i)) i
Tactic:
refine Fin.cases ?_ ?_ i <;> simp
State after:
no goals