awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
obtain :
  ∀ (δ : ℝ) (hδ₀ : δ > 0) (hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}),
    ∀ᶠ (x : E) in 𝓝[s] a,
      ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a x, ω x : F) ((ω a : (a : E) → F) (x - a) : F)‖ ≤
        ε * ‖x - a‖
⊢ ∀ᶠ (x : E) in 𝓝[s] a,
    ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a x, ω x : F) ((ω a : (a : E) → F) (x - a) : F)‖ ≤
      ε * ‖x - a‖

Tactic:
obtain ⟨δ, hδ₀, hδ⟩ : ∃ δ > 0,
      ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε} := by
    rw [← Metric.mem_nhdsWithin_iff, setOf_and, inter_mem_iff]
    exact ⟨hω, (hω.self_of_nhdsWithin ha).eventually <| closedBall_mem_nhds _ hε⟩
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
rw :
  ∀ᶠ (x : E) in 𝓝 a,
    x ∈ s →
      ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a x, ω x : F) ((ω a : (a : E) → F) (x - a) : F)‖ ≤
        ε * ‖x - a‖
⊢ ∀ᶠ (x : E) in 𝓝[s] a,
    ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a x, ω x : F) ((ω a : (a : E) → F) (x - a) : F)‖ ≤
      ε * ‖x - a‖

Tactic:
rw [eventually_nhdsWithin_iff]

Premises used: eventually_nhdsWithin_iff
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
h :
  ∀ (b : E) (hb : b ∈ ball a δ) (hbs : b ∈ s),
    ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a b, ω x : F) ((ω a : (a : E) → F) (b - a) : F)‖ ≤
      ε * ‖b - a‖
⊢ ∀ᶠ (x : E) in 𝓝 a,
    x ∈ s →
      ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a x, ω x : F) ((ω a : (a : E) → F) (x - a) : F)‖ ≤
        ε * ‖x - a‖

Tactic:
filter_upwards [Metric.ball_mem_nhds _ hδ₀] with b hb hbs

Premises used: Metric.ball_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
⊢ a ∈ ball a δ ∩ s

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
⊢ b ∈ ball a δ ∩ s

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
⊢ [a -[ℝ] b] ⊆ ball a δ ∩ s

Tactic:
have hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s :=
    ((convex_ball _ _).inter hs).segment_subset (by simp [*]) (by simp [*])
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
h : norm.{u_3} (E := F) (∫ᶜ (x : E) in Path.segment a b, (ω x - ω a)) ≤ ε * ‖b - a‖
h₁ : CurveIntegrable ω (Path.segment a b)
h₂ : CurveIntegrable.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ω a) (Path.segment a b)
⊢ ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a b, ω x : F) ((ω a : (a : E) → F) (b - a) : F)‖ ≤
    ε * ‖b - a‖

Tactic:
rw [← curveIntegral_segment_const, ← curveIntegral_fun_sub]

Premises used: curveIntegral_segment_const, curveIntegral_fun_sub
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ norm.{u_3} (E := F) (∫ᶜ (x : E) in Path.segment a b, (ω x - ω a)) ≤ ε * ‖b - a‖

Tactic:
norm_curveIntegral_segment_le fun z hz ↦ ?_

Premises used: norm_curveIntegral_segment_le
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
h : ∀ (z : E) (hz : z ∈ [a -[ℝ] b]), ‖ω z - ω a‖ ≤ ε
⊢ norm.{u_3} (E := F) (∫ᶜ (x : E) in Path.segment a b, (ω x - ω a)) ≤ ε * ‖b - a‖

Tactic:
refine norm_curveIntegral_segment_le fun z hz ↦ ?_

Premises used: norm_curveIntegral_segment_le
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
z : E
hz : z ∈ [a -[ℝ] b]
⊢ ‖ω z - ω a‖ ≤ ε

Tactic:
simpa [dist_eq_norm] using (hδ (hsub hz)).2

Premises used: dist_eq_norm, And.right
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
h :
  IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a)) volume 0 1
⊢ CurveIntegrable ω (Path.segment a b)

Tactic:
rw [curveIntegrable_segment]

Premises used: curveIntegrable_segment
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a)) volume 0 1

Tactic:
ContinuousOn.intervalIntegrable_of_Icc zero_le_one fun t ht ↦ ?_

Premises used: ContinuousOn.intervalIntegrable_of_Icc, zero_le_one
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
h :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t),
    ContinuousWithinAt.{0, u_3} (Y := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
      (Icc 0 1) t
⊢ IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a)) volume 0 1

