-- 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] ψ
hψUt : MapsTo ψ U t
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
hs' : s' = Prod.map (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) '' s
hmem_s' : ∀ (x y : (↑I : Type)), ((↑x : ℝ), (↑y : ℝ)) ∈ s' ↔ (x, y) ∈ s
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)
dη : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ →L[ℝ] F :=
  fun (a : ℝ × ℝ) ↦
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
        ((ContinuousLinearMap.compL ℝ (ℝ × ℝ) E F : (a : E →L[ℝ] F) → (ℝ × ℝ →L[ℝ] E) →L[ℝ] ℝ × ℝ →L[ℝ] F) (ω (ψ a)))
        (d2ψ a) +
      (dω (ψ a)).bilinearComp (dψ a) (dψ a)
hdη : ∀ a ∈ U \ s', HasFDerivAt η (dη a) a
hdη_symm :
  ∀ a ∈ U \ s',
    ∀ (u v : ℝ × ℝ),
      Eq (α := F) ((((dη a : (a : ℝ × ℝ) → ℝ × ℝ →L[ℝ] F) u : ℝ × ℝ →L[ℝ] F) : (a : ℝ × ℝ) → F) v : F)
        ((((dη a : (a : ℝ × ℝ) → ℝ × ℝ →L[ℝ] F) v : ℝ × ℝ →L[ℝ] F) : (a : ℝ × ℝ) → F) u : F)
f' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F :=
  fun (a : ℝ × ℝ) ↦
    ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
      ((ContinuousLinearMap.apply ℝ F : (a : ℝ × ℝ) → (ℝ × ℝ →L[ℝ] F) →L[ℝ] F) (0, 1)) (dη a)
hf' : ∀ a ∈ U \ s', HasFDerivAt f (f' a) a
g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] F :=
  fun (a : ℝ × ℝ) ↦
    -ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
        ((ContinuousLinearMap.apply ℝ F : (a : ℝ × ℝ) → (ℝ × ℝ →L[ℝ] F) →L[ℝ] F) (1, 0)) (dη a)
hg' : ∀ a ∈ U \ s', HasFDerivAt g (g' a) a
hf'g' :
  EventuallyEq.{0, u_3} (β := F) (ae (F := Measure (ℝ × ℝ)) (Measure.restrict volume (Icc 0 1)))
    (fun (a : ℝ × ℝ) ↦
      HAdd.hAdd (α := F) (β := F) ((f' a : (a : ℝ × ℝ) → F) (1, 0) : F) ((g' a : (a : ℝ × ℝ) → F) (0, 1) : F))
    0
suffices :
  Eq.{u_3 + 1} (α := F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Icc 0 1)) fun (a : ℝ × ℝ) ↦
      HAdd.hAdd (α := F) (β := F) ((f' a : (a : ℝ × ℝ) → F) (1, 0) : F) ((g' a : (a : ℝ × ℝ) → F) (0, 1) : F))
    0
⊢ (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

Tactic:
suffices ∫ a : ℝ × ℝ in Icc 0 1, f' a (1, 0) + g' a (0, 1) = 0 by
    have hηc : ContinuousOn η (Icc 0 1) := by
      refine .clm_comp (hωc.comp hψ_cont.continuousOn ?_) ?_
      · rw [← hclosure]
        refine MapsTo.closure (fun a ha ↦ ?_) hψ_cont
        lift a to I × I using ⟨Ioo_subset_Icc_self ha.1, Ioo_subset_Icc_self ha.2⟩
        simpa [ψ] using hφt a.1 ha.1 a.2 ha.2
      · exact hcontdiff.continuousOn_fderivWithin hunique (by decide)
    rwa [integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le] at this
    · exact zero_le_one
    · exact s'
    · exact hs'c
    · fun_prop
    · fun_prop
    · exact hf'
    · exact hg'
    · rw [integrableOn_congr_fun_ae hf'g']
      apply integrableOn_zero