-- 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)
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)
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
hcontdiff₁ :
  let ψ : ℝ × ℝ → 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;
  ContDiffOn ℝ 2 ψ (Icc 0 1)
⊢ let ψ : ℝ × ℝ → 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;
  ψ = 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

Tactic:
set ψ : ℝ × ℝ → E := fun xy : ℝ × ℝ ↦ Set.IccExtend zero_le_one (φ.extend xy.1) xy.2 with hψ

Premises used: Prod.fst, zero_le_one, ContinuousMap.Homotopy.extend, Set.IccExtend, Prod.snd, DFunLike.coe