awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁
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
⊢ 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 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))
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)
-- 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₂) ↦
      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
have 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
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]
-- 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 𝕜
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
⊢ 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
have 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
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]
-- 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 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
have 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)
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)
-- 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₂) ↦ ((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₂
⊢ 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
have 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
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)
-- 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₂) ↦ ((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
⊢ 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
have 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))
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)
-- 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₂) ↦
      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
have 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
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]
-- 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 𝕜
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pi (goal)
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
⊢ 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
have 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
Tactic: rw [hasFDerivAt_pi]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pi (goal)
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 : ι
⊢ 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
have 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
Tactic: rcases eq_or_ne j i with rfl | hij
Cleared hypotheses: i, y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pi (goal)
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
⊢ 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
have 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
Tactic: rcases eq_or_ne j i with rfl | hij
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• f x ^ (n + 1) =
    ∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i
have rw : ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ ((n + 1).pred - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
  ∑ x_1 ∈ Finset.range (n + 1), f x ^ ((n + 1 + 1).pred - x_1) •> f' <• f x ^ x_1 +
    f x ^ ((n + 1 + 1).pred - (n + 1)) •> f' <• f x ^ (n + 1)
Tactic: rw [Finset.sum_range_succ _ (n + 1), Finset.smul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ ((n + 1).pred - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ ((n + 1 + 1).pred - x_1) •> f' <• f x ^ x_1 +
      f x ^ ((n + 1 + 1).pred - (n + 1)) •> f' <• f x ^ (n + 1)
have simp : ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ (n - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
  ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n + 1 - x_1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1)
Tactic: simp only [Nat.pred_eq_sub_one, add_tsub_cancel_right, tsub_self, pow_zero, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ (n - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n + 1 - x_1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1)
have simp_rw : ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n - x_1 + 1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1) =
  ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n + 1 - x_1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1)
Tactic: simp_rw [smul_comm (_ : 𝔸) (_ : 𝔸ᵐᵒᵖ), smul_smul, ← pow_succ']
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
⊢ ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n - x_1 + 1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n + 1 - x_1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1)
have h : ∀ (x : ℕ) (hx : x ∈ Finset.range (n + 1)), n - x + 1 = n + 1 - x
Tactic: congr! 5 with x hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (hypothesis)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x_1 : E
n x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ n - x + 1 = n + 1 - x
have hx₁ : x ≤ n
Tactic: simp only [Finset.mem_range, Nat.lt_succ_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Pow (goal)
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x_1 : E
n x : ℕ
hx : x ≤ n
⊢ n - x + 1 = n + 1 - x
have h : n + 1 - x = n + 1 - x
Tactic: rw [tsub_add_eq_add_tsub hx]