-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare (goal)
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_1 b c d : E
γ₁ : Path a_1 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 : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a →
      ∀ (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, b_1) : E)
hω :
  ∀ (a : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a, b_1) ∉ s →
            HasFDerivWithinAt ω (dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b_1))) t
              ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b_1))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ (a : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a →
      ∀ (b_1 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b_1 →
          (a, b_1) ∉ s →
            ∀ u ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b_1)),
              ∀ v ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b_1)),
                Eq.{u_3 + 1} (α := F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b_1)) : (a : E) → E →L[ℝ] F) u : E →L[ℝ] F) :
                        (a : E) → F)
                      v :
                    F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, 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 b_1 : (↑I : Type)), ψ ((↑a : ℝ), (↑b_1 : ℝ)) = (φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, 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)
a : ℝ × ℝ
ha : Membership.mem (γ := Set (ℝ × ℝ)) (Icc 0 1) a
this : HasDerivWithinAt (F := ℝ × ℝ) (fun (x : ℝ) ↦ (x, a.2)) (1, 0) I a.1
⊢ (fderivWithin ℝ ψ (Icc 0 1) a : (a : ℝ × ℝ) → E) (1, 0) = derivWithin (ψ ∘ fun (x : ℝ) ↦ (x, a.2)) I a.1
have e_a : DifferentiableWithinAt ℝ ψ (Icc 0 1) (a.1, a.2)
Tactic: refine DifferentiableWithinAt.hasFDerivWithinAt ?_ |>.comp_hasDerivWithinAt _ this ?_
      |>.derivWithin ?_ |>.symm