awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
f₂ : E → F × G
h : DifferentiableAt 𝕜 f₂ x
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (x : E) ↦ (f₂ x).1) x)
    (comp (σ₁₂ := RingHom.id 𝕜) (ContinuousLinearMap.fst 𝕜 F G) (fderiv 𝕜 f₂ x))

Tactic:
h.hasFDerivAt.fst.fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
s : Set (E × F)
hs : UniqueDiffWithinAt 𝕜 s p
⊢ Eq (α := E × F →L[𝕜] E) (fderivWithin 𝕜 Prod.fst s p : E × F →L[𝕜] E) (fst 𝕜 E F : E × F →L[𝕜] E)

Tactic:
hasFDerivWithinAt_fst.fderivWithin hs

Premises used: HasFDerivWithinAt.fderivWithin, hasFDerivWithinAt_fst
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
f₂ : E → F × G
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f₂ s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ (f₂ x).1) s x)
    (comp (σ₁₂ := RingHom.id 𝕜) (ContinuousLinearMap.fst 𝕜 F G) (fderivWithin 𝕜 f₂ s x))

Tactic:
h.hasFDerivWithinAt.fst.fderivWithin hs

Premises used: HasFDerivWithinAt.fst, HasFDerivWithinAt.fderivWithin, 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter ((E × F) × E × F)
⊢ HasFDerivAtFilter (𝕜 := 𝕜) Prod.snd (snd 𝕜 E F) L

Tactic:
(snd 𝕜 E F).hasFDerivAtFilter

Premises used: ContinuousLinearMap.hasFDerivAtFilter, ContinuousLinearMap.snd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
L : Filter (E × E)
f₂ : E → F × G
f₂' : E →L[𝕜] F × G
h : HasFDerivAtFilter (𝕜 := 𝕜) f₂ f₂' L
⊢ HasFDerivAtFilter (fun (x : E) ↦ (f₂ x).2) (snd 𝕜 F G ∘SL f₂') L

Tactic:
hasFDerivAtFilter_snd.comp h tendsto_map

Premises used: setOf, HasFDerivAtFilter.comp, Filter.tendsto_map
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
⊢ HasStrictFDerivAt (𝕜 := 𝕜) Prod.snd (snd 𝕜 E F) p

Tactic:
hasFDerivAtFilter_snd

Premises used: hasFDerivAtFilter_snd, 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
f₂ : E → F × G
f₂' : E →L[𝕜] F × G
h : HasStrictFDerivAt (𝕜 := 𝕜) f₂ f₂' x
⊢ HasStrictFDerivAt (fun (x : E) ↦ (f₂ x).2) (snd 𝕜 F G ∘SL f₂') x

Tactic:
HasFDerivAtFilter.snd h

Premises used: HasFDerivAtFilter.snd, 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
⊢ HasFDerivAt (𝕜 := 𝕜) Prod.snd (snd 𝕜 E F) p

Tactic:
hasFDerivAtFilter_snd

Premises used: HasFDerivAt, hasFDerivAtFilter_snd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
f₂ : E → F × G
f₂' : E →L[𝕜] F × G
h : HasFDerivAt (𝕜 := 𝕜) f₂ f₂' x
⊢ HasFDerivAt (fun (x : E) ↦ (f₂ x).2) (snd 𝕜 F G ∘SL f₂') x

Tactic:
HasFDerivAtFilter.snd h

Premises used: HasFDerivAt, HasFDerivAtFilter.snd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
s : Set (E × F)
⊢ HasFDerivWithinAt (𝕜 := 𝕜) Prod.snd (snd 𝕜 E F) s p

Tactic:
hasFDerivAtFilter_snd

Premises used: HasFDerivWithinAt, hasFDerivAtFilter_snd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
f₂ : E → F × G
f₂' : E →L[𝕜] F × G
h : HasFDerivWithinAt (𝕜 := 𝕜) f₂ f₂' s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ (f₂ x).2) (snd 𝕜 F G ∘SL f₂') s x

Tactic:
HasFDerivAtFilter.snd h

Premises used: HasFDerivWithinAt, HasFDerivAtFilter.snd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
⊢ DifferentiableAt 𝕜 Prod.snd p

Tactic:
hasFDerivAt_snd.differentiableAt

Premises used: hasFDerivAt_snd, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
f₂ : E → F × G
h : DifferentiableAt 𝕜 f₂ x
⊢ DifferentiableAt.{u_1, u_2, u_4} 𝕜 (F := G) (fun (x : E) ↦ (f₂ x).2) x

Tactic:
differentiableAt_snd.comp x h

Premises used: DifferentiableAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
⊢ Differentiable 𝕜 (E := E × F) Prod.snd

Tactic:
fun _ =>
  differentiableAt_snd

Premises used: Differentiable, differentiableAt_snd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f₂ : E → F × G
h : Differentiable 𝕜 f₂
⊢ Differentiable.{u_1, u_2, u_4} 𝕜 (F := G) fun (x : E) ↦ (f₂ x).2

Tactic:
differentiable_snd.comp h

Premises used: Differentiable.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
s : Set (E × F)
⊢ DifferentiableWithinAt 𝕜 Prod.snd s p

Tactic:
differentiableAt_snd.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, differentiableAt_snd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
f₂ : E → F × G
h : DifferentiableWithinAt 𝕜 f₂ s x
⊢ DifferentiableWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) (fun (x : E) ↦ (f₂ x).2) s x

Tactic:
differentiableAt_snd.comp_differentiableWithinAt x h

Premises used: DifferentiableAt.comp_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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set (E × F)
⊢ DifferentiableOn 𝕜 Prod.snd s

Tactic:
differentiable_snd.differentiableOn

Premises used: differentiable_snd, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f₂ : E → F × G
h : DifferentiableOn 𝕜 f₂ s
⊢ DifferentiableOn.{u_1, u_2, u_4} 𝕜 (F := G) (fun (x : E) ↦ (f₂ x).2) s

Tactic:
differentiable_snd.comp_differentiableOn h

Premises used: Differentiable.comp_differentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
⊢ Eq (α := E × F →L[𝕜] F) (fderiv 𝕜 Prod.snd p : E × F →L[𝕜] F) (snd 𝕜 E F : E × F →L[𝕜] F)

Tactic:
hasFDerivAt_snd.fderiv

Premises used: hasFDerivAt_snd, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
f₂ : E → F × G
h : DifferentiableAt 𝕜 f₂ x
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 (fun (x : E) ↦ (f₂ x).2) x)
    (comp (σ₁₂ := RingHom.id 𝕜) (ContinuousLinearMap.snd 𝕜 F G) (fderiv 𝕜 f₂ x))

