awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℝ F
a_1 b_1 c d : E
γ₁ : Path a_1 b_1
γ₂ : Path c d
s : Set ((↑I : Type) × (↑I : Type))
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : Homotopy (↑γ₁ : C((↑I : Type), E)) (↑γ₂ : C((↑I : Type), E))
hs : s.Countable
hφt :
  ∀ (a : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a →
      ∀ (b : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b →
          Membership.mem (α := E) t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b) : E)
hω :
  ∀ (a : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a →
      ∀ (b : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b →
          (a, b) ∉ s →
            HasFDerivWithinAt ω (dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b))) t
              ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ (a : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a →
      ∀ (b : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b →
          (a, b) ∉ s →
            ∀ u ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)),
              ∀ v ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)),
                Eq.{u_3 + 1} (α := F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)) : (a : E) → E →L[ℝ] F) u : E →L[ℝ] F) :
                        (a : E) → F)
                      v :
                    F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)) : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) :
                        (a : E) → F)
                      u :
                    F)
U : Set (ℝ × ℝ) := SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)
hU : U = SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (E := ℝ × ℝ) (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E :=
  fun (xy : ℝ × ℝ) ↦
    Set.IccExtend (a := 0) (b := 1) ⋯
      (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ :
  ψ = fun (xy : ℝ × ℝ) ↦
    Set.IccExtend (a := 0) (b := 1) ⋯
      (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2
hψφ : ∀ (a b : (↑I : Type)), ψ ((↑a : ℝ), (↑b : ℝ)) = (φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
b : ℝ
a : { x : ℝ // x ∈ I }
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) ((↑a : ℝ), b).1
hb : Membership.mem (γ := Set ℝ) (Ioo 0 1) ((↑a : ℝ), b).2
⊢ b ∈ I

Tactic:
Ioo_subset_Icc_self hb

Premises used: Set.Ioo_subset_Icc_self, Set.Mem
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℝ F
a_1 b_1 c d : E
γ₁ : Path a_1 b_1
γ₂ : Path c d
s : Set ((↑I : Type) × (↑I : Type))
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : Homotopy (↑γ₁ : C((↑I : Type), E)) (↑γ₂ : C((↑I : Type), E))
hs : s.Countable
hφt :
  ∀ (a : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a →
      ∀ (b : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b →
          Membership.mem (α := E) t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b) : E)
hω :
  ∀ (a : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a →
      ∀ (b : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b →
          (a, b) ∉ s →
            HasFDerivWithinAt ω (dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b))) t
              ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ (a : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a →
      ∀ (b : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b →
          (a, b) ∉ s →
            ∀ u ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)),
              ∀ v ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)),
                Eq.{u_3 + 1} (α := F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)) : (a : E) → E →L[ℝ] F) u : E →L[ℝ] F) :
                        (a : E) → F)
                      v :
                    F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)) : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) :
                        (a : E) → F)
                      u :
                    F)
U : Set (ℝ × ℝ) := SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)
hU : U = SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (E := ℝ × ℝ) (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E :=
  fun (xy : ℝ × ℝ) ↦
    Set.IccExtend (a := 0) (b := 1) ⋯
      (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ :
  ψ = fun (xy : ℝ × ℝ) ↦
    Set.IccExtend (a := 0) (b := 1) ⋯
      (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2
hψφ : ∀ (a b : (↑I : Type)), ψ ((↑a : ℝ), (↑b : ℝ)) = (φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
a b : { x : ℝ // x ∈ I }
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) ((↑a : ℝ), (↑b : ℝ)).1
hb : Membership.mem (γ := Set ℝ) (Ioo 0 1) ((↑a : ℝ), (↑b : ℝ)).2
⊢ ψ ((↑a : ℝ), (↑b : ℝ)) ∈ t

Tactic:
simpa [hψφ] using hφt a ha b hb
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare
Goal:
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℝ F
a b c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set ((↑I : Type) × (↑I : Type))
t : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : Homotopy (↑γ₁ : C((↑I : Type), E)) (↑γ₂ : C((↑I : Type), E))
hs : s.Countable
hφt :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          Membership.mem (α := E) t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
hω :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            HasFDerivWithinAt ω (dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))) t
              ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            ∀ u ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
              ∀ v ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
                Eq.{u_3 + 1} (α := F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[ℝ] F) u : E →L[ℝ] F) :
                        (a : E) → F)
                      v :
                    F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) :
                        (a : E) → F)
                      u :
                    F)
U : Set (ℝ × ℝ) := SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)
hU : U = SProd.sprod (α := Set ℝ) (β := Set ℝ) (Ioo 0 1) (Ioo 0 1)
hinterior : interior (Icc 0 1) = U
hunique : UniqueDiffOn ℝ (E := ℝ × ℝ) (Icc 0 1)
hUopen : IsOpen U
hU_subset : U ⊆ Icc 0 1
hclosure : closure U = Icc 0 1
ψ : ℝ × ℝ → E :=
  fun (xy : ℝ × ℝ) ↦
    Set.IccExtend (a := 0) (b := 1) ⋯
      (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2
hcontdiff : ContDiffOn ℝ 2 ψ (Icc 0 1)
hψ :
  ψ = fun (xy : ℝ × ℝ) ↦
    Set.IccExtend (a := 0) (b := 1) ⋯
      (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2
hψφ : ∀ (a_1 b_1 : (↑I : Type)), ψ ((↑a_1 : ℝ), (↑b_1 : ℝ)) = (φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)
hψ_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ψ
⊢ MapsTo ψ U t

Tactic:
have hψUt : MapsTo ψ U t := by
    rintro ⟨a, b⟩ ⟨ha, hb⟩
    lift a to I using Ioo_subset_Icc_self ha
    lift b to I using Ioo_subset_Icc_self hb
    simpa [hψφ] using hφt a ha b 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 c d : E
γ₁ : Path a b
γ₂ : Path c d
s : Set ((↑I : Type) × (↑I : Type))
t : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
φ : Homotopy (↑γ₁ : C((↑I : Type), E)) (↑γ₂ : C((↑I : Type), E))
hs : s.Countable
hφt :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          Membership.mem (α := E) t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
hω :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            HasFDerivWithinAt ω (dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))) t
              ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a_1, b_1) ∉ s →
            ∀ u ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
              ∀ v ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
                Eq.{u_3 + 1} (α := F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[𝕜] F) u : E →L[𝕜] F) :
                        (a : E) → F)
                      v :
                    F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)) : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) :
                        (a : E) → F)
                      u :
                    F)
