-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem hasFDerivWithinAt_apply (i : ι) (f : ∀ i, F' i) (s' : Set (∀ i, F' i)) :
    HasFDerivWithinAt (𝕜 := 𝕜) (fun f : ∀ i, F' i => f i) (proj i) s' 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
s' : Set ((i : ι) → F' i)
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
⊢ HasFDerivWithinAt (fun f => f i) (proj i) s' f

Tactic:
have h := ((hasFDerivWithinAt_pi'
           (Φ := fun (f : ∀ i, F' i) (i' : ι) => f i') (Φ' := id') (x := f) (s := s'))).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
s' : Set ((i : ι) → F' i)
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasFDerivWithinAt (fun f i' => f i') id' s' f → ∀ (i : ι), HasFDerivWithinAt (fun x => x i) ((proj i).comp id') s' f
⊢ HasFDerivWithinAt (fun f => f i) (proj i) s' 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
s' : Set ((i : ι) → F' i)
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasFDerivWithinAt (fun f i' => f i') id' s' f → ∀ (i : ι), HasFDerivWithinAt (fun x => x i) ((proj i).comp id') s' f
h' : (proj i).comp id' = proj i
⊢ HasFDerivWithinAt (fun f => f i) ((proj i).comp id') s' 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
s' : Set ((i : ι) → F' i)
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasFDerivWithinAt (fun f i' => f i') id' s' f → ∀ (i : ι), HasFDerivWithinAt (fun x => x i) ((proj i).comp id') s' f
h' : (proj i).comp id' = proj i
⊢ HasFDerivWithinAt (fun f i' => f i') id' s' 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
s' : Set ((i : ι) → F' i)
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasFDerivWithinAt (fun f i' => f i') id' s' f → ∀ (i : ι), HasFDerivWithinAt (fun x => x i) ((proj i).comp id') s' f
⊢ (proj i).comp id' = proj i

Tactic:
rfl

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
s' : Set ((i : ι) → F' i)
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasFDerivWithinAt (fun f i' => f i') id' s' f → ∀ (i : ι), HasFDerivWithinAt (fun x => x i) ((proj i).comp id') s' f
⊢ HasFDerivWithinAt (fun f => f i) (proj i) s' f

Tactic:
have h' : comp (proj i) id' = proj i := by rfl

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
s' : Set ((i : ι) → F' i)
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasFDerivWithinAt (fun f i' => f i') id' s' f → ∀ (i : ι), HasFDerivWithinAt (fun x => x i) ((proj i).comp id') s' f
h' : (proj i).comp id' = proj i
⊢ HasFDerivWithinAt (fun f => f i) (proj i) s' 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
s' : Set ((i : ι) → F' i)
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasFDerivWithinAt (fun f i' => f i') id' s' f → ∀ (i : ι), HasFDerivWithinAt (fun x => x i) ((proj i).comp id') s' f
h' : (proj i).comp id' = proj i
⊢ HasFDerivWithinAt (fun f i' => f i') id' s' f

Tactic:
apply hasFDerivWithinAt_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
s' : Set ((i : ι) → F' i)
⊢ HasFDerivWithinAt (fun f => f i) (proj i) s' 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
s' : Set ((i : ι) → F' i)
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
⊢ HasFDerivWithinAt (fun f => f i) (proj i) s' 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
s' : Set ((i : ι) → F' i)
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasFDerivWithinAt (fun f i' => f i') id' s' f → ∀ (i : ι), HasFDerivWithinAt (fun x => x i) ((proj i).comp id') s' f
h' : (proj i).comp id' = proj i
⊢ HasFDerivWithinAt (fun f => f i) (proj i) s' 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
s' : Set ((i : ι) → F' i)
id' : ((i : ι) → F' i) →L[𝕜] (i : ι) → F' i := ContinuousLinearMap.id 𝕜 ((i : ι) → F' i)
h : HasFDerivWithinAt (fun f i' => f i') id' s' f → ∀ (i : ι), HasFDerivWithinAt (fun x => x i) ((proj i).comp id') s' f
h' : (proj i).comp id' = proj i
⊢ HasFDerivWithinAt (fun f => f i) ((proj i).comp id') s' f