awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 𝕜
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
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
⊢ 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:
apply IsLittleO.add

Premises used: Asymptotics.IsLittleO.add
-- 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 𝕜
⊢ 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)
-- 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_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₁
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
cf' :
  Tendsto
    (Function.HasUncurry.uncurry (α := (E₁ × E₂) × E₁ × E₂ → E₁ → E₁ →L[𝕜] F) fun (x : (E₁ × E₂) × E₁ × E₂) (x_1 : E₁) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → E₁ →L[𝕜] F) x with
      | (v, w) => f₁ x_1 w.2)
    (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝[Set.univ] u.1) (𝓝 (↿f₁ u))
⊢ 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

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)

Premises used: _private.0.isLittleO_sub_sub_fderiv, Set.univ, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- 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_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₁
⊢ ∀ᶠ (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:
simpa using h.eventually df₁

Premises used: Filter.Tendsto.eventually
-- 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_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₁
⊢ Tendsto
    (Function.HasUncurry.uncurry (α := (E₁ × E₂) × E₁ × E₂ → E₁ → E₁ →L[𝕜] F) fun (x : (E₁ × E₂) × E₁ × E₂) (x_1 : E₁) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → E₁ →L[𝕜] F) x with
      | (v, w) => f₁ x_1 w.2)
    (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝[Set.univ] u.1) (𝓝 (↿f₁ u))

Tactic:
simpa using cf₁.comp h

Premises used: Filter.Tendsto.comp
-- 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 𝕜
⊢ IsBigO (E := E₁) (F := E₁ × E₂) ((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2)
    (fun (x : (E₁ × E₂) × E₁ × E₂) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → E₁) x with
      | (v, w) => v.1 - w.1)
    fun (x : (E₁ × E₂) × E₁ × E₂) ↦
    match (motive := (E₁ × E₂) × E₁ × E₂ → E₁ × E₂) x with
    | (v, w) => v - w

Tactic:
simp [isBigO_of_le]

Premises used: Asymptotics.isBigO_of_le
-- 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 𝕜
fun :
  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
fun₁ :
  IsBigO (E := E₁) (F := E₁ × E₂) ((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2)
    (fun (x : (E₁ × E₂) × E₁ × E₂) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → E₁) x with
      | (v, w) => v.1 - w.1)
    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₂) ↦
      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:
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]

Premises used: SProd.sprod, nhds, Prod.fst, Prod.snd
-- 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 𝕜
⊢ Tendsto (fun (x : ((E₁ × E₂) × E₁ × E₂) × E₂) ↦ ((Prod.fst ∘ Prod.fst ∘ Prod.fst) x, x.2))
    (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.2) (𝓝 u.1 ×ˢ 𝓝 u.2)

Tactic:
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)
-- 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_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
h :
  Tendsto (fun (x : ((E₁ × E₂) × E₁ × E₂) × E₂) ↦ ((Prod.fst ∘ Prod.fst ∘ Prod.fst) x, x.2))
    (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.2) (𝓝 u.1 ×ˢ 𝓝 u.2)
this : NormedSpace ℝ E₂ := RestrictScalars.normedSpace ℝ 𝕜 E₂
df' :
  ∀ᶠ (p : ((E₁ × E₂) × E₁ × E₂) × E₂) in ((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝[Set.univ] u.2,
    HasFDerivWithinAt.{u_1, u_3, u_4} (𝕜 := 𝕜) (f p.1.1.1)
      (match (motive := (E₁ × E₂) × E₁ × E₂ → E₂ →L[𝕜] F) p.1 with
      | (v, w) => f₂ v.1 p.2)
      Set.univ p.2
cf' :
  Tendsto
    (Function.HasUncurry.uncurry (α := (E₁ × E₂) × E₁ × E₂ → E₂ → E₂ →L[𝕜] F) fun (x : (E₁ × E₂) × E₁ × E₂) (y : E₂) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → E₂ →L[𝕜] F) x with
      | (v, w) => f₂ v.1 y)
    (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝[Set.univ] u.2) (𝓝 (↿f₂ u))
⊢ 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 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₂) x with
    | (v, w) => v.2 - w.2

