awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (goal)
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) (𝓝 φ)
⊢ 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 χ
have 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‖
Tactic: rw [isLittleO_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (hypothesis)
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 < ε
⊢ ∀ᶠ (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‖
have df'₁ : ∀ᶠ (χ : α) 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
Cleared hypotheses: df'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (hypothesis)
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 - φ‖ < ε
have cf'₁ : ∀ ε > 0, ∀ᶠ (x : α × E) in l ×ˢ 𝓝[s] u, ‖↿f' x - φ‖ < ε
Tactic: simp_rw [Metric.tendsto_nhds, dist_eq_norm_sub] at cf'
Cleared hypotheses: cf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (hypothesis)
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
⊢ ∀ᶠ (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‖
have cf'₁ : ∀ᶠ (χ : α) 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
Cleared hypotheses: cf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (goal)
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 - φ‖ < ε
⊢ ∀ᶠ (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‖
have 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 χ‖
Tactic: filter_upwards [seg, df', cf'] with χ seg df' cf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (goal)
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
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (↿f) ((↿f₁ u).coprod (↿f₂ u)) u
have 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
Tactic: rw [hasStrictFDerivAt_iff_isLittleO]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (hypothesis)
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))
⊢ 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
have df₃ : ∀ᶠ (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₂
Cleared hypotheses: df₁, df₂, cf₁, cf₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (hypothesis)
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
⊢ 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
have df₄ : ∀ᶠ (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₂
Cleared hypotheses: df₁, df₂, cf₁, cf₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (hypothesis)
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
⊢ 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
have cf₃ : Tendsto (↿f₁) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₁ u))
Tactic: rw [nhds_prod_eq] at df₁ df₂ cf₁ cf₂
Cleared hypotheses: df₁, df₂, cf₁, cf₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (hypothesis)
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))
⊢ 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
have cf₄ : Tendsto (↿f₂) (𝓝 u.1 ×ˢ 𝓝 u.2) (𝓝 (↿f₂ u))
Tactic: rw [nhds_prod_eq] at df₁ df₂ cf₁ cf₂
Cleared hypotheses: df₁, df₂, cf₁, cf₂
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (goal)
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))
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (goal)
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₂
⊢ 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)
have 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)
Tactic: dsimp only [ContinuousLinearMap.coprod_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (goal)
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 𝕜
⊢ 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
have 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
Tactic: rw [nhds_prod_eq, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (goal)
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 𝕜
⊢ 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
have h₁ : IsLittleO (E := F) (F := E₁ × E₂) ((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2)
  (fun (x : (E₁ × E₂) × E₁ × E₂) ↦
    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))
  fun (x : (E₁ × E₂) × E₁ × E₂) ↦
  match (motive := (E₁ × E₂) × E₁ × E₂ → E₁ × E₂) x with
  | (v, w) => v - w
Tactic: apply IsLittleO.add
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (goal)
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 𝕜
h₁ :
  IsLittleO (E := F) (F := E₁ × E₂) ((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2)
    (fun (x : (E₁ × E₂) × E₁ × E₂) ↦
      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))
    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.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
have h₂ : IsLittleO (E := F) (F := E₁ × E₂) ((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2)
  (fun (x : (E₁ × E₂) × E₁ × E₂) ↦
    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))
  fun (x : (E₁ × E₂) × E₁ × E₂) ↦
  match (motive := (E₁ × E₂) × E₁ × E₂ → E₁ × E₂) x with
  | (v, w) => v - w
Tactic: apply IsLittleO.add
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (hypothesis)
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 𝕜
⊢ IsLittleO (E := F) (F := 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))
    fun (x : (E₁ × E₂) × E₁ × E₂) ↦
    match (motive := (E₁ × E₂) × E₁ × E₂ → E₁) x with
    | (v, w) => v.1 - w.1
have h : Tendsto (fun (x : ((E₁ × E₂) × E₁ × E₂) × E₁) ↦ (x.2, (Prod.snd ∘ Prod.snd ∘ Prod.fst) x))
  (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1) (𝓝 u.1 ×ˢ 𝓝 u.2)
Tactic: have h := tendsto_snd.prodMk <| tendsto_snd.comp <| tendsto_snd.comp <|
              tendsto_fst (f := (𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)) (g := 𝓝 u.1)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Partial (goal)
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_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
h :
  Tendsto (fun (x : ((E₁ × E₂) × E₁ × E₂) × E₁) ↦ (x.2, (Prod.snd ∘ Prod.snd ∘ Prod.fst) x))
    (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1) (𝓝 u.1 ×ˢ 𝓝 u.2)
this : NormedSpace ℝ E₁ := RestrictScalars.normedSpace ℝ 𝕜 E₁
⊢ IsLittleO (E := F) (F := 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))
    fun (x : (E₁ × E₂) × E₁ × E₂) ↦
    match (motive := (E₁ × E₂) × E₁ × E₂ → E₁) x with
    | (v, w) => v.1 - w.1
have df' : ∀ᶠ (p : ((E₁ × E₂) × E₁ × E₂) × E₁) in ((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝[Set.univ] u.1,
  HasFDerivWithinAt.{u_1, u_2, u_4} (𝕜 := 𝕜) (F := F)
    (fun (x : E₁) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → F) p.1 with
      | (v, w) => f x w.2)
    (match (motive := (E₁ × E₂) × E₁ × E₂ → E₁ →L[𝕜] F) p.1 with
    | (v, w) => f₁ p.2 w.2)
    Set.univ p.2
Tactic: apply isLittleO_sub_sub_fderiv (α := (E₁ × E₂) × (E₁ × E₂))
              (f := fun (v, w) x => f x w.2) (f' := fun (v, w) x => f₁ x w.2)
              (tendsto_fst.comp tendsto_fst) (tendsto_fst.comp tendsto_snd)