∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → E} {x₀ : E} (t₀ ε : ℝ)
  (motive : (∃ α, α t₀ = x₀ ∧ ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t) → Prop)
  (x : ∃ α, α t₀ = x₀ ∧ ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t),
  (∀ (α : ℝ → E) (hα1 : α t₀ = x₀) (hα2 : ∀ t ∈ Set.Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t), motive ⋯) →
    motive x