awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
refine : ContinuousOn ω s
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∫ᶜ (x : E) in Path.segment b x, ω x) (ω b) s b

Tactic:
refine HasFDerivWithinAt.curveIntegral_segment_source hs ?_ hb

Premises used: HasFDerivWithinAt.curveIntegral_segment_source
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
⊢ ContinuousOn ω s

Tactic:
fun x hx ↦ (hω x hx).continuousWithinAt

Premises used: ContinuousOn, HasFDerivWithinAt.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
⊢ ContinuousOn ω s

Tactic:
exact fun x hx ↦ (hω x hx).continuousWithinAt

Premises used: HasFDerivWithinAt.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
inl :
  ∀ (hs : Convex.{0, u_2} ℝ (E := E) ∅)
    (hω : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt ω (dω x) ∅ x)
    (hdω :
      ∀ (a : E),
        Membership.mem (γ := Set E) ∅ a →
          ∀ x ∈ tangentConeAt ℝ ∅ a,
            ∀ y ∈ tangentConeAt ℝ ∅ a,
              Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
                ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)),
    ∃ (f : E → F), ∀ (a : E), Membership.mem (γ := Set E) ∅ a → HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) ∅ a
inr : ∀ (a : E) (ha : a ∈ s), ∃ (f : E → F), ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex.{0, u_2} ℝ (E := E) ∅
hω : ∀ (x : E), Membership.mem (γ := Set E) ∅ x → HasFDerivWithinAt ω (dω x) ∅ x
hdω :
  ∀ (a : E),
    Membership.mem (γ := Set E) ∅ a →
      ∀ x ∈ tangentConeAt ℝ ∅ a,
        ∀ y ∈ tangentConeAt ℝ ∅ a,
          Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
            ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
⊢ ∃ (f : E → F), ∀ (a : E), Membership.mem (γ := Set E) ∅ a → HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) ∅ a

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
a : E
ha : a ∈ s
h :
  ∀ a_1 ∈ s,
    HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ curveIntegral ω (Path.segment a x)) (ω a_1) s a_1
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a

Tactic:
use (curveIntegral ω <| .segment a ·)

Premises used: curveIntegral, Path.segment
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
a : E
ha : a ∈ s
b : E
hb : b ∈ s
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ curveIntegral ω (Path.segment a x)) (ω b) s b

Tactic:
hs.hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric hω hdω ha hb

Premises used: Convex.hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
a : E
ha : a ∈ s
b : E
hb : b ∈ s
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ curveIntegral ω (Path.segment a x)) (ω b) s b

Tactic:
exact hs.hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric hω hdω ha hb

Premises used: Convex.hasFDerivWithinAt_curveIntegral_segment_of_hasFDerivWithinAt_symmetric
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a

Tactic:
hs.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric
    (fun a ha ↦ (hω a ha).hasFDerivWithinAt) hdω

Premises used: Convex.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a

Tactic:
hs.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric hω fun a ha x _ y _ ↦ ?_

Premises used: Convex.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
refine :
  ∀ (a : E) (ha : a ∈ s),
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a

Tactic:
refine hs.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric hω fun a ha x _ y _ ↦ ?_

