-- 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_1 : Set ((↑I : Type) × (↑I : Type))
t_1 : Set E
ω : E → E →L[ℝ] F
dω : E → E →L[ℝ] E →L[ℝ] F
φ : Homotopy (↑γ₁ : C((↑I : Type), E)) (↑γ₂ : C((↑I : Type), E))
hs : s_1.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_1 ((φ : (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_1 →
            HasFDerivWithinAt ω (dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))) t_1
              ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t_1)
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_1 →
            ∀ u ∈ tangentConeAt ℝ t_1 ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a_1, b_1)),
              ∀ v ∈ tangentConeAt ℝ t_1 ((φ : (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] ψ
hψUt : MapsTo ψ U t_1
dψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] E := fderivWithin ℝ ψ (Icc 0 1)
s' : Set (ℝ × ℝ) := Prod.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) '' s_1
hs' : s' = Prod.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) '' s_1
hmem_s' : ∀ (x y : (↑I : Type)), ((↑x : ℝ), (↑y : ℝ)) ∈ s' ↔ (x, y) ∈ s_1
hs'c : s'.Countable
hdψ : ∀ a ∈ U, HasFDerivAt ψ (dψ a) a
d2ψ : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] E := fderivWithin ℝ dψ (Icc 0 1)
hd2ψ : ∀ a ∈ U, HasFDerivAt dψ (d2ψ a) a
hd2ψ_symm :
  ∀ (a : ℝ × ℝ),
    Membership.mem (γ := Set (ℝ × ℝ)) (Icc 0 1) a →
      ∀ (x y : ℝ × ℝ),
        Eq (α := E) ((((d2ψ a : (a : ℝ × ℝ) → ℝ × ℝ →L[ℝ] E) x : ℝ × ℝ →L[ℝ] E) : (a : ℝ × ℝ) → E) y : E)
          ((((d2ψ a : (a : ℝ × ℝ) → ℝ × ℝ →L[ℝ] E) y : ℝ × ℝ →L[ℝ] E) : (a : ℝ × ℝ) → E) x : E)
η : ℝ × ℝ → ℝ × ℝ →L[ℝ] F := fun (a : ℝ × ℝ) ↦ ω (ψ a) ∘SL dψ a
f : ℝ × ℝ → F := fun (a : ℝ × ℝ) ↦ (η a : (a : ℝ × ℝ) → F) (0, 1)
hf :
  ∀ (a : ℝ × ℝ),
    Membership.mem (γ := Set (ℝ × ℝ)) (Icc 0 1) a →
      f a = (ω (ψ a) : (a : E) → F) (derivWithin (ψ ∘ fun (x : ℝ) ↦ (a.1, x)) I a.2)
g : ℝ × ℝ → F := fun (a : ℝ × ℝ) ↦ -(η a : (a : ℝ × ℝ) → F) (1, 0)
hg :
  ∀ (a : ℝ × ℝ),
    Membership.mem (γ := Set (ℝ × ℝ)) (Icc 0 1) a →
      g a = (ω (ψ a) : (a : E) → F) (-derivWithin (ψ ∘ fun (x : ℝ) ↦ (x, a.2)) I a.1)
this :
  (HSub.hSub (α := F) (∫ (x : ℝ) in 0..1, g (x, 1)) (∫ (x : ℝ) in 0..1, g (x, 0)) + ∫ (y : ℝ) in 0..1, f (1, y)) -
      ∫ (y : ℝ) in 0..1, f (0, y) =
    0
s : (↑I : Type)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ Eq.{u_3 + 1} (α := F) ((fun (x : ℝ) ↦ f ((↑s : ℝ), x)) t)
    ((fun (x : ℝ) ↦
        ((ω
                ((Path.extend (x :=
                      ContinuousMap.toFun (X := (↑I : Type)) ((φ.curry : (a : (↑I : Type)) → C((↑I : Type), E)) s) 0)
                      { toContinuousMap := (φ.curry : (a : (↑I : Type)) → C((↑I : Type), E)) s, source' := ⋯,
                        target' := ⋯ :
                        Path (X := E)
                          (ContinuousMap.toFun (X := (↑I : Type)) ((φ.curry : (a : (↑I : Type)) → C((↑I : Type), E)) s)
                            0)
                          (ContinuousMap.toFun (X := (↑I : Type)) ((φ.curry : (a : (↑I : Type)) → C((↑I : Type), E)) s)
                            1) } :
                    (a : ℝ) → E)
                  x) :
              (a : E) → F)
            (derivWithin
              (⇑(Path.extend (x :=
                    ContinuousMap.toFun (X := (↑I : Type)) ((φ.curry : (a : (↑I : Type)) → C((↑I : Type), E)) s) 0)
                    { toContinuousMap := (φ.curry : (a : (↑I : Type)) → C((↑I : Type), E)) s, source' := ⋯,
                      target' := ⋯ }) :
                (a : ℝ) → E)
              I x) :
          F))
      t)

Tactic:
simp [Path.extend, hf (s, t), Prod.le_def, s.2.1, s.2.2, ht.1, ht.2, Function.comp_def, hψ]

Premises used: Prod.mk, Function.comp_def, Path.extend, And.right, And.left, Subtype.val, Prod.le_def, Subtype.property