awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_6
F' : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (F' i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
s' : Set ((i : ι) → F' i)
h : HasFDerivWithinAt (𝕜 := 𝕜) (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) (proj (φ := F') i) s' f
f' : ((i : ι) → F' i) →L[𝕜] F' i
⊢ DifferentiableWithinAt 𝕜 (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) s' f

Tactic:
apply HasFDerivWithinAt.differentiableWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
ι : Type u_6
F' : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (F' i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
⊢ DifferentiableAt 𝕜 Φ x ↔ ∀ (i : ι), DifferentiableAt.{u_1, u_2, u_7} 𝕜 (F := F' i) (fun (x : E) ↦ Φ x i) x

Tactic:
⟨fun h i => (hasFDerivAt_pi'.1 h.hasFDerivAt i).differentiableAt, fun h =>
    (hasFDerivAt_pi.2 fun i => (h i).hasFDerivAt).differentiableAt⟩

Premises used: Iff.mpr, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, Iff.intro, Iff.mp, hasFDerivAt_pi', hasFDerivAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
ι : Type u_6
F' : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (F' i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
hφ : ∀ (i : ι), DifferentiableAt.{u_1, u_2, u_7} 𝕜 (F := F' i) (fun (x : E) ↦ Φ x i) x
⊢ DifferentiableAt 𝕜 Φ x

Tactic:
differentiableAt_pi.2 hφ

Premises used: Iff.mpr, differentiableAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_6
F' : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (F' i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
⊢ DifferentiableAt 𝕜 (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) f

Tactic:
⟨_, hasFDerivAt_apply ..⟩

Premises used: DifferentiableAt, hasFDerivAt_apply, Exists.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_6
F' : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (F' i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
⊢ DifferentiableOn 𝕜 Φ s ↔ ∀ (i : ι), DifferentiableOn.{u_1, u_2, u_7} 𝕜 (F := F' i) (fun (x : E) ↦ Φ x i) s

Tactic:
⟨fun h i x hx => differentiableWithinAt_pi.1 (h x hx) i, fun h x hx =>
    differentiableWithinAt_pi.2 fun i => h i x hx⟩

Premises used: Iff.mpr, differentiableWithinAt_pi, Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_6
F' : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (F' i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
hφ : ∀ (i : ι), DifferentiableOn.{u_1, u_2, u_7} 𝕜 (F := F' i) (fun (x : E) ↦ Φ x i) s
⊢ DifferentiableOn 𝕜 Φ s

Tactic:
differentiableOn_pi.2 hφ

Premises used: Iff.mpr, differentiableOn_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_6
F' : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (F' i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
i : ι
s' : Set ((i : ι) → F' i)
⊢ DifferentiableOn 𝕜 (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) s'

Tactic:
fun _ _ ↦ differentiableWithinAt_apply ..

Premises used: DifferentiableOn, differentiableWithinAt_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_6
F' : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (F' i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
⊢ Differentiable 𝕜 Φ ↔ ∀ (i : ι), Differentiable.{u_1, u_2, u_7} 𝕜 (F := F' i) fun (x : E) ↦ Φ x i

Tactic:
⟨fun h i x => differentiableAt_pi.1 (h x) i, fun h x => differentiableAt_pi.2 fun i => h i x⟩

Premises used: Iff.mpr, Iff.intro, Iff.mp, differentiableAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_6
F' : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (F' i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
hφ : ∀ (i : ι), Differentiable.{u_1, u_2, u_7} 𝕜 (F := F' i) fun (x : E) ↦ Φ x i
⊢ Differentiable 𝕜 Φ

Tactic:
differentiable_pi.2 hφ

Premises used: Iff.mpr, differentiable_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_6
F' : ι → Type u_7
inst_1 : (i : ι) → NormedAddCommGroup (F' i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
i : ι
x : (i : ι) → F' i
⊢ DifferentiableAt 𝕜 (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) x

Tactic:
apply differentiableAt_apply

Premises used: differentiableAt_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
ι : Type u_6
F' : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (F' i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
φ : (i : ι) → E → F' i
h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (φ i) s x
hs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] (i : ι) → F' i)
    (fderivWithin 𝕜 (F := (i : ι) → F' i) (fun (x : E) (i : ι) ↦ φ i x) s x : E →L[𝕜] (i : ι) → F' i)
    (ContinuousLinearMap.pi (φ := F') fun (i : ι) ↦ fderivWithin 𝕜 (φ i) s x : E →L[𝕜] (i : ι) → F' i)

Tactic:
(hasFDerivWithinAt_pi.2 fun i => (h i).hasFDerivWithinAt).fderivWithin hs

Premises used: Iff.mpr, HasFDerivWithinAt.fderivWithin, hasFDerivWithinAt_pi, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
ι : Type u_6
F' : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (F' i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
φ : (i : ι) → E → F' i
h : ∀ (i : ι), DifferentiableAt 𝕜 (φ i) x
⊢ Eq (α := E →L[𝕜] (i : ι) → F' i)
    (fderiv 𝕜 (F := (i : ι) → F' i) (fun (x : E) (i : ι) ↦ φ i x) x : E →L[𝕜] (i : ι) → F' i)
    (ContinuousLinearMap.pi (φ := F') fun (i : ι) ↦ fderiv 𝕜 (φ i) x : E →L[𝕜] (i : ι) → F' i)

Tactic:
(hasFDerivAt_pi.2 fun i => (h i).hasFDerivAt).fderiv

Premises used: Iff.mpr, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, hasFDerivAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
ι : Type u_6
F' : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (F' i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
hΦ : DifferentiableWithinAt 𝕜 Φ s x
hs : UniqueDiffWithinAt 𝕜 s x
i : ι
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_7} (RingHom.id 𝕜) E (F' i)) (fderivWithin 𝕜 (fun (x : E) ↦ Φ x i) s x)
    (comp (σ₂₃ := RingHom.id 𝕜) (proj (φ := F') i : ((i : ι) → F' i) →L[𝕜] F' i)
      (fderivWithin 𝕜 Φ s x : E →L[𝕜] (i : ι) → F' i))

Tactic:
(hasFDerivWithinAt_pi'.1 hΦ.hasFDerivWithinAt i).fderivWithin hs

Premises used: hasFDerivWithinAt_pi', HasFDerivWithinAt.fderivWithin, Iff.mp, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
ι : Type u_6
F' : ι → Type u_7
inst_3 : (i : ι) → NormedAddCommGroup (F' i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_7} 𝕜 (F' i)
Φ : E → (i : ι) → F' i
hΦ : DifferentiableAt 𝕜 Φ x
i : ι
⊢ Eq (α := ContinuousLinearMap.{u_1, u_1, u_2, u_7} (RingHom.id 𝕜) E (F' i)) (fderiv 𝕜 (fun (x : E) ↦ Φ x i) x)
    (comp (σ₂₃ := RingHom.id 𝕜) (proj (φ := F') i : ((i : ι) → F' i) →L[𝕜] F' i)
      (fderiv 𝕜 Φ x : E →L[𝕜] (i : ι) → F' i))

Tactic:
(hasFDerivAt_pi'.1 hΦ.hasFDerivAt i).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, Iff.mp, hasFDerivAt_pi'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n.succ) → F' i)
l : Filter (E × E)
rw :
  (HasFDerivAtFilter (F := F' 0) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) 0) (proj (φ := F') 0 ∘SL φ') l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) i.succ) (proj (φ := F') i.succ ∘SL φ') l) ↔
    HasFDerivAtFilter φ (proj (φ := F') 0 ∘SL φ') l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun (x : E) ↦ φs x i)
          (comp (σ₂₃ := RingHom.id 𝕜) (proj (φ := fun (i : Fin n) ↦ F' i.succ) i) (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ'))
          l
⊢ HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i)
      (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) φ' l ↔
    HasFDerivAtFilter φ (proj (φ := F') 0 ∘SL φ') l ∧
      HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l

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

Premises used: Fin.forall_fin_succ, hasFDerivAtFilter_pi'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n.succ) → F' i)
l : Filter (E × E)
dsimp :
  (HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := F' 0) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) 0)
        { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x 0, map_add' := ⋯, map_smul' := ⋯,
          cont := ⋯ }
        l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := F' i.succ)
          (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) i.succ)
          { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x i.succ, map_add' := ⋯, map_smul' := ⋯,
            cont := ⋯ }
          l) ↔
    HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) φ
        { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x 0, map_add' := ⋯, map_smul' := ⋯,
          cont := ⋯ }
        l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := F' i.succ) (fun (x : E) ↦ φs x i)
          { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x i.succ, map_add' := ⋯, map_smul' := ⋯,
            cont := ⋯ }
          l
⊢ (HasFDerivAtFilter (F := F' 0) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) 0) (proj (φ := F') 0 ∘SL φ') l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) i.succ) (proj (φ := F') i.succ ∘SL φ') l) ↔
    HasFDerivAtFilter φ (proj (φ := F') 0 ∘SL φ') l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter (fun (x : E) ↦ φs x i)
          (comp (σ₂₃ := RingHom.id 𝕜) (proj (φ := fun (i : Fin n) ↦ F' i.succ) i) (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ'))
          l

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

Premises used: ContinuousLinearMap.comp, LinearMap.comp, Function.comp_def
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n.succ) → F' i)
l : Filter (E × E)
⊢ (HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := F' 0) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) 0)
        { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x 0, map_add' := ⋯, map_smul' := ⋯,
          cont := ⋯ }
        l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := F' i.succ)
          (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x) i.succ)
          { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x i.succ, map_add' := ⋯, map_smul' := ⋯,
            cont := ⋯ }
          l) ↔
    HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) φ
        { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x 0, map_add' := ⋯, map_smul' := ⋯,
          cont := ⋯ }
        l ∧
      ∀ (i : Fin n),
        HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := F' i.succ) (fun (x : E) ↦ φs x i)
          { toFun := fun (x : E) ↦ (φ' : (a : E) → (i : Fin (n + 1)) → F' i) x i.succ, map_add' := ⋯, map_smul' := ⋯,
            cont := ⋯ }
          l

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

Premises used: Fin.cons_succ, Fin.cons_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E (F' 0)
φs' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n) → F' i.succ)
l : Filter (E × E)
⊢ HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i)
      (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) (φ'.finCons (M := F') φs') l ↔
    HasFDerivAtFilter φ φ' l ∧ HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) φs φs' l

Tactic:
hasFDerivAtFilter_finCons

Premises used: ContinuousLinearMap.comp, Eq.mpr, Fin.cons, Fin.induction.go, Fin.ofNat, Fin.induction, hasFDerivAtFilter_finCons, Nat.mod, Fin.cases
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E (F' 0)
φs' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n) → F' i.succ)
l : Filter (E × E)
h : HasFDerivAtFilter φ φ' l
hs : HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) φs φs' l
⊢ HasFDerivAtFilter.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i)
    (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) (φ'.finCons (M := F') φs') l

Tactic:
hasFDerivAtFilter_finCons'.mpr ⟨h, hs⟩

Premises used: Iff.mpr, And.intro, hasFDerivAtFilter_finCons'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n.succ) → F' i)
⊢ HasStrictFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i)
      (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) φ' x ↔
    HasStrictFDerivAt φ (proj (φ := F') 0 ∘SL φ') x ∧
      HasStrictFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') x

Tactic:
hasFDerivAtFilter_finCons

Premises used: hasFDerivAtFilter_finCons, HasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E (F' 0)
φs' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n) → F' i.succ)
⊢ HasStrictFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i)
      (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) (φ'.finCons (M := F') φs') x ↔
    HasStrictFDerivAt φ φ' x ∧ HasStrictFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) φs φs' x

Tactic:
hasStrictFDerivAt_finCons

Premises used: ContinuousLinearMap.comp, Eq.mpr, Fin.cons, Fin.induction.go, Fin.ofNat, hasStrictFDerivAt_finCons, Fin.induction, Nat.mod, Fin.cases
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E (F' 0)
φs' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n) → F' i.succ)
h : HasStrictFDerivAt φ φ' x
hs : HasStrictFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) φs φs' x
⊢ HasStrictFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i)
    (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) (φ'.finCons (M := F') φs') x

Tactic:
hasStrictFDerivAt_finCons'.mpr ⟨h, hs⟩

Premises used: Iff.mpr, hasStrictFDerivAt_finCons', And.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n.succ) → F' i)
⊢ HasFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x))
      φ' x ↔
    HasFDerivAt φ (proj (φ := F') 0 ∘SL φ') x ∧
      HasFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') x

Tactic:
hasFDerivAtFilter_finCons

Premises used: HasFDerivAt, hasFDerivAtFilter_finCons
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E (F' 0)
φs' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n) → F' i.succ)
⊢ HasFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x))
      (φ'.finCons (M := F') φs') x ↔
    HasFDerivAt φ φ' x ∧ HasFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) φs φs' x

Tactic:
hasFDerivAt_finCons

Premises used: ContinuousLinearMap.comp, Eq.mpr, hasFDerivAt_finCons, Fin.cons, Fin.induction.go, Fin.ofNat, Fin.induction, Nat.mod, Fin.cases
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E (F' 0)
φs' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n) → F' i.succ)
h : HasFDerivAt φ φ' x
hs : HasFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) φs φs' x
⊢ HasFDerivAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i) (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x))
    (φ'.finCons (M := F') φs') x

Tactic:
hasFDerivAt_finCons'.mpr ⟨h, hs⟩

Premises used: Iff.mpr, hasFDerivAt_finCons', And.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n.succ) → F' i)
⊢ HasFDerivWithinAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i)
      (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) φ' s x ↔
    HasFDerivWithinAt φ (proj (φ := F') 0 ∘SL φ') s x ∧
      HasFDerivWithinAt.{u_1, u_2, u_6} (𝕜 := 𝕜) φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') s x

Tactic:
hasFDerivAtFilter_finCons

Premises used: HasFDerivWithinAt, hasFDerivAtFilter_finCons
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E (F' 0)
φs' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n) → F' i.succ)
⊢ HasFDerivWithinAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i)
      (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) (φ'.finCons (M := F') φs') s x ↔
    HasFDerivWithinAt φ φ' s x ∧ HasFDerivWithinAt.{u_1, u_2, u_6} (𝕜 := 𝕜) φs φs' s x

Tactic:
hasFDerivAtFilter_finCons

Premises used: ContinuousLinearMap.comp, Eq.mpr, Fin.cons, Fin.induction.go, Fin.ofNat, HasFDerivWithinAt, Fin.induction, hasFDerivAtFilter_finCons, Nat.mod, Fin.cases
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
n : ℕ
F' : Fin n.succ → Type u_6
inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst_4 : (i : Fin n.succ) → NormedSpace.{u_1, u_6} 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E (F' 0)
φs' : ContinuousLinearMap.{u_1, u_1, u_2, u_6} (RingHom.id 𝕜) E ((i : Fin n) → F' i.succ)
h : HasFDerivWithinAt φ φ' s x
hs : HasFDerivWithinAt.{u_1, u_2, u_6} (𝕜 := 𝕜) φs φs' s x
⊢ HasFDerivWithinAt.{u_1, u_2, u_6} (𝕜 := 𝕜) (F := (i : Fin (n + 1)) → F' i)
    (fun (x : E) ↦ Fin.cons (α := F') (φ x) (φs x)) (φ'.finCons (M := F') φs') s x

Tactic:
hasFDerivWithinAt_finCons'.mpr ⟨h, hs⟩

Premises used: Iff.mpr, hasFDerivWithinAt_finCons', And.intro