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 c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
⊢ CurveIntegrable ω (γab.trans γbc)

Tactic:
(h₁.intervalIntegrable_curveIntegralFun_trans_left γbc).trans
    (h₂.intervalIntegrable_curveIntegralFun_trans_right γab)

Premises used: CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_left, IntervalIntegrable.trans, CurveIntegrable, CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
instF : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
rw :
  HAdd.hAdd (α := F) (∫ (x : ℝ) in 0..1 / 2, HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * x)))
      (∫ (x : ℝ) in 1 / 2..1, HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * x - 1))) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γab, ω x) (∫ᶜ (x : E) in γbc, ω x)
⊢ ∫ᶜ (x : E) in γab.trans γbc, ω x = HAdd.hAdd (α := F) (∫ᶜ (x : E) in γab, ω x) (∫ᶜ (x : E) in γbc, ω x)

Tactic:
rw [curveIntegral_def, ← intervalIntegral.integral_add_adjacent_intervals
    (h₁.intervalIntegrable_curveIntegralFun_trans_left γbc)
    (h₂.intervalIntegrable_curveIntegralFun_trans_right γab),
    intervalIntegral.integral_congr_ae_restrict (curveIntegralFun_trans_aeeq_left _ _ _),
    intervalIntegral.integral_congr_ae_restrict (curveIntegralFun_trans_aeeq_right _ _ _)]

Premises used: curveIntegralFun_trans_aeeq_right, intervalIntegral.integral_add_adjacent_intervals, curveIntegral_def, CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_left, intervalIntegral.integral_congr_ae_restrict, curveIntegralFun_trans_aeeq_left, CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
instF : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
simp :
  HAdd.hAdd (α := F) (∫ (x : ℝ) in 0..1 / 2, HSMul.hSMul (α := ℝ) 2 (curveIntegralFun ω γab (2 * x)))
      (∫ (x : ℝ) in 1 / 2..1, HSMul.hSMul (α := ℝ) 2 (curveIntegralFun ω γbc (2 * x - 1))) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γab, ω x) (∫ᶜ (x : E) in γbc, ω x)
⊢ HAdd.hAdd (α := F) (∫ (x : ℝ) in 0..1 / 2, HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * x)))
      (∫ (x : ℝ) in 1 / 2..1, HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * x - 1))) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γab, ω x) (∫ᶜ (x : E) in γbc, ω x)

Tactic:
simp only [← ofNat_smul_eq_nsmul (R := ℝ)]

Premises used: Real, ofNat_smul_eq_nsmul
-- 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 c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
instF : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
rw :
  HAdd.hAdd (α := F) (∫ (x : ℝ) in HMul.hMul (α := ℝ) 2 0..2 * (1 / 2), curveIntegralFun ω γab x)
      (∫ (x : ℝ) in 2 * (1 / 2) - 1..HMul.hMul (α := ℝ) 2 1 - 1, curveIntegralFun ω γbc x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γab, ω x) (∫ᶜ (x : E) in γbc, ω x)
⊢ HAdd.hAdd (α := F) (∫ (x : ℝ) in 0..1 / 2, HSMul.hSMul (α := ℝ) 2 (curveIntegralFun ω γab (2 * x)))
      (∫ (x : ℝ) in 1 / 2..1, HSMul.hSMul (α := ℝ) 2 (curveIntegralFun ω γbc (2 * x - 1))) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γab, ω x) (∫ᶜ (x : E) in γbc, ω x)

Tactic:
rw [intervalIntegral.integral_smul, intervalIntegral.smul_integral_comp_mul_left,
    intervalIntegral.integral_smul,
    intervalIntegral.smul_integral_comp_mul_left (f := (curveIntegralFun ω γbc <| · - 1)),
    intervalIntegral.integral_comp_sub_right]

Premises used: intervalIntegral.integral_comp_sub_right, HSub.hSub, intervalIntegral.integral_smul, intervalIntegral.smul_integral_comp_mul_left, curveIntegralFun, OfNat.ofNat
-- 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 c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
instF : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
simp :
  HAdd.hAdd (α := F) (∫ (x : ℝ) in HMul.hMul (α := ℝ) 2 0..2 * (1 / 2), curveIntegralFun ω γab x)
      (∫ (x : ℝ) in 2 * (1 / 2) - 1..HMul.hMul (α := ℝ) 2 1 - 1, curveIntegralFun ω γbc x) =
    HAdd.hAdd (α := F) (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω x) γab t)
      (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω x) γbc t)
⊢ HAdd.hAdd (α := F) (∫ (x : ℝ) in HMul.hMul (α := ℝ) 2 0..2 * (1 / 2), curveIntegralFun ω γab x)
      (∫ (x : ℝ) in 2 * (1 / 2) - 1..HMul.hMul (α := ℝ) 2 1 - 1, curveIntegralFun ω γbc x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γab, ω x) (∫ᶜ (x : E) in γbc, ω x)

