awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : F → E
f' : F ≃L[𝕜] E
a : E
hg : ContinuousAt g a
hf : HasFDerivAt f (↑f' : F →L[𝕜] E) (g a)
hfg : ∀ᶠ (y : E) in 𝓝 a, f (g y) = y
⊢ HasFDerivAt g (↑f'.symm : E →L[𝕜] F) a

Tactic:
hf.of_comp_of_leftInverse (f'symm := (f'.symm : E →L[𝕜] F)) hg (hasFDerivAt_id _) hfg
    f'.symm_apply_apply

Premises used: ContinuousLinearMap.comp, hasFDerivAt_id, ContinuousLinearEquiv.symm_apply_apply, ContinuousLinearEquiv.toContinuousLinearMap, HasFDerivAt.of_comp_of_leftInverse
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
g : E → F
f : F → E
f' : F ≃L[𝕜] E
a : E
s : Set E
t : Set F
hg : Tendsto g (𝓝[s] a) (𝓝[t] g a)
hf : HasFDerivWithinAt f (↑f' : F →L[𝕜] E) t (g a)
ha : a ∈ s
hfg : ∀ᶠ (x : E) in 𝓝[s] a, f (g x) = x
⊢ HasFDerivWithinAt g (↑f'.symm : E →L[𝕜] F) s a

Tactic:
hf.of_comp_of_leftInverse (f'symm := (f'.symm : E →L[𝕜] F)) hg (hasFDerivWithinAt_id _ _) hfg
    f'.symm_apply_apply ha

Premises used: ContinuousLinearMap.comp, HasFDerivWithinAt.of_comp_of_leftInverse, ContinuousLinearEquiv.symm_apply_apply, ContinuousLinearEquiv.toContinuousLinearMap, hasFDerivWithinAt_id
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E ≃L[𝕜] F
g : F → E
a : F
hg : ContinuousAt g a
hf : HasStrictFDerivAt f (↑f' : E →L[𝕜] F) (g a)
hfg : ∀ᶠ (y : F) in 𝓝 a, f (g y) = y
⊢ HasStrictFDerivAt g (↑f'.symm : F →L[𝕜] E) a

Tactic:
hf.of_comp_of_leftInverse (f'symm := (f'.symm : F →L[𝕜] E)) hg (hasStrictFDerivAt_id _) hfg
    f'.symm_apply_apply

Premises used: ContinuousLinearMap.comp, HasStrictFDerivAt.of_comp_of_leftInverse, ContinuousLinearEquiv.symm_apply_apply, ContinuousLinearEquiv.toContinuousLinearMap, hasStrictFDerivAt_id
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
f' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
htff' : HasStrictFDerivAt (↑f : E → F) (↑f' : E →L[𝕜] F) ((↑f.symm : F → E) a)
⊢ HasStrictFDerivAt (↑f.symm : F → E) (↑f'.symm : F →L[𝕜] E) a

Tactic:
htff'.of_local_left_inverse (f.symm.continuousAt ha) (f.eventually_right_inverse ha)

Premises used: OpenPartialHomeomorph.continuousAt, HasStrictFDerivAt.of_local_left_inverse, OpenPartialHomeomorph.eventually_right_inverse, OpenPartialHomeomorph.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
f' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
htff' : HasFDerivAt (↑f : E → F) (↑f' : E →L[𝕜] F) ((↑f.symm : F → E) a)
⊢ HasFDerivAt (↑f.symm : F → E) (↑f'.symm : F →L[𝕜] E) a

Tactic:
htff'.of_local_left_inverse (f.symm.continuousAt ha) (f.eventually_right_inverse ha)

Premises used: OpenPartialHomeomorph.continuousAt, OpenPartialHomeomorph.eventually_right_inverse, HasFDerivAt.of_local_left_inverse, OpenPartialHomeomorph.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
u : E
v w : α → E
l : Filter α
hv : Tendsto v l (𝓝 u)
hw : Tendsto w l (𝓝 u)
s : Set E
seg : ∀ᶠ (χ : α) in l, [w χ -[ℝ] v χ] ⊆ s
f : α → E → F
f' : α → E → E →L[𝕜] F
df' : ∀ᶠ (p : α × E) in l ×ˢ 𝓝[s] u, HasFDerivWithinAt (f p.1) (f' p.1 p.2) s p.2
φ : E →L[𝕜] F
cf' : Tendsto (↿f') (l ×ˢ 𝓝[s] u) (𝓝 φ)
rw :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x : α) in l,
        ‖HSub.hSub (β := F) (f x (v x) - f x (w x)) ((φ : (a : E) → F) (v x - w x) : F)‖ ≤ c * ‖v x - w x‖
