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 : E
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in γ, ω x)
    (∫ (t : ℝ) in 0..1, (ω ((γ.extend : (a : ℝ) → E) t) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) t))
have simp : Eq.{u_3 + 1} (α := F)
  (∫ (t : ℝ) in 0..1, (ω ((γ.extend : (a : ℝ) → E) t) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I t))
  (∫ (t : ℝ) in 0..1, (ω ((γ.extend : (a : ℝ) → E) t) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) t))
Tactic: simp only [curveIntegral_def, 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
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
⊢ Eq.{u_3 + 1} (α := F)
    (∫ (t : ℝ) in 0..1, (ω ((γ.extend : (a : ℝ) → E) t) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I t))
    (∫ (t : ℝ) in 0..1, (ω ((γ.extend : (a : ℝ) → E) t) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) t))
have h : EventuallyEq.{0, u_3} (β := F) (ae (F := Measure ℝ) (Measure.restrict volume (Ι 0 1)))
  (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x))
  fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x)
Tactic: apply intervalIntegral.integral_congr_ae_restrict
-- 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
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
⊢ EventuallyEq.{0, u_3} (β := F) (ae (F := Measure ℝ) (Measure.restrict volume (Ι 0 1)))
    (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x))
    fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x)
have h : EventuallyEq.{0, u_3} (β := F) (ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 1)))
  (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x))
  fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x)
Tactic: rw [uIoc_of_le zero_le_one, ← 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 : E
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
⊢ EventuallyEq.{0, u_3} (β := F) (ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 1)))
    (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x))
    fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x)
have h : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x),
  Eq.{u_3 + 1} (α := F) ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x) : F)
    ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x) : F)
Tactic: filter_upwards [ae_restrict_mem (by measurability)] with x hx
-- 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
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ Eq.{u_3 + 1} (α := F) ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x) : F)
    ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x) : F)
have h : Eq.{u_3 + 1} (α := F) ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x) : F)
  ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x) : F)
Tactic: rw [derivWithin_of_mem_nhds (by simpa)]
-- 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
ω : E → E →L[𝕜] F
a : E
⊢ curveIntegralFun ω (Path.refl a) = 0
have h : ∀ (x : ℝ), curveIntegralFun ω (Path.refl a) 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 c d : E
ω : E → E →L[𝕜] F
γ : Path a b
hc : c = a
hd : d = b
⊢ curveIntegralFun ω (γ.cast hc hd) = curveIntegralFun ω γ
have h : ∀ (t : ℝ), curveIntegralFun ω (γ.cast hc hd) t = curveIntegralFun ω γ t
Tactic: ext t
-- 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
⊢ curveIntegralFun ω (γab.trans γbc) t = HSMul.hSMul (α := ℕ) 2 (curveIntegralFun ω γab (2 * t))
have H₁ : (𝓝 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 _ _
-- 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)
⊢ HSMul.hSMul (α := ℝ) 2 I =ᶠ[𝓝 (2 * t)] I
have rw : 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
Tactic: rw [LinearOrderedField.smul_Icc two_pos, mul_zero, mul_one, ← nhdsWithin_eq_iff_eventuallyEq]
-- 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)
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
have inl : ∀ (ht₀ : t < 0), 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
Tactic: rcases lt_trichotomy t 0 with ht₀ | rfl | 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 : 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)
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
have 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
Tactic: rcases lt_trichotomy t 0 with ht₀ | rfl | ht₀
Cleared hypotheses: t, ht, 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)
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
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
have inr₁ : ∀ (ht₀ : 0 < t), 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
Tactic: rcases lt_trichotomy t 0 with ht₀ | rfl | 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 : 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
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
have inl : 2 * t ∉ closure I
Tactic: rw [notMem_closure_iff_nhdsWithin_eq_bot.mp, notMem_closure_iff_nhdsWithin_eq_bot.mp]
-- 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₀ : t < 0
inl : 2 * t ∉ closure I
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
have inl₁ : 2 * t ∉ closure (Icc 0 2)
Tactic: rw [notMem_closure_iff_nhdsWithin_eq_bot.mp, notMem_closure_iff_nhdsWithin_eq_bot.mp]
-- 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₀ : t < 0
⊢ 2 * t ∉ closure I
have inl : ∀ (h : 0 ≤ t ∧ 2 * t ≤ 1), False
Tactic: simp_intro 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)
ht₀ : t < 0
⊢ 2 * t ∉ closure (Icc 0 2)
have inl : ∀ (h : 0 ≤ t ∧ t ≤ 1), False
Tactic: simp_intro 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)
ht₀ : t < 0
h : 0 ≤ t ∧ 2 * t ≤ 1
⊢ False
have linarith : 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 : 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
⊢ False
have linarith₁ : 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 : 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
⊢ False
have linarith₂ : 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₀ : t < 0
h : 0 ≤ t ∧ 2 * t ≤ 1
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
⊢ False
have linarith₃ : t - 0 + (0 - 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 : 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
⊢ False
have linarith : 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 : 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
⊢ False
have linarith₁ : 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 : 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
⊢ False
have linarith₂ : 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₀ : t < 0
h : 0 ≤ t ∧ t ≤ 1
linarith : 2 / 2 = 1
linarith₁ : HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : GT.gt (α := ℝ) 2 0
⊢ False
have linarith₃ : t - 0 + (0 - 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 : 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
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
have inr : I ∈ 𝓝 (2 * t)
Tactic: rw [nhdsWithin_eq_nhds.2, nhdsWithin_eq_nhds.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
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)
⊢ 𝓝[Icc 0 2] (2 * t) = 𝓝[I] (2 * t)
have inr₁ : Icc 0 2 ∈ 𝓝 (2 * t)
Tactic: rw [nhdsWithin_eq_nhds.2, nhdsWithin_eq_nhds.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
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
⊢ I ∈ 𝓝 (2 * t)
have inr : 2 * t < 1
Tactic: simp [*]
-- 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
⊢ Icc 0 2 ∈ 𝓝 (2 * t)
have inr : t < 1
Tactic: simp [*]
-- 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
⊢ 2 * t < 1
have linarith : 1 ≤ 2 * 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 : 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
⊢ 2 * t < 1
have linarith₁ : 1 ≤ 2 * 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 : 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
⊢ 2 * t < 1
have linarith₂ : 1 ≤ 2 * 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 ≤ 2 * t → 2 / 2 = 1
linarith₁ : 1 ≤ 2 * t → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 ≤ 2 * t → GT.gt (α := ℝ) 2 0
⊢ 2 * t < 1
have linarith₃ : 1 ≤ 2 * t → 2 * t - HMul.hMul (α := ℝ) 1 1 + (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 : 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
⊢ t < 1
have linarith : 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 : 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
⊢ t < 1
have linarith₁ : 1 ≤ t → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith