awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
        (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)
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.cast (Path.segment a a) sorry sorry, ω x)
Tactic: rw [← Path.cast_segment (lineMap_apply_zero a b) (lineMap_apply_zero a c)]
-- 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
⊢ ContinuousOn ω
    (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)))
have refine_3 : ContinuousOn ω (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E))
Tactic: rw [(isCompact_range <| map_continuous _).isClosed.closure_eq]
-- 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
x : E
hx : Membership.mem (γ := Set E) (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
u : E
hu : u ∈ tangentConeAt ℝ (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
v : E
hv : 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)
have refine_4 : x ∈ s
Tactic: apply hdω
-- 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
x : E
hx : Membership.mem (γ := Set E) (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
u : E
hu : u ∈ tangentConeAt ℝ (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
v : E
hv : v ∈ tangentConeAt ℝ (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
refine_4 : x ∈ s
⊢ 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)
have refine_4₁ : u ∈ tangentConeAt ℝ s x
Tactic: apply hdω
-- 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
x : E
hx : Membership.mem (γ := Set E) (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
u : E
hu : u ∈ tangentConeAt ℝ (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
v : E
hv : v ∈ tangentConeAt ℝ (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
refine_4 : x ∈ s
refine_4₁ : u ∈ tangentConeAt ℝ s 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)
have refine_4₂ : v ∈ tangentConeAt ℝ s x
Tactic: apply hdω
-- 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
⊢ EqOn.{0, u_2} (β := E)
    (fun (x : ℝ × ℝ) ↦
      IccExtend (a := 0) (b := 1) ⋯
        (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) x.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) x.2)
    (fun (x : ℝ × ℝ) ↦
      ((lineMap ((lineMap a b : (a : ℝ) → E) x.2) ((lineMap a c : (a : ℝ) → E) x.2) : ℝ →ᵃ[ℝ] E) : (a : ℝ) → E) x.1)
    (Icc 0 1)
have rw : EqOn.{0, u_2} (β := E)
  (fun (x : ℝ × ℝ) ↦
    IccExtend (a := 0) (b := 1) sorry
      (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) x.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) x.2)
  (fun (x : ℝ × ℝ) ↦
    ((lineMap ((lineMap a b : (a : ℝ) → E) x.2) ((lineMap a c : (a : ℝ) → E) x.2) : ℝ →ᵃ[ℝ] E) : (a : ℝ) → E) x.1)
  (SProd.sprod (α := Set ℝ) (β := Set ℝ) (Icc 0.1 1.1) (Icc 0.2 1.2))
Tactic: rw [Icc_prod_eq]
-- 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
x y : ℝ
hx : Membership.mem (γ := Set ℝ) (Icc 0.1 1.1) (x, y).1
hy : Membership.mem (γ := Set ℝ) (Icc 0.2 1.2) (x, y).2
⊢ Eq.{u_2 + 1} (α := E)
    ((fun (x : ℝ × ℝ) ↦
        (IccExtend (a := 0) (b := 1) ⋯
            (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) x.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) x.2 :
          E))
      (x, y))
    ((fun (x : ℝ × ℝ) ↦
        (((lineMap ((lineMap a b : (a : ℝ) → E) x.2) ((lineMap a c : (a : ℝ) → E) x.2) : ℝ →ᵃ[ℝ] E) : (a : ℝ) → E) x.1 :
          E))
      (x, y))
have lift : ∀ (x : { x : ℝ // x ∈ I }) (hy : Membership.mem (γ := Set ℝ) (Icc 0.2 1.2) ((↑x : ℝ), y).2),
  Eq.{u_2 + 1} (α := E)
    ((fun (x : ℝ × ℝ) ↦
        (IccExtend (a := 0) (b := 1) sorry
            (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) x.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) x.2 :
          E))
      ((↑x : ℝ), y))
    ((fun (x : ℝ × ℝ) ↦
        (((lineMap ((lineMap a b : (a : ℝ) → E) x.2) ((lineMap a c : (a : ℝ) → E) x.2) : ℝ →ᵃ[ℝ] E) : (a : ℝ) → E) x.1 :
          E))
      ((↑x : ℝ), y))
Tactic: lift x to I using hx
Cleared hypotheses: x, hx, hy
-- 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
y : ℝ
x : { x : ℝ // x ∈ I }
hy : Membership.mem (γ := Set ℝ) (Icc 0.2 1.2) ((↑x : ℝ), y).2
⊢ Eq.{u_2 + 1} (α := E)
    ((fun (x : ℝ × ℝ) ↦
        (IccExtend (a := 0) (b := 1) ⋯
            (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) x.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) x.2 :
          E))
      ((↑x : ℝ), y))
    ((fun (x : ℝ × ℝ) ↦
        (((lineMap ((lineMap a b : (a : ℝ) → E) x.2) ((lineMap a c : (a : ℝ) → E) x.2) : ℝ →ᵃ[ℝ] E) : (a : ℝ) → E) x.1 :
          E))
      ((↑x : ℝ), y))
have lift : ∀ (y : { x : ℝ // x ∈ I }),
  Eq.{u_2 + 1} (α := E)
    ((fun (x : ℝ × ℝ) ↦
        (IccExtend (a := 0) (b := 1) sorry
            (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) x.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) x.2 :
          E))
      ((↑x : ℝ), (↑y : ℝ)))
    ((fun (x : ℝ × ℝ) ↦
        (((lineMap ((lineMap a b : (a : ℝ) → E) x.2) ((lineMap a c : (a : ℝ) → E) x.2) : ℝ →ᵃ[ℝ] E) : (a : ℝ) → E) x.1 :
          E))
      ((↑x : ℝ), (↑y : ℝ)))
Tactic: lift y to I using hy
Cleared hypotheses: y, hy
-- 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))
hφs : range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s
⊢ ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
    (fun (xy : ℝ × ℝ) ↦
      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)
have this : EqOn.{0, u_2} (β := E)
  (fun (x : ℝ × ℝ) ↦
    IccExtend (a := 0) (b := 1) sorry
      (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) x.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) x.2)
  (fun (x : ℝ × ℝ) ↦
    ((lineMap ((lineMap a b : (a : ℝ) → E) x.2) ((lineMap a c : (a : ℝ) → E) x.2) : ℝ →ᵃ[ℝ] E) : (a : ℝ) → E) x.1)
  (Icc 0 1)
Tactic: have : EqOn (fun x : ℝ × ℝ ↦ IccExtend zero_le_one (φ.extend x.1) x.2)
        (fun x ↦ lineMap (lineMap a b x.2) (lineMap a c x.2) x.1) (Icc 0 1) := by
      rw [Icc_prod_eq]
      rintro ⟨x, y⟩ ⟨hx, hy⟩
      lift x to I using hx
      lift y to I using hy
      simp [φ]
-- 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 :
  EqOn.{0, u_2} (β := E)
    (fun (x : ℝ × ℝ) ↦
      IccExtend (a := 0) (b := 1) ⋯
        (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) x.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) x.2)
    (fun (x : ℝ × ℝ) ↦
      ((lineMap ((lineMap a b : (a : ℝ) → E) x.2) ((lineMap a c : (a : ℝ) → E) x.2) : ℝ →ᵃ[ℝ] E) : (a : ℝ) → E) x.1)
    (Icc 0 1)