Tactic:
simp only [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 c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
h₁ : CurveIntegrable ω γab
h₂ : CurveIntegrable ω γbc
instF : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ HAdd.hAdd (α := F) (∫ (x : ℝ) in HMul.hMul (α := ℝ) 2 0..2 * (1 / 2), curveIntegralFun ω γab x)
      (∫ (x : ℝ) in 2 * (1 / 2) - 1..HMul.hMul (α := ℝ) 2 1 - 1, curveIntegralFun ω γbc x) =
    HAdd.hAdd (α := F) (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω x) γab t)
      (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω x) γbc t)

Tactic:
norm_num
-- 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
inst_5 : NormedSpace ℝ E
ω : E → E →L[𝕜] F
a b : E
t : ℝ
ht : t ∈ I
⊢ EqOn (β := E) (⇑(Path.extend (Path.segment a b)) : (a : ℝ) → E) (⇑(lineMap a b) : (a : ℝ) → E) I

Tactic:
have := Path.eqOn_extend_segment a b
-- 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
inst_5 : NormedSpace ℝ E
ω : E → E →L[𝕜] F
a b : E
t : ℝ
ht : t ∈ I
this : EqOn (β := E) (⇑(Path.extend (Path.segment a b)) : (a : ℝ) → E) (⇑(lineMap a b) : (a : ℝ) → E) I
⊢ curveIntegralFun ω (Path.segment a b) t = (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a)

Tactic:
simp only [curveIntegralFun_def, this ht, derivWithin_congr this (this ht),
    (hasDerivWithinAt_lineMap ..).derivWithin (uniqueDiffOn_Icc_zero_one t ht)]

Premises used: derivWithin_congr, AffineMap.hasDerivWithinAt_lineMap, HasDerivWithinAt.derivWithin, uniqueDiffOn_Icc_zero_one, 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
inst_5 : NormedSpace ℝ E
rw :
  EqOn (curveIntegralFun ω (Path.segment a b)) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
    (Ι 0 1)
⊢ CurveIntegrable ω (Path.segment a b) ↔
    IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a)) volume 0
      1

Tactic:
rw [CurveIntegrable, intervalIntegrable_congr]

Premises used: intervalIntegrable_congr, 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
inst_5 : NormedSpace ℝ E
rw :
  EqOn (curveIntegralFun ω (Path.segment a b)) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
    (Ioc 0 1)
⊢ EqOn (curveIntegralFun ω (Path.segment a b)) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
    (Ι 0 1)

Tactic:
rw [uIoc_of_le zero_le_one]

Premises used: zero_le_one, Set.uIoc_of_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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
inst_5 : NormedSpace ℝ E
⊢ EqOn (curveIntegralFun ω (Path.segment a b)) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
    (Ioc 0 1)

Tactic:
.mono Ioc_subset_Icc_self fun _t ↦ curveIntegralFun_segment ω a b

Premises used: curveIntegralFun_segment, Set.Ioc_subset_Icc_self, Set.EqOn.mono
-- 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
inst_5 : NormedSpace ℝ E
⊢ EqOn (curveIntegralFun ω (Path.segment a b)) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
    (Ioc 0 1)

Tactic:
exact .mono Ioc_subset_Icc_self fun _t ↦ curveIntegralFun_segment ω a b
-- 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
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
a b : E
rw :
  Eq.{u_3 + 1} (α := F)
    (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω x) (Path.segment a b) t)
    (∫ (t : ℝ) in 0..1, (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x)
    (∫ (t : ℝ) in 0..1, (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))

Tactic:
rw [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
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
a b : E
⊢ Eq.{u_3 + 1} (α := F)
    (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω x) (Path.segment a b) t)
    (∫ (t : ℝ) in 0..1, (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))

Tactic:
intervalIntegral.integral_congr fun t ht ↦ ?_

Premises used: intervalIntegral.integral_congr
-- 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
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
a b : E
refine :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) [[0, 1]] t),
    Eq.{u_3 + 1} (α := F) (curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω x) (Path.segment a b) t : F)
      ((ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F)
⊢ Eq.{u_3 + 1} (α := F)
    (∫ (t : ℝ) in 0..1, curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω x) (Path.segment a b) t)
    (∫ (t : ℝ) in 0..1, (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))

Tactic:
refine intervalIntegral.integral_congr fun t ht ↦ ?_

Premises used: intervalIntegral.integral_congr
-- 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
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
a b : E
t : ℝ
ht : Membership.mem (γ := Set ℝ) [[0, 1]] t
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) t

Tactic:
rw [uIcc_of_le zero_le_one] at ht

