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

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
⊢ (HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x) 0)
        { toFun := fun x => φ' x 0, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x ∧
      ∀ (i : Fin n),
        HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x) i.succ)
          { toFun := fun x => φ' x i.succ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x) ↔
    HasStrictFDerivAt φ { toFun := fun x => φ' x 0, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x ∧
      ∀ (i : Fin n),
        HasStrictFDerivAt (fun x => φs x i) { toFun := fun x => φ' x i.succ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
          x

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
⊢ HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x)) φ' x ↔
    HasStrictFDerivAt φ ((proj 0).comp φ') x ∧ HasStrictFDerivAt φs ((Pi.compRightL 𝕜 F' Fin.succ).comp φ') x

Tactic:
rw [hasStrictFDerivAt_pi', Fin.forall_fin_succ, hasStrictFDerivAt_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
⊢ (HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x) 0) ((proj 0).comp φ') x ∧
      ∀ (i : Fin n), HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x) i.succ) ((proj i.succ).comp φ') x) ↔
    HasStrictFDerivAt φ ((proj 0).comp φ') x ∧
      ∀ (i : Fin n), HasStrictFDerivAt (fun x => φs x i) ((proj i).comp ((Pi.compRightL 𝕜 F' Fin.succ).comp φ')) x

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
⊢ (HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x) 0) ((proj 0).comp φ') x ∧
      ∀ (i : Fin n), HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x) i.succ) ((proj i.succ).comp φ') x) ↔
    HasStrictFDerivAt φ ((proj 0).comp φ') x ∧
      ∀ (i : Fin n), HasStrictFDerivAt (fun x => φs x i) ((proj i).comp ((Pi.compRightL 𝕜 F' Fin.succ).comp φ')) x

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
⊢ (HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x) 0)
        { toFun := fun x => φ' x 0, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x ∧
      ∀ (i : Fin n),
        HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x) i.succ)
          { toFun := fun x => φ' x i.succ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x) ↔
    HasStrictFDerivAt φ { toFun := fun x => φ' x 0, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } x ∧
      ∀ (i : Fin n),
        HasStrictFDerivAt (fun x => φs x i) { toFun := fun x => φ' x i.succ, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
          x