awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
    ∫ᶜ (x : E) in Path.segment a c, ω x
have hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
Tactic: have hφs : range φ ⊆ s := by
    rw [range_subset_iff]
    intro x
    simp [φ, ha, hb, hc, hs.lineMap_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
    ∫ᶜ (x : E) in Path.segment a c, ω x
have refine_6 : ∀
  (this :
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
      HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)),
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
    ∫ᶜ (x : E) in Path.segment a c, ω x
Tactic: have := φ.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt (t := range φ) (ω := ω)
    (dω := dω) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
refine_6 :
  ∀
    (this :
      HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
        HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)),
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
      ∫ᶜ (x : E) in Path.segment a c, ω x
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
    ∫ᶜ (x : E) in Path.segment a c, ω x
have refine_1 : ∀ (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) (γ := Set E)
          (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E))
          ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
Tactic: have := φ.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt (t := range φ) (ω := ω)
    (dω := dω) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
refine_6 :
  ∀
    (this :
      HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
        HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)),
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
      ∫ᶜ (x : E) in Path.segment a c, ω x
refine_1 :
  ∀ (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) (γ := Set E)
            (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E))
            ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
    ∫ᶜ (x : E) in Path.segment a c, ω x
have refine_2 : ∀ (x : E),
  Membership.mem (γ := Set E) (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x →
    HasFDerivWithinAt ω (dω x) (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
Tactic: have := φ.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt (t := range φ) (ω := ω)
    (dω := dω) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
refine_6 :
  ∀
    (this :
      HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
        HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)),
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
      ∫ᶜ (x : E) in Path.segment a c, ω x
refine_1 :
  ∀ (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) (γ := Set E)
            (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E))
            ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
refine_2 :
  ∀ (x : E),
    Membership.mem (γ := Set E) (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x →
      HasFDerivWithinAt ω (dω x) (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
    ∫ᶜ (x : E) in Path.segment a c, ω x
have refine_3 : ContinuousOn ω
  (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)))
Tactic: have := φ.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt (t := range φ) (ω := ω)
    (dω := dω) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
refine_6 :
  ∀
    (this :
      HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
        HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)),
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
      ∫ᶜ (x : E) in Path.segment a c, ω x
refine_1 :
  ∀ (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) (γ := Set E)
            (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E))
            ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
refine_2 :
  ∀ (x : E),
    Membership.mem (γ := Set E) (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x →
      HasFDerivWithinAt ω (dω x) (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
refine_3 :
  ContinuousOn ω
    (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)))
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
    ∫ᶜ (x : E) in Path.segment a c, ω x
have refine_4 : ∀ (x : E),
  Membership.mem (γ := Set E) (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x →
    ∀ u ∈ tangentConeAt ℝ (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x,
      ∀ v ∈ tangentConeAt ℝ (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x,
        Eq.{u_3 + 1} (α := F) ((((dω x : (a : E) → E →L[𝕜] F) u : E →L[𝕜] F) : (a : E) → F) v : F)
          ((((dω x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) u : F)
Tactic: have := φ.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt (t := range φ) (ω := ω)
    (dω := dω) ?_ ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
this :
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
    ∫ᶜ (x : E) in Path.segment a c, ω x
have h : Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment b c, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x)
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
this :
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)
h : Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment b c, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x)
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x) =
    ∫ᶜ (x : E) in Path.segment a c, ω x
have h₁ : ∫ᶜ (x : E) in Path.segment a c, ω x =
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
this :
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment b c, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x)
have h : Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment b c, ω x)
  (∫ᶜ (x : E) in
    (Path.segment ((lineMap a b : (a : ℝ) → E) 1) ((lineMap a c : (a : ℝ) → E) 1) :
      Path (X := E) ((lineMap a b : (a : ℝ) → E) 1 : E) ((lineMap a c : (a : ℝ) → E) 1 : E)),
    ω x)
Tactic: dsimp [φ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
this :
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment b c, ω x)
    (∫ᶜ (x : E) in
      (Path.segment ((lineMap a b : (a : ℝ) → E) 1) ((lineMap a c : (a : ℝ) → E) 1) :
        Path (X := E) ((lineMap a b : (a : ℝ) → E) 1 : E) ((lineMap a c : (a : ℝ) → E) 1 : E)),
      ω x)
have h : Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment b c, ω x) (∫ᶜ (x : E) in Path.cast (Path.segment b c) sorry sorry, ω x)
Tactic: rw [← Path.cast_segment (lineMap_apply_one a b) (lineMap_apply_one a c), curveIntegral_cast]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
this :
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)
h : Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment b c, ω x) (∫ᶜ (x : E) in Path.cast (Path.segment b c) ⋯ ⋯, ω x)
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment b c, ω x)
    (∫ᶜ (x : E) in
      (Path.segment ((lineMap a b : (a : ℝ) → E) 1) ((lineMap a c : (a : ℝ) → E) 1) :
        Path (X := E) ((lineMap a b : (a : ℝ) → E) 1 : E) ((lineMap a c : (a : ℝ) → E) 1 : E)),
      ω x)
have h₁ : Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment b c, ω x) (∫ᶜ (x : E) in Path.segment b c, ω x)
Tactic: rw [← Path.cast_segment (lineMap_apply_one a b) (lineMap_apply_one a c), curveIntegral_cast]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
a b c : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
hs : Convex ℝ s
hω : ∀ x ∈ s, HasFDerivWithinAt ω (dω x) s x
hdω :
  ∀ a ∈ s,
    ∀ x ∈ tangentConeAt ℝ s a,
      ∀ y ∈ tangentConeAt ℝ s a,
        Eq.{u_3 + 1} (α := F) ((((dω a : (a : E) → E →L[𝕜] F) x : E →L[𝕜] F) : (a : E) → F) y : F)
          ((((dω a : (a : E) → E →L[𝕜] F) y : E →L[𝕜] F) : (a : E) → F) x : F)
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
φ : ContinuousMap.Homotopy (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E)) :=
  ContinuousMap.Homotopy.affine (↑(Path.segment a b) : C((↑I : Type), E)) (↑(Path.segment a c) : C((↑I : Type), E))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
this :
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)
⊢ ∫ᶜ (x : E) in Path.segment a c, ω x =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)
have h : ∫ᶜ (x : E) in Path.segment a c, ω x =
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a c, ω x)
    (∫ᶜ (x : E) in
      (Path.segment ((lineMap a b : (a : ℝ) → E) 0) ((lineMap a c : (a : ℝ) → E) 0) :
        Path (X := E) ((lineMap a b : (a : ℝ) → E) 0 : E) ((lineMap a c : (a : ℝ) → E) 0 : E)),
      ω x)
Tactic: dsimp [φ]