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
ω : E → E →L[𝕜] F
γ : Path a b
𝕝 : Type u_4
inst_5 : RCLike 𝕝
inst_6 : NormedSpace 𝕝 F
inst_7 : SMulCommClass 𝕜 𝕝 F
c : 𝕝
⊢ CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ
have inl : CurveIntegrable (HSMul.hSMul (α := 𝕝) 0 ω) γ ↔ Eq.{u_4 + 1} (α := 𝕝) 0 0 ∨ CurveIntegrable ω γ
Tactic: rcases eq_or_ne c 0 with rfl | hc
Cleared hypotheses: c
-- 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 : 𝕝
inl : CurveIntegrable (HSMul.hSMul (α := 𝕝) 0 ω) γ ↔ Eq.{u_4 + 1} (α := 𝕝) 0 0 ∨ CurveIntegrable ω γ
⊢ CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ
have inr : ∀ (hc : c ≠ 0), CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ
Tactic: rcases eq_or_ne c 0 with rfl | hc
-- 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 : 𝕝
hc : c ≠ 0
⊢ CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ
have inr : CurveIntegrable (c • ω) γ ↔ CurveIntegrable ω γ
Tactic: simp only [hc, false_or]
-- 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 : 𝕝
hc : c ≠ 0
⊢ CurveIntegrable (c • ω) γ ↔ CurveIntegrable ω γ
have inr : ∀ (h : CurveIntegrable (c • ω) γ), CurveIntegrable ω γ
Tactic: refine ⟨fun h ↦ ?_, .smul⟩
-- 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∫ᶜ (x : E) in Path.segment a x, ω x) (ω a) s a
have simp : ∀ ⦃c : ℝ⦄,
  0 < c →
    ∀ᶠ (x : E) in 𝓝[s] a,
      ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a x, ω x : F) ((ω a : (a : E) → F) (x - a) : F)‖ ≤
        c * ‖x - a‖
Tactic: simp only [hasFDerivWithinAt_iff_isLittleO, Path.segment_same, curveIntegral_refl, sub_zero,
    Asymptotics.isLittleO_iff]
-- 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
⊢ ∃ δ > 0, ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
have rw : {a : E | ContinuousWithinAt ω s a} ∈ 𝓝[s] a ∧ {a_1 : E | dist (ω a_1) (ω a) ≤ ε} ∈ 𝓝[s] a
Tactic: rw [← Metric.mem_nhdsWithin_iff, setOf_and, inter_mem_iff]
-- 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (x : E) in 𝓝[s] a,
    ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a x, ω x : F) ((ω a : (a : E) → F) (x - a) : F)‖ ≤
      ε * ‖x - a‖
have obtain : ∀ (δ : ℝ) (hδ₀ : δ > 0) (hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}),
  ∀ᶠ (x : E) in 𝓝[s] a,
    ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a x, ω x : F) ((ω a : (a : E) → F) (x - a) : F)‖ ≤
      ε * ‖x - a‖
Tactic: obtain ⟨δ, hδ₀, hδ⟩ : ∃ δ > 0,
      ball a δ ∩ s ⊆ {z | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε} := by
    rw [← Metric.mem_nhdsWithin_iff, setOf_and, inter_mem_iff]
    exact ⟨hω, (hω.self_of_nhdsWithin ha).eventually <| closedBall_mem_nhds _ 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
⊢ ∀ᶠ (x : E) in 𝓝[s] a,
    ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a x, ω x : F) ((ω a : (a : E) → F) (x - a) : F)‖ ≤
      ε * ‖x - a‖
have rw : ∀ᶠ (x : E) in 𝓝 a,
  x ∈ s →
    ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a x, ω x : F) ((ω a : (a : E) → F) (x - a) : F)‖ ≤
      ε * ‖x - a‖
Tactic: rw [eventually_nhdsWithin_iff]
-- 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
⊢ ∀ᶠ (x : E) in 𝓝 a,
    x ∈ s →
      ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a x, ω x : F) ((ω a : (a : E) → F) (x - a) : F)‖ ≤
        ε * ‖x - a‖
