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
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)
h₁ h₂ : Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment b c, ω x) (∫ᶜ (x : E) in 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)

Tactic:
rw [← Path.cast_segment (lineMap_apply_one a b) (lineMap_apply_one a c), curveIntegral_cast]

Premises used: AffineMap.lineMap_apply_one, curveIntegral_cast, Path.cast_segment
-- 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 :
  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 :
  ∫ᶜ (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)
⊢ ∫ᶜ (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:
dsimp [φ]
-- 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 :
  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 :
  ∫ᶜ (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) ⋯ ⋯, ω 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)

Tactic:
rw [← Path.cast_segment (lineMap_apply_zero a b) (lineMap_apply_zero a c)]

Premises used: AffineMap.lineMap_apply_zero, Path.cast_segment
-- 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 :
  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.cast (Path.segment a a) ⋯ ⋯, ω x)

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
a_1 : (↑I : Type)
h : Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1
b_1 : (↑I : Type)
h_1 : 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:
apply mem_range_self

Premises used: Set.mem_range_self
-- 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),
    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:
fun x hx ↦ (hω x (hφs hx)).mono hφs

Premises used: HasFDerivWithinAt.mono
-- 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),
    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:
exact fun x hx ↦ (hω x (hφs hx)).mono hφs

Premises used: HasFDerivWithinAt.mono
-- 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
refine_3 : ContinuousOn ω (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E))
⊢ ContinuousOn ω
    (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)))

Tactic:
rw [(isCompact_range <| map_continuous _).isClosed.closure_eq]

Premises used: IsClosed.closure_eq, isCompact_range, ContinuousMapClass.map_continuous, IsCompact.isClosed
-- 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
⊢ ContinuousOn ω (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E))

Tactic:
fun x hx ↦ (hω x <| hφs hx).continuousWithinAt.mono hφs

Premises used: ContinuousWithinAt.mono, ContinuousOn, HasFDerivWithinAt.continuousWithinAt
-- 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
⊢ ContinuousOn ω (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E))

Tactic:
exact fun x hx ↦ (hω x <| hφs hx).continuousWithinAt.mono hφs

Premises used: ContinuousWithinAt.mono, HasFDerivWithinAt.continuousWithinAt
-- 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
refine_4 : x ∈ s
refine_4₁ : u ∈ tangentConeAt ℝ s x
refine_4₂ : v ∈ 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)

Tactic:
apply hdω
-- 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
refine_4 :
  Membership.mem (γ := Set E) (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
⊢ x ∈ s

Tactic:
grw [← hφs]
-- 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
refine_4 : u ∈ tangentConeAt ℝ (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
⊢ u ∈ tangentConeAt ℝ s x

Tactic:
grw [← hφs]
-- 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 refine_4 : v ∈ tangentConeAt ℝ (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x
⊢ v ∈ tangentConeAt ℝ s x

Tactic:
grw [← hφs]
-- 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
⊢ Membership.mem (γ := Set E) (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
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
⊢ u ∈ tangentConeAt ℝ (range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E)) x

Tactic:
assumption