hcontdiff :
  ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
    (fun (xy : ℝ × ℝ) ↦
      Set.IccExtend (a := 0) (b := 1) ⋯
        (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2)
    (Icc 0 1)
simp :
  HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ₁, ContinuousLinearMap.restrictScalars ℝ (ω x))
      (∫ᶜ (x : E) in φ.evalAt 1, ContinuousLinearMap.restrictScalars ℝ (ω x)) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ₂, ContinuousLinearMap.restrictScalars ℝ (ω x))
      (∫ᶜ (x : E) in φ.evalAt 0, ContinuousLinearMap.restrictScalars ℝ (ω x))
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ₁, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ₂, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)

Tactic:
simp only [← curveIntegral_restrictScalars (𝕜 := 𝕜) (𝕝 := ℝ)]

Premises used: curveIntegral_restrictScalars
-- 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 d : E
γ₁ : Path a b
γ₂ : Path c d
t : Set E
ω : E → E →L[𝕜] F
dω : E → E →L[ℝ] E →L[𝕜] F
φ : Homotopy (↑γ₁ : C((↑I : Type), E)) (↑γ₂ : C((↑I : Type), E))
hφt :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          Membership.mem (α := E) t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
hω : ∀ x ∈ t, HasFDerivWithinAt ω (dω x) t x
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ x ∈ t,
    ∀ u ∈ tangentConeAt ℝ t x,
      ∀ v ∈ tangentConeAt ℝ t 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)
hcontdiff :
  ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
    (fun (xy : ℝ × ℝ) ↦
      Set.IccExtend (a := 0) (b := 1) ⋯
        (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2)
    (Icc 0 1)
⊢ Set.Countable (α := (↑I : Type) × (↑I : Type)) ∅

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 d : E
γ₁ : Path a b
γ₂ : Path c d
t : Set E
ω : E → E →L[𝕜] F
φ : Homotopy (↑γ₁ : C((↑I : Type), E)) (↑γ₂ : C((↑I : Type), E))
hφt :
  ∀ (a_1 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a_1 →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          Membership.mem (α := E) t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1) : E)
hω : DiffContOnCl ℝ ω t
hdω_symm :
  ∀ x ∈ t,
    ∀ u ∈ tangentConeAt ℝ t x,
      ∀ v ∈ tangentConeAt ℝ t x,
        Eq.{u_3 + 1} (α := F) ((((fderivWithin ℝ ω t x : (a : E) → E →L[𝕜] F) u : E →L[𝕜] F) : (a : E) → F) v : F)
          ((((fderivWithin ℝ ω t x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) u : F)
hcontdiff :
  ContDiffOn.{0, 0, u_2} ℝ (F := E) 2
    (fun (xy : ℝ × ℝ) ↦
      Set.IccExtend (a := 0) (b := 1) ⋯
        (⇑((φ.extend : (a : ℝ) → C((↑I : Type), E)) xy.1 : C((↑I : Type), E)) : (a : (↑I : Type)) → E) xy.2)
    (Icc 0 1)
⊢ HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ₁, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x) =
    HAdd.hAdd (α := F) (∫ᶜ (x : E) in γ₂, ω x) (∫ᶜ (x : E) in φ.evalAt 0, ω x)

Tactic:
φ.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt
    hφt (fun t ht ↦ (hω.differentiableOn t ht).hasFDerivWithinAt) hω.continuousOn
    hdω_symm hcontdiff

Premises used: ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt, DiffContOnCl.continuousOn, DiffContOnCl.differentiableOn, DifferentiableWithinAt.hasFDerivWithinAt
-- 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))
rw : ∀ (y : (↑I : Type) × (↑I : Type)), Membership.mem (α := E) s ((φ : (a : (↑I : Type) × (↑I : Type)) → E) y : E)
⊢ range (ι := (↑I : Type) × (↑I : Type)) (⇑φ : (a : (↑I : Type) × (↑I : Type)) → E) ⊆ s

Tactic:
rw [range_subset_iff]

Premises used: Set.range_subset_iff
-- 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))
x : (↑I : Type) × (↑I : Type)
⊢ Membership.mem (α := E) s ((φ : (a : (↑I : Type) × (↑I : Type)) → E) x : E)

Tactic:
simp [φ, ha, hb, hc, hs.lineMap_mem]

Premises used: Convex.lineMap_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))
⊢ 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]
-- 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)
⊢ 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)

Tactic:
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 :
  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)
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)
⊢ 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:
convert! this using 2
-- 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.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)
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.segment b c, ω x) (∫ᶜ (x : E) in φ.evalAt 1, ω x)

Tactic:
dsimp [φ]