Premises used: Convex.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
a : E
ha : a ∈ s
x : E
h_1 : x ∈ tangentConeAt ℝ s a
y : E
h_2 : y ∈ tangentConeAt ℝ s a
hs₁ : UniqueDiffWithinAt ℝ s a
h : DifferentiableAt ℝ ω a
⊢ Eq.{u_3 + 1} (α := F) ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
    ((((fderivWithin ℝ ω s a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)

Tactic:
rw [fderivWithin_eq_fderiv, hdω a ha]

Premises used: fderivWithin_eq_fderiv
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
a : E
ha : a ∈ s
x : E
h : x ∈ tangentConeAt ℝ s a
y : E
h_1 : y ∈ tangentConeAt ℝ s a
⊢ UniqueDiffWithinAt ℝ s a

Tactic:
hso.uniqueDiffOn a ha

Premises used: IsOpen.uniqueDiffOn
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
a : E
ha : a ∈ s
x : E
h : x ∈ tangentConeAt ℝ s a
y : E
h_1 : y ∈ tangentConeAt ℝ s a
⊢ DifferentiableAt ℝ ω a

Tactic:
hω.differentiableAt (hso.mem_nhds ha)

Premises used: DifferentiableOn.differentiableAt, IsOpen.mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
a : E
ha : a ∈ s
x : E
h : x ∈ tangentConeAt ℝ s a
y : E
h_1 : y ∈ tangentConeAt ℝ s a
⊢ UniqueDiffWithinAt ℝ s a

Tactic:
exacts [hso.uniqueDiffOn a ha, hω.differentiableAt (hso.mem_nhds ha)]

Premises used: DifferentiableOn.differentiableAt, IsOpen.mem_nhds, IsOpen.uniqueDiffOn
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
obtain :
  ∀ (f : E → F) (hf : ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a),
    ∃ (f : E → F), ∀ a ∈ s, HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) a
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) a

Tactic:
obtain ⟨f, hf⟩ : ∃ f, ∀ a ∈ s, HasFDerivWithinAt f (ω a) s a := by
    refine hs.exists_forall_hasFDerivWithinAt_of_fderivWithin_symmetric hω fun a ha x _ y _ ↦ ?_
    rw [fderivWithin_eq_fderiv, hdω a ha]
    exacts [hso.uniqueDiffOn a ha, hω.differentiableAt (hso.mem_nhds ha)]
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
f : E → F
hf : ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) a

Tactic:
⟨f, fun a ha ↦ (hf a ha).hasFDerivAt (hso.mem_nhds ha)⟩

Premises used: IsOpen.mem_nhds, Exists.intro, HasFDerivWithinAt.hasFDerivAt
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
s : Set E
ω : E → E →L[𝕜] F
inst_7 : CompleteSpace F
hs : Convex ℝ s
hso : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hω : DifferentiableOn ℝ ω s
hdω :
  ∀ a ∈ s,
    ∀ (x y : E),
      Eq.{u_3 + 1} (α := F) ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
        ((((fderiv ℝ ω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
f : E → F
hf : ∀ a ∈ s, HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) s a
⊢ ∃ (f : E → F), ∀ a ∈ s, HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f (ω a) a

Tactic:
exact ⟨f, fun a ha ↦ (hf a ha).hasFDerivAt (hso.mem_nhds ha)⟩
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hω :
  ∀ x ∈ s,
    HasFDerivWithinAt (𝕜 := ℝ) (F := 𝕜 →L[𝕜] E) (fun (a : 𝕜) ↦ ContinuousLinearMap.toSpanSingleton 𝕜 (f a))
      (ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
        (ContinuousLinearMap.toSpanSingleton 𝕜
          (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 : (a : E) → 𝕜 →L[𝕜] E)
            (derivWithin f s x))))
      s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_2 + 1} (α := E)
          (((((ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
                          (ContinuousLinearMap.toSpanSingleton 𝕜
                            (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 :
                                (a : E) → 𝕜 →L[𝕜] E)
                              (derivWithin f s a))) :
                        𝕜 →L[ℝ] 𝕜 →L[𝕜] E) :
                      (a : 𝕜) → 𝕜 →L[𝕜] E)
                    x :
                  𝕜 →L[𝕜] E) :
                (a : 𝕜) → E)
              y :
            E)
          (((((ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
                          (ContinuousLinearMap.toSpanSingleton 𝕜
                            (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 :
                                (a : E) → 𝕜 →L[𝕜] E)
                              (derivWithin f s a))) :
                        𝕜 →L[ℝ] 𝕜 →L[𝕜] E) :
                      (a : 𝕜) → 𝕜 →L[𝕜] E)
                    y :
                  𝕜 →L[𝕜] E) :
                (a : 𝕜) → E)
              x :
            E)
apply : 𝕜 → 𝕜 →L[ℝ] 𝕜 →L[𝕜] E
⊢ ∃ (g : 𝕜 → E), ∀ a ∈ s, HasDerivWithinAt g (f a) s a

