awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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
⊢ v ∈ tangentConeAt ℝ (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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
rw :
  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)
    (SProd.sprod (α := Set ℝ) (β := Set ℝ) (Icc 0.1 1.1) (Icc 0.2 1.2))
⊢ 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)

Tactic:
rw [Icc_prod_eq]

Premises used: Set.Icc_prod_eq
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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
⊢ x ∈ I

Tactic:
hx

Premises used: Set.Mem
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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
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) ⋯
              (⇑((φ.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))
⊢ 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))

Tactic:
lift x to I using hx
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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
⊢ y ∈ I

Tactic:
hy

Premises used: Set.Mem
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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
lift :
  ∀ (y : { x : ℝ // x ∈ I }),
    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 : ℝ)))
⊢ 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))

Tactic:
lift y to I using hy
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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 : { x : ℝ // x ∈ I }
⊢ 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 : ℝ)))

Tactic:
simp [φ]
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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)

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 [φ]
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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)

Tactic:
.congr ?_ this

Premises used: ContDiffOn.congr
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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)
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)
⊢ 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)

Tactic:
refine .congr ?_ this
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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)
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)
⊢ 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:
simp only [AffineMap.lineMap_apply_module]

Premises used: AffineMap.lineMap_apply_module
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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 : ℝ × ℝ) ↦ (1 - x.1) • ((1 - x.2) • a + x.2 • b) + x.1 • ((1 - x.2) • a + x.2 • c)) (Icc 0 1)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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
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
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∫ᶜ (x : E) in Path.segment a 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
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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

Tactic:
.const_add _ <| ?_

Premises used: HasFDerivWithinAt.const_add
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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
refine :
  HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (x : E) ↦ ∫ᶜ (x : E) in Path.segment b x, ω x) (ω b) s b
⊢ 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:
refine .const_add _ <| ?_
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
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

Tactic:
HasFDerivWithinAt.curveIntegral_segment_source hs ?_ hb

Premises used: HasFDerivWithinAt.curveIntegral_segment_source