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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
inst_5 : NormedSpace ℝ E
s : Set E
hω : ContinuousOn ω s
hγ : ContDiffOn ℝ (F := E) 1 (⇑γ.extend : (a : ℝ) → E) I
hγs : ∀ (t : (↑I : Type)), Membership.mem (α := E) s ((γ : (a : (↑I : Type)) → E) t : E)
⊢ ContinuousOn (Y := E) (derivWithin (⇑γ.extend : (a : ℝ) → E) I) (Icc 0 1)

Tactic:
exact hγ.continuousOn_derivWithin uniqueDiffOn_Icc_zero_one le_rfl

Premises used: le_rfl, uniqueDiffOn_Icc_zero_one, ContDiffOn.continuousOn_derivWithin
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h : ∀ (x : ℝ), curveIntegralFun (ω₁ + ω₂) γ x = (curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ) x
⊢ curveIntegralFun (ω₁ + ω₂) γ = curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ

Tactic:
ext
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
x : ℝ
⊢ curveIntegralFun (ω₁ + ω₂) γ x = (curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ) x

Tactic:
simp [curveIntegralFun]

Premises used: curveIntegralFun
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ CurveIntegrable (ω₁ + ω₂) γ

Tactic:
simpa [CurveIntegrable] using IntervalIntegrable.add h₁ h₂

Premises used: IntervalIntegrable.add, CurveIntegrable
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
simp :
  ∫ (t : ℝ) in 0..1, (curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ) t =
    HAdd.hAdd (α := F) (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω₁ x) γ t)
      (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω₂ x) γ t)
⊢ curveIntegral (ω₁ + ω₂) γ = HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, ω₂ x)

Tactic:
simp only [curveIntegral, curveIntegralFun_add]

Premises used: curveIntegral, curveIntegralFun_add
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ ∫ (t : ℝ) in 0..1, (curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ) t =
    HAdd.hAdd (α := F) (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω₁ x) γ t)
      (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω₂ x) γ t)

Tactic:
intervalIntegral.integral_add h₁ h₂

Premises used: intervalIntegral.integral_add
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ ∫ (t : ℝ) in 0..1, (curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ) t =
    HAdd.hAdd (α := F) (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω₁ x) γ t)
      (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω₂ x) γ t)

Tactic:
exact intervalIntegral.integral_add h₁ h₂

Premises used: intervalIntegral.integral_add
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ ∫ᶜ (x : E) in γ, (ω₁ x + ω₂ x) = HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, ω₂ x)

Tactic:
curveIntegral_add h₁ h₂

Premises used: curveIntegral_add
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
γ : Path a b
h : ∀ (x : ℝ), Eq.{u_3 + 1} (α := F) (curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) 0 γ x) (0 x)
⊢ Eq.{u_3 + 1} (α := (t : ℝ) → F) (curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) 0 γ) 0

Tactic:
ext
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
γ : Path a b
x : ℝ
⊢ Eq.{u_3 + 1} (α := F) (curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) 0 γ x) (0 x)

Tactic:
simp [curveIntegralFun]

Premises used: curveIntegralFun
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
γ : Path a b
⊢ Eq.{u_3 + 1} (α := (t : ℝ) → F) (curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ 0) γ) 0

Tactic:
curveIntegralFun_zero

Premises used: curveIntegralFun_zero
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
γ : Path a b
⊢ CurveIntegrable.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) 0 γ

Tactic:
simp [CurveIntegrable, IntervalIntegrable.zero]

Premises used: IntervalIntegrable.zero, CurveIntegrable
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
γ : Path a b
⊢ Eq.{u_3 + 1} (α := F) (curveIntegral.{u_1, u_2, u_3} (𝕜 := 𝕜) 0 γ) 0

Tactic:
simp [curveIntegral]

Premises used: curveIntegral
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
γ : Path a b
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in γ, 0) 0

Tactic:
curveIntegral_zero

Premises used: curveIntegral_zero
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
h : ∀ (x : ℝ), curveIntegralFun (-ω) γ x = (-curveIntegralFun ω γ) x
⊢ curveIntegralFun (-ω) γ = -curveIntegralFun ω γ

Tactic:
ext
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
x : ℝ
⊢ curveIntegralFun (-ω) γ x = (-curveIntegralFun ω γ) x

Tactic:
simp [curveIntegralFun]

Premises used: curveIntegralFun
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
h : CurveIntegrable ω γ
⊢ CurveIntegrable (-ω) γ

Tactic:
simpa [CurveIntegrable] using IntervalIntegrable.neg h

