-- Mathlib/Analysis/Calculus/FDeriv/Pi.lean
theorem hasFDerivAt_update (x : ∀ i, E i) {i : ι} (y : E i) :
    HasFDerivAt (Function.update x i) (.pi (Pi.single i (.id 𝕜 (E i)))) y

Proof state:
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
update_eq : Function.update x i = (fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i
⊢ HasFDerivAt ((fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i) l y

Tactic:
convert (hasFDerivAt_const _ _).add (l.hasFDerivAt.comp y (hasFDerivAt_sub_const (x i)))

Result:
case h.e'_12.h.h
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
update_eq : Function.update x i = (fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i
e_8✝ : Pi.addCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : Pi.module ι E 𝕜 = NormedSpace.toModule
e_10✝ : Pi.topologicalSpace = UniformSpace.toTopologicalSpace
⊢ l = 0 + l.comp (ContinuousLinearMap.id 𝕜 (E i))

Proof state:
case pos
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
t : E i
j : ι
hji : j = i
⊢ ⋯ ▸ t = x j + (⋯ ▸ ContinuousLinearMap.id 𝕜 (E i)) (t - x i)

Tactic:
subst hji

Result:
case pos
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
j : ι
y : E j
l : E j →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single j (ContinuousLinearMap.id 𝕜 (E j)))
t : E j
⊢ ⋯ ▸ t = x j + (⋯ ▸ ContinuousLinearMap.id 𝕜 (E j)) (t - x j)

Proof state:
case h.h
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
t : E i
j : ι
⊢ Function.update x i t j = ((fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i) t j

Tactic:
dsimp [l, Pi.single, Function.update]

Result:
case h.h
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
t : E i
j : ι
⊢ (if h : j = i then ⋯ ▸ t else x j) = x j + (if h : j = i then ⋯ ▸ ContinuousLinearMap.id 𝕜 (E i) else 0) (t - x i)

Proof state:
case pos
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
j : ι
y : E j
l : E j →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single j (ContinuousLinearMap.id 𝕜 (E j)))
t : E j
⊢ ⋯ ▸ t = x j + (⋯ ▸ ContinuousLinearMap.id 𝕜 (E j)) (t - x j)

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
⊢ HasFDerivAt (Function.update x i) (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))) y

Tactic:
set l := (ContinuousLinearMap.pi (Pi.single i (.id 𝕜 (E i))))

Result:
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
⊢ HasFDerivAt (Function.update x i) l y

Proof state:
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
update_eq : Function.update x i = (fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i
⊢ HasFDerivAt (Function.update x i) l y

Tactic:
rw [update_eq]

Result:
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
update_eq : Function.update x i = (fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i
⊢ HasFDerivAt ((fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i) l y

Proof state:
case h.h
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
t : E i
j : ι
⊢ (if h : j = i then ⋯ ▸ t else x j) = x j + (if h : j = i then ⋯ ▸ ContinuousLinearMap.id 𝕜 (E i) else 0) (t - x i)

Tactic:
split_ifs with hji

Result:
case pos
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
t : E i
j : ι
hji : j = i
⊢ ⋯ ▸ t = x j + (⋯ ▸ ContinuousLinearMap.id 𝕜 (E i)) (t - x i)

case neg
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
t : E i
j : ι
hji : ¬j = i
⊢ x j = x j + 0 (t - x i)

Proof state:
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
⊢ Function.update x i = (fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i

Tactic:
ext t j

Result:
case h.h
𝕜 : Type u_1
ι : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
l : E i →L[𝕜] (i : ι) → E i := ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))
t : E i
j : ι
⊢ Function.update x i t j = ((fun x_1 => x) + ⇑l ∘ fun x_1 => x_1 - x i) t j