Tactic:
h.hasFDerivAt.snd.fderiv

Premises used: HasFDerivAt.snd, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : E × F
s : Set (E × F)
hs : UniqueDiffWithinAt 𝕜 s p
⊢ Eq (α := E × F →L[𝕜] F) (fderivWithin 𝕜 Prod.snd s p : E × F →L[𝕜] F) (snd 𝕜 E F : E × F →L[𝕜] F)

Tactic:
hasFDerivWithinAt_snd.fderivWithin hs

Premises used: HasFDerivWithinAt.fderivWithin, hasFDerivWithinAt_snd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
s : Set E
f₂ : E → F × G
hs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f₂ s x
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (fun (x : E) ↦ (f₂ x).2) s x)
    (comp (σ₁₂ := RingHom.id 𝕜) (ContinuousLinearMap.snd 𝕜 F G) (fderivWithin 𝕜 f₂ s x))

Tactic:
h.hasFDerivWithinAt.snd.fderivWithin hs

Premises used: HasFDerivWithinAt.snd, HasFDerivWithinAt.fderivWithin, 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
f : E → F
f' : E →L[𝕜] F
f₂ : G → G'
f₂' : G →L[𝕜] G'
p : E × G
hf : HasStrictFDerivAt f f' p.1
hf₂ : HasStrictFDerivAt f₂ f₂' p.2
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (Prod.map f f₂) (f'.prodMap f₂') p

Tactic:
(hf.comp p hasStrictFDerivAt_fst).prodMk (hf₂.comp p hasStrictFDerivAt_snd)