⊢ IsLittleO.{u_1, u_4, u_3} (E := F) (F := E) l
    (fun (χ : α) ↦ HSub.hSub (β := F) (f χ (v χ) - f χ (w χ)) ((φ : (a : E) → F) (v χ - w χ) : F)) fun (χ : α) ↦
    v χ - w χ

Tactic:
rw [isLittleO_iff]

Premises used: Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
u : E
v w : α → E
l : Filter α
hv : Tendsto v l (𝓝 u)
hw : Tendsto w l (𝓝 u)
s : Set E
seg : ∀ᶠ (χ : α) in l, [w χ -[ℝ] v χ] ⊆ s
f : α → E → F
f' : α → E → E →L[𝕜] F
df' : ∀ᶠ (p : α × E) in l ×ˢ 𝓝[s] u, HasFDerivWithinAt (f p.1) (f' p.1 p.2) s p.2
φ : E →L[𝕜] F
cf' : Tendsto (↿f') (l ×ˢ 𝓝[s] u) (𝓝 φ)
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z

Tactic:
replace df' : ∀ᶠ χ in l, ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z :=
    df'.segment_of_prod_nhdsWithin hw hv seg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
u : E
v w : α → E
l : Filter α
hv : Tendsto v l (𝓝 u)
hw : Tendsto w l (𝓝 u)
s : Set E
seg : ∀ᶠ (χ : α) in l, [w χ -[ℝ] v χ] ⊆ s
f : α → E → F
f' : α → E → E →L[𝕜] F
φ : E →L[𝕜] F
cf' : Tendsto (↿f') (l ×ˢ 𝓝[s] u) (𝓝 φ)
ε : ℝ
hε : 0 < ε
df' : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z
⊢ ∀ ε > 0, ∀ᶠ (x : α × E) in l ×ˢ 𝓝[s] u, ‖↿f' x - φ‖ < ε

Tactic:
simp_rw [Metric.tendsto_nhds, dist_eq_norm_sub] at cf'

Premises used: dist_eq_norm_sub, Metric.tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
u : E
v w : α → E
l : Filter α
hv : Tendsto v l (𝓝 u)
hw : Tendsto w l (𝓝 u)
s : Set E
seg : ∀ᶠ (χ : α) in l, [w χ -[ℝ] v χ] ⊆ s
f : α → E → F
f' : α → E → E →L[𝕜] F
φ : E →L[𝕜] F
ε : ℝ
hε : 0 < ε
df' : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z
cf' : ∀ ε > 0, ∀ᶠ (x : α × E) in l ×ˢ 𝓝[s] u, ‖↿f' x - φ‖ < ε
⊢ ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε

