-- 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_1 b_1 c d : E
γ₁ : Path a_1 b_1
γ₂ : 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 : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b →
          Membership.mem (α := E) t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b) : E)
hω :
  ∀ (a : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a →
      ∀ (b : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b →
          (a, b) ∉ s →
            HasFDerivWithinAt ω (dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b))) t
              ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b))
hωc : ContinuousOn ω (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
hdω_symm :
  ∀ (a : (↑I : Type)),
    Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) a →
      ∀ (b : (↑I : Type)),
        Membership.mem (γ := Set (↑I : Type)) (Ioo 0 1) b →
          (a, b) ∉ s →
            ∀ u ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)),
              ∀ v ∈ tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)),
                Eq.{u_3 + 1} (α := F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)) : (a : E) → E →L[ℝ] F) u : E →L[ℝ] F) :
                        (a : E) → F)
                      v :
                    F)
                  ((((dω ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)) : (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_1 : 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 : (↑I : Type)), ψ ((↑a : ℝ), (↑b : ℝ)) = (φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)
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'_1 : 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
u v : ℝ × ℝ
a b : { x : ℝ // x ∈ I }
hU : ((↑a : ℝ), (↑b : ℝ)) ∈ U
hs' : ((↑a : ℝ), (↑b : ℝ)) ∉ s'
⊢ ∀ (u : ℝ × ℝ),
    Membership.mem (α := E) (tangentConeAt ℝ t ((φ : (a : (↑I : Type) × (↑I : Type)) → E) (a, b)))
      ((dψ ((↑a : ℝ), (↑b : ℝ)) : (a : ℝ × ℝ) → E) u : E)

Tactic:
have hdψ_mem (u) : dψ (a, b) u ∈ tangentConeAt ℝ t (φ (a, b)) := by
      refine tangentConeAt_mono hψUt.image_subset ?_
      rw [← hψφ]
      refine (hdψ _ hU).hasFDerivWithinAt.mapsTo_tangent_cone ?_
      simp [tangentConeAt_of_mem_nhds (hUopen.mem_nhds hU)]