Premises used: hasStrictFDerivAt_snd, setOf, HasStrictFDerivAt.prodMk, ContinuousLinearMap.prodMap, Prod.map, hasStrictFDerivAt_fst, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
f : E → F
f' : E →L[𝕜] F
f₂ : G → G'
f₂' : G →L[𝕜] G'
p : E × G
s : Set (E × G)
hf : HasFDerivWithinAt f f' (Prod.fst '' s) p.1
hf₂ : HasFDerivWithinAt f₂ f₂' (Prod.snd '' s) p.2
⊢ s ⊆ (Prod.fst '' s) ×ˢ (Prod.snd '' s)

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
f : E → F
f' : E →L[𝕜] F
f₂ : G → G'
f₂' : G →L[𝕜] G'
p : E × G
hf : HasFDerivAt f f' p.1
hf₂ : HasFDerivAt f₂ f₂' p.2
⊢ HasFDerivAt (𝕜 := 𝕜) (Prod.map f f₂) (f'.prodMap f₂') p

Tactic:
(hf.comp p hasFDerivAt_fst).prodMk (hf₂.comp p hasFDerivAt_snd)

Premises used: hasFDerivAt_snd, setOf, ContinuousLinearMap.prodMap, Prod.map, HasFDerivAt.prodMk, hasFDerivAt_fst, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
f : E → F
f₂ : G → G'
p : E × G
hf : DifferentiableAt 𝕜 f p.1
hf₂ : DifferentiableAt 𝕜 f₂ p.2
⊢ DifferentiableAt 𝕜 (F := F × G') (fun (p : E × G) ↦ (f p.1, f₂ p.2)) p

Tactic:
(hf.comp p differentiableAt_fst).prodMk (hf₂.comp p differentiableAt_snd)

Premises used: setOf, differentiableAt_fst, DifferentiableAt.prodMk, differentiableAt_snd, DifferentiableAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Prod
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
L : Filter (E × 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
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ HasFDerivAtFilter (𝕜 := 𝕜) Φ Φ' L ↔ ∀ (i : ι), HasFDerivAtFilter (fun (x : E) ↦ Φ x i) (proj (φ := F') i ∘SL Φ') L

Tactic:
simp [hasFDerivAtFilter_iff_isLittleOTVS, isLittleOTVS_pi]

Premises used: hasFDerivAtFilter_iff_isLittleOTVS, Asymptotics.isLittleOTVS_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
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ HasStrictFDerivAt (𝕜 := 𝕜) Φ Φ' x ↔ ∀ (i : ι), HasStrictFDerivAt (fun (x : E) ↦ Φ x i) (proj (φ := F') i ∘SL Φ') x

Tactic:
hasFDerivAtFilter_pi'

Premises used: HasStrictFDerivAt, 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
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
Φ' : E →L[𝕜] (i : ι) → F' i
hφ : ∀ (i : ι), HasStrictFDerivAt (fun (x : E) ↦ Φ x i) (proj (φ := F') i ∘SL Φ') x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) Φ Φ' x

Tactic:
hasStrictFDerivAt_pi'.2 hφ