Tactic:
apply hs.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric

Premises used: Convex.exists_forall_hasFDerivWithinAt_of_hasFDerivWithinAt_symmetric
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
a : 𝕜
ha : a ∈ s
⊢ HasFDerivWithinAt (𝕜 := ℝ) (F := 𝕜 →L[𝕜] E) (fun (a : 𝕜) ↦ ContinuousLinearMap.toSpanSingleton 𝕜 (f a))
    (ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
      (ContinuousLinearMap.toSpanSingleton 𝕜
        (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 : (a : E) → 𝕜 →L[𝕜] E)
          (derivWithin f s a))))
    s a

Tactic:
(ContinuousLinearMap.smulRightL 𝕜 𝕜 E 1).hasFDerivAt
      |>.comp_hasDerivWithinAt a (hf a ha).hasDerivWithinAt |>.restrictScalars ℝ

Premises used: Real, ContinuousLinearMap.hasFDerivAt, ContinuousLinearMap.smulRight, Set.Mem, setOf, DifferentiableWithinAt.hasDerivWithinAt, HasFDerivWithinAt, ContinuousLinearMap.smulRightL, HasFDerivAt.comp_hasDerivWithinAt, ContinuousLinearMap.toSpanSingleton, OfNat.ofNat, HasFDerivAtFilter.restrictScalars, DFunLike.coe, LinearMap.toSpanSingleton
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
a : 𝕜
ha : a ∈ s
⊢ HasFDerivWithinAt (𝕜 := ℝ) (F := 𝕜 →L[𝕜] E) (fun (a : 𝕜) ↦ ContinuousLinearMap.toSpanSingleton 𝕜 (f a))
    (ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
      (ContinuousLinearMap.toSpanSingleton 𝕜
        (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 : (a : E) → 𝕜 →L[𝕜] E)
          (derivWithin f s a))))
    s a

Tactic:
exact (ContinuousLinearMap.smulRightL 𝕜 𝕜 E 1).hasFDerivAt
      |>.comp_hasDerivWithinAt a (hf a ha).hasDerivWithinAt |>.restrictScalars ℝ

Premises used: Real, ContinuousLinearMap.hasFDerivAt, DifferentiableWithinAt.hasDerivWithinAt, ContinuousLinearMap.smulRightL, HasFDerivAt.comp_hasDerivWithinAt, OfNat.ofNat, HasFDerivAtFilter.restrictScalars, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : CompleteSpace E
f : 𝕜 → E
s : Set 𝕜
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
a : 𝕜
ha : a ∈ s
x y : 𝕜
⊢ Eq.{u_2 + 1} (α := E)
    (((((ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
                    (ContinuousLinearMap.toSpanSingleton 𝕜
                      (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 :
                          (a : E) → 𝕜 →L[𝕜] E)
                        (derivWithin f s a))) :
                  𝕜 →L[ℝ] 𝕜 →L[𝕜] E) :
                (a : 𝕜) → 𝕜 →L[𝕜] E)
              x :
            𝕜 →L[𝕜] E) :
          (a : 𝕜) → E)
        y :
      E)
    (((((ContinuousLinearMap.restrictScalars (A := 𝕜) ℝ
                    (ContinuousLinearMap.toSpanSingleton 𝕜
                      (((ContinuousLinearMap.smulRightL 𝕜 𝕜 E : (a : StrongDual 𝕜 𝕜) → E →L[𝕜] 𝕜 →L[𝕜] E) 1 :
                          (a : E) → 𝕜 →L[𝕜] E)
                        (derivWithin f s a))) :
                  𝕜 →L[ℝ] 𝕜 →L[𝕜] E) :
                (a : 𝕜) → 𝕜 →L[𝕜] E)
              y :
            𝕜 →L[𝕜] E) :
          (a : 𝕜) → E)
        x :
      E)

Tactic:
simpa using smul_comm ..

Premises used: SMulCommClass.smul_comm