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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht : t < 1 / 2
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ (𝓝 t).EventuallyEq (β := E) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)

Tactic:
have H₁ : (γab.trans γbc).extend =ᶠ[𝓝 t] (fun s ↦ γab.extend (2 * s)) :=
    (eventually_le_nhds ht).mono fun _ ↦ Path.extend_trans_of_le_half _ _
-- 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
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)
rw : 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
⊢ HSMul.hSMul (α := ℝ) 2 I =ᶠ[𝓝 (2 * t)] I

Tactic:
rw [LinearOrderedField.smul_Icc two_pos, mul_zero, mul_one, ← nhdsWithin_eq_iff_eventuallyEq]

Premises used: nhdsWithin_eq_iff_eventuallyEq, MulZeroClass.mul_zero, mul_one, LinearOrderedField.smul_Icc
-- 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
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)
inl : ∀ (ht₀ : t < 0), 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
inr :
  ∀ (ht : 0 < 1 / 2)
    (H₁ :
      EventuallyEq (β := E) (𝓝 0) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦
        (γab.extend : (a : ℝ) → E) (2 * s)),
    𝓝[Icc 0 2] HMul.hMul (α := ℝ) 2 0 = 𝓝[I] HMul.hMul (α := ℝ) 2 0
inr₁ : ∀ (ht₀ : 0 < t), 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)

Tactic:
rcases lt_trichotomy t 0 with ht₀ | rfl | ht₀

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- 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
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₀ : t < 0
inl : 2 * t ∉ closure I
inl₁ : 2 * t ∉ closure (Icc 0 2)
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)

Tactic:
rw [notMem_closure_iff_nhdsWithin_eq_bot.mp, notMem_closure_iff_nhdsWithin_eq_bot.mp]

Premises used: notMem_closure_iff_nhdsWithin_eq_bot, Iff.mp
-- 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
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₀ : t < 0
inl : ∀ (h : 0 ≤ t ∧ 2 * t ≤ 1), False
⊢ 2 * t ∉ closure I

Tactic:
simp_intro h
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : 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₀ : t < 0
inl : ∀ (h : 0 ≤ t ∧ t ≤ 1), False
⊢ 2 * t ∉ closure (Icc 0 2)

Tactic:
simp_intro h
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : 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₀ : t < 0
h : 0 ≤ t ∧ 2 * t ≤ 1
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : t - 0 + (0 - t) = 0
⊢ False

Tactic:
linarith
-- 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
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₀ : t < 0
h : 0 ≤ t ∧ t ≤ 1
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
linarith₃ : t - 0 + (0 - t) = 0
⊢ False

Tactic:
linarith
-- 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
instE : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ht : 0 < 1 / 2
H₁ :
  EventuallyEq (β := E) (𝓝 0) (⇑(γab.trans γbc).extend : (a : ℝ) → E) fun (s : ℝ) ↦ (γab.extend : (a : ℝ) → E) (2 * s)
⊢ 𝓝[Icc 0 2] HMul.hMul (α := ℝ) 2 0 = 𝓝[I] HMul.hMul (α := ℝ) 2 0

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 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
inr : I ∈ 𝓝 (2 * t)
inr₁ : Icc 0 2 ∈ 𝓝 (2 * t)
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)

Tactic:
rw [nhdsWithin_eq_nhds.2, nhdsWithin_eq_nhds.2]

Premises used: Iff.mpr, nhdsWithin_eq_nhds
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : 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
inr : 2 * t < 1
⊢ I ∈ 𝓝 (2 * t)

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 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
inr : t < 1
⊢ Icc 0 2 ∈ 𝓝 (2 * t)

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 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 ≤ 2 * t → 2 / 2 = 1
linarith₁ : 1 ≤ 2 * t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 ≤ 2 * t → GT.gt (α := ℝ) 2 0
linarith₃ : 1 ≤ 2 * t → 2 * t - HMul.hMul (α := ℝ) 1 1 + (1 - 2 * t) = 0
⊢ 2 * t < 1

Tactic:
linarith
-- 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
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
linarith₃ : 1 ≤ t → 2 * t - HMul.hMul (α := ℝ) 1 1 + (0 - t) + (1 - t) = 0
⊢ t < 1

Tactic:
linarith
-- 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
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)
⊢ 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
-- 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
⊢ 0 ≤ 1 / 2

Tactic:
positivity
-- 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
rw :
  curveIntegralFun ω (γab.trans γbc) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 (1 / 2)))] fun (t : ℝ) ↦
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
⊢ curveIntegralFun ω (γab.trans γbc) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ι 0 (1 / 2)))] fun (t : ℝ) ↦
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))

Tactic:
rw [uIoc_of_le (by positivity), ← restrict_Ioo_eq_restrict_Ioc]

Premises used: MeasureTheory.restrict_Ioo_eq_restrict_Ioc, 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 c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
t : ℝ
h :
  ∀ (ht₀ : 0 < t) (ht : t < 1 / 2),
    curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
⊢ t ∈ Ioo 0 (1 / 2) → curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))

Tactic:
⟨ht₀, ht⟩
-- 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 :
  ∀ (t : ℝ) (ht₀ : 0 < t) (ht : t < 1 / 2),
    curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
⊢ curveIntegralFun ω (γab.trans γbc) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 (1 / 2)))] fun (t : ℝ) ↦
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))

Tactic:
filter_upwards [ae_restrict_mem measurableSet_Ioo] with t ⟨ht₀, ht⟩

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioo
-- 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
t : ℝ
ht₀ : 0 < t
ht : t < 1 / 2
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))

