awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ Eq (α := (x : T) → G)
    ((fun (p_1 : (E × F) × E × F) ↦
        HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
      fun (x : (E × F) × E × F) ↦ (p, p) + x)
    fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2)
have h₁ : ∀ (x₁ : E) (y₁ : F) (x₂ : E) (y₂ : F),
  Eq.{u_4 + 1} (α := G)
    (((fun (p_1 : (E × F) × E × F) ↦
            HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
          fun (x : (E × F) × E × F) ↦ (p, p) + x)
        ((x₁, y₁), x₂, y₂) :
      G)
    ((h.deriv (((x₁, y₁), x₂, y₂).1 - ((x₁, y₁), x₂, y₂).2) : (a : E × F) → G)
        (((x₁, y₁), x₂, y₂).2.1, ((x₁, y₁), x₂, y₂).1.2) :
      G)
Tactic: ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
x₁ : E
y₁ : F
x₂ : E
y₂ : F
⊢ Eq.{u_4 + 1} (α := G)
    (((fun (p_1 : (E × F) × E × F) ↦
            HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
          fun (x : (E × F) × E × F) ↦ (p, p) + x)
        ((x₁, y₁), x₂, y₂) :
      G)
    ((h.deriv (((x₁, y₁), x₂, y₂).1 - ((x₁, y₁), x₂, y₂).2) : (a : E × F) → G)
        (((x₁, y₁), x₂, y₂).2.1, ((x₁, y₁), x₂, y₂).1.2) :
      G)
have h₁ : ∀ (x : E) (y : F),
  Eq.{u_4 + 1} (α := G)
    (((fun (p : (E × F) × E × F) ↦
            HSub.hSub (β := G) (b p.1 - b p.2) ((h.deriv (x, y) : (a : E × F) → G) (p.1 - p.2) : G)) ∘
          fun (x_1 : (E × F) × E × F) ↦ ((x, y), x, y) + x_1)
        ((x₁, y₁), x₂, y₂) :
      G)
    ((h.deriv (((x₁, y₁), x₂, y₂).1 - ((x₁, y₁), x₂, y₂).2) : (a : E × F) → G)
        (((x₁, y₁), x₂, y₂).2.1, ((x₁, y₁), x₂, y₂).1.2) :
      G)
Tactic: rcases p with ⟨x, y⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
T : Type (max u_3 u_2) := (E × F) × E × F
x₁ : E
y₁ : F
x₂ : E
y₂ : F
x : E
y : F
⊢ Eq.{u_4 + 1} (α := G)
    (((fun (p : (E × F) × E × F) ↦
            HSub.hSub (β := G) (b p.1 - b p.2) ((h.deriv (x, y) : (a : E × F) → G) (p.1 - p.2) : G)) ∘
          fun (x_1 : (E × F) × E × F) ↦ ((x, y), x, y) + x_1)
        ((x₁, y₁), x₂, y₂) :
      G)
    ((h.deriv (((x₁, y₁), x₂, y₂).1 - ((x₁, y₁), x₂, y₂).2) : (a : E × F) → G)
        (((x₁, y₁), x₂, y₂).2.1, ((x₁, y₁), x₂, y₂).1.2) :
      G)
have h₁ : b (x, y) + b (x₁, y) + (b (x, y₁) + b (x₁, y₁)) - (b (x, y) + b (x₂, y) + (b (x, y₂) + b (x₂, y₂))) -
    (b (x, y) + b (x, y₁) + (b (x, y) + b (x₁, y)) - (b (x, y) + b (x, y₂) + (b (x, y) + b (x₂, y)))) =
  b (x₁, y₁) - b (x₂, y₂)
Tactic: simp only [map_sub, deriv_apply, Function.comp_apply, Prod.mk_add_mk, h.add_right, h.add_left,
        Prod.mk_sub_mk, h.map_sub_left, h.map_sub_right, sub_add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ IsLittleO (E := G) (F := E × F) (𝓝 0) (fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2))
    fun (x : T) ↦ x.1 - x.2
have refine : IsLittleO (E := ℝ) (F := E × F) (𝓝 0) (fun (x : T) ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) fun (x : T) ↦ x.1 - x.2
Tactic: refine h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp.trans_isLittleO ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ IsLittleO (E := ℝ) (F := E × F) (𝓝 0) (fun (x : T) ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) fun (x : T) ↦ x.1 - x.2
have suffices : IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : T) ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) fun (x : T) ↦ ‖x.1 - x.2‖ * 1
Tactic: suffices (fun x : T ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 by
        simpa only [mul_one, isLittleO_norm_right] using this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : T) ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) fun (x : T) ↦ ‖x.1 - x.2‖ * 1