Premises used: Iff.mpr, hasStrictFDerivAt_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
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) (proj (φ := F') i) f

Tactic:
(proj (R := 𝕜) (φ := F') i).hasStrictFDerivAt

Premises used: ContinuousLinearMap.proj, ContinuousLinearMap.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
ι : 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
φ' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_2, u_7} (RingHom.id 𝕜) E (F' i)
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := (i : ι) → F' i) (fun (x : E) (i : ι) ↦ φ i x) (ContinuousLinearMap.pi (φ := F') φ')
      x ↔
    ∀ (i : ι), HasStrictFDerivAt (φ i) (φ' i) x

Tactic:
hasStrictFDerivAt_pi'

Premises used: ContinuousLinearMap.comp, hasStrictFDerivAt_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
L : Filter (E × 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
φ' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_2, u_7} (RingHom.id 𝕜) E (F' i)
⊢ HasFDerivAtFilter (𝕜 := 𝕜) (F := (i : ι) → F' i) (fun (x : E) (i : ι) ↦ φ i x) (ContinuousLinearMap.pi (φ := F') φ')
      L ↔
    ∀ (i : ι), HasFDerivAtFilter (φ i) (φ' i) L

Tactic:
hasFDerivAtFilter_pi'

Premises used: ContinuousLinearMap.comp, 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
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
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ HasFDerivAt (𝕜 := 𝕜) Φ Φ' x ↔ ∀ (i : ι), HasFDerivAt (fun (x : E) ↦ Φ x i) (proj (φ := F') i ∘SL Φ') x

Tactic:
hasFDerivAtFilter_pi'

Premises used: HasFDerivAt, 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
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
Φ' : E →L[𝕜] (i : ι) → F' i
hφ : ∀ (i : ι), HasFDerivAt (fun (x : E) ↦ Φ x i) (proj (φ := F') i ∘SL Φ') x
⊢ HasFDerivAt (𝕜 := 𝕜) Φ Φ' x

Tactic:
hasFDerivAt_pi'.2 hφ

Premises used: Iff.mpr, hasFDerivAt_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
⊢ HasFDerivAt (𝕜 := 𝕜) (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) (proj (φ := F') i) f

Tactic:
(proj (R := 𝕜) (φ := F') i).hasFDerivAt

Premises used: ContinuousLinearMap.hasFDerivAt, ContinuousLinearMap.proj
-- 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
φ' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_2, u_7} (RingHom.id 𝕜) E (F' i)
⊢ HasFDerivAt (𝕜 := 𝕜) (F := (i : ι) → F' i) (fun (x : E) (i : ι) ↦ φ i x) (ContinuousLinearMap.pi (φ := F') φ') x ↔
    ∀ (i : ι), HasFDerivAt (φ i) (φ' i) x

Tactic:
hasFDerivAtFilter_pi

Premises used: HasFDerivAt, 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
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
Φ' : E →L[𝕜] (i : ι) → F' i
⊢ HasFDerivWithinAt (𝕜 := 𝕜) Φ Φ' s x ↔ ∀ (i : ι), HasFDerivWithinAt (fun (x : E) ↦ Φ x i) (proj (φ := F') i ∘SL Φ') s x

Tactic:
hasFDerivAtFilter_pi'

Premises used: HasFDerivWithinAt, 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
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
Φ' : E →L[𝕜] (i : ι) → F' i
hφ : ∀ (i : ι), HasFDerivWithinAt (fun (x : E) ↦ Φ x i) (proj (φ := F') i ∘SL Φ') s x
⊢ HasFDerivWithinAt (𝕜 := 𝕜) Φ Φ' s x

Tactic:
hasFDerivWithinAt_pi'.2 hφ

Premises used: Iff.mpr, hasFDerivWithinAt_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
s' : Set ((i : ι) → F' i)
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := F' i) (fun (f : (i : ι) → F' i) ↦ f i) (proj (φ := F') i) s' f

Tactic:
(hasFDerivAt_apply i f).hasFDerivWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt, hasFDerivAt_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
φ' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_2, u_7} (RingHom.id 𝕜) E (F' i)
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := (i : ι) → F' i) (fun (x : E) (i : ι) ↦ φ i x) (ContinuousLinearMap.pi (φ := F') φ') s
      x ↔
    ∀ (i : ι), HasFDerivWithinAt (φ i) (φ' i) s x

Tactic:
hasFDerivAtFilter_pi

Premises used: hasFDerivAtFilter_pi, 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
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
⊢ DifferentiableWithinAt 𝕜 Φ s x ↔
    ∀ (i : ι), DifferentiableWithinAt.{u_1, u_2, u_7} 𝕜 (F := F' i) (fun (x : E) ↦ Φ x i) s x

Tactic:
⟨fun h i => (hasFDerivWithinAt_pi'.1 h.hasFDerivWithinAt i).differentiableWithinAt, fun h =>
    (hasFDerivWithinAt_pi.2 fun i => (h i).hasFDerivWithinAt).differentiableWithinAt⟩

Premises used: Iff.mpr, hasFDerivWithinAt_pi', HasFDerivWithinAt.differentiableWithinAt, Iff.intro, Iff.mp, 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
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 : ι), DifferentiableWithinAt.{u_1, u_2, u_7} 𝕜 (F := F' i) (fun (x : E) ↦ Φ x i) s x
⊢ DifferentiableWithinAt 𝕜 Φ s x

Tactic:
differentiableWithinAt_pi.2 hφ

Premises used: Iff.mpr, differentiableWithinAt_pi