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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ :
  (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
ht₀ : 0 < t
linarith : 1 ≤ t → 2 / 2 = 1
linarith₁ : 1 ≤ t → HMul.hMul (α := ℝ) 1 2 = 2
⊢ t < 1
have linarith₂ : 1 ≤ t → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ :
  (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
ht₀ : 0 < t
linarith : 1 ≤ t → 2 / 2 = 1
linarith₁ : 1 ≤ t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 ≤ t → GT.gt (α := ℝ) 2 0
⊢ t < 1
have linarith₃ : 1 ≤ t → 2 * t - HMul.hMul (α := ℝ) 1 1 + (0 - t) + (1 - t) = 0
Tactic: linarith
-- 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 c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ :
  (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have H₂ : HSMul.hSMul (α := ℝ) 2 I =ᶠ[𝓝 (2 * t)] I
Tactic: have H₂ : (2 : ℝ) • I =ᶠ[𝓝 (2 * t)] I := by
    rw [LinearOrderedField.smul_Icc two_pos, mul_zero, mul_one, ← nhdsWithin_eq_iff_eventuallyEq]
    rcases lt_trichotomy t 0 with ht₀ | rfl | ht₀
    · rw [notMem_closure_iff_nhdsWithin_eq_bot.mp, notMem_closure_iff_nhdsWithin_eq_bot.mp] <;>
        simp_intro h <;> linarith
    · simp
    · rw [nhdsWithin_eq_nhds.2, nhdsWithin_eq_nhds.2] <;> simp [*] <;> linarith
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ :
  (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
H₂ : HSMul.hSMul (α := ℝ) 2 I =ᶠ[𝓝 (2 * t)] I
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have rw : (ω (((γab.trans γbc).extend : (a : ℝ) → E) t) : (a : E) → F) (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
  HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
Tactic: rw [curveIntegralFun_def, H₁.self_of_nhds, H₁.derivWithin_eq_of_nhds, curveIntegralFun_def,
    derivWithin_comp_mul_left, ofNat_smul_eq_nsmul, map_nsmul, derivWithin_congr_set H₂]
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ :
  (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
H₂ : HSMul.hSMul (α := ℝ) 2 I =ᶠ[𝓝 (2 * t)] I
rw :
  (ω (((γab.trans γbc).extend : (a : ℝ) → E) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have rw₁ : (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
    (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
  HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
Tactic: rw [curveIntegralFun_def, H₁.self_of_nhds, H₁.derivWithin_eq_of_nhds, curveIntegralFun_def,
    derivWithin_comp_mul_left, ofNat_smul_eq_nsmul, map_nsmul, derivWithin_congr_set H₂]
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ :
  (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
H₂ : HSMul.hSMul (α := ℝ) 2 I =ᶠ[𝓝 (2 * t)] I
rw :
  (ω (((γab.trans γbc).extend : (a : ℝ) → E) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₁ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have rw₂ : (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
    (derivWithin (fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)) I t) =
  HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
Tactic: rw [curveIntegralFun_def, H₁.self_of_nhds, H₁.derivWithin_eq_of_nhds, curveIntegralFun_def,
    derivWithin_comp_mul_left, ofNat_smul_eq_nsmul, map_nsmul, derivWithin_congr_set H₂]
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ :
  (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
H₂ : HSMul.hSMul (α := ℝ) 2 I =ᶠ[𝓝 (2 * t)] I
rw :
  (ω (((γab.trans γbc).extend : (a : ℝ) → E) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₁ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₂ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have rw₃ : (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
    (derivWithin (fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)) I t) =
  HSMul.hSMul (α := ℕ) (β := F) 2
    ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
Tactic: rw [curveIntegralFun_def, H₁.self_of_nhds, H₁.derivWithin_eq_of_nhds, curveIntegralFun_def,
    derivWithin_comp_mul_left, ofNat_smul_eq_nsmul, map_nsmul, derivWithin_congr_set H₂]
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ :
  (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
H₂ : HSMul.hSMul (α := ℝ) 2 I =ᶠ[𝓝 (2 * t)] I
rw :
  (ω (((γab.trans γbc).extend : (a : ℝ) → E) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₁ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₂ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₃ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)) I t) =
    HSMul.hSMul (α := ℕ) (β := F) 2
      ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have rw₄ : (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
    (HSMul.hSMul (α := ℝ) (β := E) 2 (derivWithin (⇑γab.extend : (a : ℝ) → E) (HSMul.hSMul (α := ℝ) 2 I) (2 * t))) =
  HSMul.hSMul (α := ℕ) (β := F) 2
    ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
Tactic: rw [curveIntegralFun_def, H₁.self_of_nhds, H₁.derivWithin_eq_of_nhds, curveIntegralFun_def,
    derivWithin_comp_mul_left, ofNat_smul_eq_nsmul, map_nsmul, derivWithin_congr_set H₂]
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ :
  (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
H₂ : HSMul.hSMul (α := ℝ) 2 I =ᶠ[𝓝 (2 * t)] I
rw :
  (ω (((γab.trans γbc).extend : (a : ℝ) → E) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₁ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₂ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₃ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)) I t) =
    HSMul.hSMul (α := ℕ) (β := F) 2
      ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
rw₄ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (HSMul.hSMul (α := ℝ) (β := E) 2 (derivWithin (⇑γab.extend : (a : ℝ) → E) (HSMul.hSMul (α := ℝ) 2 I) (2 * t))) =
    HSMul.hSMul (α := ℕ) (β := F) 2
      ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have rw₅ : (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
    (HSMul.hSMul (α := ℕ) (β := E) 2 (derivWithin (⇑γab.extend : (a : ℝ) → E) (HSMul.hSMul (α := ℝ) 2 I) (2 * t))) =
  HSMul.hSMul (α := ℕ) (β := F) 2
    ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
Tactic: rw [curveIntegralFun_def, H₁.self_of_nhds, H₁.derivWithin_eq_of_nhds, curveIntegralFun_def,
    derivWithin_comp_mul_left, ofNat_smul_eq_nsmul, map_nsmul, derivWithin_congr_set H₂]
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
H₁ :
  (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
H₂ : HSMul.hSMul (α := ℝ) 2 I =ᶠ[𝓝 (2 * t)] I
rw :
  (ω (((γab.trans γbc).extend : (a : ℝ) → E) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₁ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (⇑(γab.trans γbc).extend : (a : ℝ) → E) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₂ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)) I t) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
rw₃ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (derivWithin (fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)) I t) =
    HSMul.hSMul (α := ℕ) (β := F) 2
      ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
rw₄ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (HSMul.hSMul (α := ℝ) (β := E) 2 (derivWithin (⇑γab.extend : (a : ℝ) → E) (HSMul.hSMul (α := ℝ) 2 I) (2 * t))) =
    HSMul.hSMul (α := ℕ) (β := F) 2
      ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
rw₅ :
  (ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
      (HSMul.hSMul (α := ℕ) (β := E) 2 (derivWithin (⇑γab.extend : (a : ℝ) → E) (HSMul.hSMul (α := ℝ) 2 I) (2 * t))) =
    HSMul.hSMul (α := ℕ) (β := F) 2
      ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have rw₆ : HSMul.hSMul (α := ℕ) (β := F) 2
    ((ω ((fun (s : ℝ) ↦ ((γab.extend : (a : ℝ) → E) (2 * s) : E)) t) : (a : E) → F)
        (derivWithin (⇑γab.extend : (a : ℝ) → E) (HSMul.hSMul (α := ℝ) 2 I) (2 * t)) :
      F) =
  HSMul.hSMul (α := ℕ) (β := F) 2
    ((ω ((γab.extend : (a : ℝ) → E) (2 * t)) : (a : E) → F) (derivWithin (⇑γab.extend : (a : ℝ) → E) I (2 * t)) : F)
Tactic: rw [curveIntegralFun_def, H₁.self_of_nhds, H₁.derivWithin_eq_of_nhds, curveIntegralFun_def,
    derivWithin_comp_mul_left, ofNat_smul_eq_nsmul, map_nsmul, derivWithin_congr_set H₂]
-- 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 (Ι 0 (1 / 2)))] fun (t : ℝ) ↦
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have rw : curveIntegralFun ω (γab.trans γbc) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 (1 / 2)))] fun (t : ℝ) ↦
  HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
Tactic: rw [uIoc_of_le (by positivity), ← restrict_Ioo_eq_restrict_Ioc]
-- 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 0 (1 / 2) → curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have h : ∀ (ht₀ : 0 < t) (ht : t < 1 / 2),
  curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
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 0 (1 / 2)))] fun (t : ℝ) ↦
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have h : ∀ (t : ℝ) (ht₀ : 0 < t) (ht : t < 1 / 2),
  curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
ω_1 : E → E →L[𝕜] F
γab_1 : Path c b
γbc_1 : Path b a
⊢ 1 - t < 1 / 2
have linarith : 1 / 2 ≤ 1 - t → 2 / 2 = 1
Tactic: linarith
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
ω_1 : E → E →L[𝕜] F
γab_1 : Path c b
γbc_1 : Path b a
linarith : 1 / 2 ≤ 1 - t → 2 / 2 = 1
⊢ 1 - t < 1 / 2
have linarith₁ : 1 / 2 ≤ 1 - t → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
ω_1 : E → E →L[𝕜] F
γab_1 : Path c b
γbc_1 : Path b a
linarith : 1 / 2 ≤ 1 - t → 2 / 2 = 1
linarith₁ : 1 / 2 ≤ 1 - t → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 - t < 1 / 2
have linarith₂ : 1 / 2 ≤ 1 - t → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
ω_1 : E → E →L[𝕜] F
γab_1 : Path c b
γbc_1 : Path b a
linarith : 1 / 2 ≤ 1 - t → 2 / 2 = 1
linarith₁ : 1 / 2 ≤ 1 - t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 ≤ 1 - t → GT.gt (α := ℝ) 2 0
linarith₃ : 1 / 2 ≤ 1 - t → 2 / 2 = 1
linarith₄ : 1 / 2 ≤ 1 - t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 / 2 ≤ 1 - t → GT.gt (α := ℝ) 2 0
⊢ 1 - t < 1 / 2
have linarith₆ : 1 / 2 ≤ 1 - t → HMul.hMul (α := ℝ) 1 1 - 2 * t + (HMul.hMul (α := ℝ) 1 1 - (HMul.hMul (α := ℝ) 2 1 - 2 * t)) = 0
Tactic: linarith
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
have rw : HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (1 - 2 * (1 - t))) =
  HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
Tactic: rw [← (γab.trans γbc).symm_symm, curveIntegralFun_symm_apply, Path.trans_symm,
    curveIntegralFun_trans_of_lt_half (ht := by linarith), curveIntegralFun_symm_apply, smul_neg,
    neg_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 c : E
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
⊢ HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (1 - 2 * (1 - t))) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
have e_a : 1 - 2 * (1 - t) = 2 * t - 1
Tactic: congr 2
-- 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
⊢ 1 / 2 ≤ 1
have linarith : 1 < 1 / 2 → 2 / 2 = 1
Tactic: linarith
-- 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
linarith : 1 < 1 / 2 → 2 / 2 = 1
⊢ 1 / 2 ≤ 1
have linarith₁ : 1 < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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
linarith : 1 < 1 / 2 → 2 / 2 = 1
linarith₁ : 1 < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 1 / 2 ≤ 1
have linarith₂ : 1 < 1 / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
linarith : 1 < 1 / 2 → 2 / 2 = 1
linarith₁ : 1 < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < 1 / 2 → GT.gt (α := ℝ) 2 0
⊢ 1 / 2 ≤ 1
have linarith₃ : 1 < 1 / 2 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
Tactic: linarith
-- 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 (Ι (1 / 2) 1))] fun (t : ℝ) ↦
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
have rw : curveIntegralFun ω (γab.trans γbc) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo (1 / 2) 1))] fun (t : ℝ) ↦
  HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
Tactic: rw [uIoc_of_le (by linarith), ← restrict_Ioo_eq_restrict_Ioc]