diff --git a/Analysis/Section_10_4.lean b/Analysis/Section_10_4.lean
index 5d7c6129..fd31378c 100644
--- a/Analysis/Section_10_4.lean
+++ b/Analysis/Section_10_4.lean
@@ -61,24 +61,16 @@ theorem inverse_function_theorem {X Y: Set ℝ} {f: ℝ → ℝ} {g:ℝ → ℝ}
   (hf: HasDerivWithinAt f f'x₀ X x₀) (hg: ContinuousWithinAt g Y y₀) :
     HasDerivWithinAt g (1/f'x₀) Y y₀ := by
     -- This proof is written to follow the structure of the original text.
-    have had : AdherentPt y₀ (Y \ {y₀}) := by
-      simp [←AdherentPt_def, limit_of_AdherentPt] at *
-      choose x hx hconv using hcluster; use f ∘ x
-      split_ands; grind
-      rw [←hfx₀]
-      apply hconv.comp_of_continuous hx₀ _ (fun n ↦ (hx n).1)
-      exact ContinuousWithinAt.of_differentiableWithinAt (DifferentiableWithinAt.of_hasDeriv hf)
-    rw [HasDerivWithinAt.iff, ←Convergesto.iff, Convergesto.iff_conv _ _ had]
+    rw [HasDerivWithinAt.iff, ←Convergesto.iff, Convergesto.iff_conv _ _]
     intro y hy hconv
     set x : ℕ → ℝ := fun n ↦ g (y n)
     have hy' : ∀ n, y n ∈ Y := by aesop
     have hy₀: y₀ ∈ Y := by aesop
     have hx : ∀ n, x n ∈ X \ {x₀}:= by
       sorry
-    replace hconv := hconv.comp_of_continuous hy₀ hg hy'
-    have had' : AdherentPt x₀ (X \ {x₀}) := by rwa [AdherentPt_def]
+    replace hconv := hconv.comp_of_continuous hg hy'
     have hgy₀ : g y₀ = x₀ := by aesop
-    rw [HasDerivWithinAt.iff, ←Convergesto.iff, Convergesto.iff_conv _ _ had'] at hf
+    rw [HasDerivWithinAt.iff, ←Convergesto.iff, Convergesto.iff_conv _ _] at hf
     convert (hf _ hx _).inv₀ _ using 2 with n <;> grind
 
 /-- Exercise 10.4.1(a) -/
diff --git a/Analysis/Section_10_5.lean b/Analysis/Section_10_5.lean
index 9e772ea7..d5b2402b 100644
--- a/Analysis/Section_10_5.lean
+++ b/Analysis/Section_10_5.lean
@@ -93,7 +93,6 @@ theorem _root_.Filter.Tendsto.of_div' {a b L:ℝ} (hab: a < b) {f g f' g': ℝ 
     simp_rw [hy']; apply hderiv.comp
     solve_by_elim [tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within,
     Filter.Eventually.of_forall]
-  simp [←closure_def', closure_Ioc (show a ≠ b by grind)]; grind
 
 
 end Chapter10
diff --git a/Analysis/Section_11_9.lean b/Analysis/Section_11_9.lean
index 002ed0c1..a836c3e3 100644
--- a/Analysis/Section_11_9.lean
+++ b/Analysis/Section_11_9.lean
@@ -73,7 +73,7 @@ theorem deriv_of_integ {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: IntegrableOn
   HasDerivWithinAt (fun x => integ f (Icc a x)) (f x₀) (.Icc a b) x₀ := by
   -- This proof is written to follow the structure of the original text.
   rw [HasDerivWithinAt.iff_approx_linear]
-  simp [(ContinuousWithinAt.tfae _ f hx₀).out 0 2] at hcts
+  simp [(ContinuousWithinAt.tfae _ f x₀).out 0 2] at hcts
   peel hcts with ε hε δ hδ hconv; intro y hy hyδ
   obtain hx₀y | rfl | hx₀y := lt_trichotomy x₀ y
   . have := ((hf.join (join_Icc_Ioc hy.1 hy.2)).1.join (join_Icc_Ioc hx₀.1 (le_of_lt hx₀y))).2
diff --git a/Analysis/Section_9_3.lean b/Analysis/Section_9_3.lean
index 41160917..04720ecc 100644
--- a/Analysis/Section_9_3.lean
+++ b/Analysis/Section_9_3.lean
@@ -27,7 +27,9 @@ our functions defined on all of {lean}`ℝ` (with the understanding that they ar
 outside of the domain `X` of interest).
 -/
 
-/-- Definition 9.3.1 -/
+/-- Definition 9.3.1
+Note the books uses ≤ instead of <, but < matches mathlib's definition of neighborhood.
+-/
 abbrev Real.CloseFn (ε:ℝ) (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) : Prop :=
   ∀ x ∈ X, |f x - L| < ε
 
@@ -37,11 +39,15 @@ abbrev Real.CloseNear (ε:ℝ) (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) :
 
 namespace Chapter9
 
-/-- Example 9.3.2 -/
-example : (5:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by sorry
+/-- Example 9.3.2
+Slight change from the book to accomodate the change to {lean}`Real.CloseFn`
+-/
+example : (5.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by sorry
 
-/-- Example 9.3.2 -/
-example : (0.41:ℝ).CloseFn (.Icc 1.9 2.1) (fun x ↦ x^2) 4 := by sorry
+/-- Example 9.3.2
+Slight change from the book to accomodate the change to {lean}`Real.CloseFn`
+-/
+example : (0.42:ℝ).CloseFn (.Icc 1.9 2.1) (fun x ↦ x^2) 4 := by sorry
 
 /-- Example 9.3.4 -/
 example: ¬(0.1:ℝ).CloseFn (.Icc 1 3) (fun x ↦ x^2) 4 := by
@@ -88,91 +94,93 @@ example: Convergesto (.Icc 1 3) (fun x ↦ x^2) 4 2 := by
   sorry
 
 /-- Proposition 9.3.9 / Exercise 9.3.1 -/
-theorem Convergesto.iff_conv {E:Set ℝ} (f: ℝ → ℝ) (L:ℝ) {x₀:ℝ} (h: AdherentPt x₀ E) :
+theorem Convergesto.iff_conv {E:Set ℝ} (f: ℝ → ℝ) (L:ℝ) {x₀:ℝ} :
   Convergesto E f L x₀ ↔ ∀ a:ℕ → ℝ, (∀ n:ℕ, a n ∈ E) →
   Filter.atTop.Tendsto a (nhds x₀) →
   Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds L) := by
   sorry
 
-theorem Convergesto.comp {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hf: Convergesto E f L x₀) {a:ℕ → ℝ} (ha: ∀ n:ℕ, a n ∈ E) (hconv: Filter.atTop.Tendsto a (nhds x₀)) :
+theorem Convergesto.comp {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (hf: Convergesto E f L x₀) {a:ℕ → ℝ}
+  (ha: ∀ n:ℕ, a n ∈ E) (hconv: Filter.atTop.Tendsto a (nhds x₀)) :
   Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds L) := by
-  rw [iff_conv f L h] at hf; solve_by_elim
+  rw [iff_conv f L] at hf; solve_by_elim
 
--- Remark 9.3.11 may possibly be inaccurate, in that one may be able to safely delete the hypothesis `AdherentPt x₀ E` in the above theorems.  This is something that formalization might be able to clarify!  If so, the hypothesis may also be deletable in several of the theorems below.
+-- Remark 9.3.11 is not quite true in Lean: the hypothesis `AdherentPt x₀ E` is safely removed
+-- from most theorems (with the exception of Convergesto.uniq).
 
 /-- Corollary 9.3.13 -/
 theorem Convergesto.uniq {E:Set ℝ} {f: ℝ → ℝ} {L L':ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
   (hf: Convergesto E f L x₀) (hf': Convergesto E f L' x₀) : L = L' := by
   -- This proof is written to follow the structure of the original text.
   let ⟨ a, ha, hconv ⟩ := (limit_of_AdherentPt _ _).mp h
-  exact tendsto_nhds_unique (hf.comp h ha hconv) (hf'.comp h ha hconv)
+  exact tendsto_nhds_unique (hf.comp ha hconv) (hf'.comp ha hconv)
 
 /-- Proposition 9.3.14 (Limit laws for functions) -/
-theorem Convergesto.add {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
+theorem Convergesto.add {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ}
   (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
   Convergesto E (f + g) (L + M) x₀ := by
     -- This proof is written to follow the structure of the original text.
-    rw [iff_conv _ _ h] at hf hg ⊢
+    rw [iff_conv _ _] at hf hg ⊢
     intro a ha hconv; specialize hf a ha hconv; specialize hg a ha hconv
     convert hf.add hg using 1
 
 /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2 -/
-theorem Convergesto.sub {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
+theorem Convergesto.sub {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ}
   (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
   Convergesto E (f - g) (L - M) x₀ := by
     sorry
 
 /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2 -/
-theorem Convergesto.max {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
+theorem Convergesto.max {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ}
   (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
   Convergesto E (max f g) (max L M) x₀ := by
     sorry
 
 /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2 -/
-theorem Convergesto.min {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
+theorem Convergesto.min {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ}
   (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
   Convergesto E (min f g) (min L M) x₀ := by
     sorry
 
 /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2 -/
-theorem Convergesto.smul {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
+theorem Convergesto.smul {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ}
   (hf: Convergesto E f L x₀) (c:ℝ) :
   Convergesto E (c • f) (c * L) x₀ := by
     sorry
 
 /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2 -/
-theorem Convergesto.mul {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
+theorem Convergesto.mul {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ}
   (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
   Convergesto E (f * g) (L * M) x₀ := by
     sorry
 
 /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2.  The hypothesis in the book that g is non-vanishing on E can be dropped. -/
-theorem Convergesto.div {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (hM: M ≠ 0)
+theorem Convergesto.div {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (hM: M ≠ 0)
   (hf: Convergesto E f L x₀) (hg: Convergesto E g M x₀) :
   Convergesto E (f / g) (L / M) x₀ := by
     sorry
 
-theorem Convergesto.const {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c:ℝ)
-  : Convergesto E (fun x ↦ c) c x₀ := by
+theorem Convergesto.const (E:Set ℝ) (x₀:ℝ) (c:ℝ)
+  : Convergesto E (fun _ ↦ c) c x₀ := by
   sorry
 
-theorem Convergesto.id {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
+theorem Convergesto.id (E:Set ℝ) (x₀:ℝ)
   : Convergesto E (fun x ↦ x) x₀ x₀ := by
   sorry
 
-theorem Convergesto.sq {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E)
-  : Convergesto E (fun x ↦ x^2) x₀ (x₀^2) := by
+theorem Convergesto.sq (E:Set ℝ) (x₀:ℝ)
+  : Convergesto E (fun x ↦ x^2) (x₀^2) x₀ := by
   sorry
 
-theorem Convergesto.linear {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c:ℝ)
-  : Convergesto E (fun x ↦ c * x) x₀ (c * x₀) := by
+theorem Convergesto.linear (E:Set ℝ) (x₀:ℝ) (c:ℝ)
+  : Convergesto E (fun x ↦ c * x) (c * x₀) x₀ := by
   sorry
 
-theorem Convergesto.quadratic {E:Set ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) (c d:ℝ)
-  : Convergesto E (fun x ↦ x^2 + c * x + d) x₀ (x₀^2 + c * x₀ + d) := by
+theorem Convergesto.quadratic (E:Set ℝ) (x₀:ℝ) (c d:ℝ)
+  : Convergesto E (fun x ↦ x^2 + c * x + d) (x₀^2 + c * x₀ + d) x₀ := by
   sorry
 
-theorem Convergesto.restrict {X Y:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ X) (hf: Convergesto X f L x₀) (hY: Y ⊆ X) : Convergesto Y f L x₀ := by
+theorem Convergesto.restrict {X Y:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (hf: Convergesto X f L x₀) (hY: Y ⊆ X) : Convergesto Y f L x₀ := by
   sorry
 
 theorem Real.sign_def (x:ℝ) : Real.sign x = if x < 0 then -1 else if x > 0 then 1 else 0 := rfl
@@ -193,7 +201,7 @@ theorem Convergesto.f_9_3_17_remove : Convergesto (.univ \ {0}) f_9_3_17 0 0 :=
 theorem Convergesto.f_9_3_17_all : ¬ ∃ L, Convergesto .univ f_9_3_17 L 0 := by sorry
 
 /-- Proposition 9.3.18 / Exercise 9.3.3 -/
-theorem Convergesto.local {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (h: AdherentPt x₀ E) {δ:ℝ} (hδ: δ > 0) :
+theorem Convergesto.local {E:Set ℝ} {f: ℝ → ℝ} {L:ℝ} {x₀:ℝ} {δ:ℝ} (hδ: δ > 0) :
   Convergesto E f L x₀ ↔ Convergesto (E ∩ .Ioo (x₀-δ) (x₀+δ)) f L x₀ := by
     sorry
 
@@ -216,7 +224,7 @@ example : ¬ ∃ L, Convergesto .univ f_9_3_21 L 0 := by sorry
 /- Exercise 9.3.4: State a definition of limit superior and limit inferior for functions, and prove an analogue of Proposition 9.3.9 for those definitions. -/
 
 /-- Exercise 9.3.5 (Continuous version of squeeze test) -/
-theorem Convergesto.squeeze {E:Set ℝ} {f g h: ℝ → ℝ} {L:ℝ} {x₀:ℝ} (had: AdherentPt x₀ E)
+theorem Convergesto.squeeze {E:Set ℝ} {f g h: ℝ → ℝ} {L:ℝ} {x₀:ℝ}
   (hfg: ∀ x ∈ E, f x ≤ g x) (hgh: ∀ x ∈ E, g x ≤ h x)
   (hf: Convergesto E f L x₀) (hh: Convergesto E h L x₀) :
   Convergesto E g L x₀ := by
diff --git a/Analysis/Section_9_4.lean b/Analysis/Section_9_4.lean
index 35affd11..766428db 100644
--- a/Analysis/Section_9_4.lean
+++ b/Analysis/Section_9_4.lean
@@ -58,8 +58,8 @@ example : ¬ ContinuousAt f_9_4_6 0 := by sorry
 
 example : ContinuousWithinAt f_9_4_6 (.Ici 0) 0 := by sorry
 
-/-- Proposition 9.4.7 / Exercise 9.4.1.  It is possible that the hypothesis {lean}`x₀ ∈ X` is unnecessary. -/
-theorem ContinuousWithinAt.tfae (X:Set ℝ) (f: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) :
+/-- Proposition 9.4.7 / Exercise 9.4.1. -/
+theorem ContinuousWithinAt.tfae (X:Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) :
   [
     ContinuousWithinAt f X x₀,
     ∀ a:ℕ → ℝ, (∀ n, a n ∈ X) → Filter.atTop.Tendsto a (nhds x₀) → Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (f x₀)),
@@ -68,46 +68,46 @@ theorem ContinuousWithinAt.tfae (X:Set ℝ) (f: ℝ → ℝ) {x₀:ℝ} (h : x
   sorry
 
 /-- Remark 9.4.8 --/
-theorem _root_.Filter.Tendsto.comp_of_continuous {X:Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h : x₀ ∈ X)
+theorem _root_.Filter.Tendsto.comp_of_continuous {X:Set ℝ} {f: ℝ → ℝ} {x₀:ℝ}
   (h_cont: ContinuousWithinAt f X x₀) {a: ℕ → ℝ} (ha: ∀ n, a n ∈ X)
   (hconv: Filter.atTop.Tendsto a (nhds x₀)):
   Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (f x₀)) := by
-  have := (ContinuousWithinAt.tfae X f h).out 0 1
+  have := (ContinuousWithinAt.tfae X f x₀).out 0 1
   grind
 
 /- Proposition 9.4.9 -/
-theorem ContinuousWithinAt.add {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
+theorem ContinuousWithinAt.add {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ}
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (f + g) X x₀ := by
-  rw [iff] at hf hg ⊢; convert hf.add (AdherentPt.of_mem h) hg using 1
+  rw [iff] at hf hg ⊢; convert hf.add hg using 1
 
 
-theorem ContinuousWithinAt.sub {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
+theorem ContinuousWithinAt.sub {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ}
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (f - g) X x₀ := by
-  rw [iff] at hf hg ⊢; convert hf.sub (AdherentPt.of_mem h) hg using 1
+  rw [iff] at hf hg ⊢; convert hf.sub hg using 1
 
-theorem ContinuousWithinAt.max {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
+theorem ContinuousWithinAt.max {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ}
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (max f g) X x₀ := by
-  rw [iff] at hf hg ⊢; convert hf.max (AdherentPt.of_mem h) hg using 1
+  rw [iff] at hf hg ⊢; convert hf.max hg using 1
 
 
-theorem ContinuousWithinAt.min {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
+theorem ContinuousWithinAt.min {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ}
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (min f g) X x₀ := by
-  rw [iff] at hf hg ⊢; convert hf.min (AdherentPt.of_mem h) hg using 1
+  rw [iff] at hf hg ⊢; convert hf.min hg using 1
 
 
-theorem ContinuousWithinAt.mul' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
+theorem ContinuousWithinAt.mul' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ}
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (f * g) X x₀ := by
-  rw [iff] at hf hg ⊢; convert hf.mul (AdherentPt.of_mem h) hg using 1
+  rw [iff] at hf hg ⊢; convert hf.mul hg using 1
 
-theorem ContinuousWithinAt.div' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) (hM: g x₀ ≠ 0)
+theorem ContinuousWithinAt.div' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (hM: g x₀ ≠ 0)
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (f / g) X x₀ := by
-  rw [iff] at hf hg ⊢; convert hf.div (AdherentPt.of_mem h) hM hg using 1
+  rw [iff] at hf hg ⊢; convert hf.div hM hg using 1
 
 /-- Proposition 9.4.10 / Exercise 9.4.3  -/
 theorem Continuous.exp {a:ℝ} (ha: a>0) : Continuous (fun x:ℝ ↦ a ^ x) := by
@@ -122,7 +122,9 @@ theorem Continuous.abs : Continuous (fun x:ℝ ↦ |x|) := by
   sorry -- TODO
 
 /-- Proposition 9.4.13 / Exercise 9.4.5 -/
-theorem ContinuousWithinAt.comp {X Y: Set ℝ} {f g:ℝ → ℝ} (hf: ∀ x ∈ X, f x ∈ Y) {x₀:ℝ} (hx₀: x ∈ X) (hf_cont: ContinuousWithinAt f X x₀) (hg_cont: ContinuousWithinAt g Y (f x₀)): ContinuousWithinAt (g ∘ f) X x₀ := by sorry
+theorem ContinuousWithinAt.comp {X Y: Set ℝ} {f g:ℝ → ℝ} (hf: ∀ x ∈ X, f x ∈ Y) (x₀:ℝ)
+  (hf_cont: ContinuousWithinAt f X x₀) (hg_cont: ContinuousWithinAt g Y (f x₀)):
+  ContinuousWithinAt (g ∘ f) X x₀ := by sorry
 
 /-- Example 9.4.14 -/
 example : Continuous (fun x:ℝ ↦ 3*x + 1) := by
diff --git a/Analysis/Section_9_5.lean b/Analysis/Section_9_5.lean
index 44694b3f..b4411315 100644
--- a/Analysis/Section_9_5.lean
+++ b/Analysis/Section_9_5.lean
@@ -64,7 +64,7 @@ theorem right_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: Adherent
   (hconv: Filter.atTop.Tendsto a (nhds x₀)) :
   Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (right_limit X f x₀)) := by
   choose L hL using h
-  apply Convergesto.comp had _ ha hconv
+  apply Convergesto.comp _ ha hconv
   rwa [Convergesto.iff, (eq had hL).2]
 
 theorem left_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentPt x₀ (X ∩ .Iio x₀))
@@ -73,7 +73,7 @@ theorem left_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentP
   (hconv: Filter.atTop.Tendsto a (nhds x₀)) :
   Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (left_limit X f x₀)) := by
   choose L hL using h
-  apply Convergesto.comp had _ ha hconv
+  apply Convergesto.comp _ ha hconv
   rwa [Convergesto.iff, (eq had hL).2]
 
 /-- Proposition 9.5.3 -/
@@ -85,7 +85,7 @@ theorem ContinuousAt.iff_eq_left_right_limit {X: Set ℝ} {f: ℝ → ℝ} {x₀
   . sorry
   intro ⟨ ⟨ hre, hright⟩, ⟨ hle, lheft ⟩ ⟩
   set L := f x₀
-  have := (ContinuousWithinAt.tfae X f h).out 0 2
+  have := (ContinuousWithinAt.tfae X f x₀).out 0 2
   rw [this]
   intro ε hε
   apply right_limit.eq' at hre
diff --git a/Analysis/Section_9_6.lean b/Analysis/Section_9_6.lean
index 097560fb..a684e0eb 100644
--- a/Analysis/Section_9_6.lean
+++ b/Analysis/Section_9_6.lean
@@ -63,7 +63,7 @@ theorem BddOn.of_continuous_on_compact {a b:ℝ} (_h:a < b) {f:ℝ → ℝ} (hf:
   have why (j:ℕ) : n j ≥ j := why_7_6_3 hn j
   replace hf := hf.continuousWithinAt hLX
   rw [ContinuousWithinAt.iff] at hf
-  replace hf := hf.comp (AdherentPt.of_mem hLX) (fun j ↦ haX (n j)) hconv
+  replace hf := hf.comp (fun j ↦ haX (n j)) hconv
   apply Metric.isBounded_range_of_tendsto at hf
   rw [isBounded_def] at hf; choose M hpos hM using hf
   choose j hj using exists_nat_gt M
@@ -109,7 +109,7 @@ theorem IsMaxOn.of_continuous_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf
   use xmax, hmax
   have hn_lower (j:ℕ) : n j ≥ j := why_7_6_3 hn j
   have hconv' : Filter.atTop.Tendsto (fun j ↦ f (x (n j))) (nhds (f xmax)) :=
-    hconv.comp_of_continuous hmax (hf.continuousWithinAt hmax) (fun j ↦ hx (n j))
+    hconv.comp_of_continuous (hf.continuousWithinAt hmax) (fun j ↦ hx (n j))
   have hlower (j:ℕ) : m - 1/(j+1:ℝ) < f (x (n j)) := by
     apply lt_of_le_of_lt _ (hfx (n j)); gcongr; grind
   have hupper (j:ℕ) : f (x (n j)) ≤ m := by apply claim1; simp [Set.mem_image, E]; use x (n j), hx (n j)
diff --git a/Analysis/Section_9_7.lean b/Analysis/Section_9_7.lean
index b671a9e1..e5a20561 100644
--- a/Analysis/Section_9_7.lean
+++ b/Analysis/Section_9_7.lean
@@ -54,7 +54,7 @@ theorem intermediate_value {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: Continuou
         . exact tendsto_const_nhds
         . exact fun n ↦ le_of_lt (hx2 n)
         exact fun n ↦ le_csSup hE_bdd (hx1 n)
-      replace := this.comp_of_continuous hc (hf.continuousWithinAt hc) (fun n ↦ hE (hx1 n))
+      replace := this.comp_of_continuous (hf.continuousWithinAt hc) (fun n ↦ hE (hx1 n))
       have hfxny (n:ℕ) : f (x n) ≤ y := by specialize hx1 n; simp [E] at hx1; grind
       exact le_of_tendsto' this hfxny
     have hne : c < b := by grind
diff --git a/Analysis/Section_9_9.lean b/Analysis/Section_9_9.lean
index 368ecb4a..54836dd4 100644
--- a/Analysis/Section_9_9.lean
+++ b/Analysis/Section_9_9.lean
@@ -201,7 +201,7 @@ theorem UniformContinuousOn.of_continuousOn {a b:ℝ} {f:ℝ → ℝ}
   observe hbounded : Bornology.IsBounded (.Icc a b)
   have ⟨ j, hj, ⟨ L, hL, hconv⟩ ⟩ := (Heine_Borel (.Icc a b)).mp ⟨ hclosed, hbounded ⟩ _ hxmem
   replace hcont := ContinuousOn.continuousWithinAt hcont hL
-  have hconv' := hconv.comp_of_continuous hL hcont (fun k ↦ hxmem (j k))
+  have hconv' := hconv.comp_of_continuous hcont (fun k ↦ hxmem (j k))
   rw [Sequence.equiv_iff] at hequiv
   replace hequiv : atTop.Tendsto (fun k ↦ x (n (j k)) - y (n (j k))) (nhds 0) := by
     observe hj' : atTop.Tendsto j .atTop
@@ -212,7 +212,7 @@ theorem UniformContinuousOn.of_continuousOn {a b:ℝ} {f:ℝ → ℝ}
     convert hconv.sub hequiv with k
     . abel
     simp
-  replace hyconv := hyconv.comp_of_continuous hL hcont (fun k ↦ hymem (j k))
+  replace hyconv := hyconv.comp_of_continuous hcont (fun k ↦ hymem (j k))
   have : atTop.Tendsto (fun k ↦ f (x (n (j k))) - f (y (n (j k)))) (nhds 0) := by
     convert hconv'.sub hyconv; simp
   sorry