Tactic:
(cf' ε hε).segment_of_prod_nhdsWithin hw hv seg

Premises used: Set.Mem, Filter.Eventually.segment_of_prod_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
u : E
v w : α → E
l : Filter α
hv : Tendsto v l (𝓝 u)
hw : Tendsto w l (𝓝 u)
s : Set E
seg : ∀ᶠ (χ : α) in l, [w χ -[ℝ] v χ] ⊆ s
f : α → E → F
f' : α → E → E →L[𝕜] F
φ : E →L[𝕜] F
ε : ℝ
hε : 0 < ε
df' : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z
cf' : ∀ ε > 0, ∀ᶠ (x : α × E) in l ×ˢ 𝓝[s] u, ‖↿f' x - φ‖ < ε
⊢ ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε

Tactic:
exact (cf' ε hε).segment_of_prod_nhdsWithin hw hv seg

Premises used: Filter.Eventually.segment_of_prod_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
u : E
v w : α → E
l : Filter α
hv : Tendsto v l (𝓝 u)
hw : Tendsto w l (𝓝 u)
s : Set E
seg : ∀ᶠ (χ : α) in l, [w χ -[ℝ] v χ] ⊆ s
f : α → E → F
f' : α → E → E →L[𝕜] F
φ : E →L[𝕜] F
cf' : Tendsto (↿f') (l ×ˢ 𝓝[s] u) (𝓝 φ)
ε : ℝ
hε : 0 < ε
df' : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z
⊢ ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε

Tactic:
replace cf' : ∀ᶠ χ in l, ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε := by
    simp_rw [Metric.tendsto_nhds, dist_eq_norm_sub] at cf'
    exact (cf' ε hε).segment_of_prod_nhdsWithin hw hv seg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
u : E
v w : α → E
l : Filter α
hv : Tendsto v l (𝓝 u)
hw : Tendsto w l (𝓝 u)
s : Set E
seg : ∀ᶠ (χ : α) in l, [w χ -[ℝ] v χ] ⊆ s
f : α → E → F
f' : α → E → E →L[𝕜] F
φ : E →L[𝕜] F
ε : ℝ
hε : 0 < ε
df' : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z
cf' : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε
h :
  ∀ (χ : α) (seg : [w χ -[ℝ] v χ] ⊆ s) (df' : ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z)
    (cf' : ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε),
    ‖HSub.hSub (β := F) (f χ (v χ) - f χ (w χ)) ((φ : (a : E) → F) (v χ - w χ) : F)‖ ≤ ε * ‖v χ - w χ‖
⊢ ∀ᶠ (x : α) in l, ‖HSub.hSub (β := F) (f x (v x) - f x (w x)) ((φ : (a : E) → F) (v x - w x) : F)‖ ≤ ε * ‖v x - w x‖

Tactic:
filter_upwards [seg, df', cf'] with χ seg df' cf'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
u : E
v w : α → E
l : Filter α
hv : Tendsto v l (𝓝 u)
hw : Tendsto w l (𝓝 u)
s : Set E
seg_1 : ∀ᶠ (χ : α) in l, [w χ -[ℝ] v χ] ⊆ s
f : α → E → F
f' : α → E → E →L[𝕜] F
φ : E →L[𝕜] F
ε : ℝ
hε : 0 < ε
df'_1 : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z
cf'_1 : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε
χ : α
seg : [w χ -[ℝ] v χ] ⊆ s
df' : ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z
cf' : ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε
⊢ ‖HSub.hSub (β := F) (f χ (v χ) - f χ (w χ)) ((φ : (a : E) → F) (v χ - w χ) : F)‖ ≤ ε * ‖v χ - w χ‖

Tactic:
Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le'
    (fun z hz => (df' z hz).mono seg) (fun z hz => (cf' z hz).le)
    (convex_segment ..) (left_mem_segment ..) (right_mem_segment ..)

Premises used: left_mem_segment, LT.lt.le, right_mem_segment, Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le', HasFDerivWithinAt.mono, convex_segment
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : IsRCLikeNormedField 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
u : E
v w : α → E
l : Filter α
hv : Tendsto v l (𝓝 u)
hw : Tendsto w l (𝓝 u)
s : Set E
seg_1 : ∀ᶠ (χ : α) in l, [w χ -[ℝ] v χ] ⊆ s
f : α → E → F
f' : α → E → E →L[𝕜] F
φ : E →L[𝕜] F
ε : ℝ
hε : 0 < ε
df'_1 : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z
cf'_1 : ∀ᶠ (χ : α) in l, ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε
χ : α
seg : [w χ -[ℝ] v χ] ⊆ s
df' : ∀ z ∈ [w χ -[ℝ] v χ], HasFDerivWithinAt (f χ) (f' χ z) s z
cf' : ∀ z ∈ [w χ -[ℝ] v χ], ‖f' χ z - φ‖ < ε
⊢ ‖HSub.hSub (β := F) (f χ (v χ) - f χ (w χ)) ((φ : (a : E) → F) (v χ - w χ) : F)‖ ≤ ε * ‖v χ - w χ‖

Tactic:
exact Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le'
    (fun z hz => (df' z hz).mono seg) (fun z hz => (cf' z hz).le)
    (convex_segment ..) (left_mem_segment ..) (right_mem_segment ..)

Premises used: left_mem_segment, LT.lt.le, right_mem_segment, Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le', HasFDerivWithinAt.mono, convex_segment
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : NormedAddCommGroup E₂
inst_4 : NormedSpace 𝕜 E₂
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : ContinuousAt (↿f₁) u
cf₂ : ContinuousAt (↿f₂) u
rw :
  IsLittleO (E := F) (F := E₁ × E₂) (𝓝 (u, u))
    (fun (p : (E₁ × E₂) × E₁ × E₂) ↦
      HSub.hSub (β := F) (↿f p.1 - ↿f p.2) (((↿f₁ u).coprod (↿f₂ u) : (a : E₁ × E₂) → F) (p.1 - p.2) : F))
    fun (p : (E₁ × E₂) × E₁ × E₂) ↦ p.1 - p.2
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (↿f) ((↿f₁ u).coprod (↿f₂ u)) u

Tactic:
rw [hasStrictFDerivAt_iff_isLittleO]

Premises used: hasStrictFDerivAt_iff_isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : NormedAddCommGroup E₂
inst_4 : NormedSpace 𝕜 E₂
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u) (𝓝 (↿f₂ u))
⊢ ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1

Tactic:
rw [nhds_prod_eq] at df₁ df₂ cf₁ cf₂

Premises used: nhds_prod_eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : NormedAddCommGroup E₂
inst_4 : NormedSpace 𝕜 E₂
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u) (𝓝 (↿f₂ u))
df₃ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
⊢ ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2

Tactic:
rw [nhds_prod_eq] at df₁ df₂ cf₁ cf₂

Premises used: nhds_prod_eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : NormedAddCommGroup E₂
inst_4 : NormedSpace 𝕜 E₂
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u) (𝓝 (↿f₂ u))
df₃ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
df₄ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2
⊢ Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))