have h : ∀ (b : E) (hb : b ∈ ball a δ) (hbs : b ∈ s),
  ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a b, ω x : F) ((ω a : (a : E) → F) (b - a) : F)‖ ≤
    ε * ‖b - a‖
Tactic: filter_upwards [Metric.ball_mem_nhds _ hδ₀] with b hb hbs
-- 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
⊢ ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a b, ω x : F) ((ω a : (a : E) → F) (b - a) : F)‖ ≤
    ε * ‖b - a‖
have hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
Tactic: have hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s :=
    ((convex_ball _ _).inter hs).segment_subset (by simp [*]) (by 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a b, ω x : F) ((ω a : (a : E) → F) (b - a) : F)‖ ≤
    ε * ‖b - a‖
have h : norm.{u_3} (E := F) (∫ᶜ (x : E) in Path.segment a b, (ω x - ω a)) ≤ ε * ‖b - a‖
Tactic: rw [← curveIntegral_segment_const, ← curveIntegral_fun_sub]
-- 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
h : norm.{u_3} (E := F) (∫ᶜ (x : E) in Path.segment a b, (ω x - ω a)) ≤ ε * ‖b - a‖
⊢ ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a b, ω x : F) ((ω a : (a : E) → F) (b - a) : F)‖ ≤
    ε * ‖b - a‖
have h₁ : CurveIntegrable ω (Path.segment a b)
Tactic: rw [← curveIntegral_segment_const, ← curveIntegral_fun_sub]
-- 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
h : norm.{u_3} (E := F) (∫ᶜ (x : E) in Path.segment a b, (ω x - ω a)) ≤ ε * ‖b - a‖
h₁ : CurveIntegrable ω (Path.segment a b)
⊢ ‖HSub.hSub (α := F) (β := F) (∫ᶜ (x : E) in Path.segment a b, ω x : F) ((ω a : (a : E) → F) (b - a) : F)‖ ≤
    ε * ‖b - a‖
have h₂ : CurveIntegrable.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ω a) (Path.segment a b)
Tactic: rw [← curveIntegral_segment_const, ← curveIntegral_fun_sub]
-- 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ norm.{u_3} (E := F) (∫ᶜ (x : E) in Path.segment a b, (ω x - ω a)) ≤ ε * ‖b - a‖
have h : ∀ (z : E) (hz : z ∈ [a -[ℝ] b]), ‖ω z - ω a‖ ≤ ε
Tactic: refine norm_curveIntegral_segment_le fun z hz ↦ ?_
-- 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ CurveIntegrable ω (Path.segment a b)
have h : IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a)) volume 0 1
Tactic: rw [curveIntegrable_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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
⊢ IntervalIntegrable.{u_3} (ε := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a)) volume 0 1
have h : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t),
  ContinuousWithinAt.{0, u_3} (Y := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
    (Icc 0 1) t
Tactic: refine ContinuousOn.intervalIntegrable_of_Icc zero_le_one 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ ContinuousWithinAt.{0, u_3} (Y := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
    (Icc 0 1) t
have h : Membership.mem (α := E) (ball a δ ∩ s) ((lineMap a b : (a : ℝ) → E) t : E)
Tactic: refine ((hδ ?_).1.eval_const _).comp AffineMap.lineMap_continuous.continuousWithinAt ?_
-- 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
h : Membership.mem (α := E) (ball a δ ∩ s) ((lineMap a b : (a : ℝ) → E) t : E)
⊢ ContinuousWithinAt.{0, u_3} (Y := F) (fun (t : ℝ) ↦ (ω ((lineMap a b : (a : ℝ) → E) t) : (a : E) → F) (b - a))
    (Icc 0 1) t
have h₁ : MapsTo (α := ℝ) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1) s
Tactic: refine ((hδ ?_).1.eval_const _).comp AffineMap.lineMap_continuous.continuousWithinAt ?_
-- 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 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : CompleteSpace F
a : E
s : Set E
ω : E → E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ᶠ (x : E) in 𝓝[s] a, ContinuousWithinAt ω s x
ha : a ∈ s
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : δ > 0
hδ : ball a δ ∩ s ⊆ {z : E | ContinuousWithinAt ω s z ∧ dist (ω z) (ω a) ≤ ε}
b : E
hb : b ∈ ball a δ
hbs : b ∈ s
hsub : [a -[ℝ] b] ⊆ ball a δ ∩ s
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ MapsTo (α := ℝ) (⇑(lineMap a b) : (a : ℝ) → E) (Icc 0 1) s
have h : [a -[ℝ] b] ⊆ s
Tactic: rw [mapsTo_iff_image_subset, ← segment_eq_image_lineMap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (hypothesis)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set ((↑I : Type) × (↑I : Type))
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : Homotopy (↑γ₁ : C((↑I : Type), E)) (↑γ₂ : C((↑I : Type), E))
hs : s.Countable
hφt :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          Membership.mem (α := E) t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
hω :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            HasFDerivWithinAt ω (dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))) t
              ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            ∀ u ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
              ∀ v ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
                Eq.{u_3 + 1} (α := F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[ℝ] F) u : E →L[ℝ] F) :
                        (a : E) → F)
                      v :
                    F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) :
                        (a : E) → F)
                      u :
                    F)
