Analysis I, Section 10.4: Inverse functions and derivatives

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

The inverse function theorem.

open Chapter9namespace Chapter10

Lemma 10.4.1

theorem _root_.HasDerivWithinAt.of_inverse {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ}
  (hfXY: ∀ x ∈ X, f x ∈ Y) (hgf: ∀ x ∈ X, g (f x) = x)
  {x₀ y₀ f'x₀ g'y₀: ℝ} (hx₀: x₀ ∈ X) (hfx₀: f x₀ = y₀)
  (hcluster: ClusterPt x₀ (.principal (X \ {x₀})))
  (hf: HasDerivWithinAt f f'x₀ X x₀) (hg: HasDerivWithinAt g g'y₀ Y y₀) :
  g'y₀ * f'x₀ = 1 := byX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝf'x₀:ℝg'y₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'y₀ Y y₀⊢ g'y₀ * f'x₀ = 1
  -- This proof is written to follow the structure of the original text.
  have h1 : HasDerivWithinAt id (g'y₀ * f'x₀) X x₀ := byX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝf'x₀:ℝg'y₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'y₀ Y y₀⊢ g'y₀ * f'x₀ = 1
    apply (hf.of_comp hfx₀ hfXY _).congr _ (hgf _ hx₀).symmX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝf'x₀:ℝg'y₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'y₀ Y y₀⊢ HasDerivWithinAt g g'y₀ Y y₀X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝf'x₀:ℝg'y₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'y₀ Y y₀⊢ ∀ x ∈ X, id x = (g ∘ f) x <;>X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝf'x₀:ℝg'y₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'y₀ Y y₀⊢ HasDerivWithinAt g g'y₀ Y y₀X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝf'x₀:ℝg'y₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'y₀ Y y₀⊢ ∀ x ∈ X, id x = (g ∘ f) x grindAll goals completed! 🐙
  observe h2 : HasDerivWithinAt id 1 X x₀X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝf'x₀:ℝg'y₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:HasDerivWithinAt g g'y₀ Y y₀h1:HasDerivWithinAt id (_fvar.2401 * _fvar.2400) _fvar.2392 _fvar.2398 := ?_mvar.3643h2:HasDerivWithinAt id 1 X x₀⊢ g'y₀ * f'x₀ = 1
  solve_by_elim [derivative_unique]All goals completed! 🐙

theorem _root_.HasDerivWithinAt.of_inverse' {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ}
  (hfXY: ∀ x ∈ X, f x ∈ Y) (hgf: ∀ x ∈ X, g (f x) = x)
  {x₀ y₀ f'x₀ g'y₀: ℝ} (hx₀: x₀ ∈ X) (hfx₀: f x₀ = y₀)
  (hcluster: ClusterPt x₀ (.principal (X \ {x₀})))
  (hf: HasDerivWithinAt f f'x₀ X x₀) (hg: HasDerivWithinAt g g'y₀ Y y₀) :
  g'y₀ = 1/f'x₀ :=
    eq_one_div_of_mul_eq_one_left (hf.of_inverse hfXY hgf hx₀ hfx₀ hcluster hg)

