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 (g'y₀ * f'x₀) X x₀ := 
  HasDerivWithinAt.congr (HasDerivWithinAt.of_comp hfx₀ hfXY hf (HasDerivWithinAt.of_inverse._proof_2 hg))
    (HasDerivWithinAt.of_inverse._proof_3 hgf) (Eq.symm (hgf x₀ hx₀))h2: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 y₀ (Y \ {y₀}) := 
  Eq.mpr
    (id
      (Eq.trans (inverse_function_theorem._simp_2 (Y \ {y₀}) y₀)
        (congrArg Exists
          (funext fun a =>
            congrFun'
              (congrArg And
                (forall_congr fun n =>
                  Eq.trans (Set.mem_diff._simp_1 (a n))
                    (congrArg (And (a n ∈ Y)) (congrArg Not Set.mem_singleton_iff._simp_1))))
              (Filter.Tendsto a Filter.atTop (nhds y₀))))))
    ((fun x x_1 =>
        Exists.intro (f ∘ x)
          ⟨inverse_function_theorem._proof_2 hfXY hgf hx₀ hfx₀ x x_1.left,
            Eq.mpr (id (congrArg (fun _a => Filter.Tendsto (f ∘ x) Filter.atTop (nhds _a)) (Eq.symm hfx₀)))
              (Filter.Tendsto.comp_of_continuous hx₀
                (ContinuousWithinAt.of_differentiableWithinAt (DifferentiableWithinAt.of_hasDeriv hf))
                (fun n => (x_1.left n).left) x_1.right)⟩)
      (Classical.choose
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster))
      (Classical.choose_spec
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster)))⊢ ∀ (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 hyX: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 y₀ (Y \ {y₀}) := 
  Eq.mpr
    (id
      (Eq.trans (inverse_function_theorem._simp_2 (Y \ {y₀}) y₀)
        (congrArg Exists
          (funext fun a =>
            congrFun'
              (congrArg And
                (forall_congr fun n =>
                  Eq.trans (Set.mem_diff._simp_1 (a n))
                    (congrArg (And (a n ∈ Y)) (congrArg Not Set.mem_singleton_iff._simp_1))))
              (Filter.Tendsto a Filter.atTop (nhds y₀))))))
    ((fun x x_1 =>
        Exists.intro (f ∘ x)
          ⟨inverse_function_theorem._proof_2 hfXY hgf hx₀ hfx₀ x x_1.left,
            Eq.mpr (id (congrArg (fun _a => Filter.Tendsto (f ∘ x) Filter.atTop (nhds _a)) (Eq.symm hfx₀)))
              (Filter.Tendsto.comp_of_continuous hx₀
                (ContinuousWithinAt.of_differentiableWithinAt (DifferentiableWithinAt.of_hasDeriv hf))
                (fun n => (x_1.left n).left) x_1.right)⟩)
      (Classical.choose
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster))
      (Classical.choose_spec
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster)))y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}⊢ 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₀)) 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 y₀ (Y \ {y₀}) := 
  Eq.mpr
    (id
      (Eq.trans (inverse_function_theorem._simp_2 (Y \ {y₀}) y₀)
        (congrArg Exists
          (funext fun a =>
            congrFun'
              (congrArg And
                (forall_congr fun n =>
                  Eq.trans (Set.mem_diff._simp_1 (a n))
                    (congrArg (And (a n ∈ Y)) (congrArg Not Set.mem_singleton_iff._simp_1))))
              (Filter.Tendsto a Filter.atTop (nhds y₀))))))
    ((fun x x_1 =>
        Exists.intro (f ∘ x)
          ⟨inverse_function_theorem._proof_2 hfXY hgf hx₀ hfx₀ x x_1.left,
            Eq.mpr (id (congrArg (fun _a => Filter.Tendsto (f ∘ x) Filter.atTop (nhds _a)) (Eq.symm hfx₀)))
              (Filter.Tendsto.comp_of_continuous hx₀
                (ContinuousWithinAt.of_differentiableWithinAt (DifferentiableWithinAt.of_hasDeriv hf))
                (fun n => (x_1.left n).left) x_1.right)⟩)
      (Classical.choose
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster))
      (Classical.choose_spec
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster)))y:ℕ → ℝ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 y₀ (Y \ {y₀}) := 
  Eq.mpr
    (id
      (Eq.trans (inverse_function_theorem._simp_2 (Y \ {y₀}) y₀)
        (congrArg Exists
          (funext fun a =>
            congrFun'
              (congrArg And
                (forall_congr fun n =>
                  Eq.trans (Set.mem_diff._simp_1 (a n))
                    (congrArg (And (a n ∈ Y)) (congrArg Not Set.mem_singleton_iff._simp_1))))
              (Filter.Tendsto a Filter.atTop (nhds y₀))))))
    ((fun x x_1 =>
        Exists.intro (f ∘ x)
          ⟨inverse_function_theorem._proof_2 hfXY hgf hx₀ hfx₀ x x_1.left,
            Eq.mpr (id (congrArg (fun _a => Filter.Tendsto (f ∘ x) Filter.atTop (nhds _a)) (Eq.symm hfx₀)))
              (Filter.Tendsto.comp_of_continuous hx₀
                (ContinuousWithinAt.of_differentiableWithinAt (DifferentiableWithinAt.of_hasDeriv hf))
                (fun n => (x_1.left n).left) x_1.right)⟩)
      (Classical.choose
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster))
      (Classical.choose_spec
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster)))y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}hconv:Filter.Tendsto y Filter.atTop (nhds y₀)x:ℕ → ℝ := fun n => g (y 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 y₀ (Y \ {y₀}) := 
  Eq.mpr
    (id
      (Eq.trans (inverse_function_theorem._simp_2 (Y \ {y₀}) y₀)
        (congrArg Exists
          (funext fun a =>
            congrFun'
              (congrArg And
                (forall_congr fun n =>
                  Eq.trans (Set.mem_diff._simp_1 (a n))
                    (congrArg (And (a n ∈ Y)) (congrArg Not Set.mem_singleton_iff._simp_1))))
              (Filter.Tendsto a Filter.atTop (nhds y₀))))))
    ((fun x x_1 =>
        Exists.intro (f ∘ x)
          ⟨inverse_function_theorem._proof_2 hfXY hgf hx₀ hfx₀ x x_1.left,
            Eq.mpr (id (congrArg (fun _a => Filter.Tendsto (f ∘ x) Filter.atTop (nhds _a)) (Eq.symm hfx₀)))
              (Filter.Tendsto.comp_of_continuous hx₀
                (ContinuousWithinAt.of_differentiableWithinAt (DifferentiableWithinAt.of_hasDeriv hf))
                (fun n => (x_1.left n).left) x_1.right)⟩)
      (Classical.choose
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster))
      (Classical.choose_spec
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster)))y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => g (y n)hy':∀ (n : ℕ), y n ∈ Y := 
  fun n =>
    Eq.ndrec (motive := fun {y₀} =>
      ContinuousWithinAt g Y y₀ →
        AdherentPt y₀ (Y \ {y₀}) → (∀ (n : ℕ), y n ∈ Y \ {y₀}) → Filter.Tendsto y Filter.atTop (nhds y₀) → y n ∈ Y)
      (fun hg had hy hconv =>
        of_eq_true
          ((fun n =>
              eq_true
                (id
                    (Eq.mp
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (y n))
                          (congrArg (And (y n ∈ Y)) (congrArg Not Set.mem_singleton_iff._simp_1)))
                      hy)
                    n).1)
            n))
      hfx₀ hg had hy _fvar.31797hy₀:y₀ ∈ Y := 
  Eq.ndrec (motive := fun {y₀} =>
    ContinuousWithinAt g Y y₀ →
      AdherentPt y₀ (Y \ {y₀}) → (∀ (n : ℕ), y n ∈ Y \ {y₀}) → Filter.Tendsto y Filter.atTop (nhds y₀) → y₀ ∈ Y)
    (fun hg had hy hconv => of_eq_true ((fun x a => eq_true (hfXY x a)) x₀ hx₀)) hfx₀ hg had hy _fvar.31797hx:∀ (n : ℕ), x n ∈ X \ {x₀} := sorryhconv:Filter.Tendsto (fun n => g (y n)) Filter.atTop (nhds (g y₀)) := Filter.Tendsto.comp_of_continuous hy₀ hg hy' _fvar.31797⊢ 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 y₀ (Y \ {y₀}) := 
  Eq.mpr
    (id
      (Eq.trans (inverse_function_theorem._simp_2 (Y \ {y₀}) y₀)
        (congrArg Exists
          (funext fun a =>
            congrFun'
              (congrArg And
                (forall_congr fun n =>
                  Eq.trans (Set.mem_diff._simp_1 (a n))
                    (congrArg (And (a n ∈ Y)) (congrArg Not Set.mem_singleton_iff._simp_1))))
              (Filter.Tendsto a Filter.atTop (nhds y₀))))))
    ((fun x x_1 =>
        Exists.intro (f ∘ x)
          ⟨inverse_function_theorem._proof_2 hfXY hgf hx₀ hfx₀ x x_1.left,
            Eq.mpr (id (congrArg (fun _a => Filter.Tendsto (f ∘ x) Filter.atTop (nhds _a)) (Eq.symm hfx₀)))
              (Filter.Tendsto.comp_of_continuous hx₀
                (ContinuousWithinAt.of_differentiableWithinAt (DifferentiableWithinAt.of_hasDeriv hf))
                (fun n => (x_1.left n).left) x_1.right)⟩)
      (Classical.choose
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster))
      (Classical.choose_spec
        (Eq.mp
          (Eq.trans (inverse_function_theorem._simp_1 x₀ (X \ {x₀}))
            (Eq.trans (inverse_function_theorem._simp_2 (X \ {x₀}) x₀)
              (congrArg Exists
                (funext fun a =>
                  congrFun'
                    (congrArg And
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (a n))
                          (congrArg (And (a n ∈ X)) (congrArg Not Set.mem_singleton_iff._simp_1))))
                    (Filter.Tendsto a Filter.atTop (nhds x₀))))))
          hcluster)))y:ℕ → ℝhy:∀ (n : ℕ), y n ∈ Y \ {y₀}x:ℕ → ℝ := fun n => g (y n)hy':∀ (n : ℕ), y n ∈ Y := 
  fun n =>
    Eq.ndrec (motive := fun {y₀} =>
      ContinuousWithinAt g Y y₀ →
        AdherentPt y₀ (Y \ {y₀}) → (∀ (n : ℕ), y n ∈ Y \ {y₀}) → Filter.Tendsto y Filter.atTop (nhds y₀) → y n ∈ Y)
      (fun hg had hy hconv =>
        of_eq_true
          ((fun n =>
              eq_true
                (id
                    (Eq.mp
                      (forall_congr fun n =>
                        Eq.trans (Set.mem_diff._simp_1 (y n))
                          (congrArg (And (y n ∈ Y)) (congrArg Not Set.mem_singleton_iff._simp_1)))
                      hy)
                    n).1)
            n))
      hfx₀ hg had hy _fvar.31797hy₀:y₀ ∈ Y := 
  Eq.ndrec (motive := fun {y₀} =>
    ContinuousWithinAt g Y y₀ →
      AdherentPt y₀ (Y \ {y₀}) → (∀ (n : ℕ), y n ∈ Y \ {y₀}) → Filter.Tendsto y Filter.atTop (nhds y₀) → y₀ ∈ Y)
    (fun hg had hy hconv => of_eq_true ((fun x a => eq_true (hfXY x a)) x₀ hx₀)) hfx₀ hg had hy _fvar.31797hx:∀ (n : ℕ), x n ∈ X \ {x₀} := sorryhconv:Filter.Tendsto (fun n => g (y n)) Filter.atTop (nhds (g y₀)) := Filter.Tendsto.comp_of_continuous hy₀ hg hy' _fvar.31797⊢ 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 => g (y 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 => g (y 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 => g (y 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 => g (y 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 => g (y 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 => g (y 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 => g (y 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 => g (y 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 => g (y 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