have refine : Filter.Tendsto (β := ℝ) (fun (x : T) ↦ ‖(x.2.1, x.1.2)‖) (𝓝 0) (𝓝 0)
Tactic: refine (isBigO_refl _ _).mul_isLittleO ((isLittleO_one_iff _).2 ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
⊢ IsLittleO (α := (E × F) × E × F) (E := G) (F := E × F) (𝓝 0)
    ((fun (p_1 : (E × F) × E × F) ↦
        HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
      fun (x : (E × F) × E × F) ↦ (p, p) + x)
    ((fun (p : (E × F) × E × F) ↦ p.1 - p.2) ∘ fun (x : (E × F) × E × F) ↦ (p, p) + x)
have _ : Eq (α := (x : T) → G)
  ((fun (p_1 : (E × F) × E × F) ↦
      HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
    fun (x : (E × F) × E × F) ↦ (p, p) + x)
  fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2)
Tactic: calc
    _ = fun x ↦ h.deriv (x.1 - x.2) (x.2.1, x.1.2) := by
      ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
      rcases p with ⟨x, y⟩
      simp only [map_sub, deriv_apply, Function.comp_apply, Prod.mk_add_mk, h.add_right, h.add_left,
        Prod.mk_sub_mk, h.map_sub_left, h.map_sub_right, sub_add_sub_cancel]
      abel
    -- _ =O[𝓝 (0 : T)] fun x ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖ :=
    --     h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp
    -- _ = o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 := _
    _ =o[𝓝 (0 : T)] fun x ↦ x.1 - x.2 := by
      -- TODO : add 2 `calc` steps instead of the next 3 lines
      refine h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp.trans_isLittleO ?_
      suffices (fun x : T ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 by
        simpa only [mul_one, isLittleO_norm_right] using this
      refine (isBigO_refl _ _).mul_isLittleO ((isLittleO_one_iff _).2 ?_)
      -- TODO: `continuity` fails
      exact (continuous_snd.fst.prodMk continuous_fst.snd).norm.tendsto' _ _ (by simp)
    _ = _ := by simp [T, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
_ :
  Eq (α := (x : T) → G)
    ((fun (p_1 : (E × F) × E × F) ↦
        HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
      fun (x : (E × F) × E × F) ↦ (p, p) + x)
    fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2)
⊢ IsLittleO (α := (E × F) × E × F) (E := G) (F := E × F) (𝓝 0)
    ((fun (p_1 : (E × F) × E × F) ↦
        HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
      fun (x : (E × F) × E × F) ↦ (p, p) + x)
    ((fun (p : (E × F) × E × F) ↦ p.1 - p.2) ∘ fun (x : (E × F) × E × F) ↦ (p, p) + x)
have _₁ : IsLittleO (E := G) (F := E × F) (𝓝 0) (fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2))
  fun (x : T) ↦ x.1 - x.2
Tactic: calc
    _ = fun x ↦ h.deriv (x.1 - x.2) (x.2.1, x.1.2) := by
      ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
      rcases p with ⟨x, y⟩
      simp only [map_sub, deriv_apply, Function.comp_apply, Prod.mk_add_mk, h.add_right, h.add_left,
        Prod.mk_sub_mk, h.map_sub_left, h.map_sub_right, sub_add_sub_cancel]
      abel
    -- _ =O[𝓝 (0 : T)] fun x ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖ :=
    --     h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp
    -- _ = o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 := _
    _ =o[𝓝 (0 : T)] fun x ↦ x.1 - x.2 := by
      -- TODO : add 2 `calc` steps instead of the next 3 lines
      refine h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp.trans_isLittleO ?_
      suffices (fun x : T ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 by
        simpa only [mul_one, isLittleO_norm_right] using this
      refine (isBigO_refl _ _).mul_isLittleO ((isLittleO_one_iff _).2 ?_)
      -- TODO: `continuity` fails
      exact (continuous_snd.fst.prodMk continuous_fst.snd).norm.tendsto' _ _ (by simp)
    _ = _ := by simp [T, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
h : IsBoundedBilinearMap 𝕜 b
p : E × F
T : Type (max u_3 u_2) := (E × F) × E × F
_ :
  Eq (α := (x : T) → G)
    ((fun (p_1 : (E × F) × E × F) ↦
        HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
      fun (x : (E × F) × E × F) ↦ (p, p) + x)
    fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2)
_₁ :
  IsLittleO (E := G) (F := E × F) (𝓝 0) (fun (x : T) ↦ (h.deriv (x.1 - x.2) : (a : E × F) → G) (x.2.1, x.1.2))
    fun (x : T) ↦ x.1 - x.2
⊢ IsLittleO (α := (E × F) × E × F) (E := G) (F := E × F) (𝓝 0)
    ((fun (p_1 : (E × F) × E × F) ↦
        HSub.hSub (β := G) (b p_1.1 - b p_1.2) ((h.deriv p : (a : E × F) → G) (p_1.1 - p_1.2) : G)) ∘
      fun (x : (E × F) × E × F) ↦ (p, p) + x)
    ((fun (p : (E × F) × E × F) ↦ p.1 - p.2) ∘ fun (x : (E × F) × E × F) ↦ (p, p) + x)
have _₂ : Eq (α := (x : T) → E × F) (fun (x : T) ↦ x.1 - x.2)
  ((fun (p : (E × F) × E × F) ↦ p.1 - p.2) ∘ fun (x : (E × F) × E × F) ↦ (p, p) + x)
Tactic: calc
    _ = fun x ↦ h.deriv (x.1 - x.2) (x.2.1, x.1.2) := by
      ext ⟨⟨x₁, y₁⟩, ⟨x₂, y₂⟩⟩
      rcases p with ⟨x, y⟩
      simp only [map_sub, deriv_apply, Function.comp_apply, Prod.mk_add_mk, h.add_right, h.add_left,
        Prod.mk_sub_mk, h.map_sub_left, h.map_sub_right, sub_add_sub_cancel]
      abel
    -- _ =O[𝓝 (0 : T)] fun x ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖ :=
    --     h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp
    -- _ = o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 := _
    _ =o[𝓝 (0 : T)] fun x ↦ x.1 - x.2 := by
      -- TODO : add 2 `calc` steps instead of the next 3 lines
      refine h.toContinuousLinearMap.deriv₂.isBoundedBilinearMap.isBigO_comp.trans_isLittleO ?_
      suffices (fun x : T ↦ ‖x.1 - x.2‖ * ‖(x.2.1, x.1.2)‖) =o[𝓝 0] fun x ↦ ‖x.1 - x.2‖ * 1 by
        simpa only [mul_one, isLittleO_norm_right] using this
      refine (isBigO_refl _ _).mul_isLittleO ((isLittleO_one_iff _).2 ?_)
      -- TODO: `continuity` fails
      exact (continuous_snd.fst.prodMk continuous_fst.snd).norm.tendsto' _ _ (by simp)
    _ = _ := by simp [T, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Bilinear (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
⊢ fderivWithin 𝕜 b u p = h.deriv p
have rw : fderiv 𝕜 b p = h.deriv p
Tactic: rw [DifferentiableAt.fderivWithin (h.differentiableAt p) hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ Eq (α := (p : E × E) → G)
    (fun (p : E × E) ↦ HSub.hSub (β := G) ((g ∘ f) p.1 - (g ∘ f) p.2) ((g' ∘SL f' : (a : E) → G) (p.1 - p.2) : G))
    fun (p : E × E) ↦
    HAdd.hAdd (β := G) (HSub.hSub (β := G) (g (f p.1) - g (f p.2)) ((g' : (a : F) → G) (f p.1 - f p.2) : G))
      ((g' : (a : F) → G) (HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)) : G)
have h : ∀ (x : E × E),
  HSub.hSub (β := G) ((g ∘ f) x.1 - (g ∘ f) x.2) ((g' ∘SL f' : (a : E) → G) (x.1 - x.2) : G) =
    HAdd.hAdd (β := G) (HSub.hSub (β := G) (g (f x.1) - g (f x.2)) ((g' : (a : F) → G) (f x.1 - f x.2) : G))
      ((g' : (a : F) → G) (HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)) : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
⊢ HasFDerivAtFilter (g ∘ f) (g' ∘SL f') L
have refine : IsLittleOTVS.{u_1, u_2, u_4, u_2} 𝕜 (E := G) (F := E) L
  (fun (p : E × E) ↦ HSub.hSub (β := G) (g (f p.1) - g (f p.2)) ((g' : (a : F) → G) (f p.1 - f p.2) : G))
  fun (p : E × E) ↦ p.1 - p.2
Tactic: refine .of_isLittleOTVS <| calc
    (fun p ↦ (g ∘ f) p.1 - (g ∘ f) p.2 - (g' ∘L f') (p.1 - p.2))
      = fun p ↦ (g (f p.1) - g (f p.2) - g' (f p.1 - f p.2)) +
          g' (f p.1 - f p.2 - f' (p.1 - p.2)) := by
      ext; simp
    _ =o[𝕜; L] (fun p ↦ p.1 - p.2) := .add ?Hg ?Hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
g : F → G
g' : F →L[𝕜] G
L' : Filter (F × F)
hg : HasFDerivAtFilter g g' L'
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L'
refine :
  IsLittleOTVS.{u_1, u_2, u_4, u_2} 𝕜 (E := G) (F := E) L
    (fun (p : E × E) ↦ HSub.hSub (β := G) (g (f p.1) - g (f p.2)) ((g' : (a : F) → G) (f p.1 - f p.2) : G))
    fun (p : E × E) ↦ p.1 - p.2
⊢ HasFDerivAtFilter (g ∘ f) (g' ∘SL f') L
have refine₁ : IsLittleOTVS.{u_1, u_2, u_4, u_2} 𝕜 (E := G) (F := E) L
  (fun (p : E × E) ↦ (g' : (a : F) → G) (HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)))
  fun (p : E × E) ↦ p.1 - p.2
Tactic: refine .of_isLittleOTVS <| calc
    (fun p ↦ (g ∘ f) p.1 - (g ∘ f) p.2 - (g' ∘L f') (p.1 - p.2))
      = fun p ↦ (g (f p.1) - g (f p.2) - g' (f p.1 - f p.2)) +
          g' (f p.1 - f p.2 - f' (p.1 - p.2)) := by
      ext; simp
    _ =o[𝕜; L] (fun p ↦ p.1 - p.2) := .add ?Hg ?Hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
f' : E →L[𝕜] F
x : E
g : F → G
g' : F →L[𝕜] G
t : Set F
y : F
hg : HasFDerivWithinAt g g' t y
hf : HasFDerivAt f f' x
ht : ∀ᶠ (x' : E) in 𝓝 x, f x' ∈ t
hy : y = f x
⊢ HasFDerivAt (g ∘ f) (g' ∘SL f') x
have hg₁ : HasFDerivWithinAt g g' t (f x)
Tactic: subst y
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
x : E
s : Set E
g : F → G
t : Set F
y : F
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hy : f x = y
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (g ∘ f) s x) (fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)
have hg₁ : DifferentiableWithinAt 𝕜 g t (f x)
Tactic: subst hy
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
x : E
s : Set E
g : F → G
t : Set F
y : F
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hy : f x = y
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (fun (y : E) ↦ g (f y)) s x) (fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x)
have hg₁ : DifferentiableWithinAt 𝕜 g t (f x)
Tactic: subst hy
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
y : F
s : Set E
t : Set F
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hy : f x = y
v : E
⊢ Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t y : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    ((fderivWithin 𝕜 (g ∘ f) s x : (a : E) → G) v : G)
have subst : ∀ (hg : DifferentiableWithinAt 𝕜 g t (f x)),
  Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    ((fderivWithin 𝕜 (g ∘ f) s x : (a : E) → G) v : G)
Tactic: subst y
Cleared hypotheses: y, hg, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
s : Set E
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
v : E
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    ((fderivWithin 𝕜 (g ∘ f) s x : (a : E) → G) v : G)
have rw : Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
  ((fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x : (a : E) → G) v : G)
Tactic: rw [fderivWithin_comp x hg hf h hxs, coe_comp', Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
s : Set E
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
v : E
hg : DifferentiableWithinAt 𝕜 g t (f x)
rw :
  Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    ((fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x : (a : E) → G) v : G)
⊢ Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    ((fderivWithin 𝕜 (g ∘ f) s x : (a : E) → G) v : G)
have rw₁ : Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
  (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := F) (⇑(fderivWithin 𝕜 g t (f x)) : (a : F) → G)
      (⇑(fderivWithin 𝕜 f s x) : (a : E) → F) v :
    G)
Tactic: rw [fderivWithin_comp x hg hf h hxs, coe_comp', Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Comp (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
g : F → G
f : E → F
x : E
s : Set E
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
v : E
hg : DifferentiableWithinAt 𝕜 g t (f x)
rw :
  Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    ((fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x : (a : E) → G) v : G)
rw₁ :
  Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := F) (⇑(fderivWithin 𝕜 g t (f x)) : (a : F) → G)
        (⇑(fderivWithin 𝕜 f s x) : (a : E) → F) v :
      G)
⊢ Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
    ((fderivWithin 𝕜 (g ∘ f) s x : (a : E) → G) v : G)
have rw₂ : Eq.{u_4 + 1} (α := G) ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
  ((fderivWithin 𝕜 g t (f x) : (a : F) → G) ((fderivWithin 𝕜 f s x : (a : E) → F) v : F) : G)
Tactic: rw [fderivWithin_comp x hg hf h hxs, coe_comp', Function.comp_apply]