Tactic:
refine ContinuousOn.intervalIntegrable_of_Icc zero_le_one fun t ht ↦ ?_

Premises used: ContinuousOn.intervalIntegrable_of_Icc, zero_le_one
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ ContinuousWithinAt.{0, u_3} (Y := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
    (Icc 0 1) t

Tactic:
((hδ ?_).1.eval_const _).comp AffineMap.lineMap_continuous.continuousWithinAt ?_

Premises used: AffineMap.lineMap_continuous, ContinuousWithinAt.eval_const, And.left, ContinuousWithinAt.comp, Continuous.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
h : Membership.mem (α := E) (ball a δ ∩ s) ((lineMap a b : (a : ℝ) → E) t : E)
h₁ : MapsTo (α := ℝ) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1) s
⊢ ContinuousWithinAt.{0, u_3} (Y := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
    (Icc 0 1) t

Tactic:
refine ((hδ ?_).1.eval_const _).comp AffineMap.lineMap_continuous.continuousWithinAt ?_

Premises used: AffineMap.lineMap_continuous, ContinuousWithinAt.eval_const, And.left, ContinuousWithinAt.comp, Continuous.continuousWithinAt
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ Membership.mem (α := E) (ball a δ ∩ s) ((lineMap a b : (a : ℝ) → E) t : E)

Tactic:
hsub <| lineMap_mem_segment ℝ a b ht

Premises used: Real, lineMap_mem_segment
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ Membership.mem (α := E) (ball a δ ∩ s) ((lineMap a b : (a : ℝ) → E) t : E)

Tactic:
exact hsub <| lineMap_mem_segment ℝ a b ht

Premises used: Real, lineMap_mem_segment
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
h : [a -[ℝ] b] ⊆ s
⊢ MapsTo (α := ℝ) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1) s

Tactic:
rw [mapsTo_iff_image_subset, ← segment_eq_image_lineMap]

Premises used: Set.mapsTo_iff_image_subset, segment_eq_image_lineMap
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ [a -[ℝ] b] ⊆ s

Tactic:
hs.segment_subset ha hbs

Premises used: Convex.segment_subset
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ [a -[ℝ] b] ⊆ s

Tactic:
exact hs.segment_subset ha hbs

Premises used: Convex.segment_subset
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ (ω a : (a : E) → F) (b - a)) volume 0 1

Tactic:
intervalIntegrable_const

Premises used: intervalIntegrable_const
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ (ω a : (a : E) → F) (b - a)) volume 0 1

Tactic:
exact intervalIntegrable_const

Premises used: intervalIntegrable_const
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ContinuousOn ω s
ha : a ∈ s
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) s a

Tactic:
.curveIntegral_segment_source' hs (mem_of_superset self_mem_nhdsWithin hω) ha

Premises used: self_mem_nhdsWithin, HasFDerivWithinAt.curveIntegral_segment_source', Filter.mem_of_superset
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
ω : E → E →L[𝕜] F
hω : ∀ᶠ (z : E) in 𝓝 a, ContinuousAt ω z
⊢ ∀ᶠ (x : E) in 𝓝[univ] a, ContinuousWithinAt ω univ x

Tactic:
simpa only [nhdsWithin_univ, continuousWithinAt_univ]

Premises used: nhdsWithin_univ, continuousWithinAt_univ
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
ω : E → E →L[𝕜] F
hω : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ω
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) a

Tactic:
.curveIntegral_segment_source' <| .of_forall fun _ ↦ hω.continuousAt

Premises used: Filter.Eventually.of_forall, Continuous.continuousAt, HasFDerivAt.curveIntegral_segment_source'
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set ((↑I : Type) × (↑I : Type))
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : Homotopy (↑γ₁ : C((↑I : Type), E)) (↑γ₂ : C((↑I : Type), E))
hs : s.Countable
hφt :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          Membership.mem (α := E) t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
hω :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            HasFDerivWithinAt ω (dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))) t
              ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            ∀ u ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
              ∀ v ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
                Eq.{u_3 + 1} (α := F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[ℝ] F) u : E →L[ℝ] F) :
                        (a : E) → F)
                      v :
                    F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) :
                        (a : E) → F)
                      u :
                    F)
hcontdiff :
  ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
    (fun (xy : ℝ × ℝ) ↦
      Set.IccExtend (a := 0) (b := 1) ⋯
        (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2)
    (Icc 0 1)
⊢ let U := SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1);
  U = SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)

Tactic:
set U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1 with hU

Premises used: Real, Prod, OfNat.ofNat, Set.Ioo, Set