Tactic:
rw [nhds_prod_eq] at df₁ df₂ cf₁ cf₂

Premises used: nhds_prod_eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : NormedAddCommGroup E₂
inst_4 : NormedSpace 𝕜 E₂
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u) (𝓝 (↿f₂ u))
df₃ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
df₄ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2
cf₃ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
⊢ Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))

Tactic:
rw [nhds_prod_eq] at df₁ df₂ cf₁ cf₂

Premises used: nhds_prod_eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : NormedAddCommGroup E₂
inst_4 : NormedSpace 𝕜 E₂
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))
h :
  ∀ (x : (E₁ × E₂) × E₁ × E₂),
    Eq.{u_4 + 1} (α := F)
      (match (motive := (E₁ × E₂) × E₁ × E₂ → F) x with
        | (v, w) =>
          HSub.hSub (β := F) (f v.1 v.2 - f w.1 w.2) (((↿f₁ u).coprod (↿f₂ u) : (a : E₁ × E₂) → F) (v - w) : F) :
        F)
      (match (motive := (E₁ × E₂) × E₁ × E₂ → F) x with
        | (v, w) =>
          HSub.hSub (β := F) (f v.1 w.2 - f w.1 w.2) ((↿f₁ u : (a : E₁) → F) (v.1 - w.1) : F) +
            HSub.hSub (β := F) (f v.1 v.2 - f v.1 w.2) ((↿f₂ u : (a : E₂) → F) (v.2 - w.2) : F) :
        F)
⊢ Eq (α := (E₁ × E₂) × E₁ × E₂ → F)
    (fun (x : (E₁ × E₂) × E₁ × E₂) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → F) x with
      | (v, w) => HSub.hSub (β := F) (f v.1 v.2 - f w.1 w.2) (((↿f₁ u).coprod (↿f₂ u) : (a : E₁ × E₂) → F) (v - w) : F))
    fun (x : (E₁ × E₂) × E₁ × E₂) ↦
    match (motive := (E₁ × E₂) × E₁ × E₂ → F) x with
    | (v, w) =>
      HSub.hSub (β := F) (f v.1 w.2 - f w.1 w.2) ((↿f₁ u : (a : E₁) → F) (v.1 - w.1) : F) +
        HSub.hSub (β := F) (f v.1 v.2 - f v.1 w.2) ((↿f₂ u : (a : E₂) → F) (v.2 - w.2) : F)

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : NormedAddCommGroup E₂
inst_4 : NormedSpace 𝕜 E₂
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))
x : (E₁ × E₂) × E₁ × E₂
h :
  f x.1.1 x.1.2 - f x.2.1 x.2.2 -
      HAdd.hAdd (α := F) (β := F) ((↿f₁ u : (a : E₁) → F) (x.1 - x.2).1 : F)
        ((↿f₂ u : (a : E₂) → F) (x.1 - x.2).2 : F) =
    HSub.hSub (β := F) (f x.1.1 x.2.2 - f x.2.1 x.2.2) ((↿f₁ u : (a : E₁) → F) (x.1.1 - x.2.1) : F) +
      HSub.hSub (β := F) (f x.1.1 x.1.2 - f x.1.1 x.2.2) ((↿f₂ u : (a : E₂) → F) (x.1.2 - x.2.2) : F)
