diff --git a/analysis/Analysis/Section_6_4.lean b/analysis/Analysis/Section_6_4.lean
index 89a65373..360cdfc9 100644
--- a/analysis/Analysis/Section_6_4.lean
+++ b/analysis/Analysis/Section_6_4.lean
@@ -213,8 +213,8 @@ theorem Sequence.liminf_mono {a b:Sequence} (hm: a.m = b.m) (hab: ∀ n ≥ a.m,
 
 /-- Corollary 6.4.14 (Squeeze test) / Exercise 6.4.5 -/
 theorem Sequence.lim_of_between {a b c:Sequence} {L:ℝ} (hm: b.m = a.m ∧ c.m = a.m)
-  (hab: ∀ n ≥ a.m, a n ≤ b n ∧ b n ≤ c n) (ha: a.TendsTo L) (hb: b.TendsTo L) :
-    c.TendsTo L := by sorry
+  (hab: ∀ n ≥ a.m, a n ≤ b n ∧ b n ≤ c n) (ha: a.TendsTo L) (hb: c.TendsTo L) :
+    b.TendsTo L := by sorry
 
 /-- Example 6.4.15 -/
 example : ((fun (n:ℕ) ↦ 2/(n+1:ℝ)):Sequence).TendsTo 0 := by