Theorem: HasFDerivAt.hasDerivAt_comp_update (ForML/IndexDerivBasic.lean)

State before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasDerivAt (fun u => f (Function.update x i u)) (f' (Pi.single i 1)) (x i)
Tactic:
change HasDerivAt (f ∘ Function.update x i) _ _
State after:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)

State before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)
Tactic:
have : HasFDerivAt (f ∘ Function.update x i) (f'.comp (.pi (Pi.single i (.id 𝕜 𝕜)))) (x i)
State after:
case this
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)

ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)

State before:
case this
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)

ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)
Tactic:
. refine HasFDerivAt.comp _ (by simpa using hf) (hasFDerivAt_update x _)
State after:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)

State before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ HasDerivAt (f ∘ Function.update x i) (f' (Pi.single i 1)) (x i)
Tactic:
refine HasDerivAt.congr_deriv this.hasDerivAt ?_
State after:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) 1 =
    f' (Pi.single i 1)

State before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) 1 =
    f' (Pi.single i 1)
Tactic:
simp
State after:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (f' fun i_1 => (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i_1) 1) = f' (Pi.single i 1)

State before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (f' fun i_1 => (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i_1) 1) = f' (Pi.single i 1)
Tactic:
refine congrArg _ ?_
State after:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (fun i_1 => (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i_1) 1) = Pi.single i 1

State before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
⊢ (fun i_1 => (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i_1) 1) = Pi.single i 1
Tactic:
ext j
State after:
case h
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j

State before:
case h
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Tactic:
by_cases h : j = i
State after:
case pos
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j

case neg
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : ¬j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j

State before:
case pos
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j

case neg
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : ¬j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Tactic:
. rw [h]; simp
State after:
case neg
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : ¬j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j

State before:
case neg
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : ¬j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Tactic:
. simp [h]
State after:
no goals

State before:
case this
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
Tactic:
refine HasFDerivAt.comp _ (by simpa using hf) (hasFDerivAt_update x _)
State after:
no goals

State before:
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
⊢ HasFDerivAt f f' (Function.update x i (x i))
Tactic:
simpa using hf
State after:
no goals

State before:
case pos
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Tactic:
rw [h]
State after:
case pos
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i) 1 = Pi.single i 1 i

State before:
case pos
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) i) 1 = Pi.single i 1 i
Tactic:
simp
State after:
no goals

State before:
case neg
ι : Type u_1
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
i : ι
f : (ι → 𝕜) → F
f' : (ι → 𝕜) →L[𝕜] F
x : ι → 𝕜
hf : HasFDerivAt f f' x
this :
  HasFDerivAt (f ∘ Function.update x i)
    (ContinuousLinearMap.comp f' (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜)))) (x i)
j : ι
h : ¬j = i
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 𝕜) j) 1 = Pi.single i 1 j
Tactic:
simp [h]
State after:
no goals