awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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
t : ℝ
⊢ t ∈ Ioo (1 / 2) 1 → curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
have h : ∀ (ht₁ : 1 / 2 < t) (ht₂ : t < 1),
  curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
Tactic: ⟨ht₁, ht₂⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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
⊢ curveIntegralFun ω (γab.trans γbc) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo (1 / 2) 1))] fun (t : ℝ) ↦
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
have h : ∀ (t : ℝ) (ht₁ : 1 / 2 < t) (ht₂ : t < 1),
  curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
Tactic: filter_upwards [ae_restrict_mem measurableSet_Ioo] with t ⟨ht₁, ht₂⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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
h : CurveIntegrable ω γab
γbc : Path b c
⊢ IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) volume 0 (1 / 2)
have refine : IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))) volume 0
  (1 / 2)
Tactic: refine .congr_ae ?_ (curveIntegralFun_trans_aeeq_left _ _ _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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
γbc : Path b c
γab : Path a b
h : CurveIntegrable ω γbc
⊢ IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) volume (1 / 2) 1
have refine : IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))) volume
  (1 / 2) 1
Tactic: refine .congr_ae ?_ (curveIntegralFun_trans_aeeq_right _ _ _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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
⊢ ∫ᶜ (x : E) in γab.trans γbc, ω x = HAdd.hAdd (α := F) (∫ᶜ (x : E) in γab, ω x) (∫ᶜ (x : E) in γbc, ω x)
have 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)
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 _ _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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 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)
have 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)
Tactic: simp only [← ofNat_smul_eq_nsmul (R := ℝ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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) (∫ᶜ (x : E) in γab, ω x) (∫ᶜ (x : E) in γbc, ω x)
have 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)
Tactic: simp only [curveIntegral_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (hypothesis)
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
⊢ curveIntegralFun ω (Path.segment a b) t = (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a)
have this : EqOn (β := E) (⇑(Path.extend (Path.segment a b)) : (a : ℝ) → E) (⇑(lineMap a b) : (a : ℝ) → E) I
Tactic: have := Path.eqOn_extend_segment a b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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
⊢ 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
have rw : EqOn (curveIntegralFun ω (Path.segment a b)) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
  (Ι 0 1)
Tactic: rw [CurveIntegrable, intervalIntegrable_congr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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))
    (Ι 0 1)
have rw : EqOn (curveIntegralFun ω (Path.segment a b)) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
  (Ioc 0 1)
Tactic: rw [uIoc_of_le zero_le_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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) (∫ᶜ (x : E) in Path.segment a b, ω x)
    (∫ (t : ℝ) in 0..1, (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
have 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))
Tactic: rw [curveIntegral_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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))
have 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)
Tactic: refine intervalIntegral.integral_congr fun t ht ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (hypothesis)
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
⊢ 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)
have ht₁ : Membership.mem (γ := Set ℝ) (Icc 0 1) t
Tactic: rw [uIcc_of_le zero_le_one] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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) (∫ᶜ (x : E) in Path.segment a b, ω x) ≤ C * ‖b - a‖ * |HSub.hSub (α := ℝ) 1 0|
have 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|
Tactic: rw [curveIntegral_segment]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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|
have 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‖
Tactic: refine intervalIntegral.norm_integral_le_of_norm_le_const fun t ht ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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
⊢ norm.{u_3} (E := F) ((ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F) ≤ C * ‖b - a‖
have 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‖
Tactic: rw [segment_eq_image_lineMap] at h
Cleared hypotheses: h, this, t, ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (hypothesis)
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
⊢ norm.{u_3} (E := F) ((ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a) : F) ≤ C * ‖b - a‖
have ht₁ : Membership.mem (γ := Set ℝ) (Ioc 0 1) t
Tactic: rw [uIoc_of_le zero_le_one] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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)
⊢ CurveIntegrable ω γ
have apply : ContinuousOn (curveIntegralFun ω γ) (Icc 0 1)
Tactic: apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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 (curveIntegralFun ω γ) (Icc 0 1)
have 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)
Tactic: simp only [funext (curveIntegralFun_def ω γ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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.{0, u_3} (Y := F)
    (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x)) (Icc 0 1)
have hf : ContinuousOn (Y := E →L[𝕜] F) (fun (x : ℝ) ↦ ω ((γ.extend : (a : ℝ) → E) x)) (Icc 0 1)
Tactic: apply ContinuousOn.clm_apply
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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)
⊢ ContinuousOn.{0, u_3} (Y := F)
    (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x)) (Icc 0 1)
have hg : ContinuousOn (Y := E) (derivWithin (⇑γ.extend : (a : ℝ) → E) I) (Icc 0 1)
Tactic: apply ContinuousOn.clm_apply
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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 ω₂ γ
have h : ∀ (x : ℝ), curveIntegralFun (ω₁ + ω₂) γ x = (curveIntegralFun ω₁ γ + curveIntegralFun ω₂ γ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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
⊢ curveIntegral (ω₁ + ω₂) γ = HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, ω₂ x)
have 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)
Tactic: simp only [curveIntegral, curveIntegralFun_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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} (𝕜 := 𝕜) 0 γ) 0
have h : ∀ (x : ℝ), Eq.{u_3 + 1} (α := F) (curveIntegralFun.{u_1, u_2, u_3} (𝕜 := 𝕜) 0 γ x) (0 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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 ω γ
have h : ∀ (x : ℝ), curveIntegralFun (-ω) γ x = (-curveIntegralFun ω γ) x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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 ω₂ γ
⊢ curveIntegral (ω₁ - ω₂) γ = HSub.hSub (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, ω₂ x)
have rw : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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)
⊢ curveIntegral (ω₁ - ω₂) γ = HSub.hSub (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, ω₂ x)
have rw₁ : curveIntegral (ω₁ + -ω₂) γ = HAdd.hAdd (α := 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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)
⊢ curveIntegral (ω₁ - ω₂) γ = HSub.hSub (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, ω₂ x)
have rw₂ : HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, (-ω₂) x) =
  HAdd.hAdd (α := 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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)
⊢ curveIntegral (ω₁ - ω₂) γ = HSub.hSub (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (∫ᶜ (x : E) in γ, ω₂ x)
have rw₃ : HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ, ω₁ x) (-∫ᶜ (x : E) in γ, ω₂ x) =
  HAdd.hAdd (α := 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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 𝕝 𝕜
⊢ curveIntegralFun.{u_4, u_2, u_3} (𝕜 := 𝕝) (fun (t : E) ↦ ContinuousLinearMap.restrictScalars 𝕝 (ω t)) γ =
    curveIntegralFun ω γ
have h : ∀ (x : ℝ),
  curveIntegralFun.{u_4, u_2, u_3} (𝕜 := 𝕝) (fun (t : E) ↦ ContinuousLinearMap.restrictScalars 𝕝 (ω t)) γ x =
    curveIntegralFun ω γ x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Basic (goal)
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 : 𝕝
⊢ curveIntegralFun (c • ω) γ = c • curveIntegralFun ω γ
have h : ∀ (x : ℝ), curveIntegralFun (c • ω) γ x = (c • curveIntegralFun ω γ) x
Tactic: ext