Premises used: Set.uIcc_of_le, 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
a b : E
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ Eq.{u_3 + 1} (α := F) (curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω x) (Path.segment a b) t : F)
    ((ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F)

Tactic:
curveIntegralFun_segment ω a b ht

Premises used: curveIntegralFun_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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
a b : E
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ Eq.{u_3 + 1} (α := F) (curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) (fun (x : E) ↦ ω x) (Path.segment a b) t : F)
    ((ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F)

Tactic:
exact curveIntegralFun_segment ω a b ht

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

Tactic:
simp [curveIntegral_segment]

Premises used: curveIntegral_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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
inst_5 : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
rw :
  norm.{u_3} (E := F) (∫ (t : ℝ) in 0..1, (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a)) ≤
    C * ‖b - a‖ * |HSub.hSub (α := ℝ) 1 0|
⊢ norm.{u_3} (E := F) (∫ᶜ (x : E) in Path.segment a b, ω x) ≤ C * ‖b - a‖ * |HSub.hSub (α := ℝ) 1 0|

Tactic:
rw [curveIntegral_segment]

Premises used: curveIntegral_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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
inst_5 : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
⊢ norm.{u_3} (E := F) (∫ (t : ℝ) in 0..1, (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a)) ≤
    C * ‖b - a‖ * |HSub.hSub (α := ℝ) 1 0|

Tactic:
intervalIntegral.norm_integral_le_of_norm_le_const fun t ht ↦ ?_

Premises used: intervalIntegral.norm_integral_le_of_norm_le_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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
inst_5 : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
refine :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ι 0 1) t),
    norm.{u_3} (E := F) ((ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F) ≤ C * ‖b - a‖
⊢ norm.{u_3} (E := F) (∫ (t : ℝ) in 0..1, (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a)) ≤
    C * ‖b - a‖ * |HSub.hSub (α := ℝ) 1 0|

Tactic:
refine intervalIntegral.norm_integral_le_of_norm_le_const fun t ht ↦ ?_

Premises used: intervalIntegral.norm_integral_le_of_norm_le_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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
inst_5 : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ι 0 1) t
rw :
  ∀ (h : ∀ (z : E), Membership.mem (γ := Set E) (image (α := ℝ) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1)) z → ‖ω z‖ ≤ C)
    (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ι 0 1) t),
    norm.{u_3} (E := F) ((ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F) ≤ C * ‖b - a‖
⊢ norm.{u_3} (E := F) ((ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F) ≤ C * ‖b - a‖

Tactic:
rw [segment_eq_image_lineMap] at h

Premises used: 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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
inst_5 : NormedSpace ℝ E
C : ℝ
h : ∀ (z : E), Membership.mem (γ := Set E) (image (α := ℝ) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1)) z → ‖ω z‖ ≤ C
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ι 0 1) t
⊢ Membership.mem (γ := Set ℝ) (Ioc 0 1) t

Tactic:
rw [uIoc_of_le zero_le_one] at ht

Premises used: zero_le_one, Set.uIoc_of_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 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
inst_5 : NormedSpace ℝ E
C : ℝ
h : ∀ (z : E), Membership.mem (γ := Set E) (image (α := ℝ) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1)) z → ‖ω z‖ ≤ C
this : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
⊢ norm.{u_3} (E := F) ((ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F) ≤ C * ‖b - a‖

Tactic:
apply_rules [(ω _).le_of_opNorm_le, mem_image_of_mem, Ioc_subset_Icc_self]

Premises used: Set.Ioc_subset_Icc_self, ContinuousLinearMap.le_of_opNorm_le, Set.mem_image_of_mem
-- 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
inst_5 : NormedSpace ℝ E
C : ℝ
h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C
⊢ C * ‖b - a‖ * |HSub.hSub (α := ℝ) 1 0| = C * ‖b - a‖

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 : 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)
apply : ContinuousOn (curveIntegralFun ω γ) (Icc 0 1)
⊢ CurveIntegrable ω γ

Tactic:
apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one

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 : 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)
simp :
  ContinuousOn.{0, u_3} (Y := F)
    (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x)) (Icc 0 1)
⊢ ContinuousOn (curveIntegralFun ω γ) (Icc 0 1)

Tactic:
simp only [funext (curveIntegralFun_def ω γ)]

Premises used: funext, 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
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)
hf : ContinuousOn (Y := E →L[𝕜] F) (fun (x : ℝ) ↦ ω ((γ.extend : (a : ℝ) → E) x)) (Icc 0 1)
hg : ContinuousOn (Y := E) (derivWithin (⇑γ.extend : (a : ℝ) → E) I) (Icc 0 1)
⊢ ContinuousOn.{0, u_3} (Y := F)
    (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x)) (Icc 0 1)

Tactic:
apply ContinuousOn.clm_apply

Premises used: ContinuousOn.clm_apply
-- 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 (X := ℝ) (Y := E) (⇑γ.extend : (a : ℝ) → E) (Icc 0 1)

Tactic:
fun_prop
-- 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 →L[𝕜] F) (fun (x : ℝ) ↦ ω ((γ.extend : (a : ℝ) → E) x)) (Icc 0 1)

Tactic:
exact hω.comp (by fun_prop) fun _ _ ↦ hγs _

Premises used: ContinuousOn.comp
-- 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:
hγ.continuousOn_derivWithin uniqueDiffOn_Icc_zero_one le_rfl

Premises used: le_rfl, uniqueDiffOn_Icc_zero_one, ContDiffOn.continuousOn_derivWithin