Premises used: IntervalIntegrable.neg, CurveIntegrable
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
h : CurveIntegrable (-ω) γ
⊢ CurveIntegrable ω γ

Tactic:
simpa using h.neg

Premises used: CurveIntegrable.neg
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
⊢ CurveIntegrable.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ -ω x) γ ↔ CurveIntegrable ω γ

Tactic:
curveIntegrable_neg_iff

Premises used: curveIntegrable_neg_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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
⊢ curveIntegral (-ω) γ = -∫ᶜ (x : E) in γ, ω x

Tactic:
simp [curveIntegral]

Premises used: curveIntegral
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in γ, -ω x) (-∫ᶜ (x : E) in γ, ω x)

Tactic:
curveIntegral_neg

Premises used: curveIntegral_neg
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
⊢ curveIntegralFun (ω₁ - ω₂) γ = curveIntegralFun ω₁ γ - curveIntegralFun ω₂ γ

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ CurveIntegrable (ω₁ - ω₂) γ

Tactic:
sub_eq_add_neg ω₁ ω₂ ▸ h₁.add h₂.neg

Premises used: sub_eq_add_neg, Eq.rec, Eq.symm, CurveIntegrable.add, CurveIntegrable.neg
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
rw : curveIntegral (ω₁ + -ω₂) γ = HSub.hSub (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, ω₂ x)
rw₁ : curveIntegral (ω₁ + -ω₂) γ = HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (-∫ᶜ (x : E) in γ, ω₂ x)
rw₂ :
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, (-ω₂) x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (-∫ᶜ (x : E) in γ, ω₂ x)
rw₃ rw₄ :
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (-∫ᶜ (x : E) in γ, ω₂ x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (-∫ᶜ (x : E) in γ, ω₂ x)
⊢ curveIntegral (ω₁ - ω₂) γ = HSub.hSub (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, ω₂ x)

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, curveIntegral_add h₁ h₂.neg, curveIntegral_neg]

Premises used: curveIntegral_neg, sub_eq_add_neg, curveIntegral_add, CurveIntegrable.neg
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω₁ ω₂ : E → E →L[𝕜] F
γ : Path a b
h₁ : CurveIntegrable ω₁ γ
h₂ : CurveIntegrable ω₂ γ
⊢ ∫ᶜ (x : E) in γ, (ω₁ x - ω₂ x) = HSub.hSub (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, ω₂ x)

Tactic:
curveIntegral_sub h₁ h₂

Premises used: curveIntegral_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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : NormedSpace 𝕝 E
inst_8 : LinearMap.CompatibleSMul E F 𝕝 𝕜
h :
  ∀ (x : ℝ),
    curveIntegralFun.{u_4, u_2, u_3} (𝕜 := 𝕝) (fun (t : E) ↦ ContinuousLinearMap.restrictScalars 𝕝 (ω t)) γ x =
      curveIntegralFun ω γ x
⊢ curveIntegralFun.{u_4, u_2, u_3} (𝕜 := 𝕝) (fun (t : E) ↦ ContinuousLinearMap.restrictScalars 𝕝 (ω t)) γ =
    curveIntegralFun ω γ

Tactic:
ext
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : NormedSpace 𝕝 E
inst_8 : LinearMap.CompatibleSMul E F 𝕝 𝕜
x : ℝ
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ curveIntegralFun.{u_4, u_2, u_3} (𝕜 := 𝕝) (fun (t : E) ↦ ContinuousLinearMap.restrictScalars 𝕝 (ω t)) γ x =
    curveIntegralFun ω γ x

Tactic:
simp [curveIntegralFun_def]

Premises used: curveIntegralFun_def
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : NormedSpace 𝕝 E
inst_8 : LinearMap.CompatibleSMul E F 𝕝 𝕜
⊢ CurveIntegrable.{u_4, u_2, u_3} (𝕜 := 𝕝) (F := F) (fun (t : E) ↦ ContinuousLinearMap.restrictScalars 𝕝 (ω t)) γ ↔
    CurveIntegrable ω γ

Tactic:
simp [CurveIntegrable]

Premises used: CurveIntegrable
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : NormedSpace 𝕝 E
inst_8 : LinearMap.CompatibleSMul E F 𝕝 𝕜
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in γ, ContinuousLinearMap.restrictScalars 𝕝 (ω x)) (∫ᶜ (x : E) in γ, ω x)

Tactic:
simp [curveIntegral_def]

Premises used: curveIntegral_def
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
c : 𝕝
h : ∀ (x : ℝ), curveIntegralFun (c • ω) γ x = (c • curveIntegralFun ω γ) x
⊢ curveIntegralFun (c • ω) γ = c • curveIntegralFun ω γ