hcontdiff :
  ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
    (fun (xy : ℝ × ℝ) ↦
      Set.IccExtend (a := 0) (b := 1) ⋯
        (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2)
    (Icc 0 1)
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ₁, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ₂, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)
have hU : let U := SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1);
U = SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)
Tactic: set U : Set (ℝ × ℝ) := Ioo 0 1 ×ˢ Ioo 0 1 with hU
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set ((↑I : Type) × (↑I : Type))
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : Homotopy (↑γ₁ : C((↑I : Type), E)) (↑γ₂ : C((↑I : Type), E))
hs : s.Countable
hφt :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          Membership.mem (α := E) t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
hω :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            HasFDerivWithinAt ω (dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))) t
              ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            ∀ u ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
              ∀ v ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
                Eq.{u_3 + 1} (α := F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[ℝ] F) u : E →L[ℝ] F) :
                        (a : E) → F)
                      v :
                    F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) :
                        (a : E) → F)
                      u :
                    F)
hcontdiff :
  ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
    (fun (xy : ℝ × ℝ) ↦
      Set.IccExtend (a := 0) (b := 1) ⋯
        (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2)
    (Icc 0 1)
U : Set (ℝ × ℝ) := SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)
hU : U = SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)
⊢ interior (Icc 0 1) = U
have rw : interior (Icc 0 1) = interior (SProd.sprod (α := Set ℝ) (β := Set ℝ) (Icc 0 1) (Icc 0 1))
Tactic: rw [hU, ← interior_Icc, ← interior_prod_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (hypothesis)
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set ((↑I : Type) × (↑I : Type))
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : Homotopy (↑γ₁ : C((↑I : Type), E)) (↑γ₂ : C((↑I : Type), E))
hs : s.Countable
hφt :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          Membership.mem (α := E) t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
hω :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            HasFDerivWithinAt ω (dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))) t
              ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            ∀ u ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
              ∀ v ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
                Eq.{u_3 + 1} (α := F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[ℝ] F) u : E →L[ℝ] F) :
                        (a : E) → F)
                      v :
                    F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) :
                        (a : E) → F)
                      u :
                    F)
hcontdiff :
  ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
    (fun (xy : ℝ × ℝ) ↦
      Set.IccExtend (a := 0) (b := 1) ⋯
        (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2)
    (Icc 0 1)
U : Set (ℝ × ℝ) := SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)
hU : U = SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ₁, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ₂, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)
have hinterior : interior (Icc 0 1) = U
Tactic: have hinterior : interior (Icc 0 1) = U := by
    rw [hU, ← interior_Icc, ← interior_prod_eq]
    simp [Prod.mk_zero_zero, Prod.mk_one_one]