-- 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)
⊢ ∀ (a : ℝ × ℝ),
    Membership.mem (γ := Set (ℝ × ℝ)) (Icc 0 1) a →
      f a = (ω (ψ a) : (a : E) → F) (derivWithin (ψ ∘ fun (x : ℝ) ↦ (a.1, x)) I a.2)

Tactic:
have hf : ∀ a ∈ Icc 0 1, f a = ω (ψ a) (derivWithin (ψ ∘ (a.1, ·)) I a.2) := by
    intro a ha
    simp only [f, η, dψ, ContinuousLinearMap.comp_apply]
    congr 1
    have : HasDerivWithinAt (a.1, ·) (0, 1) I a.2 :=
      .prodMk (hasDerivWithinAt_const ..) (hasDerivWithinAt_id ..)
    refine DifferentiableWithinAt.hasFDerivWithinAt ?_ |>.comp_hasDerivWithinAt _ this ?_
      |>.derivWithin ?_ |>.symm
    · exact hcontdiff.differentiableOn (by decide) _ ha
    · exact fun t ht ↦ ⟨⟨ha.1.1, ht.1⟩, ⟨ha.2.1, ht.2⟩⟩
    · exact uniqueDiffOn_Icc_zero_one _ ⟨ha.1.2, ha.2.2⟩