-- 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)
e : (E →L[𝕜] F) →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.restrictScalarsL 𝕜 E F ℝ ℝ
⊢ 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))

Tactic:
exact φ.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable_real hs hφt
    (dω := fun x ↦ e ∘L dω x)
    (fun a ha b hb hs ↦ e.hasFDerivAt.comp_hasFDerivWithinAt _ (hω a ha b hb hs))
    (e.continuous.comp_continuousOn hωc) hdω_symm hcontdiff

Premises used: ContinuousLinearMap.hasFDerivAt, Continuous.comp_continuousOn, HasFDerivAt.comp_hasFDerivWithinAt, Prod.mk, _private.0.ContinuousMap.Homotopy.curveIntegral_add_curveIntegral_eq_of_hasFDerivWithinAt_off_countable_real, ContinuousLinearMap.continuous, DFunLike.coe