-- 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))
fun :
  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)
fun₁ :
  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
⊢ 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:
calc
    fun (v, w) => f v.1 v.2 - f w.1 w.2 - ((↿f₁ u).coprod (↿f₂ u)) (v - w)
    _ = fun (v, w) => (f v.1 w.2 - f w.1 w.2 - ↿f₁ u (v.1 - w.1))
          + (f v.1 v.2 - f v.1 w.2 - ↿f₂ u (v.2 - w.2)) := by
      ext
      dsimp only [ContinuousLinearMap.coprod_apply]
      abel
    _ =o[𝓝 (u, u)] fun (v, w) => v - w := by
      let : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
      rw [nhds_prod_eq, nhds_prod_eq]
      apply IsLittleO.add
      · calc
          fun (v, w) => f v.1 w.2 - f w.1 w.2 - ↿f₁ u (v.1 - w.1)
          _ =o[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)] (fun (v, w) => v.1 - w.1 : _ → E₁) := by
            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)
            let : NormedSpace ℝ E₁ := RestrictScalars.normedSpace ℝ 𝕜 E₁
            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)
            · simpa using h.eventually df₁
            · simpa using cf₁.comp h
          _ =O[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)] (fun (v, w) => v - w : _ → E₁ × E₂) := by
            simp [isBigO_of_le]
      · calc
          fun (v, w) => f v.1 v.2 - f v.1 w.2 - ↿f₂ u (v.2 - w.2)
          _ =o[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)] (fun (v, w) => v.2 - w.2 : _ → E₂) := by
            have h := (tendsto_fst.comp <| tendsto_fst.comp tendsto_fst).prodMk <|
              tendsto_snd (f := (𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)) (g := 𝓝 u.2)
            let : NormedSpace ℝ E₂ := RestrictScalars.normedSpace ℝ 𝕜 E₂
            apply isLittleO_sub_sub_fderiv (f' := fun (v, w) y => f₂ v.1 y)
              (tendsto_snd.comp tendsto_fst) (tendsto_snd.comp tendsto_snd)
            · simpa using h.eventually df₂
            · simpa using cf₂.comp h
          _ =O[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ (𝓝 u.1 ×ˢ 𝓝 u.2)] (fun (v, w) => v - w : _ → E₁ × E₂) := by
            simp [isBigO_of_le]

Premises used: nhds, Prod.mk