theorem _root_.HasDerivWithinAt.of_inverse_of_zero_deriv {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ}
  (hfXY: ∀ x ∈ X, f x ∈ Y) (hgf: ∀ x ∈ X, g (f x) = x)
  {x₀ y₀: ℝ} (hx₀: x₀ ∈ X) (hfx₀: f x₀ = y₀)
  (hcluster: ClusterPt x₀ (.principal (X \ {x₀})))
  (hf: HasDerivWithinAt f 0 X x₀) :
  ¬ DifferentiableWithinAt ℝ g Y y₀ := byX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀⊢ ¬DifferentiableWithinAt ℝ g Y y₀
  by_contra thisX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀this:DifferentiableWithinAt ℝ g Y y₀⊢ False; rw [DifferentiableWithinAt.iff] at thisX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀this:∃ L, HasDerivWithinAt g L Y y₀⊢ False; choose _ hg using thisX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:HasDerivWithinAt g L✝ Y y₀⊢ False
  apply hf.of_inverse at hgX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:L✝ * 0 = 1⊢ FalsehfXYX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:HasDerivWithinAt g L✝ Y y₀⊢ ∀ x ∈ X, f x ∈ YhgfX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:HasDerivWithinAt g L✝ Y y₀⊢ ∀ x ∈ X, g (f x) = xhx₀X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:HasDerivWithinAt g L✝ Y y₀⊢ x₀ ∈ Xhfx₀X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:HasDerivWithinAt g L✝ Y y₀⊢ f x₀ = y₀hclusterX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:HasDerivWithinAt g L✝ Y y₀⊢ ClusterPt x₀ (Filter.principal (X \ {x₀})) <;>X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:L✝ * 0 = 1⊢ FalsehfXYX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:HasDerivWithinAt g L✝ Y y₀⊢ ∀ x ∈ X, f x ∈ YhgfX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:HasDerivWithinAt g L✝ Y y₀⊢ ∀ x ∈ X, g (f x) = xhx₀X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:HasDerivWithinAt g L✝ Y y₀⊢ x₀ ∈ Xhfx₀X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:HasDerivWithinAt g L✝ Y y₀⊢ f x₀ = y₀hclusterX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ Yhgf:∀ x ∈ X, g (f x) = xx₀:ℝy₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f 0 X x₀L✝:ℝhg:HasDerivWithinAt g L✝ Y y₀⊢ ClusterPt x₀ (Filter.principal (X \ {x₀})) grindAll goals completed! 🐙

declaration uses 'sorry'example : ¬ DifferentiableWithinAt ℝ (fun x:ℝ ↦ x^(1/3:ℝ)) (.Ici 0) 0 := by⊢ ¬DifferentiableWithinAt ℝ (fun x => x ^ (1 / 3)) (Set.Ici 0) 0 sorryAll goals completed! 🐙

Theorem 10.4.2 (Inverse function theorem)

