Module: Mathlib.Analysis.Calculus.FDeriv.Partial

Goal state before:
pp: case h₁
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E₁
inst✝⁵ : NormedSpace 𝕜 E₁
inst✝⁴ : NormedAddCommGroup E₂
inst✝³ : NormedSpace 𝕜 E₂
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : 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 ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ 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 𝕜 := ⋯
⊢ (fun x ↦ f x.1.1 x.2.2 - f x.2.1 x.2.2 - (↿f₁ u) (x.1.1 - x.2.1)) =o[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2] fun x ↦
    match x with
    | (v, w) => v - w

pp: case h₂
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E₁
inst✝⁵ : NormedSpace 𝕜 E₁
inst✝⁴ : NormedAddCommGroup E₂
inst✝³ : NormedSpace 𝕜 E₂
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : 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 ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ 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 𝕜 := ⋯
⊢ (fun x ↦ f x.1.1 x.1.2 - f x.1.1 x.2.2 - (↿f₂ u) (x.1.2 - x.2.2)) =o[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2] fun x ↦
    match x with
    | (v, w) => v - w

Tactic:
· 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]

Goal state after:
case h₂
𝕜 : Type u_1
E₁ : Type u_2
E₂ : Type u_3
F : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E₁
inst✝⁵ : NormedSpace 𝕜 E₁
inst✝⁴ : NormedAddCommGroup E₂
inst✝³ : NormedSpace 𝕜 E₂
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : 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 ↦ f x v.2) (↿f₁ v) v.1
df₂ : ∀ᶠ (v : E₁ × E₂) in 𝓝 u.1 ×ˢ 𝓝 u.2, HasFDerivAt (fun x ↦ 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 𝕜 := ⋯
⊢ (fun x ↦ f x.1.1 x.1.2 - f x.1.1 x.2.2 - (↿f₂ u) (x.1.2 - x.2.2)) =o[(𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2] fun x ↦
    match x with
    | (v, w) => v - w