Tactic:
apply isLittleO_sub_sub_fderiv (f' := fun (v, w) y => f₂ v.1 y)
              (tendsto_snd.comp tendsto_fst) (tendsto_snd.comp tendsto_snd)

Premises used: _private.0.isLittleO_sub_sub_fderiv, Set.univ, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- 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_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
h :
  Tendsto (fun (x : ((E₁ × E₂) × E₁ × E₂) × E₂) ↦ ((Prod.fst ∘ Prod.fst ∘ Prod.fst) x, x.2))
    (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.2) (𝓝 u.1 ×ˢ 𝓝 u.2)
this : NormedSpace ℝ E₂ := RestrictScalars.normedSpace ℝ 𝕜 E₂
⊢ ∀ᶠ (p : ((E₁ × E₂) × E₁ × E₂) × E₂) in ((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝[Set.univ] u.2,
    HasFDerivWithinAt.{u_1, u_3, u_4} (𝕜 := 𝕜) (f p.1.1.1)
      (match (motive := (E₁ × E₂) × E₁ × E₂ → E₂ →L[𝕜] F) p.1 with
      | (v, w) => f₂ v.1 p.2)
      Set.univ p.2

Tactic:
simpa using h.eventually df₂

Premises used: Filter.Tendsto.eventually
-- 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_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
h :
  Tendsto (fun (x : ((E₁ × E₂) × E₁ × E₂) × E₂) ↦ ((Prod.fst ∘ Prod.fst ∘ Prod.fst) x, x.2))
    (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.2) (𝓝 u.1 ×ˢ 𝓝 u.2)
this : NormedSpace ℝ E₂ := RestrictScalars.normedSpace ℝ 𝕜 E₂
⊢ Tendsto
    (Function.HasUncurry.uncurry (α := (E₁ × E₂) × E₁ × E₂ → E₂ → E₂ →L[𝕜] F) fun (x : (E₁ × E₂) × E₁ × E₂) (y : E₂) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → E₂ →L[𝕜] F) x with
      | (v, w) => f₂ v.1 y)
    (((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝[Set.univ] u.2) (𝓝 (↿f₂ u))

Tactic:
simpa using cf₂.comp h

Premises used: Filter.Tendsto.comp
-- 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 𝕜
⊢ IsBigO (E := E₂) (F := E₁ × E₂) ((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2)
    (fun (x : (E₁ × E₂) × E₁ × E₂) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → E₂) x with
      | (v, w) => v.2 - w.2)
    fun (x : (E₁ × E₂) × E₁ × E₂) ↦
    match (motive := (E₁ × E₂) × E₁ × E₂ → E₁ × E₂) x with
    | (v, w) => v - w

Tactic:
simp [isBigO_of_le]

Premises used: Asymptotics.isBigO_of_le
-- 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 𝕜
fun :
  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 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₂) x with
    | (v, w) => v.2 - w.2
fun₁ :
  IsBigO (E := E₂) (F := E₁ × E₂) ((𝓝 u.1 ×ˢ 𝓝 u.2) ×ˢ 𝓝 u.1 ×ˢ 𝓝 u.2)
    (fun (x : (E₁ × E₂) × E₁ × E₂) ↦
      match (motive := (E₁ × E₂) × E₁ × E₂ → E₂) x with
      | (v, w) => v.2 - w.2)
    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₂) ↦
      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:
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: SProd.sprod, nhds, Prod.fst, Prod.snd
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
rw :
  ∀ (i_1 : ι),
    HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕜) (F := E i_1) (fun (x_1 : E i) ↦ Function.update (β := E) x i x_1 i_1)
      (Pi.single (M := fun (i_2 : ι) ↦ E i →L[𝕜] E i_2) i (ContinuousLinearMap.id 𝕜 (E i) : E i →L[𝕜] E i) i_1) y
⊢ HasFDerivAt (𝕜 := 𝕜) (Function.update (β := E) x i)
    (ContinuousLinearMap.pi (φ := E)
      (Pi.single (M := fun (i_1 : ι) ↦ E i →L[𝕜] E i_1) i (ContinuousLinearMap.id 𝕜 (E i))))
    y

Tactic:
rw [hasFDerivAt_pi]

Premises used: hasFDerivAt_pi
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
j : ι
inl :
  ∀ (y : E j),
    HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕜) (F := E j) (fun (x_1 : E j) ↦ Function.update (β := E) x j x_1 j)
      (Pi.single (M := fun (i : ι) ↦ E j →L[𝕜] E i) j (ContinuousLinearMap.id 𝕜 (E j)) j) y
inr :
  ∀ (hij : j ≠ i),
    HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕜) (F := E j) (fun (x_1 : E i) ↦ Function.update (β := E) x i x_1 j)
      (Pi.single (M := fun (i_1 : ι) ↦ E i →L[𝕜] E i_1) i (ContinuousLinearMap.id 𝕜 (E i) : E i →L[𝕜] E i) j) y
⊢ HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕜) (F := E j) (fun (x_1 : E i) ↦ Function.update (β := E) x i x_1 j)
    (Pi.single (M := fun (i_1 : ι) ↦ E i →L[𝕜] E i_1) i (ContinuousLinearMap.id 𝕜 (E i) : E i →L[𝕜] E i) j) y

Tactic:
rcases eq_or_ne j i with rfl | hij

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
x : (i : ι) → E i
j : ι
y : E j
⊢ HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕜) (F := E j) (fun (x_1 : E j) ↦ Function.update (β := E) x j x_1 j)
    (Pi.single (M := fun (i : ι) ↦ E j →L[𝕜] E i) j (ContinuousLinearMap.id 𝕜 (E j)) j) y

Tactic:
simpa using hasFDerivAt_id _

Premises used: hasFDerivAt_id