-- Mathlib/Analysis/Calculus/FDeriv/Prod.lean
theorem hasFDerivAtFilter_finCons
    {φ' : E →L[𝕜] Π i, F' i} {l : Filter E} :
    HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) φ' x l ↔
      HasFDerivAtFilter φ (.proj 0 ∘L φ') x l ∧
      HasFDerivAtFilter φs (Pi.compRightL 𝕜 F' Fin.succ ∘L φ') x l

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter E
⊢ (HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x) 0) ((proj 0).comp φ') x l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x) i.succ) ((proj i.succ).comp φ') x l) ↔
    HasFDerivAtFilter φ ((proj 0).comp φ') x l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x => φs x i) ((proj i).comp ((Pi.compRightL 𝕜 F' Fin.succ).comp φ')) x l

Tactic:
dsimp [ContinuousLinearMap.comp, LinearMap.comp, Function.comp_def]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter E
⊢ (HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x) 0)
        { toFun := fun x => φ' x 0, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x) i.succ)
          { toFun := fun x => φ' x i.succ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x l) ↔
    HasFDerivAtFilter φ { toFun := fun x => φ' x 0, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun x => φs x i) { toFun := fun x => φ' x i.succ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
          x l

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter E
⊢ (HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x) 0)
        { toFun := fun x => φ' x 0, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x) i.succ)
          { toFun := fun x => φ' x i.succ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x l) ↔
    HasFDerivAtFilter φ { toFun := fun x => φ' x 0, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun x => φs x i) { toFun := fun x => φ' x i.succ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
          x l

Tactic:
simp only [Fin.cons_zero, Fin.cons_succ]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter E
⊢ HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x)) φ' x l ↔
    HasFDerivAtFilter φ ((proj 0).comp φ') x l ∧ HasFDerivAtFilter φs ((Pi.compRightL 𝕜 F' Fin.succ).comp φ') x l

Tactic:
rw [hasFDerivAtFilter_pi', Fin.forall_fin_succ, hasFDerivAtFilter_pi']

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter E
⊢ (HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x) 0) ((proj 0).comp φ') x l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x => Fin.cons (φ x) (φs x) i.succ) ((proj i.succ).comp φ') x l) ↔
    HasFDerivAtFilter φ ((proj 0).comp φ') x l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x => φs x i) ((proj i).comp ((Pi.compRightL 𝕜 F' Fin.succ).comp φ')) x l