theorem declaration uses 'sorry'inverse_function_theorem {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ}
  (hfXY: ∀ x ∈ X, f x ∈ Y) (hgYX: ∀ y ∈ Y, g y ∈ X)
  (hgf: ∀ x ∈ X, g (f x) = x) (hfg: ∀ y ∈ Y, f (g y) = y)
  {x₀ y₀ f'x₀: ℝ} (hx₀: x₀ ∈ X) (hfx₀: f x₀ = y₀) (hne : f'x₀ ≠ 0)
  (hcluster: ClusterPt x₀ (.principal (X \ {x₀})))
  (hf: HasDerivWithinAt f f'x₀ X x₀) (hg: ContinuousWithinAt g Y y₀) :
    HasDerivWithinAt g (1/f'x₀) Y y₀ := byX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀⊢ HasDerivWithinAt g (1 / f'x₀) Y y₀
    -- This proof is written to follow the structure of the original text.
    have had : AdherentPt y₀ (Y \ {y₀}) := byX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀⊢ HasDerivWithinAt g (1 / f'x₀) Y y₀
      simp [←AdherentPt_def, limit_of_AdherentPt] at *X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:¬f'x₀ = 0hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀hcluster:∃ a, (∀ (n : ℕ), a n ∈ X ∧ ¬a n = x₀) ∧ Filter.Tendsto a Filter.atTop (nhds x₀)⊢ ∃ a, (∀ (n : ℕ), a n ∈ Y ∧ ¬a n = y₀) ∧ Filter.Tendsto a Filter.atTop (nhds y₀)
      choose x hx hconv using hclusterX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:¬f'x₀ = 0hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ X ∧ ¬x n = x₀hconv:Filter.Tendsto x Filter.atTop (nhds x₀)⊢ ∃ a, (∀ (n : ℕ), a n ∈ Y ∧ ¬a n = y₀) ∧ Filter.Tendsto a Filter.atTop (nhds y₀); use f ∘ xhX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:¬f'x₀ = 0hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ X ∧ ¬x n = x₀hconv:Filter.Tendsto x Filter.atTop (nhds x₀)⊢ (∀ (n : ℕ), (f ∘ x) n ∈ Y ∧ ¬(f ∘ x) n = y₀) ∧ Filter.Tendsto (f ∘ x) Filter.atTop (nhds y₀)
      split_andsh.refine_1X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:¬f'x₀ = 0hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ X ∧ ¬x n = x₀hconv:Filter.Tendsto x Filter.atTop (nhds x₀)⊢ ∀ (n : ℕ), (f ∘ x) n ∈ Y ∧ ¬(f ∘ x) n = y₀h.refine_2X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:¬f'x₀ = 0hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ X ∧ ¬x n = x₀hconv:Filter.Tendsto x Filter.atTop (nhds x₀)⊢ Filter.Tendsto (f ∘ x) Filter.atTop (nhds y₀); grindh.refine_2X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:¬f'x₀ = 0hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ X ∧ ¬x n = x₀hconv:Filter.Tendsto x Filter.atTop (nhds x₀)⊢ Filter.Tendsto (f ∘ x) Filter.atTop (nhds y₀)
      rw [←hfx₀]h.refine_2X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:¬f'x₀ = 0hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ X ∧ ¬x n = x₀hconv:Filter.Tendsto x Filter.atTop (nhds x₀)⊢ Filter.Tendsto (f ∘ x) Filter.atTop (nhds (f x₀))
      apply hconv.comp_of_continuous hx₀ _ (fun n ↦ (hx n).1)X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:¬f'x₀ = 0hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀x:ℕ → ℝhx:∀ (n : ℕ), x n ∈ X ∧ ¬x n = x₀hconv:Filter.Tendsto x Filter.atTop (nhds x₀)⊢ ContinuousWithinAt f X x₀
      exact ContinuousWithinAt.of_differentiableWithinAt (DifferentiableWithinAt.of_hasDeriv hf)All goals completed! 🐙
    rw [HasDerivWithinAt.iff, ←Convergesto.iff, Convergesto.iff_conv _ _ had]X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀had:AdherentPt _fvar.77603 (_fvar.77595 \ {_fvar.77603}) := ?_mvar.77703⊢ ∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ Y \ {y₀}) →
    Filter.Tendsto a Filter.atTop (nhds y₀) →
      Filter.Tendsto (fun n => (g (a n) - g y₀) / (a n - y₀)) Filter.atTop (nhds (1 / f'x₀))
    intro y hy hconvX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀had:AdherentPt _fvar.77603 (_fvar.77595 \ {_fvar.77603}) := ?_mvar.77703y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}hconv:Filter.Tendsto y Filter.atTop (nhds y₀)⊢ Filter.Tendsto (fun n => (g (y n) - g y₀) / (y n - y₀)) Filter.atTop (nhds (1 / f'x₀))
    set x : ℕ → ℝ := fun n ↦ g (y n)X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀had:AdherentPt _fvar.77603 (_fvar.77595 \ {_fvar.77603}) := ?_mvar.77703y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}hconv:Filter.Tendsto y Filter.atTop (nhds y₀)x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.87026 n)⊢ Filter.Tendsto (fun n => (g (y n) - g y₀) / (y n - y₀)) Filter.atTop (nhds (1 / f'x₀))
    have hy' : ∀ n, y n ∈ Y := byX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀⊢ HasDerivWithinAt g (1 / f'x₀) Y y₀ aesopAll goals completed! 🐙
    have hy₀: y₀ ∈ Y := byX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀⊢ HasDerivWithinAt g (1 / f'x₀) Y y₀ aesopAll goals completed! 🐙
    have hx : ∀ n, x n ∈ X \ {x₀}:= byX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀⊢ HasDerivWithinAt g (1 / f'x₀) Y y₀
      sorryAll goals completed! 🐙
    replace hconv := hconv.comp_of_continuous hy₀ hg hy'X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀had:AdherentPt _fvar.77603 (_fvar.77595 \ {_fvar.77603}) := ?_mvar.77703y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.87026 n)hy':∀ (n : ℕ), @_fvar.87026 n ∈ _fvar.77595 := ?_mvar.87373hy₀:_fvar.77603 ∈ _fvar.77595 := ?_mvar.91738hx:∀ (n : ℕ), @_fvar.87044 n ∈ _fvar.77594 \ {_fvar.77602} := ?_mvar.96428hconv:?_mvar.96439 := Filter.Tendsto.comp_of_continuous _fvar.91739 _fvar.77610 _fvar.87374 _fvar.87033⊢ Filter.Tendsto (fun n => (g (y n) - g y₀) / (y n - y₀)) Filter.atTop (nhds (1 / f'x₀))
    have had' : AdherentPt x₀ (X \ {x₀}) := byX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀⊢ HasDerivWithinAt g (1 / f'x₀) Y y₀ rwa [AdherentPt_def]X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀had:AdherentPt _fvar.77603 (_fvar.77595 \ {_fvar.77603}) := ?_mvar.77703y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.87026 n)hy':∀ (n : ℕ), @_fvar.87026 n ∈ _fvar.77595 := ?_mvar.87373hy₀:_fvar.77603 ∈ _fvar.77595 := ?_mvar.91738hx:∀ (n : ℕ), @_fvar.87044 n ∈ _fvar.77594 \ {_fvar.77602} := ?_mvar.96428hconv:?_mvar.96439 := Filter.Tendsto.comp_of_continuous _fvar.91739 _fvar.77610 _fvar.87374 _fvar.87033⊢ ClusterPt x₀ (Filter.principal (X \ {x₀}))
    have hgy₀ : g y₀ = x₀ := byX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:HasDerivWithinAt f f'x₀ X x₀hg:ContinuousWithinAt g Y y₀⊢ HasDerivWithinAt g (1 / f'x₀) Y y₀ aesopAll goals completed! 🐙
    rw [HasDerivWithinAt.iff, ←Convergesto.iff, Convergesto.iff_conv _ _ had'] at hfX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ X \ {x₀}) →
    Filter.Tendsto a Filter.atTop (nhds x₀) →
      Filter.Tendsto (fun n => (f (a n) - f x₀) / (a n - x₀)) Filter.atTop (nhds f'x₀)hg:ContinuousWithinAt g Y y₀had:AdherentPt y₀ (Y \ {y₀})y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.102591 n)hy':∀ (n : ℕ), y n ∈ Yhy₀:y₀ ∈ Yhx:∀ (n : ℕ), x n ∈ X \ {x₀}hconv:Filter.Tendsto (fun n => g (y n)) Filter.atTop (nhds (g y₀))had':AdherentPt x₀ (X \ {x₀})hgy₀:g y₀ = x₀⊢ Filter.Tendsto (fun n => (g (y n) - g y₀) / (y n - y₀)) Filter.atTop (nhds (1 / f'x₀))
    convert (hf _ hx _).inv₀ _ using 2 with nh.e'_3.hX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ X \ {x₀}) →
    Filter.Tendsto a Filter.atTop (nhds x₀) →
      Filter.Tendsto (fun n => (f (a n) - f x₀) / (a n - x₀)) Filter.atTop (nhds f'x₀)hg:ContinuousWithinAt g Y y₀had:AdherentPt y₀ (Y \ {y₀})y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.102591 n)hy':∀ (n : ℕ), y n ∈ Yhy₀:y₀ ∈ Yhx:∀ (n : ℕ), x n ∈ X \ {x₀}hconv:Filter.Tendsto (fun n => g (y n)) Filter.atTop (nhds (g y₀))had':AdherentPt x₀ (X \ {x₀})hgy₀:g y₀ = x₀n:ℕ⊢ (g (y n) - g y₀) / (y n - y₀) = ((f (x n) - f x₀) / (x n - x₀))⁻¹h.e'_5.h.e'_3X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ X \ {x₀}) →
    Filter.Tendsto a Filter.atTop (nhds x₀) →
      Filter.Tendsto (fun n => (f (a n) - f x₀) / (a n - x₀)) Filter.atTop (nhds f'x₀)hg:ContinuousWithinAt g Y y₀had:AdherentPt y₀ (Y \ {y₀})y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.102591 n)hy':∀ (n : ℕ), y n ∈ Yhy₀:y₀ ∈ Yhx:∀ (n : ℕ), x n ∈ X \ {x₀}hconv:Filter.Tendsto (fun n => g (y n)) Filter.atTop (nhds (g y₀))had':AdherentPt x₀ (X \ {x₀})hgy₀:g y₀ = x₀⊢ 1 / f'x₀ = f'x₀⁻¹convert_1X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ X \ {x₀}) →
    Filter.Tendsto a Filter.atTop (nhds x₀) →
      Filter.Tendsto (fun n => (f (a n) - f x₀) / (a n - x₀)) Filter.atTop (nhds f'x₀)hg:ContinuousWithinAt g Y y₀had:AdherentPt y₀ (Y \ {y₀})y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.102591 n)hy':∀ (n : ℕ), y n ∈ Yhy₀:y₀ ∈ Yhx:∀ (n : ℕ), x n ∈ X \ {x₀}hconv:Filter.Tendsto (fun n => g (y n)) Filter.atTop (nhds (g y₀))had':AdherentPt x₀ (X \ {x₀})hgy₀:g y₀ = x₀⊢ Filter.Tendsto x Filter.atTop (nhds x₀)convert_2X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ X \ {x₀}) →
    Filter.Tendsto a Filter.atTop (nhds x₀) →
      Filter.Tendsto (fun n => (f (a n) - f x₀) / (a n - x₀)) Filter.atTop (nhds f'x₀)hg:ContinuousWithinAt g Y y₀had:AdherentPt y₀ (Y \ {y₀})y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.102591 n)hy':∀ (n : ℕ), y n ∈ Yhy₀:y₀ ∈ Yhx:∀ (n : ℕ), x n ∈ X \ {x₀}hconv:Filter.Tendsto (fun n => g (y n)) Filter.atTop (nhds (g y₀))had':AdherentPt x₀ (X \ {x₀})hgy₀:g y₀ = x₀⊢ f'x₀ ≠ 0 <;>h.e'_3.hX:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ X \ {x₀}) →
    Filter.Tendsto a Filter.atTop (nhds x₀) →
      Filter.Tendsto (fun n => (f (a n) - f x₀) / (a n - x₀)) Filter.atTop (nhds f'x₀)hg:ContinuousWithinAt g Y y₀had:AdherentPt y₀ (Y \ {y₀})y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.102591 n)hy':∀ (n : ℕ), y n ∈ Yhy₀:y₀ ∈ Yhx:∀ (n : ℕ), x n ∈ X \ {x₀}hconv:Filter.Tendsto (fun n => g (y n)) Filter.atTop (nhds (g y₀))had':AdherentPt x₀ (X \ {x₀})hgy₀:g y₀ = x₀n:ℕ⊢ (g (y n) - g y₀) / (y n - y₀) = ((f (x n) - f x₀) / (x n - x₀))⁻¹h.e'_5.h.e'_3X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ X \ {x₀}) →
    Filter.Tendsto a Filter.atTop (nhds x₀) →
      Filter.Tendsto (fun n => (f (a n) - f x₀) / (a n - x₀)) Filter.atTop (nhds f'x₀)hg:ContinuousWithinAt g Y y₀had:AdherentPt y₀ (Y \ {y₀})y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.102591 n)hy':∀ (n : ℕ), y n ∈ Yhy₀:y₀ ∈ Yhx:∀ (n : ℕ), x n ∈ X \ {x₀}hconv:Filter.Tendsto (fun n => g (y n)) Filter.atTop (nhds (g y₀))had':AdherentPt x₀ (X \ {x₀})hgy₀:g y₀ = x₀⊢ 1 / f'x₀ = f'x₀⁻¹convert_1X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ X \ {x₀}) →
    Filter.Tendsto a Filter.atTop (nhds x₀) →
      Filter.Tendsto (fun n => (f (a n) - f x₀) / (a n - x₀)) Filter.atTop (nhds f'x₀)hg:ContinuousWithinAt g Y y₀had:AdherentPt y₀ (Y \ {y₀})y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.102591 n)hy':∀ (n : ℕ), y n ∈ Yhy₀:y₀ ∈ Yhx:∀ (n : ℕ), x n ∈ X \ {x₀}hconv:Filter.Tendsto (fun n => g (y n)) Filter.atTop (nhds (g y₀))had':AdherentPt x₀ (X \ {x₀})hgy₀:g y₀ = x₀⊢ Filter.Tendsto x Filter.atTop (nhds x₀)convert_2X:Set ℝY:Set ℝf:ℝ → ℝg:ℝ → ℝhfXY:∀ x ∈ X, f x ∈ YhgYX:∀ y ∈ Y, g y ∈ Xhgf:∀ x ∈ X, g (f x) = xhfg:∀ y ∈ Y, f (g y) = yx₀:ℝy₀:ℝf'x₀:ℝhx₀:x₀ ∈ Xhfx₀:f x₀ = y₀hne:f'x₀ ≠ 0hcluster:ClusterPt x₀ (Filter.principal (X \ {x₀}))hf:∀ (a : ℕ → ℝ),
  (∀ (n : ℕ), a n ∈ X \ {x₀}) →
    Filter.Tendsto a Filter.atTop (nhds x₀) →
      Filter.Tendsto (fun n => (f (a n) - f x₀) / (a n - x₀)) Filter.atTop (nhds f'x₀)hg:ContinuousWithinAt g Y y₀had:AdherentPt y₀ (Y \ {y₀})y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => @_fvar.77597 (@_fvar.102591 n)hy':∀ (n : ℕ), y n ∈ Yhy₀:y₀ ∈ Yhx:∀ (n : ℕ), x n ∈ X \ {x₀}hconv:Filter.Tendsto (fun n => g (y n)) Filter.atTop (nhds (g y₀))had':AdherentPt x₀ (X \ {x₀})hgy₀:g y₀ = x₀⊢ f'x₀ ≠ 0 grindAll goals completed! 🐙

Exercise 10.4.1(a)

declaration uses 'sorry'example {n:ℕ} (hn: n > 0) : ContinuousOn (fun x:ℝ ↦ x^(1/n:ℝ)) (.Ici 0) := byn:ℕhn:n > 0⊢ ContinuousOn (fun x => x ^ (1 / ↑n)) (Set.Ici 0) sorryAll goals completed! 🐙

Exercise 10.4.1(b)

declaration uses 'sorry'example {n:ℕ} (hn: n > 0) {x:ℝ} (hx: x ∈ Set.Ici 0) : HasDerivWithinAt (fun x:ℝ ↦ x^(1/n:ℝ))
  ((n:ℝ)⁻¹ * x^((n:ℝ)⁻¹-1)) (.Ici 0) x := byn:ℕhn:n > 0x:ℝhx:x ∈ Set.Ici 0⊢ HasDerivWithinAt (fun x => x ^ (1 / ↑n)) ((↑n)⁻¹ * x ^ ((↑n)⁻¹ - 1)) (Set.Ici 0) x sorryAll goals completed! 🐙

Exercise 10.4.2(a)

declaration uses 'sorry'example (q:ℚ) {x:ℝ} (hx: x ∈ Set.Ici 0) :
  HasDerivWithinAt (fun x:ℝ ↦ x^(q:ℝ)) (q * x^(q-1:ℝ)) (.Ici 0) x := byq:ℚx:ℝhx:x ∈ Set.Ici 0⊢ HasDerivWithinAt (fun x => x ^ ↑q) (↑q * x ^ (↑q - 1)) (Set.Ici 0) x
  sorryAll goals completed! 🐙

Exercise 10.4.2(b)

declaration uses 'sorry'example (q:ℚ) : (nhdsWithin 1 (.Ici 0 \ {1})).Tendsto (fun x:ℝ ↦ (x^(q:ℝ)-1)/(x-1)) (nhds q) := byq:ℚ⊢ Filter.Tendsto (fun x => (x ^ ↑q - 1) / (x - 1)) (nhdsWithin 1 (Set.Ici 0 \ {1})) (nhds ↑q)
  sorryAll goals completed! 🐙

Exercise 10.4.3(a)

declaration uses 'sorry'example (α:ℝ) : (nhdsWithin 1 (.Ici 0 \ {1})).Tendsto (fun x:ℝ ↦ (x^α-1^α)/(x-1)) (nhds α) := byα:ℝ⊢ Filter.Tendsto (fun x => (x ^ α - 1 ^ α) / (x - 1)) (nhdsWithin 1 (Set.Ici 0 \ {1})) (nhds α)
  sorryAll goals completed! 🐙

Exercise 10.4.2(b)

declaration uses 'sorry'example (α:ℝ) {x:ℝ} (hx: x ∈ Set.Ici 0) : HasDerivWithinAt (fun x:ℝ ↦ x^α) (α * x^(α-1)) (.Ici 0) x := byα:ℝx:ℝhx:x ∈ Set.Ici 0⊢ HasDerivWithinAt (fun x => x ^ α) (α * x ^ (α - 1)) (Set.Ici 0) x
  sorryAll goals completed! 🐙

end Chapter10