-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem hasStrictFDerivAt_apply (i : ι) (f : ∀ i, F' i) :
    HasStrictFDerivAt (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) (proj i) f

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f
⊢ HasStrictFDerivAt (fun f => f i) (proj i) f

Tactic:
have h' : comp (proj i) id' = proj i := by ext; simp [id']

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f
h' : (proj i).comp id' = proj i
⊢ HasStrictFDerivAt (fun f => f i) (proj i) f

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
⊢ HasStrictFDerivAt (fun f => f i) (proj i) f

Tactic:
have h := ((hasStrictFDerivAt_pi'
           (Φ := fun (f : ∀ i, F' i) (i' : ι) => f i') (Φ' := id') (x := f))).1

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f
⊢ HasStrictFDerivAt (fun f => f i) (proj i) f

Proof state:
case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f
x✝ : (i : ι) → F' i
⊢ ((proj i).comp id') x✝ = (proj i) x✝

Tactic:
simp [id']

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
⊢ HasStrictFDerivAt (fun f => f i) (proj i) f

Tactic:
let id' := ContinuousLinearMap.id 𝕜 (∀ i, F' i)

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
⊢ HasStrictFDerivAt (fun f => f i) (proj i) f

Proof state:
case a
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f
h' : (proj i).comp id' = proj i
⊢ HasStrictFDerivAt (fun f i' => f i') id' f

Tactic:
apply hasStrictFDerivAt_id

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f
h' : (proj i).comp id' = proj i
⊢ HasStrictFDerivAt (fun f => f i) ((proj i).comp id') f

Tactic:
apply h

Result:
case a
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f
h' : (proj i).comp id' = proj i
⊢ HasStrictFDerivAt (fun f i' => f i') id' f

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f
⊢ (proj i).comp id' = proj i

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f
x✝ : (i : ι) → F' i
⊢ ((proj i).comp id') x✝ = (proj i) x✝

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f
h' : (proj i).comp id' = proj i
⊢ HasStrictFDerivAt (fun f => f i) (proj i) f

Tactic:
rw [← h']

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
ι : Type u_6
inst✝² : Fintype ι
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasStrictFDerivAt (fun f i' => f i') id' f → ∀ (i : ι), HasStrictFDerivAt (fun x => x i) ((proj i).comp id') f
h' : (proj i).comp id' = proj i
⊢ HasStrictFDerivAt (fun f => f i) ((proj i).comp id') f