Tactic:
curveIntegralFun_trans_of_lt_half ω γab γbc ht

Premises used: curveIntegralFun_trans_of_lt_half
-- 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
t : ℝ
ht₀ : 0 < t
ht : t < 1 / 2
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))

Tactic:
exact curveIntegralFun_trans_of_lt_half ω γab γbc ht

Premises used: curveIntegralFun_trans_of_lt_half
-- 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
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
linarith₆ :
  1 / 2 ≤ 1 - t → HMul.hMul (α := ℝ) 1 1 - 2 * t + (HMul.hMul (α := ℝ) 1 1 - (HMul.hMul (α := ℝ) 2 1 - 2 * t)) = 0
⊢ 1 - t < 1 / 2

Tactic:
linarith
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
rw :
  HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (1 - 2 * (1 - t))) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
⊢ curveIntegralFun ω (γab.trans γbc) 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]

Premises used: Path.trans, curveIntegralFun_symm_apply, neg_neg, smul_neg, Path.symm_symm, Path.trans_symm, curveIntegralFun_trans_of_lt_half
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
e_a : 1 - 2 * (1 - t) = 2 * t - 1
⊢ HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (1 - 2 * (1 - t))) =
    HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))

Tactic:
congr 2
-- 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
t : ℝ
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
ht₀ : 1 / 2 < t
⊢ 1 - 2 * (1 - t) = 2 * t - 1

Tactic:
ring
-- 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
linarith : 1 < 1 / 2 → 2 / 2 = 1
linarith₁ : 1 < 1 / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < 1 / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 < 1 / 2 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
⊢ 1 / 2 ≤ 1

Tactic:
linarith
-- 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
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))
⊢ curveIntegralFun ω (γab.trans γbc) =ᶠ[ae (F := Measure ℝ) (Measure.restrict volume (Ι (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]

Premises used: MeasureTheory.restrict_Ioo_eq_restrict_Ioc, 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 c : E
ω : E → E →L[𝕜] F
γab : Path a b
γbc : Path b c
t : ℝ
h :
  ∀ (ht₁ : 1 / 2 < t) (ht₂ : t < 1),
    curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
⊢ t ∈ Ioo (1 / 2) 1 → curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))

Tactic:
⟨ht₁, ht₂⟩
-- 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 :
  ∀ (t : ℝ) (ht₁ : 1 / 2 < t) (ht₂ : t < 1),
    curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))
⊢ 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:
filter_upwards [ae_restrict_mem measurableSet_Ioo] with t ⟨ht₁, ht₂⟩

Premises used: MeasureTheory.ae_restrict_mem, measurableSet_Ioo
-- 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
t : ℝ
ht₁ : 1 / 2 < t
ht₂ : t < 1
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))

Tactic:
curveIntegralFun_trans_of_half_lt ω γab γbc ht₁

Premises used: curveIntegralFun_trans_of_half_lt
-- 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
t : ℝ
ht₁ : 1 / 2 < t
ht₂ : t < 1
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))

Tactic:
exact curveIntegralFun_trans_of_half_lt ω γab γbc ht₁

Premises used: curveIntegralFun_trans_of_half_lt
-- 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
h : CurveIntegrable ω γab
γbc : Path b c
⊢ IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) volume 0 (1 / 2)

Tactic:
.congr_ae ?_ (curveIntegralFun_trans_aeeq_left _ _ _).symm

Premises used: curveIntegralFun_trans_aeeq_left, IntervalIntegrable.congr_ae, Filter.EventuallyEq.symm
-- 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
h : CurveIntegrable ω γab
γbc : Path b c
refine :
  IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))) volume 0
    (1 / 2)
⊢ IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) volume 0 (1 / 2)

Tactic:
refine .congr_ae ?_ (curveIntegralFun_trans_aeeq_left _ _ _).symm
-- 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
h : CurveIntegrable ω γab
γbc : Path b c
⊢ IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))) volume 0
    (1 / 2)

Tactic:
simpa [ofNat_smul_eq_nsmul] using h.comp_mul_left.smul (2 : 𝕜)

Premises used: ofNat_smul_eq_nsmul, IntervalIntegrable.comp_mul_left, IntervalIntegrable.smul, 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
γbc : Path b c
γab : Path a b
h : CurveIntegrable ω γbc
⊢ IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) volume (1 / 2) 1

Tactic:
.congr_ae ?_ (curveIntegralFun_trans_aeeq_right _ _ _).symm

Premises used: curveIntegralFun_trans_aeeq_right, IntervalIntegrable.congr_ae, Filter.EventuallyEq.symm
-- 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
γbc : Path b c
γab : Path a b
h : CurveIntegrable ω γbc
refine :
  IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))) volume
    (1 / 2) 1
⊢ IntervalIntegrable (curveIntegralFun ω (γab.trans γbc)) volume (1 / 2) 1

Tactic:
refine .congr_ae ?_ (curveIntegralFun_trans_aeeq_right _ _ _).symm
-- 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
γbc : Path b c
γab : Path a b
h : CurveIntegrable ω γbc
⊢ IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γbc (2 * t - 1))) volume
    (1 / 2) 1

Tactic:
simpa [ofNat_smul_eq_nsmul] using h.comp_sub_right 1 |>.comp_mul_left (c := 2) |>.smul (2 : 𝕜)

Premises used: IntervalIntegrable.comp_sub_right, ofNat_smul_eq_nsmul, IntervalIntegrable.comp_mul_left, IntervalIntegrable.smul, OfNat.ofNat