Tactic:
ext
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
c : 𝕝
x : ℝ
⊢ curveIntegralFun (c • ω) γ x = (c • curveIntegralFun ω γ) x

Tactic:
simp [curveIntegralFun]

Premises used: curveIntegralFun
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
c : 𝕝
h : CurveIntegrable ω γ
⊢ CurveIntegrable (c • ω) γ

Tactic:
simpa [CurveIntegrable] using IntervalIntegrable.smul h c

Premises used: CurveIntegrable, IntervalIntegrable.smul
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
c : 𝕝
inl : CurveIntegrable (HSMul.hSMul (α := 𝕝) 0 ω) γ ↔ Eq.{u_4 + 1} (α := 𝕝) 0 0 ∨ CurveIntegrable ω γ
inr : ∀ (hc : c ≠ 0), CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ
⊢ CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
⊢ CurveIntegrable (HSMul.hSMul (α := 𝕝) 0 ω) γ ↔ Eq.{u_4 + 1} (α := 𝕝) 0 0 ∨ CurveIntegrable ω γ

Tactic:
simp [CurveIntegrable.zero]

Premises used: CurveIntegrable.zero
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
c : 𝕝
hc : c ≠ 0
inr : CurveIntegrable (c • ω) γ ↔ CurveIntegrable ω γ
⊢ CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ

Tactic:
simp only [hc, false_or]

Premises used: false_or
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
c : 𝕝
hc : c ≠ 0
⊢ CurveIntegrable (c • ω) γ ↔ CurveIntegrable ω γ

Tactic:
⟨fun h ↦ ?_, .smul⟩

Premises used: Iff.intro, CurveIntegrable.smul
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
c : 𝕝
hc : c ≠ 0
inr : ∀ (h : CurveIntegrable (c • ω) γ), CurveIntegrable ω γ
⊢ CurveIntegrable (c • ω) γ ↔ CurveIntegrable ω γ

Tactic:
refine ⟨fun h ↦ ?_, .smul⟩
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
c : 𝕝
hc : c ≠ 0
h : CurveIntegrable (c • ω) γ
⊢ CurveIntegrable ω γ

Tactic:
simpa [hc] using h.smul (c := c⁻¹)

Premises used: CurveIntegrable.smul
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
c : 𝕝
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ curveIntegral (c • ω) γ = c • curveIntegral ω γ

Tactic:
simp [curveIntegral_def, intervalIntegral.integral_smul]

Premises used: curveIntegral_def, intervalIntegral.integral_smul
-- 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
c : 𝕝
⊢ ∫ᶜ (x : E) in γ, c • ω x = HSMul.hSMul (β := F) c (∫ᶜ (x : E) in γ, ω x)

Tactic:
curveIntegral_smul

Premises used: curveIntegral_smul
-- 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
simp :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (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)‖ ≤
          c * ‖x - a‖
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) s a

Tactic:
simp only [hasFDerivWithinAt_iff_isLittleO, Path.segment_same, curveIntegral_refl, sub_zero,
    Asymptotics.isLittleO_iff]

Premises used: sub_zero, hasFDerivWithinAt_iff_isLittleO, Path.segment_same, curveIntegral_refl, Asymptotics.isLittleO_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 < ε
rw : {a : E | ContinuousWithinAt ω s a} ∈ 𝓝[s] a ∧ {a_1 : E | dist (ω a_1) (ω a) ≤ ε} ∈ 𝓝[s] a
⊢ ∃ δ > 0, ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}

Tactic:
rw [← Metric.mem_nhdsWithin_iff, setOf_and, inter_mem_iff]

Premises used: Set.setOf_and, Metric.mem_nhdsWithin_iff, Filter.inter_mem_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 < ε
⊢ {a : E | ContinuousWithinAt ω s a} ∈ 𝓝[s] a ∧ {a_1 : E | dist (ω a_1) (ω a) ≤ ε} ∈ 𝓝[s] a

Tactic:
⟨hω, (hω.self_of_nhdsWithin ha).eventually <| closedBall_mem_nhds _ hε⟩

Premises used: Filter.Eventually.self_of_nhdsWithin, Metric.closedBall_mem_nhds, And.intro, Filter.Tendsto.eventually
-- 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 < ε
⊢ {a : E | ContinuousWithinAt ω s a} ∈ 𝓝[s] a ∧ {a_1 : E | dist (ω a_1) (ω a) ≤ ε} ∈ 𝓝[s] a

Tactic:
exact ⟨hω, (hω.self_of_nhdsWithin ha).eventually <| closedBall_mem_nhds _ hε⟩