⊢ Eq.{u_4 + 1} (α := F)
    (match (motive := (E₁ × E₂) × E₁ × E₂ → F) x with
      | (v, w) =>
        HSub.hSub (β := F) (f v.1 v.2 - f w.1 w.2) (((↿f₁ u).coprod (↿f₂ u) : (a : E₁ × E₂) → F) (v - w) : F) :
      F)
    (match (motive := (E₁ × E₂) × E₁ × E₂ → F) x with
      | (v, w) =>
        HSub.hSub (β := F) (f v.1 w.2 - f w.1 w.2) ((↿f₁ u : (a : E₁) → F) (v.1 - w.1) : F) +
          HSub.hSub (β := F) (f v.1 v.2 - f v.1 w.2) ((↿f₂ u : (a : E₂) → F) (v.2 - w.2) : F) :
      F)

Tactic:
dsimp only [ContinuousLinearMap.coprod_apply]

Premises used: ContinuousLinearMap.coprod_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : NormedAddCommGroup E₂
inst_4 : NormedSpace 𝕜 E₂
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))
x : (E₁ × E₂) × E₁ × E₂
⊢ f x.1.1 x.1.2 - f x.2.1 x.2.2 -
      HAdd.hAdd (α := F) (β := F) ((↿f₁ u : (a : E₁) → F) (x.1 - x.2).1 : F)
        ((↿f₂ u : (a : E₂) → F) (x.1 - x.2).2 : F) =
    HSub.hSub (β := F) (f x.1.1 x.2.2 - f x.2.1 x.2.2) ((↿f₁ u : (a : E₁) → F) (x.1.1 - x.2.1) : F) +
      HSub.hSub (β := F) (f x.1.1 x.1.2 - f x.1.1 x.2.2) ((↿f₂ u : (a : E₂) → F) (x.1.2 - x.2.2) : F)

Tactic:
abel
-- Module: Mathlib.Analysis.Calculus.FDeriv.Partial
Goal:
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E₁
inst_2 : NormedSpace 𝕜 E₁
inst_3 : NormedAddCommGroup E₂
inst_4 : NormedSpace 𝕜 E₂
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
inst_7 : IsRCLikeNormedField 𝕜
u : E₁ × E₂
f : E₁ → E₂ → F
f₁ : E₁ → E₂ → E₁ →L[𝕜] F
f₂ : E₁ → E₂ → E₂ →L[𝕜] F
df₁ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₁) ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun (x : E₂) ↦ f v.1 x) (↿f₂ v) v.2
cf₁ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
cf₂ : Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
rw :
  IsLittleO (E := F) (F := E₁ × E₂) ((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2)
    (fun (x : (E₁ × E₂) × E₁ × E₂) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → F) x with
      | (v, w) =>
        HSub.hSub (β := F) (f v.1 w.2 - f w.1 w.2) ((↿f₁ u : (a : E₁) → F) (v.1 - w.1) : F) +
          HSub.hSub (β := F) (f v.1 v.2 - f v.1 w.2) ((↿f₂ u : (a : E₂) → F) (v.2 - w.2) : F))
    fun (x : (E₁ × E₂) × E₁ × E₂) ↦
    match (motive := (E₁ × E₂) × E₁ × E₂ → E₁ × E₂) x with
    | (v, w) => v - w
⊢ IsLittleO (E := F) (F := E₁ × E₂) (𝓝 (u, u))
    (fun (x : (E₁ × E₂) × E₁ × E₂) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → F) x with
      | (v, w) =>
        HSub.hSub (β := F) (f v.1 w.2 - f w.1 w.2) ((↿f₁ u : (a : E₁) → F) (v.1 - w.1) : F) +
          HSub.hSub (β := F) (f v.1 v.2 - f v.1 w.2) ((↿f₂ u : (a : E₂) → F) (v.2 - w.2) : F))
    fun (x : (E₁ × E₂) × E₁ × E₂) ↦
    match (motive := (E₁ × E₂) × E₁ × E₂ → E₁ × E₂) x with
    | (v, w) => v - w

Tactic:
rw [nhds_prod_eq, nhds_prod_eq]

Premises used: nhds_prod_eq