⊢ ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
    (fun (xy : ℝ × ℝ) ↦
      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)
have refine_5 : ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
  (fun (x : ℝ × ℝ) ↦
    ((lineMap ((lineMap a b : (a : ℝ) → E) x.2) ((lineMap a c : (a : ℝ) → E) x.2) : ℝ →ᵃ[ℝ] E) : (a : ℝ) → E) x.1)
  (Icc 0 1)
Tactic: refine .congr ?_ this
-- 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 :
  EqOn.{0, u_2} (β := E)
    (fun (x : ℝ × ℝ) ↦
      IccExtend (a := 0) (b := 1) ⋯
        (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) x.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) x.2)
    (fun (x : ℝ × ℝ) ↦
      ((lineMap ((lineMap a b : (a : ℝ) → E) x.2) ((lineMap a c : (a : ℝ) → E) x.2) : ℝ →ᵃ[ℝ] E) : (a : ℝ) → E) x.1)
    (Icc 0 1)
⊢ ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
    (fun (x : ℝ × ℝ) ↦
      ((lineMap ((lineMap a b : (a : ℝ) → E) x.2) ((lineMap a c : (a : ℝ) → E) x.2) : ℝ →ᵃ[ℝ] E) : (a : ℝ) → E) x.1)
    (Icc 0 1)
have refine_5 : ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
  (fun (x : ℝ × ℝ) ↦ (1 - x.1) • ((1 - x.2) • a + x.2 • b) + x.1 • ((1 - x.2) • a + x.2 • c)) (Icc 0 1)
Tactic: simp only [AffineMap.lineMap_apply_module]
-- 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 : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace 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
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∫ᶜ (x : E) in Path.segment a x, ω x) (ω b) s b
have suffices : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F)
  (fun (x : E) ↦ HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b x, ω x)) (ω b) s
  b
Tactic: suffices HasFDerivWithinAt (∫ᶜ x in .segment a b, ω x + ∫ᶜ x in .segment b ·, ω x) (ω b) s b from
    this.congr' (fun _ h ↦
      (hs.curveIntegral_segment_add_eq_of_hasFDerivWithinAt_symmetric hω hdω ha hb h).symm) hb
-- 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 : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace 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
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F)
    (fun (x : E) ↦ HAdd.hAdd (α := F) (∫ᶜ (x : E) in Path.segment a b, ω x) (∫ᶜ (x : E) in Path.segment b x, ω x)) (ω b)
    s b
have refine : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∫ᶜ (x : E) in Path.segment b x, ω x) (ω b) s b
Tactic: refine .const_add _ <| ?_
-- 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 : E
s : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
inst_7 : CompleteSpace 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
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∫ᶜ (x : E) in Path.segment b x, ω x) (ω b) s b
have refine : ContinuousOn ω s
Tactic: refine HasFDerivWithinAt.curveIntegral_segment_source hs ?_ hb