diff --git a/analysis/Analysis/Appendix_A_3.lean b/analysis/Analysis/Appendix_A_3.lean
index 8162191..6ed412f 100644
--- a/analysis/Analysis/Appendix_A_3.lean
+++ b/analysis/Analysis/Appendix_A_3.lean
@@ -53,7 +53,7 @@ example {r:ℝ} (h: 0 < r) (h': r < 1) : Summable (fun n:ℕ ↦ n * r^n) := by
     use 1
     intro b hb
     simp [show b ≠ 0 by linarith, show r ≠ 0 by linarith]
-  suffices hconv: Filter.Tendsto (fun n:ℕ ↦ r * ((n+1) / n)) Filter.atTop (nhds r)
+  suffices hconv: Filter.Tendsto (fun n:ℕ ↦ r * ((n+1) / n)) .atTop (nhds r)
   . apply Filter.Tendsto.congr' _ hconv
     simp [Filter.EventuallyEq, Filter.eventually_atTop]
     use 1
@@ -63,17 +63,17 @@ example {r:ℝ} (h: 0 < r) (h': r < 1) : Summable (fun n:ℕ ↦ n * r^n) := by
     simp [abs_of_pos h, abs_of_pos hb1]
     field_simp
     ring_nf
-  suffices hconv : Filter.Tendsto (fun n:ℕ ↦ ((n+1:ℝ) / n)) Filter.atTop (nhds 1)
+  suffices hconv : Filter.Tendsto (fun n:ℕ ↦ ((n+1:ℝ) / n)) .atTop (nhds 1)
   . convert Filter.Tendsto.const_mul r hconv
     simp
-  suffices hconv : Filter.Tendsto (fun n:ℕ ↦ 1 + 1/(n:ℝ)) Filter.atTop (nhds 1)
+  suffices hconv : Filter.Tendsto (fun n:ℕ ↦ 1 + 1/(n:ℝ)) .atTop (nhds 1)
   . apply Filter.Tendsto.congr' _ hconv
     simp [Filter.EventuallyEq, Filter.eventually_atTop]
     use 1
     intro b hb
     have : (b:ℝ) > 0 := by norm_cast
     field_simp
-  suffices hconv : Filter.Tendsto (fun n:ℕ ↦ 1/(n:ℝ)) Filter.atTop (nhds 0)
+  suffices hconv : Filter.Tendsto (fun n:ℕ ↦ 1/(n:ℝ)) .atTop (nhds 0)
   . convert Filter.Tendsto.const_add 1 hconv
     simp
   exact tendsto_one_div_atTop_nhds_zero_nat
diff --git a/analysis/Analysis/Appendix_B_2.lean b/analysis/Analysis/Appendix_B_2.lean
index 4517fea..46cd279 100644
--- a/analysis/Analysis/Appendix_B_2.lean
+++ b/analysis/Analysis/Appendix_B_2.lean
@@ -56,19 +56,19 @@ theorem NNRealDecimal.surj (x:NNReal) : ∃ d:NNRealDecimal, x = d := by
   set a : ℕ → Digit := fun n ↦ (hdigit n).choose
   have ha (n:ℕ) : s (n+1) = 10 * s n + (a n : ℕ) := (hdigit n).choose_spec
   set d := mk (s 0) a; use d
-  have hsum (n:ℕ) : s n * (10:NNReal)^(-n:ℝ) = s 0 + ∑ i ∈ Finset.range n, a i * (10:NNReal)^(-i-1:ℝ) := by
+  have hsum (n:ℕ) : s n * (10:NNReal)^(-n:ℝ) = s 0 + ∑ i ∈ .range n, a i * (10:NNReal)^(-i-1:ℝ) := by
     induction' n with n hn
     . simp
     rw [ha n]; calc
       _ = s n * (10:NNReal)^(-n:ℝ) + a n * 10^(-n-1:ℝ) := by
         simp [add_mul]; congr 1 <;> ring_nf
         rw [mul_assoc, ←NNReal.rpow_add_one (by norm_num)]; congr; ring
-      _ = s 0 + (∑ i ∈ Finset.range n, a i * (10:NNReal)^(-i-1:ℝ) + a n * 10^(-n-1:ℝ)) := by
+      _ = s 0 + (∑ i ∈ .range n, a i * (10:NNReal)^(-i-1:ℝ) + a n * 10^(-n-1:ℝ)) := by
         rw [hn]; abel
       _ = _ := by congr; exact (Finset.sum_range_succ _ _).symm
   have := d.toNNReal_conv.tendsto_sum_tsum_nat
   replace := this.const_add (s 0:NNReal)
-  convert_to Filter.Tendsto (fun n ↦ s n * (10:NNReal)^(-n:ℝ)) Filter.atTop (nhds (d:NNReal)) at this
+  convert_to Filter.Tendsto (fun n ↦ s n * (10:NNReal)^(-n:ℝ)) .atTop (nhds (d:NNReal)) at this
   . ext n; rw [hsum n]
   apply tendsto_nhds_unique _ this
   apply Filter.Tendsto.squeeze (g := fun n:ℕ ↦ x - (10:NNReal)^(-n:ℝ)) (h := fun n ↦ x)
@@ -94,7 +94,7 @@ theorem NNRealDecimal.not_inj : (1:NNReal) = (mk 1 fun _ ↦ 0) ∧ (1:NNReal) =
   have := (mk 0 fun _ ↦ 9).toNNReal_conv.tendsto_sum_tsum_nat
   simp at this
   apply tendsto_nhds_unique _ this
-  convert_to Filter.Tendsto (fun n:ℕ ↦ 1 - (10:NNReal)^(-n:ℝ)) Filter.atTop (nhds 1) using 2 with n
+  convert_to Filter.Tendsto (fun n:ℕ ↦ 1 - (10:NNReal)^(-n:ℝ)) .atTop (nhds 1) using 2 with n
   . induction' n with n hn
     . simp
     rw [Finset.sum_range_succ, hn, Nat.cast_add, Nat.cast_one, neg_add']
diff --git a/analysis/Analysis/Section_10_5.lean b/analysis/Analysis/Section_10_5.lean
index cf050d4..9572fec 100644
--- a/analysis/Analysis/Section_10_5.lean
+++ b/analysis/Analysis/Section_10_5.lean
@@ -31,95 +31,84 @@ theorem _root_.Filter.Tendsto.of_div {X: Set ℝ} {f g: ℝ → ℝ} {x₀ f'x
 
 /-- Proposition 10.5.2 (L'Hôpital's rule, II) -/
 theorem _root_.Filter.Tendsto.of_div' {a b L:ℝ} (hab: a < b) {f g f' g': ℝ → ℝ}
-  (hf: DifferentiableOn ℝ f (Set.Icc a b)) (hg: DifferentiableOn ℝ g (Set.Icc a b))
-  (hf': f' = derivWithin f (Set.Icc a b)) (hg': g' = derivWithin g (Set.Icc a b))
+  (hf: DifferentiableOn ℝ f (.Icc a b)) (hg: DifferentiableOn ℝ g (.Icc a b))
+  (hf': f' = derivWithin f (.Icc a b)) (hg': g' = derivWithin g (.Icc a b))
   (hfa: f a = 0) (hga: g a = 0) (hgnon: ∀ x ∈ Set.Icc a b, g' x ≠ 0)
 
-  (hderiv: Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (Set.Icc a b)) (nhds L)) :
+  (hderiv: Filter.Tendsto (fun x ↦ f' x / g' x) (nhdsWithin a (.Icc a b)) (nhds L)) :
   (∀ x ∈ Set.Ioc a b, g x ≠ 0) ∧
   Filter.Tendsto (fun x ↦ f x / g x) (nhdsWithin a (Set.Ioc a b)) (nhds L) := by
   -- This proof is written to follow the structure of the original text.
-  have hfcon : ContinuousOn f (Set.Icc a b) := ContinuousOn.of_differentiableOn hf
-  have hgcon : ContinuousOn g (Set.Icc a b) := ContinuousOn.of_differentiableOn hg
+  have hfcon : ContinuousOn f (.Icc a b) := .of_differentiableOn hf
+  have hgcon : ContinuousOn g (.Icc a b) := .of_differentiableOn hg
   have (x:ℝ) (hx: x ∈ Set.Ioc a b) : g x ≠ 0 := by
     by_contra this
     simp at hx
-    have := HasDerivWithinAt.exist_zero hx.1 (ContinuousOn.mono hgcon ?_) (DifferentiableOn.mono hg ?_) (by rw [hga, this])
+    have := HasDerivWithinAt.exist_zero hx.1 (hgcon.mono ?_) (hg.mono ?_) (by rw [hga, this])
     . obtain ⟨ y, hy, hgy ⟩ := this; simp at hy
-      have : y ∈ Set.Icc a b := by simp; exact ⟨ by linarith, by linarith ⟩
+      have : y ∈ Set.Icc a b := by simp; constructor <;> linarith
       specialize hgnon y this
       rw [DifferentiableOn.eq_1] at hf hg; specialize hg y this
-      replace hg := DifferentiableWithinAt.hasDerivWithinAt hg
+      replace hg := hg.hasDerivWithinAt
       replace hg : HasDerivWithinAt g (g' y) (Set.Ioo a x) y:= by
-        rw [hg']
-        apply HasDerivWithinAt.mono hg
-        intro z; simp; intro h1 h2; exact ⟨ by linarith, by linarith ⟩
+        rw [hg']; apply hg.mono; intro z; simp; intros; constructor <;> linarith
       have hd := derivative_unique ?_ hg hgy
       . contradiction
       apply ClusterPt.mono _ ((Filter.principal_mono (s := Set.Ioo a y)).mpr  _)
       . simp [←mem_closure_iff_clusterPt, closure_Ioo (show a ≠ y by linarith), le_of_lt hy.1]
-      intro _; simp; intros; exact ⟨ ⟨ by linarith, by linarith ⟩, by linarith ⟩
-    . intro _; simp; intro h1 _; exact ⟨ h1, by linarith ⟩
-    intro _; simp; intro h1 _; exact ⟨ le_of_lt h1, by linarith ⟩
+      intro _; simp; intros; refine ⟨ ⟨ ?_, ?_ ⟩, ?_ ⟩ <;> linarith
+    . intro _; simp; intro h1 _; constructor <;> linarith
+    intro _; simp; intros; constructor <;> linarith
   refine ⟨ this, ?_ ⟩
   rw [nhdsWithin.eq_1] at hderiv ⊢
   rw [←Convergesto.iff, Convergesto.iff_conv _ _ _]
   . intro x hx hconv
     have hxy (n:ℕ) : ∃ yn ∈ Set.Ioo a (x n), (f (x n))/(g (x n)) = f' yn / (g' yn) := by
       set h : ℝ → ℝ := fun x' ↦ (f x') * (g (x n)) - (g x') * (f (x n))
-      have hdiff : DifferentiableOn ℝ h (Set.Icc a b) := by fun_prop
-      have hcon : ContinuousOn h (Set.Icc a b) := by fun_prop
+      have hdiff : DifferentiableOn ℝ h (.Icc a b) := by fun_prop
+      have hcon : ContinuousOn h (.Icc a b) := by fun_prop
       specialize hx n; simp at hx
-      replace hcon : ContinuousOn h (Set.Icc a (x n)) := by
-        apply ContinuousOn.mono hcon
-        intro _; simp; intros; exact ⟨ by linarith, by linarith ⟩
-      replace hdiff : DifferentiableOn ℝ h (Set.Ioo a (x n)) := by
-        apply DifferentiableOn.mono hdiff
-        intro _; simp; intros; exact ⟨ by linarith, by linarith ⟩
+      replace hcon : ContinuousOn h (.Icc a (x n)) := by
+        apply hcon.mono; intro _; simp; intros; constructor <;> linarith
+      replace hdiff : DifferentiableOn ℝ h (.Ioo a (x n)) := by
+        apply hdiff.mono; intro _; simp; intros; constructor <;> linarith
       have ha : h a = 0 := by simp [h, hfa, hga]
       have hb : h (x n) = 0 := by simp [h]; ring
       obtain ⟨ yn, hyn, hdh ⟩ := HasDerivWithinAt.exist_zero hx.1 hcon hdiff (by rw [ha, hb])
       use yn, hyn
       rw [DifferentiableOn.eq_1] at hf hg
-      have h1 : HasDerivWithinAt f (f' yn) (Set.Ioo a (x n)) yn := by
-        specialize hf yn (by simp at hyn ⊢; exact ⟨ by linarith, by linarith ⟩)
-        rw [hf']
-        apply HasDerivWithinAt.mono (DifferentiableWithinAt.hasDerivWithinAt hf)
-        intro _; simp; intros; exact ⟨ by linarith, by linarith ⟩
-      have h2 : HasDerivWithinAt g (g' yn) (Set.Ioo a (x n)) yn := by
-        specialize hg yn (by simp at hyn ⊢; exact ⟨ by linarith, by linarith ⟩)
-        rw [hg']
-        apply HasDerivWithinAt.mono (DifferentiableWithinAt.hasDerivWithinAt hg)
-        intro _; simp; intros; exact ⟨ by linarith, by linarith ⟩
-      have h3 : HasDerivWithinAt (fun x' ↦ (f x') * (g (x n))) ((f' yn)*(g (x n))) (Set.Ioo a (x n)) yn :=
-        HasDerivWithinAt.mul_const h1 _
-      have h4 : HasDerivWithinAt (fun x' ↦ (g x') * (f (x n))) ((g' yn)*(f (x n))) (Set.Ioo a (x n)) yn :=
-        HasDerivWithinAt.mul_const h2 _
-      have h5 : HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (Set.Ioo a (x n)) yn := by
+      have h1 : HasDerivWithinAt f (f' yn) (.Ioo a (x n)) yn := by
+        specialize hf yn (by simp at hyn ⊢; constructor <;> linarith)
+        rw [hf']; apply hf.hasDerivWithinAt.mono; intro _; simp; intros; constructor <;> linarith
+      have h2 : HasDerivWithinAt g (g' yn) (.Ioo a (x n)) yn := by
+        specialize hg yn (by simp at hyn ⊢; constructor <;> linarith)
+        rw [hg']; apply hg.hasDerivWithinAt.mono; intro _; simp; intros; constructor <;> linarith
+      have h3 : HasDerivWithinAt (fun x' ↦ (f x') * (g (x n))) ((f' yn)*(g (x n))) (.Ioo a (x n)) yn :=
+        h1.mul_const _
+      have h4 : HasDerivWithinAt (fun x' ↦ (g x') * (f (x n))) ((g' yn)*(f (x n))) (.Ioo a (x n)) yn :=
+        h2.mul_const _
+      have h5 : HasDerivWithinAt h (f' yn * g (x n) - g' yn * f (x n)) (.Ioo a (x n)) yn := by
         simp [h]
         exact HasDerivWithinAt.sub h3 h4
       have h6 : f' yn * g (x n) - g' yn * f (x n) = 0 := by
         apply derivative_unique _ h5 hdh
         simp at hyn
-        apply ClusterPt.mono _ ((Filter.principal_mono (s := Set.Ioo a yn)).mpr  _)
+        apply ClusterPt.mono _ ((Filter.principal_mono (s := .Ioo a yn)).mpr  _)
         . simp [←mem_closure_iff_clusterPt, closure_Ioo (show a ≠ yn by linarith), le_of_lt hyn.1]
-        intro _; simp; intros; exact ⟨ ⟨ by linarith, by linarith ⟩, by linarith ⟩
+        intro _; simp; intros; refine ⟨ ⟨ ?_, ?_ ⟩, ?_ ⟩ <;> linarith
       have h7 : g (x n) ≠ 0 := this _ (by simp [hx])
-      have h8 : g' (yn) ≠ 0 := hgnon _ (by simp at hyn; exact ⟨ by linarith, by linarith ⟩)
+      have h8 : g' (yn) ≠ 0 := hgnon _ (by simp at hyn; constructor <;> linarith)
       field_simp; rw [mul_comm]; linarith
     set y : ℕ → ℝ := fun n ↦ (hxy n).choose
     have hy (n:ℕ) : y n ∈ Set.Ioo a (x n) := (hxy n).choose_spec.1
     have hy' (n:ℕ) : (f (x n))/(g (x n)) = f' (y n) / (g' (y n)) := (hxy n).choose_spec.2
-    have hyconv : Filter.Tendsto y Filter.atTop (nhds a) := by
+    have hyconv : Filter.Tendsto y .atTop (nhds a) := by
       simp at hy
       apply Filter.Tendsto.squeeze tendsto_const_nhds hconv _
       all_goals intro n; linarith [hy n]
     replace hy : ∀ n, y n ∈ Set.Icc a b := by
-      intro n; simp at hx hy ⊢; specialize hy n; specialize hx n
-      exact ⟨ by linarith, by linarith ⟩
-    simp_rw [hy' _]
-    apply Filter.Tendsto.comp hderiv _
-    rw [←nhdsWithin.eq_1]
+      intro n; simp at hx hy ⊢; specialize hy n; specialize hx n; constructor <;> linarith
+    simp_rw [hy' _]; apply hderiv.comp _; rw [←nhdsWithin.eq_1]
     apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hyconv _
     exact Filter.Eventually.of_forall hy
   simp [←closure_def', closure_Ioc (show a ≠ b by linarith), le_of_lt hab]
diff --git a/analysis/Analysis/Section_11_1.lean b/analysis/Analysis/Section_11_1.lean
index 402674e..e95acdf 100644
--- a/analysis/Analysis/Section_11_1.lean
+++ b/analysis/Analysis/Section_11_1.lean
@@ -176,7 +176,7 @@ theorem BoundedInterval.dist_le_length {I:BoundedInterval} {x y:ℝ} (hx: x ∈
   replace hx := subset_Icc I _ hx
   replace hy := subset_Icc I _ hy
   simp [mem_iff, abs_le'] at hx hy ⊢
-  left; exact ⟨ by linarith, by linarith ⟩
+  left; constructor <;> linarith
 
 abbrev BoundedInterval.joins (K I J: BoundedInterval) : Prop := (I:Set ℝ) ∩ (J:Set ℝ) = ∅
   ∧ (K:Set ℝ) = (I:Set ℝ) ∪ (J:Set ℝ) ∧ |K|ₗ = |I|ₗ + |J|ₗ
diff --git a/analysis/Analysis/Section_11_10.lean b/analysis/Analysis/Section_11_10.lean
index ef7f3f7..0310994 100644
--- a/analysis/Analysis/Section_11_10.lean
+++ b/analysis/Analysis/Section_11_10.lean
@@ -112,20 +112,18 @@ theorem RS_integ_eq_integ_of_mul_deriv
     rw [←mem_closure_iff_clusterPt]
     simp at hx
     rcases le_iff_lt_or_eq.mp hx.1 with h | h
-    . apply (closure_mono (s := Set.Ico a x)) _
+    . apply (closure_mono (s := .Ico a x)) _
       . simp [closure_Ico (show a ≠ x by linarith), hx.1]
-      intro y hy; simp at hy ⊢
-      simp [hy]; exact ⟨ by linarith, by linarith ⟩
-    apply (closure_mono (s := Set.Ioc x b)) _
+      intro y hy; simp at hy ⊢; simp [hy]; constructor <;> linarith
+    apply (closure_mono (s := .Ioc x b)) _
     . simp [closure_Ioc (show x ≠ b by linarith), hx.2]
-    intro y hy; simp at hy ⊢
-    simp [hy]; exact ⟨ by linarith, by linarith ⟩
+    intro y hy; simp at hy ⊢; simp [hy]; constructor <;> linarith
   have h0 := hf.2
   have h1 : RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b) := by
     apply le_of_forall_sub_le
     intro ε hε
     obtain ⟨ h, hhminor, hhconst, hh ⟩ := gt_of_lt_lower_RS_integral hf.1 hα (show RS_integ f (Icc a b) α - ε < lower_RS_integral f (Icc a b) α by linarith)
-    have := PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv hα_diff hαcont hα' hhconst
+    have := hhconst.RS_integ_eq_integ_of_mul_deriv hα_diff hαcont hα'
     rw [←this.2] at hh
     replace : lower_integral (h * α') (Icc a b) = integ (h * α') (Icc a b) := this.1.2
     have why : lower_integral (h * α') (Icc a b) ≤ lower_integral (f * α') (Icc a b) := by
@@ -135,7 +133,7 @@ theorem RS_integ_eq_integ_of_mul_deriv
     apply le_of_forall_pos_le_add
     intro ε hε
     obtain ⟨ h, hhmajor, hhconst, hh ⟩ := lt_of_gt_upper_RS_integral hf.1 hα (show upper_RS_integral f (Icc a b) α + ε > RS_integ f (Icc a b) α by linarith)
-    have := PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv hα_diff hαcont hα' hhconst
+    have := hhconst.RS_integ_eq_integ_of_mul_deriv hα_diff hαcont hα'
     rw [←this.2] at hh
     have why : upper_integral (f * α') (Icc a b) ≤ upper_integral (h * α') (Icc a b) := by
       sorry
@@ -156,7 +154,7 @@ theorem PiecewiseConstantOn.RS_integ_of_comp {a b:ℝ} (hab: a < b) {φ f:ℝ 
     intro J hJ
     simp [P, Partition.remove_empty, Partition.instMembership] at hJ
     exact hf J hJ.1
-  rw [PiecewiseConstantOn.integ_def hf]
+  rw [integ_def hf]
   unfold PiecewiseConstantWith.integ
   set φ_inv : P.intervals → Set ℝ := fun J ↦ { x:ℝ | x ∈ Set.Icc a b ∧ φ x ∈ (J:Set ℝ) }
   have hφ_inv_bounded (J: P.intervals) : Bornology.IsBounded (φ_inv J) := by
@@ -178,7 +176,7 @@ theorem PiecewiseConstantOn.RS_integ_of_comp {a b:ℝ} (hab: a < b) {φ f:ℝ 
     sorry
   have hfφ_piecewise' : PiecewiseConstantOn (f ∘ φ) (Icc a b) := ⟨ Q, hfφ_piecewise ⟩
   refine ⟨ hfφ_piecewise' , ?_ ⟩
-  rw [PiecewiseConstantOn.RS_integ_def hfφ_piecewise _]
+  rw [RS_integ_def hfφ_piecewise _]
   unfold PiecewiseConstantWith.RS_integ
   rw [Finset.sum_image _, ←Finset.sum_coe_sort (s := P.intervals)]
   . apply Finset.sum_congr rfl
diff --git a/analysis/Analysis/Section_11_4.lean b/analysis/Analysis/Section_11_4.lean
index af309f3..416d47a 100644
--- a/analysis/Analysis/Section_11_4.lean
+++ b/analysis/Analysis/Section_11_4.lean
@@ -149,8 +149,7 @@ theorem integ_of_max {I: BoundedInterval} {f g:ℝ → ℝ} (hf: IntegrableOn f
       specialize hg''max x hx
       have hmaxl := le_max_left (f' x) (g' x)
       have hmaxr := le_max_right (f' x) (g' x)
-      simp [h]
-      refine ⟨ by linarith, by linarith ⟩
+      simp [h]; constructor <;> linarith
     have hf'g'_integ := integ_of_piecewise_const hf'g'_const
     have hf''g''_integ := integ_of_piecewise_const hf''g''_const
     have hf'g'h_integ := integ_of_add hf'g'_integ.1 hh_integ_eq.1
diff --git a/analysis/Analysis/Section_11_5.lean b/analysis/Analysis/Section_11_5.lean
index 629224a..80a10ac 100644
--- a/analysis/Analysis/Section_11_5.lean
+++ b/analysis/Analysis/Section_11_5.lean
@@ -179,7 +179,7 @@ theorem integ_of_bdd_cts {I: BoundedInterval} {f:ℝ → ℝ} (hbound: BddOn f I
     have hf' : IntegrableOn f I' := by
       apply integ_of_cts (ContinuousOn.mono hf _)
       apply subset_trans _ ((subset_iff _ _).mp (Ioo_subset I))
-      intro x; simp; intros; exact ⟨ by linarith, by linarith ⟩
+      intro x; simp; intros; constructor <;> linarith
     obtain ⟨ h, hhmin, hhconst, hhint ⟩ := lt_of_gt_upper_integral hf'.1 (show upper_integral f I' < integ f I' + ε by linarith [hf'.2])
     classical
     set h' : ℝ → ℝ := fun x ↦ if x ∈ I' then h x else M
diff --git a/analysis/Analysis/Section_11_6.lean b/analysis/Analysis/Section_11_6.lean
index 70fe2e0..a80def3 100644
--- a/analysis/Analysis/Section_11_6.lean
+++ b/analysis/Analysis/Section_11_6.lean
@@ -99,8 +99,8 @@ theorem integ_of_monotone {a b:ℝ} {f:ℝ → ℝ} (hf: MonotoneOn f (Icc a b))
     }
     have hup := calc
       upper_integral f I ≤ ∑ J ∈ P.intervals, (sSup (f '' (J:Set ℝ))) * |J|ₗ := upper_integ_le_upper_sum hbound P
-      _ = ∑ j ∈ Finset.range N, (sSup (f '' (Ico (a + δ*j) (a + δ*(j+1))))) * |Ico (a + δ*j) (a + δ*(j+1))|ₗ := by simp [P]; congr
-      _ ≤ ∑ j ∈ Finset.range N, f (a + δ*(j+1)) * δ := by
+      _ = ∑ j ∈ .range N, (sSup (f '' (Ico (a + δ*j) (a + δ*(j+1))))) * |Ico (a + δ*j) (a + δ*(j+1))|ₗ := by simp [P]; congr
+      _ ≤ ∑ j ∈ .range N, f (a + δ*(j+1)) * δ := by
         apply Finset.sum_le_sum
         intro j hj
         convert (mul_le_mul_right hδpos).mpr ?_
@@ -113,12 +113,12 @@ theorem integ_of_monotone {a b:ℝ} {f:ℝ → ℝ} (hf: MonotoneOn f (Icc a b))
         have hδj : 0 ≤ δ*j := by positivity
         have hδj1 : 0 ≤ δ*(j+1) := by positivity
         apply hf _ _ (le_of_lt hx2) <;> simp [I, hδj1, this]
-        exact ⟨ by linarith, by linarith ⟩
+        constructor <;> linarith
     have hdown := calc
       lower_integral f I ≥ ∑ J ∈ P.intervals, (sInf (f '' (J:Set ℝ))) * |J|ₗ :=
         lower_integ_ge_lower_sum hbound P
-      _ = ∑ j ∈ Finset.range N, (sInf (f '' (Ico (a + δ*j) (a + δ*(j+1))))) * |Ico (a + δ*j) (a + δ*(j+1))|ₗ := by simp [P]; congr
-      _ ≥ ∑ j ∈ Finset.range N, f (a + δ*j) * δ := by
+      _ = ∑ j ∈ .range N, (sInf (f '' (Ico (a + δ*j) (a + δ*(j+1))))) * |Ico (a + δ*j) (a + δ*(j+1))|ₗ := by simp [P]; congr
+      _ ≥ ∑ j ∈ .range N, f (a + δ*j) * δ := by
         apply Finset.sum_le_sum
         intro j hj
         convert (mul_le_mul_right hδpos).mpr ?_
@@ -130,10 +130,10 @@ theorem integ_of_monotone {a b:ℝ} {f:ℝ → ℝ} (hf: MonotoneOn f (Icc a b))
         have hδj : 0 ≤ δ*j := by positivity
         have hδj1 : 0 ≤ δ*(j+1) := by positivity
         apply hf _ _ hx1
-        . simp [I]; exact ⟨ by linarith, by linarith ⟩
-        simp [I, hδj]; exact ⟨ by linarith, by linarith ⟩
+        . simp [I, hδj]; linarith
+        simp [I, hδj]; constructor <;> linarith
     calc
-      _ ≤ ∑ j ∈ Finset.range N, f (a + δ*(j+1)) * δ - ∑ j ∈ Finset.range N, f (a + δ*j) * δ := by linarith
+      _ ≤ ∑ j ∈ .range N, f (a + δ*(j+1)) * δ - ∑ j ∈ .range N, f (a + δ*j) * δ := by linarith
       _ = (f b - f a) * δ := by
         rw [←Finset.sum_sub_distrib]
         have := Finset.sum_range_sub (fun n ↦ f (a + δ*n) * δ) N
diff --git a/analysis/Analysis/Section_11_9.lean b/analysis/Analysis/Section_11_9.lean
index df74377..4a9784a 100644
--- a/analysis/Analysis/Section_11_9.lean
+++ b/analysis/Analysis/Section_11_9.lean
@@ -41,16 +41,14 @@ theorem cts_of_integ {a b:ℝ} {f:ℝ → ℝ} (hf: IntegrableOn f (Icc a b)) :
       . simp [integ_of_const, le_of_lt hxy]
       intro z hz
       specialize hM z ?_
-      . simp at hz ⊢
-        exact ⟨ by linarith, by linarith ⟩
+      . simp at hz ⊢; constructor <;> linarith
       rw [abs_le'] at hM; simp [hM]
     rw [neg_le]
     convert integ_mono (f := fun _ ↦ -M) (integ_of_const _ _).1 this.1 _
     . simp [integ_of_const, le_of_lt hxy]
     intro z hz
     specialize hM z ?_
-    . simp at hz ⊢
-      exact ⟨ by linarith, by linarith ⟩
+    . simp at hz ⊢; constructor <;> linarith
     rw [abs_le'] at hM; simp; linarith
   replace {x y:ℝ} (hx: x ∈ Set.Icc a b) (hy: y ∈ Set.Icc a b) :
     |F y - F x| ≤ M * |x-y| := by
@@ -231,15 +229,11 @@ theorem integ_eq_antideriv_sub {a b:ℝ} (h:a ≤ b) {f F: ℝ → ℝ}
                   exact ((subset_iff _ _).mp (Ioo_subset J)) he
             rw [←mem_closure_iff_clusterPt]
             apply closure_mono (s := Set.Ioo e d)
-            . intro x hx; simp at he hx ⊢
-              exact ⟨ ⟨ by linarith, by linarith ⟩, by linarith ⟩
-            simp at he
-            rw [closure_Ioo (by linarith)]
-            simp; linarith
-          . simp; rw [Set.Icc_subset_Ioo_iff (le_of_lt hJab)]
-            exact ⟨ by linarith, by linarith ⟩
+            . intro x hx; simp at he hx ⊢; refine ⟨ ⟨ ?_, ?_ ⟩, ?_ ⟩ <;> linarith
+            simp at he; rw [closure_Ioo (by linarith)]; simp; linarith
+          . simp; rw [Set.Icc_subset_Ioo_iff (le_of_lt hJab)]; constructor <;> linarith
           apply DifferentiableOn.congr (f := F)
-          . apply DifferentiableOn.mono hF.1
+          . apply hF.1.mono
             replace hJ := (Ioo_subset J).trans hJ
             simpa [subset_iff] using hJ
           intro x hx
@@ -251,7 +245,7 @@ theorem integ_eq_antideriv_sub {a b:ℝ} (h:a ≤ b) {f F: ℝ → ℝ}
         _ = F' b - F' a := by
           apply α_length_of_cts (by linarith) _ (by linarith) _ hF'_cts
           . simp [le_of_lt h]
-          intro x hx; simp [mem_iff] at hx ⊢; exact ⟨ by linarith, by linarith ⟩
+          intro x hx; simp [mem_iff] at hx ⊢; constructor <;> linarith
         _ = _ := by
           congr 1 <;> apply hFF' <;> simp [le_of_lt h]
     have hlower (P: Partition (Icc a b)) : lower_riemann_sum f P ≤ F b - F a := by
@@ -259,13 +253,12 @@ theorem integ_eq_antideriv_sub {a b:ℝ} (h:a ≤ b) {f F: ℝ → ℝ}
     replace hupper : upper_integral f (Icc a b) ≥ F b - F a := by
       rw [upper_integ_eq_inf_upper_sum hf.1]
       apply le_csInf <;> simp [Set.range_nonempty]
-      intro P; specialize hupper P; linarith
+      intro P; linarith [hupper P]
     replace hlower : lower_integral f (Icc a b) ≤ F b - F a := by
       rw [lower_integ_eq_sup_lower_sum hf.1]
       apply csSup_le <;> simp [Set.range_nonempty]
-      intro P; specialize hlower P; linarith
-    replace hf := hf.2
-    linarith
+      intro P; linarith [hlower P]
+    linarith [hf.2]
   simp [h]
   apply (integ_on_subsingleton _).2
   simp [length]
diff --git a/analysis/Analysis/Section_6_7.lean b/analysis/Analysis/Section_6_7.lean
index ed4d551..7522896 100644
--- a/analysis/Analysis/Section_6_7.lean
+++ b/analysis/Analysis/Section_6_7.lean
@@ -119,7 +119,7 @@ lemma ratPow_lim_uniq {x α:ℝ} (hx: x > 0) {q q': ℕ → ℚ}
     rw [←Real.rpow_neg (by linarith)]
     gcongr; linarith
     simp [r]; linarith
-  exact ⟨ by linarith, by linarith ⟩
+  constructor <;> linarith
 
 theorem Real.eq_lim_of_rat (α:ℝ) : ∃ q: ℕ → ℚ, ((fun n ↦ (q n:ℝ)):Sequence).TendsTo α := by
   obtain ⟨ q, hcauchy, hLIM ⟩ := Chapter5.Real.eq_lim (Chapter5.Real.equivR.symm α); use q
diff --git a/analysis/Analysis/Section_6_epilogue.lean b/analysis/Analysis/Section_6_epilogue.lean
index 2efaec6..5c58422 100644
--- a/analysis/Analysis/Section_6_epilogue.lean
+++ b/analysis/Analysis/Section_6_epilogue.lean
@@ -33,7 +33,7 @@ theorem Chapter6.Sequence.Cauchy_iff_CauchySeq (a: ℕ → ℝ) :
 
 /-- Identification with `Filter.Tendsto` -/
 theorem Chapter6.Sequence.tendsto_iff_Tendsto (a: ℕ → ℝ) (L:ℝ) :
-    (a:Sequence).TendsTo L ↔ Filter.Tendsto a Filter.atTop (nhds L) := by
+    (a:Sequence).TendsTo L ↔ Filter.Tendsto a .atTop (nhds L) := by
   rw [Metric.tendsto_atTop, tendsTo_iff]
   constructor <;> intro h ε hε
   . specialize h (ε/2) (half_pos hε)
@@ -49,7 +49,7 @@ theorem Chapter6.Sequence.tendsto_iff_Tendsto (a: ℕ → ℝ) (L:ℝ) :
   specialize hN n.toNat hn
   simp [hpos, ←Real.dist_eq, le_of_lt hN]
 
-theorem Chapter6.Sequence.tendsto_iff_Tendsto' (a: Sequence) (L:ℝ) : a.TendsTo L ↔ Filter.Tendsto a.seq Filter.atTop (nhds L) := by
+theorem Chapter6.Sequence.tendsto_iff_Tendsto' (a: Sequence) (L:ℝ) : a.TendsTo L ↔ Filter.Tendsto a.seq .atTop (nhds L) := by
   rw [Metric.tendsto_atTop, tendsTo_iff]
   constructor <;> intro h ε hε
   . specialize h (ε/2) (half_pos hε)
@@ -63,10 +63,10 @@ theorem Chapter6.Sequence.tendsto_iff_Tendsto' (a: Sequence) (L:ℝ) : a.TendsTo
   simp [←Real.dist_eq, le_of_lt hN]
 
 theorem Chapter6.Sequence.converges_iff_Tendsto (a: ℕ → ℝ) :
-    (a:Sequence).Convergent ↔ ∃ L, Filter.Tendsto a Filter.atTop (nhds L) := by
+    (a:Sequence).Convergent ↔ ∃ L, Filter.Tendsto a .atTop (nhds L) := by
   simp_rw [←tendsto_iff_Tendsto]
 
-theorem Chapter6.Sequence.converges_iff_Tendsto' (a: Sequence) : a.Convergent ↔ ∃ L, Filter.Tendsto a.seq Filter.atTop (nhds L) := by
+theorem Chapter6.Sequence.converges_iff_Tendsto' (a: Sequence) : a.Convergent ↔ ∃ L, Filter.Tendsto a.seq .atTop (nhds L) := by
   simp_rw [←tendsto_iff_Tendsto']
 
 /-- A technicality: `CauSeq.IsComplete ℝ` was established for `_root_.abs` but not for `norm`. -/
@@ -122,7 +122,7 @@ theorem Chapter6.Sequence.Antitone_iff (a:ℕ → ℝ): (a:Sequence).IsAntitone
 
 /-- Identification with `MapClusterPt` -/
 theorem Chapter6.Sequence.limit_point_iff (a:ℕ → ℝ) (L:ℝ) :
-    (a:Sequence).LimitPoint L ↔ MapClusterPt L Filter.atTop a := by
+    (a:Sequence).LimitPoint L ↔ MapClusterPt L .atTop a := by
   simp_rw [limit_point_def, mapClusterPt_iff_frequently,
            Filter.frequently_atTop, Metric.mem_nhds_iff]
   constructor
@@ -144,13 +144,13 @@ theorem Chapter6.Sequence.limit_point_iff (a:ℕ → ℝ) (L:ℝ) :
 
 /-- Identification with `Filter.limsup` -/
 theorem Chapter6.Sequence.limsup_eq (a:ℕ → ℝ) :
-    (a:Sequence).limsup = Filter.limsup (fun n ↦ (a n:EReal)) Filter.atTop := by
+    (a:Sequence).limsup = Filter.limsup (fun n ↦ (a n:EReal)) .atTop := by
   simp_rw [Filter.limsup_eq, Filter.eventually_atTop]
   sorry
 
 /-- Identification with `Filter.liminf` -/
 theorem Chapter6.Sequence.liminf_eq (a:ℕ → ℝ) :
-    (a:Sequence).liminf = Filter.liminf (fun n ↦ (a n:EReal)) Filter.atTop := by
+    (a:Sequence).liminf = Filter.liminf (fun n ↦ (a n:EReal)) .atTop := by
   simp_rw [Filter.liminf_eq, Filter.eventually_atTop]
   sorry
 
diff --git a/analysis/Analysis/Section_7_1.lean b/analysis/Analysis/Section_7_1.lean
index fd4fb07..43fb675 100644
--- a/analysis/Analysis/Section_7_1.lean
+++ b/analysis/Analysis/Section_7_1.lean
@@ -323,8 +323,8 @@ theorem binomial_theorem (x y:ℝ) (n:ℕ) :
 
 /-- Exercise 7.1.5 -/
 theorem lim_of_finite_series {X:Type*} [Fintype X] (a: X → ℕ → ℝ) (L : X → ℝ)
-  (h: ∀ x, Filter.Tendsto (a x) Filter.atTop (nhds (L x))) :
-    Filter.Tendsto (fun n ↦ ∑ x, a x n) Filter.atTop (nhds (∑ x, L x)) := by
+  (h: ∀ x, Filter.Tendsto (a x) .atTop (nhds (L x))) :
+    Filter.Tendsto (fun n ↦ ∑ x, a x n) .atTop (nhds (∑ x, L x)) := by
   sorry
 
 
diff --git a/analysis/Analysis/Section_7_2.lean b/analysis/Analysis/Section_7_2.lean
index ad3f874..7f5680f 100644
--- a/analysis/Analysis/Section_7_2.lean
+++ b/analysis/Analysis/Section_7_2.lean
@@ -65,7 +65,7 @@ theorem Series.partial_of_lt {s : Series} {N:ℤ} (h: N < s.m) : s.partial N = 0
   rw [Finset.sum_eq_zero]
   intro n hn; simp at hn; linarith
 
-abbrev Series.convergesTo (s : Series) (L:ℝ) : Prop := Filter.Tendsto (s.partial) Filter.atTop (nhds L)
+abbrev Series.convergesTo (s : Series) (L:ℝ) : Prop := Filter.Tendsto (s.partial) .atTop (nhds L)
 
 abbrev Series.converges (s : Series) : Prop := ∃ L, s.convergesTo L
 
@@ -112,10 +112,10 @@ theorem Series.converges_iff_tail_decay (s:Series) :
 
 /-- Corollary 7.2.6 (Zero test) / Exercise 7.2.3 -/
 theorem Series.decay_of_converges {s:Series} (h: s.converges) :
-    Filter.Tendsto s.seq Filter.atTop (nhds 0) := by
+    Filter.Tendsto s.seq .atTop (nhds 0) := by
   sorry
 
-theorem Series.diverges_of_nodecay {s:Series} (h: ¬ Filter.Tendsto s.seq Filter.atTop (nhds 0)) :
+theorem Series.diverges_of_nodecay {s:Series} (h: ¬ Filter.Tendsto s.seq .atTop (nhds 0)) :
     s.diverges := by
   sorry
 
@@ -145,7 +145,7 @@ theorem Series.abs_le {s:Series} (h : s.absConverges) : |s.sum| ≤ s.abs.sum :=
 /-- Proposition 7.2.12 (Alternating series test) -/
 theorem Series.converges_of_alternating {m:ℤ} {a: { n // n ≥ m} → ℝ} (ha: ∀ n, a n ≥ 0)
   (ha': Antitone a) :
-    ((mk' (fun n ↦ (-1)^(n:ℤ) * a n)).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0)) := by
+    ((mk' (fun n ↦ (-1)^(n:ℤ) * a n)).converges ↔ Filter.Tendsto a .atTop (nhds 0)) := by
   -- This proof is written to follow the structure of the original text.
   constructor
   . intro h; replace h := decay_of_converges h
@@ -278,7 +278,7 @@ theorem Series.shift {s:Series} {x:ℝ} (h: s.convergesTo x) (L:ℤ) :
   sorry
 
 /-- Lemma 7.2.15 (telescoping series) / Exercise 7.2.6 -/
-theorem Series.telescope {a:ℕ → ℝ} (ha: Filter.Tendsto a Filter.atTop (nhds 0)) :
+theorem Series.telescope {a:ℕ → ℝ} (ha: Filter.Tendsto a .atTop (nhds 0)) :
     ((fun n:ℕ ↦ a (n+1) - a n):Series).convergesTo (a 0) := by
   sorry
 
diff --git a/analysis/Analysis/Section_7_3.lean b/analysis/Analysis/Section_7_3.lean
index 7f437d6..45587ae 100644
--- a/analysis/Analysis/Section_7_3.lean
+++ b/analysis/Analysis/Section_7_3.lean
@@ -205,7 +205,7 @@ theorem Series.zeta_eq {q:ℝ} (hq: q > 1) : (mk' (m := 1) fun n ↦ 1 / (n:ℝ)
   have : Summable (fun (n : ℕ)↦ 1 / (n+1:ℝ) ^ q) := by
     convert (Real.summable_one_div_nat_add_rpow 1 q).mpr hq using 4 with n
     rw [abs_of_nonneg (by positivity)]
-  have tail (a: ℤ → ℝ) (L:ℝ) : Filter.Tendsto a Filter.atTop (nhds L) ↔ Filter.Tendsto (fun n:ℕ ↦ a n) Filter.atTop (nhds L) := by
+  have tail (a: ℤ → ℝ) (L:ℝ) : Filter.Tendsto a .atTop (nhds L) ↔ Filter.Tendsto (fun n:ℕ ↦ a n) .atTop (nhds L) := by
     convert Filter.tendsto_map'_iff (g:= fun n:ℕ ↦ (n:ℤ) )
     simp
   unfold convergesTo
diff --git a/analysis/Analysis/Section_7_5.lean b/analysis/Analysis/Section_7_5.lean
index 494ac00..0e6ce00 100644
--- a/analysis/Analysis/Section_7_5.lean
+++ b/analysis/Analysis/Section_7_5.lean
@@ -21,9 +21,9 @@ namespace Chapter7
 
 /-- Theorem 7.5.1(a) (Root test).  A technical condition is needed to ensure the limsup is finite. -/
 theorem Series.root_test_pos {s : Series}
-  (h : Filter.limsup (fun n ↦ ((|s.seq n|^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop < 1) : s.absConverges := by
+  (h : Filter.limsup (fun n ↦ ((|s.seq n|^(1/(n:ℝ)):ℝ):EReal)) .atTop < 1) : s.absConverges := by
     -- This proof is written to follow the structure of the original text.
-    set α':EReal := Filter.limsup (fun n ↦ ((|s.seq n|^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop
+    set α':EReal := Filter.limsup (fun n ↦ ((|s.seq n|^(1/(n:ℝ)):ℝ):EReal)) .atTop
     have hpos : 0 ≤ α' := by
       apply Filter.le_limsup_of_frequently_le (Filter.Frequently.of_forall _) (by isBoundedDefault)
       intros; positivity
@@ -75,7 +75,7 @@ theorem Series.root_test_pos {s : Series}
 
 /-- Theorem 7.5.1(b) (Root test) -/
 theorem Series.root_test_neg {s : Series}
-  (h : Filter.limsup (fun n ↦ ((|s.seq n|^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop > 1) : s.diverges := by
+  (h : Filter.limsup (fun n ↦ ((|s.seq n|^(1/(n:ℝ)):ℝ):EReal)) .atTop > 1) : s.diverges := by
     -- This proof is written to follow the structure of the original text.
     replace h := Filter.frequently_lt_of_lt_limsup (by isBoundedDefault) h
     apply diverges_of_nodecay
@@ -87,27 +87,27 @@ theorem Series.root_test_neg {s : Series}
 
 /-- Theorem 7.5.1(c) (Root test) / Exercise 7.5.3 -/
 theorem Series.root_test_inconclusive: ∃ s:Series,
-  Filter.Tendsto (fun n ↦ |s.seq n|^(1/(n:ℝ))) Filter.atTop (nhds 1) ∧ s.diverges := by
+  Filter.Tendsto (fun n ↦ |s.seq n|^(1/(n:ℝ))) .atTop (nhds 1) ∧ s.diverges := by
     sorry
 
 /-- Theorem 7.5.1 (Root test) / Exercise 7.5.3 -/
 theorem Series.root_test_inconclusive' : ∃ s:Series,
-  Filter.Tendsto (fun n ↦ |s.seq n|^(1/(n:ℝ))) Filter.atTop (nhds 1) ∧ s.absConverges := by
+  Filter.Tendsto (fun n ↦ |s.seq n|^(1/(n:ℝ))) .atTop (nhds 1) ∧ s.absConverges := by
     sorry
 
 /-- Lemma 7.5.2 / Exercise 7.5.1 -/
 theorem Series.ratio_ineq {c:ℤ → ℝ} (m:ℤ) (hpos: ∀ n ≥ m, c n > 0) :
-  Filter.liminf (fun n ↦ ((c (n+1) / c n:ℝ): EReal)) Filter.atTop ≤
-    Filter.liminf (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop
-  ∧ Filter.liminf (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop ≤
-    Filter.limsup (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop
-  ∧ Filter.limsup (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop ≤
-    Filter.limsup (fun n ↦ ((c (n+1) / c n:ℝ):EReal)) Filter.atTop
+  Filter.liminf (fun n ↦ ((c (n+1) / c n:ℝ): EReal)) .atTop ≤
+    Filter.liminf (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) .atTop
+  ∧ Filter.liminf (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) .atTop ≤
+    Filter.limsup (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) .atTop
+  ∧ Filter.limsup (fun n ↦ (((c n)^(1/(n:ℝ)):ℝ):EReal)) .atTop ≤
+    Filter.limsup (fun n ↦ ((c (n+1) / c n:ℝ):EReal)) .atTop
     := by
   -- This proof is written to follow the structure of the original text.
   refine ⟨ ?_, Filter.liminf_le_limsup (by isBoundedDefault) (by isBoundedDefault), ?_ ⟩
   . sorry
-  set L' := Filter.limsup (fun n ↦ ((c (n+1) / c n:ℝ):EReal)) Filter.atTop
+  set L' := Filter.limsup (fun n ↦ ((c (n+1) / c n:ℝ):EReal)) .atTop
   by_cases hL : L' = ⊤; simp [hL]
   have hL'pos : 0 ≤ L' := by
     apply Filter.le_limsup_of_frequently_le'
@@ -160,11 +160,11 @@ theorem Series.ratio_ineq {c:ℤ → ℝ} (m:ℤ) (hpos: ∀ n ≥ m, c n > 0) :
         convert (Real.rpow_one _)
         field_simp
   calc
-    _ ≤ Filter.limsup (fun n:ℤ ↦ ((A^(1/(n:ℝ)) * (L+ε):ℝ):EReal)) Filter.atTop := by
+    _ ≤ Filter.limsup (fun n:ℤ ↦ ((A^(1/(n:ℝ)) * (L+ε):ℝ):EReal)) .atTop := by
       apply Filter.limsup_le_limsup _ (by isBoundedDefault) (by isBoundedDefault)
       unfold Filter.EventuallyLE; rw [Filter.eventually_atTop]
       use N
-    _ ≤ (Filter.limsup (fun n:ℤ ↦ ((A^(1/(n:ℝ)):ℝ):EReal)) Filter.atTop) * (Filter.limsup (fun n:ℤ ↦ ((L+ε:ℝ):EReal)) Filter.atTop) := by
+    _ ≤ (Filter.limsup (fun n:ℤ ↦ ((A^(1/(n:ℝ)):ℝ):EReal)) .atTop) * (Filter.limsup (fun n:ℤ ↦ ((L+ε:ℝ):EReal)) .atTop) := by
       convert EReal.limsup_mul_le _ _ _ _ with n
       . rfl
       . apply Filter.Frequently.of_forall; intros; positivity
@@ -184,7 +184,7 @@ theorem Series.ratio_ineq {c:ℤ → ℝ} (m:ℤ) (hpos: ∀ n ≥ m, c n > 0) :
 
 /-- Corollary 7.5.3 (Ratio test)-/
 theorem Series.ratio_test_pos {s : Series} (hnon: ∀ n ≥ s.m, s.seq n ≠ 0)
-  (h : Filter.limsup (fun n ↦ ((|s.seq (n+1)| / |s.seq n|:ℝ):EReal)) Filter.atTop < 1) : s.absConverges := by
+  (h : Filter.limsup (fun n ↦ ((|s.seq (n+1)| / |s.seq n|:ℝ):EReal)) .atTop < 1) : s.absConverges := by
     apply Series.root_test_pos (lt_of_le_of_lt _ h)
     convert (ratio_ineq s.m _).2.2
     convert hnon using 1 with n
@@ -192,19 +192,19 @@ theorem Series.ratio_test_pos {s : Series} (hnon: ∀ n ≥ s.m, s.seq n ≠ 0)
 
 /-- Corollary 7.5.3 (Ratio test)-/
 theorem Series.ratio_test_neg {s : Series} (hnon: ∀ n ≥ s.m, s.seq n ≠ 0)
-  (h : Filter.liminf (fun n ↦ ((|s.seq (n+1)| / |s.seq n|:ℝ):EReal)) Filter.atTop > 1) : s.diverges := by
+  (h : Filter.liminf (fun n ↦ ((|s.seq (n+1)| / |s.seq n|:ℝ):EReal)) .atTop > 1) : s.diverges := by
     apply Series.root_test_neg (lt_of_lt_of_le h _)
     convert (ratio_ineq s.m _).1.trans (ratio_ineq s.m _).2.1 with n; rfl
     all_goals convert hnon using 1 with n; simp
 
 /-- Corollary 7.5.3 (Ratio test) / Exercise 7.5.3 -/
 theorem Series.ratio_test_inconclusive: ∃ s:Series, (∀ n ≥ s.m, s.seq n ≠ 0) ∧
-  Filter.Tendsto (fun n ↦ |s.seq n+1| / |s.seq n|) Filter.atTop (nhds 1) ∧ s.diverges := by
+  Filter.Tendsto (fun n ↦ |s.seq n+1| / |s.seq n|) .atTop (nhds 1) ∧ s.diverges := by
     sorry
 
 /-- Corollary 7.5.3 (Ratio test) / Exercise 7.5.3 -/
 theorem Series.ratio_test_inconclusive' : ∃ s:Series, (∀ n ≥ s.m, s.seq n ≠ 0) ∧
-  Filter.Tendsto (fun n ↦ |s.seq n+1| / |s.seq n|) Filter.atTop (nhds 1) ∧ s.absConverges := by
+  Filter.Tendsto (fun n ↦ |s.seq n+1| / |s.seq n|) .atTop (nhds 1) ∧ s.absConverges := by
     sorry
 
 /-- Proposition 7.5.4 -/
@@ -213,7 +213,7 @@ theorem Series.root_self_converges : (fun (n:ℕ) ↦ (n:ℝ)^(1 / n : ℝ) : Se
   sorry
 
 /-- Exercise 7.5.2 -/
-theorem Series.poly_mul_geom_converges {x:ℝ} (hx: |x|<1) (q:ℝ) : (fun n:ℕ ↦ (n:ℝ)^q * x^n : Series).converges ∧ Filter.Tendsto (fun n:ℕ ↦ (n:ℝ)^q * x^n) Filter.atTop (nhds 0) := by
+theorem Series.poly_mul_geom_converges {x:ℝ} (hx: |x|<1) (q:ℝ) : (fun n:ℕ ↦ (n:ℝ)^q * x^n : Series).converges ∧ Filter.Tendsto (fun n:ℕ ↦ (n:ℝ)^q * x^n) .atTop (nhds 0) := by
   sorry
 
 
diff --git a/analysis/Analysis/Section_8_1.lean b/analysis/Analysis/Section_8_1.lean
index 27b23af..98c757c 100644
--- a/analysis/Analysis/Section_8_1.lean
+++ b/analysis/Analysis/Section_8_1.lean
@@ -27,18 +27,14 @@ the Chapter 3 set theory is deprecated. -/
 abbrev EqualCard (X Y : Type) : Prop := ∃ f : X → Y, Function.Bijective f
 
 /-- Relation with Mathlib's `Equiv` concept -/
-theorem EqualCard.iff {X Y : Type} :
-  EqualCard X Y ↔ Nonempty (X ≃ Y) := by
+theorem EqualCard.iff {X Y : Type} : EqualCard X Y ↔ Nonempty (X ≃ Y) := by
   simp [EqualCard]
   constructor
-  . rintro ⟨ f, hf ⟩
-    exact ⟨ Equiv.ofBijective f hf ⟩
-  rintro ⟨ e ⟩
-  exact ⟨ e.toFun, e.bijective ⟩
+  . rintro ⟨ f, hf ⟩; exact ⟨ Equiv.ofBijective f hf ⟩
+  rintro ⟨ e ⟩; exact ⟨ e.toFun, e.bijective ⟩
 
 /-- Equivalence with Mathlib's `Cardinal.mk` concept -/
-theorem EqualCard.iff' {X Y : Type} :
-  EqualCard X Y ↔ Cardinal.mk X = Cardinal.mk Y := by
+theorem EqualCard.iff' {X Y : Type} : EqualCard X Y ↔ Cardinal.mk X = Cardinal.mk Y := by
   simp [Cardinal.eq, iff]
 
 theorem EqualCard.refl (X : Type) : EqualCard X X := sorry
@@ -60,10 +56,7 @@ abbrev CountablyInfinite (X : Type) : Prop := EqualCard X ℕ
 abbrev AtMostCountable (X : Type) : Prop := CountablyInfinite X ∨ Finite X
 
 theorem CountablyInfinite.equiv {X Y: Type} (hXY : EqualCard X Y) :
-  CountablyInfinite X ↔ CountablyInfinite Y := by
-  constructor <;> intro h
-  . exact hXY.symm.trans h
-  exact hXY.trans h
+  CountablyInfinite X ↔ CountablyInfinite Y := ⟨ hXY.symm.trans, hXY.trans ⟩
 
 theorem Finite.equiv {X Y: Type} (hXY : EqualCard X Y) :
   Finite X ↔ Finite Y := by
@@ -92,9 +85,9 @@ theorem CountablyInfinite.toInfinite {X : Type} (hX: CountablyInfinite X) : Infi
   rw [iff'] at hX; tauto
 
 theorem AtMostCountable.iff (X : Type) : AtMostCountable X ↔ Countable X := by
-  have h1 := CountablyInfinite.iff' X
-  have h2 : Finite X ∨ Infinite X := finite_or_infinite _
-  have h3 : Finite X → Countable X := by intro h; exact Finite.to_countable
+  observe h1 : CountablyInfinite X ↔ Countable X ∧ Infinite X
+  observe h2 : Finite X ∨ Infinite X
+  observe h3 : Finite X → Countable X
   unfold AtMostCountable; tauto
 
 theorem CountablyInfinite.iff_image_inj {A:Type} (X: Set A) : CountablyInfinite X ↔ ∃ f : ℕ ↪ A, X = f '' Set.univ := by
@@ -102,8 +95,7 @@ theorem CountablyInfinite.iff_image_inj {A:Type} (X: Set A) : CountablyInfinite
   . rintro ⟨ g, hg ⟩
     obtain ⟨ f, hleft, hright ⟩ := Function.bijective_iff_has_inverse.mp hg
     refine ⟨ ⟨ Subtype.val ∘ f, ?_ ⟩, ?_ ⟩
-    . intro x y hxy; simp [Subtype.val_inj] at hxy
-      rw [←hright x, ←hright y, hxy]
+    . intro x y hxy; simp [Subtype.val_inj] at hxy; rw [←hright x, ←hright y, hxy]
     ext x; simp; constructor
     . intro hx; use g ⟨ x, hx ⟩; simp [hleft _]
     rintro ⟨ n, rfl ⟩; aesop
@@ -117,8 +109,7 @@ theorem CountablyInfinite.iff_image_inj {A:Type} (X: Set A) : CountablyInfinite
     obtain ⟨ n, rfl ⟩ := hx
     obtain ⟨ m, rfl ⟩ := hy
     simp [this n, this m] at h; aesop
-  intro n; use ⟨ f n, by aesop ⟩
-  simp [this n]
+  intro n; use ⟨ f n, by aesop ⟩; simp [this n]
 
 /-- Examples 8.1.3 -/
 example : CountablyInfinite ℕ := by sorry
@@ -147,8 +138,7 @@ noncomputable abbrev Nat.min (X : Set ℕ) : ℕ := if hX : X.Nonempty then (exi
 
 theorem Nat.min_spec {X : Set ℕ} (hX : X.Nonempty) :
   min X ∈ X ∧ ∀ n ∈ X, min X ≤ n := by
-  simp [hX, min]
-  exact (exists_unique_min hX).exists.choose_spec
+  simp [hX, min]; exact (exists_unique_min hX).exists.choose_spec
 
 theorem Nat.min_eq {X : Set ℕ} (hX : X.Nonempty) {a:ℕ} (ha : a ∈ X ∧ ∀ n ∈ X, a ≤ n) : min X = a :=
   (exists_unique_min hX).unique (min_spec hX) ha
@@ -165,9 +155,7 @@ open Classical in
 /-- Equivalence with Mathlib's `Nat.find` method -/
 theorem Nat.min_eq_find {X : Set ℕ} (hX : X.Nonempty) : min X = Nat.find hX := by
   symm; rw [Nat.find_eq_iff]
-  have := min_spec hX
-  simp [this]
-  intro n hn; contrapose! hn; exact this.2 n hn
+  have := min_spec hX; simp [this]; intro n hn; contrapose! hn; exact this.2 n hn
 
 /-- Proposition 8.1.5 -/
 theorem Nat.monotone_enum_of_infinite (X : Set ℕ) [Infinite X] : ∃! f : ℕ → X, Function.Bijective f ∧ StrictMono f := by
@@ -185,38 +173,30 @@ theorem Nat.monotone_enum_of_infinite (X : Set ℕ) [Infinite X] : ∃! f : ℕ
     sorry
   set f : ℕ → X := fun n ↦ ⟨ a n, haX n ⟩
   have hf_injective : Function.Injective f := by
-    intro x y hxy; simp [f] at hxy
-    solve_by_elim
+    intro x y hxy; simp [f] at hxy; solve_by_elim
   have hf_surjective : Function.Surjective f := by
-    rintro ⟨ x, hx ⟩
-    simp [f]; by_contra
+    rintro ⟨ x, hx ⟩; simp [f]; by_contra
     have h1 (n:ℕ) : x ∈ { x ∈ X | ∀ (m:ℕ) (h:m < n), x ≠ a m } := by
       sorry
     have h2 (n:ℕ) : x ≥ a n := by
-      rw [ha n]
-      exact ge_iff_le.mpr ((min_spec (ha_nonempty n)).2 _ (h1 n))
+      rw [ha n]; exact ge_iff_le.mpr ((min_spec (ha_nonempty n)).2 _ (h1 n))
     have h3 (n:ℕ) : a n ≥ n := by
       sorry
     have h4 (n:ℕ) : x ≥ n := (h3 n).trans (h2 n)
     linarith [h4 (x+1)]
-  have hf_bijective : Function.Bijective f := ⟨ hf_injective, hf_surjective ⟩
-  apply ExistsUnique.intro f ⟨ hf_bijective, ha_mono ⟩
-  rintro g ⟨ hg_bijective, hg_mono ⟩
-  by_contra!
+  apply ExistsUnique.intro f ⟨ ⟨ hf_injective, hf_surjective ⟩, ha_mono ⟩
+  rintro g ⟨ hg_bijective, hg_mono ⟩; by_contra!
   replace : { n | g n ≠ f n }.Nonempty := by
     contrapose! this
     simp [Set.eq_empty_iff_forall_notMem] at this
     ext n; simp [this n]
   set m := min { n | g n ≠ f n }
   have hm : g m ≠ f m := (min_spec this).1
-  have hm' {n:ℕ} (hn: n < m) : g n = f n := by
-    by_contra hgfn
-    linarith [(min_spec this).2 n (by simp [hgfn])]
+  have hm' {n:ℕ} (hn: n < m) : g n = f n := by by_contra hgfn; linarith [(min_spec this).2 n (by simp [hgfn])]
   have hgm : g m = min { x ∈ X | ∀ (n:ℕ) (h:n < m), x ≠ a n } := by
     sorry
   rw [←ha m] at hgm
-  contrapose! hm
-  exact Subtype.val_injective hgm
+  contrapose! hm; exact Subtype.val_injective hgm
 
 theorem Nat.countable_of_infinite (X : Set ℕ) [Infinite X] : CountablyInfinite X := by
   apply EqualCard.symm
@@ -238,20 +218,17 @@ theorem AtMostCountable.subset {X: Type} (hX : AtMostCountable X) (Y: Set X) : A
     let f' : Y → f '' Y := fun y ↦ ⟨ f y, by aesop ⟩
     have hf' : Function.Bijective f' := by
       sorry
-    rw [AtMostCountable.equiv ⟨ f', hf' ⟩ ]
-    exact Nat.atMostCountable_subset _
+    rw [AtMostCountable.equiv ⟨ f', hf' ⟩ ]; exact Nat.atMostCountable_subset _
   simp [AtMostCountable, show Finite Y by infer_instance]
 
 theorem AtMostCountable.subset' {A: Type} {X Y: Set A} (hX: AtMostCountable X) (hY: Y ⊆ X) : AtMostCountable Y := by
   set Y' := { x : X | ↑x ∈ Y }
   have : AtMostCountable Y' := subset hX _
-  apply (AtMostCountable.equiv _).mp this
-  use (fun y ↦ ⟨ y.val.val, y.property ⟩ )
+  apply (equiv _).mp this
+  use (fun y ↦ ⟨ ↑↑y, y.property ⟩ )
   constructor
-  . rintro ⟨ ⟨ y, hy ⟩, hy2 ⟩ ⟨ ⟨ y', hy' ⟩, hy2' ⟩ h
-    simp [Y'] at hy hy2 hy' hy2' h ⊢; assumption
-  rintro ⟨ y, hy ⟩
-  use ⟨ ⟨ y, hY hy ⟩, by aesop ⟩
+  . rintro ⟨ ⟨ y, hy ⟩, hy2 ⟩ ⟨ ⟨ y', hy' ⟩, hy2' ⟩ h; simp_all [Y']
+  rintro ⟨ y, hy ⟩; use ⟨ ⟨ y, hY hy ⟩, by aesop ⟩
 
 /-- Proposition 8.1.8 / Exercise 8.1.4 -/
 theorem AtMostCountable.image_nat (Y: Type) (f: ℕ → Y) : AtMostCountable (f '' Set.univ) := by
@@ -281,45 +258,42 @@ theorem Int.countablyInfinite : CountablyInfinite ℤ := by
     ext n; simp; constructor
     . intro h; use (-n).toNat; simp [h]
     rintro ⟨ m, rfl ⟩; simp
-  have : CountablyInfinite (Set.univ : Set ℤ) := by
-    convert CountablyInfinite.union h1 h2
-    ext n; simp; omega
-  exact (CountablyInfinite.equiv (EqualCard.univ _)).mp this
+  have : CountablyInfinite (.univ : Set ℤ) := by
+    convert CountablyInfinite.union h1 h2; ext n; simp; omega
+  exact (CountablyInfinite.equiv (.univ _)).mp this
 
 /-- Lemma 8.1.12 -/
 theorem CountablyInfinite.lower_diag : CountablyInfinite { n : ℕ × ℕ | n.2 ≤ n.1 } := by
   -- This proof is written to follow the structure of the original text.
   let A := { n : ℕ × ℕ | n.2 ≤ n.1 }
-  let a : ℕ → ℕ := fun n ↦ ∑ m ∈ Finset.range (n+1), m
+  let a : ℕ → ℕ := fun n ↦ ∑ m ∈ .range (n+1), m
   have ha : StrictMono a := by
     sorry
   let f : A → ℕ := fun ⟨ (n, m), _ ⟩ ↦ a n + m
   have hf : Function.Injective f := by
-    rintro ⟨ ⟨ n, m ⟩, hnm ⟩ ⟨ ⟨ n',m'⟩, hn'm' ⟩ h
-    simp [A,f] at hnm hn'm' ⊢ h
+    rintro ⟨ ⟨ n, m ⟩, hnm ⟩ ⟨ ⟨ n',m'⟩, hnm' ⟩ h
+    simp [A,f] at hnm hnm' ⊢ h
     rcases lt_trichotomy n n' with hnn' | rfl | hnn'
     . have : a n' + m' > a n + m := by calc
         _ ≥ a n' := by linarith
-        _ ≥ a (n+1) := by apply (StrictMono.monotone ha); linarith
+        _ ≥ a (n+1) := ha.monotone (by linarith)
         _ = a n + (n + 1) := Finset.sum_range_succ (fun x ↦ x) _
         _ > a n + m := by linarith
       linarith
     . simp at h; tauto
     have : a n + m > a n' + m' := by calc
         _ ≥ a n := by linarith
-        _ ≥ a (n'+1) := by apply (StrictMono.monotone ha); linarith
+        _ ≥ a (n'+1) := ha.monotone (by linarith)
         _ = a n' + (n' + 1) := Finset.sum_range_succ (fun x ↦ x) _
         _ > a n' + m' := by linarith
     linarith
-  let f' : A → f '' Set.univ := fun p ↦ ⟨ f p, by aesop ⟩
+  let f' : A → f '' .univ := fun p ↦ ⟨ f p, by aesop ⟩
   have hf' : Function.Bijective f' := by
     constructor
     . intro p q hpq; simp [f'] at hpq; solve_by_elim
     rintro ⟨ l, hl ⟩; simp at hl
     obtain ⟨ n, m, q, rfl ⟩ := hl; use ⟨ (n, m), q ⟩
-  have : AtMostCountable A := by
-    rw [AtMostCountable.equiv ⟨ f', hf' ⟩]
-    exact Nat.atMostCountable_subset _
+  have : AtMostCountable A := by rw [AtMostCountable.equiv ⟨ f', hf' ⟩]; exact Nat.atMostCountable_subset _
   have hfin : ¬ Finite A := by
     sorry
   simp [AtMostCountable] at this; tauto
@@ -327,17 +301,14 @@ theorem CountablyInfinite.lower_diag : CountablyInfinite { n : ℕ × ℕ | n.2
 /-- Corollary 8.1.13 -/
 theorem CountablyInfinite.prod_nat : CountablyInfinite (ℕ × ℕ) := by
   have upper_diag : CountablyInfinite { n : ℕ × ℕ | n.1 ≤ n.2 } := by
-    apply (CountablyInfinite.equiv _).mp lower_diag
+    apply (equiv _).mp lower_diag
     use fun ⟨ (n, m), hnm ⟩ ↦ ⟨ (m, n), by aesop ⟩
     constructor
-    . intro ⟨ (n, m), hnm ⟩ ⟨ (n', m'), hn'm' ⟩ h
-      simp at hnm hn'm' h ⊢; tauto
-    intro ⟨ (n, m), hnm ⟩
-    use ⟨ (m, n), by aesop ⟩
-  have : CountablyInfinite (Set.univ : Set (ℕ × ℕ)) := by
-    convert CountablyInfinite.union lower_diag upper_diag
-    ext ⟨ n, m ⟩; simp; omega
-  exact (CountablyInfinite.equiv (EqualCard.univ _)).mp this
+    . intro ⟨ (n, m), hnm ⟩ ⟨ (n', m'), hn'm' ⟩ h; simp at hnm hn'm' h ⊢; tauto
+    intro ⟨ (n, m), hnm ⟩; use ⟨ (m, n), by aesop ⟩
+  have : CountablyInfinite (.univ : Set (ℕ × ℕ)) := by
+    convert union lower_diag upper_diag; ext ⟨ n, m ⟩; simp; omega
+  exact (equiv (.univ _)).mp this
 
 /-- Corollary 8.1.14 / Exercise 8.1.8 -/
 theorem CountablyInfinite.prod {X Y:Type} (hX: CountablyInfinite X) (hY: CountablyInfinite Y) :
@@ -349,16 +320,15 @@ theorem Rat.countablyInfinite : CountablyInfinite ℚ := by
   -- This proof is written to follow the structure of the original text.
   have : CountablyInfinite { n:ℤ | n ≠ 0 } := by
     sorry
-  replace :  CountablyInfinite (ℤ × { n:ℤ | n ≠ 0 }) :=
-    CountablyInfinite.prod Int.countablyInfinite this
+  replace :  CountablyInfinite (ℤ × { n:ℤ | n ≠ 0 }) := Int.countablyInfinite.prod this
   let f : ℤ × { n:ℤ | n ≠ 0 } → ℚ := fun (a,b) ↦ (a/b:ℚ)
   replace := AtMostCountable.image this f
-  have h : f '' Set.univ = Set.univ := by
+  have h : f '' .univ = .univ := by
     sorry
   simp [h, AtMostCountable.equiv (EqualCard.univ _), AtMostCountable] at this
   have hfin : ¬ Finite ℚ := by
     by_contra!
-    replace : Finite (Set.univ : Set ℕ) := by
+    replace : Finite (.univ : Set ℕ) := by
       apply Finite.Set.finite_of_finite_image (f := fun n:ℕ ↦ (n:ℚ))
       intro x _ y _; simp
     rw [Set.finite_coe_iff, Set.finite_univ_iff,←not_infinite_iff_finite] at this
diff --git a/analysis/Analysis/Section_8_2.lean b/analysis/Analysis/Section_8_2.lean
index 70c6849..9aaedb6 100644
--- a/analysis/Analysis/Section_8_2.lean
+++ b/analysis/Analysis/Section_8_2.lean
@@ -54,8 +54,7 @@ theorem AbsConvergent.comp {X: Type} {f:X → ℝ} {g:ℕ → X} (h: Function.Bi
   obtain ⟨ hbij, hconv ⟩ := hf.choose_spec
   set g' := hf.choose
   obtain ⟨ g'_inv, hleft, hright ⟩ := Function.bijective_iff_has_inverse.mp hbij
-  have hG : Function.Bijective (g'_inv ∘ g) :=
-    Function.Bijective.comp ⟨ Function.LeftInverse.injective hright, Function.RightInverse.surjective hleft⟩ h
+  have hG : Function.Bijective (g'_inv ∘ g) := .comp ⟨hright.injective, hleft.surjective⟩ h
   convert (Series.absConverges_of_permute hconv hG).1 using 4 with n
   simp [hright (g n.toNat)]
 
@@ -66,8 +65,7 @@ theorem Sum.eq {X: Type} {f:X → ℝ} {g:ℕ → X} (h: Function.Bijective g) (
   set g' := this.choose
   obtain ⟨ g'_inv, hleft, hright ⟩ := Function.bijective_iff_has_inverse.mp hbij
   convert Series.convergesTo_sum (Series.converges_of_absConverges hfg) using 1
-  have hG : Function.Bijective (g'_inv ∘ g) :=
-    Function.Bijective.comp ⟨ Function.LeftInverse.injective hright, Function.RightInverse.surjective hleft⟩ h
+  have hG : Function.Bijective (g'_inv ∘ g) := .comp ⟨hright.injective, hleft.surjective⟩ h
   convert (Series.absConverges_of_permute hconv hG).2 using 4 with _ n
   by_cases hn : n ≥ 0 <;> simp [hn, hright (g n.toNat)]
 
@@ -75,8 +73,7 @@ theorem Sum.of_comp {X Y:Type} {f:X → ℝ} (h: AbsConvergent f) {g: Y → X} (
   obtain ⟨ hbij', hconv' ⟩ := h.choose_spec
   set g' := h.choose
   obtain ⟨ g_inv, hleft, hright ⟩ := Function.bijective_iff_has_inverse.mp hbij
-  have hbij_g_inv_g' : Function.Bijective (g_inv ∘ g') :=
-    Function.Bijective.comp ⟨ Function.LeftInverse.injective hright, Function.RightInverse.surjective hleft⟩ hbij'
+  have hbij_g_inv_g' : Function.Bijective (g_inv ∘ g') := .comp ⟨hright.injective, hleft.surjective⟩ hbij'
   have hident : (f ∘ g) ∘ g_inv ∘ g' = f ∘ g' := by ext n; simp [hright (g' n)]
   refine ⟨ ⟨ g_inv ∘ g', ⟨ hbij_g_inv_g', by convert hconv' ⟩ ⟩, ?_ ⟩
   have h := eq (f := f ∘ g) hbij_g_inv_g' (by convert hconv')
@@ -98,24 +95,21 @@ theorem sum_of_sum_of_AbsConvergent_nonneg {f:ℕ × ℕ → ℝ} (hf:AbsConverg
   (fun n ↦ ((fun m ↦ f (n, m)):Series).sum:Series).convergesTo (Sum f) := by
   set L := Sum f
   have hLpos : 0 ≤ L := by
-    simp [L, Sum, hf]
-    apply Series.sum_of_nonneg
-    intro n; by_cases h: n ≥ 0 <;> simp [h]; exact hpos _ _
+    simp [L, Sum, hf]; apply Series.sum_of_nonneg; intro n; by_cases h: n ≥ 0 <;> simp [h]; exact hpos _ _
   have hfinsum (X: Finset (ℕ × ℕ)) : ∑ p ∈ X, f p ≤ L := by sorry
   have hfinsum' (n M:ℕ) : ((fun m ↦ f (n, m)):Series).partial M ≤ L := by
     simp [Series.partial, Finset.Icc_eq_cast]
-    convert_to ∑ x ∈ Finset.map (Function.Embedding.sectR n ℕ) (Finset.Icc 0 M), f x ≤ L
+    convert_to ∑ x ∈ .map (Function.Embedding.sectR n ℕ) (.Icc 0 M), f x ≤ L
     . simp
     solve_by_elim
   have hnon (n:ℕ) : ((fun m ↦ f (n, m)):Series).nonneg := by
-    simp [Series.nonneg]
-    intro m; by_cases h: m ≥ 0 <;> simp [h, hpos]
+    simp [Series.nonneg]; intro m; by_cases h: m ≥ 0 <;> simp [h, hpos]
   have hconv (n:ℕ) : ((fun m ↦ f (n, m)):Series).converges := by
     rw [Series.converges_of_nonneg_iff (hnon n)]
     use L; intro N; by_cases h: N ≥ 0
     . lift N to ℕ using h; solve_by_elim
     rw [Series.partial_of_lt (by simp; linarith)]; simp [hLpos]
-  have (N M:ℤ) : ∑ n ∈ Finset.Icc 0 N, ((fun m ↦ f (n.toNat, m)):Series).partial M ≤ L := by
+  have (N M:ℤ) : ∑ n ∈ .Icc 0 N, ((fun m ↦ f (n.toNat, m)):Series).partial M ≤ L := by
     by_cases hN : N ≥ 0; swap
     . simp [Finset.Icc_empty hN, hLpos]
     lift N to ℕ using hN
@@ -124,15 +118,14 @@ theorem sum_of_sum_of_AbsConvergent_nonneg {f:ℕ × ℕ → ℝ} (hf:AbsConverg
       apply Finset.sum_eq_zero; intro n _
       simp [Finset.Icc_empty hM]
     lift M to ℕ using hM
-    convert_to ∑ x ∈ (Finset.Icc 0 N) ×ˢ (Finset.Icc 0 M), f x ≤ L
+    convert_to ∑ x ∈ (.Icc 0 N) ×ˢ (.Icc 0 M), f x ≤ L
     . simp [Finset.sum_product, Series.partial]
     solve_by_elim
-  replace (N:ℤ) : ∑ n ∈ Finset.Icc 0 N, ((fun m ↦ f (n.toNat, m)):Series).sum ≤ L := by
-    apply le_of_tendsto' (x := Filter.atTop) (tendsto_finset_sum _ _) (this N)
+  replace (N:ℤ) : ∑ n ∈ .Icc 0 N, ((fun m ↦ f (n.toNat, m)):Series).sum ≤ L := by
+    apply le_of_tendsto' (x := .atTop) (tendsto_finset_sum _ _) (this N)
     intro n _; exact Series.convergesTo_sum (by solve_by_elim)
   replace (N:ℤ) : (fun n ↦ ((fun m ↦ f (n, m)):Series).sum:Series).partial N ≤ L := by
-    convert this N with n hn
-    simp_all
+    convert this N with n hn; simp_all
   have hnon' : (fun n ↦ ((fun m ↦ f (n, m)):Series).sum:Series).nonneg := by
     intro n; by_cases h: n ≥ 0 <;> simp [h]
     exact Series.sum_of_nonneg (hnon n.toNat)
@@ -145,15 +138,14 @@ theorem sum_of_sum_of_AbsConvergent_nonneg {f:ℕ × ℕ → ℝ} (hf:AbsConverg
     replace : ∃ X, ∑ p ∈ X, f p ≥ L - ε := by
       sorry
     obtain ⟨ X, hX ⟩ := this
-    have : ∃ N, ∃ M, X ⊆ (Finset.Icc 0 N) ×ˢ (Finset.Icc 0 M) := by
+    have : ∃ N, ∃ M, X ⊆ (.Icc 0 N) ×ˢ (.Icc 0 M) := by
       sorry
     obtain ⟨ N, M, hX' ⟩ := this
     calc
       _ ≤ ∑ p ∈ X, f p := hX
-      _ ≤ ∑ p ∈ (Finset.Icc 0 N) ×ˢ (Finset.Icc 0 M), f p :=
-        Finset.sum_le_sum_of_subset_of_nonneg hX' (by solve_by_elim)
-      _ = ∑ n ∈ Finset.Icc 0 N, ∑ m ∈ Finset.Icc 0 M, f (n, m) := Finset.sum_product _ _ _
-      _ ≤ ∑ n ∈ Finset.Icc 0 N, ((fun m ↦ f (n, m)):Series).sum := by
+      _ ≤ ∑ p ∈ (.Icc 0 N) ×ˢ (.Icc 0 M), f p := Finset.sum_le_sum_of_subset_of_nonneg hX' (by solve_by_elim)
+      _ = ∑ n ∈ .Icc 0 N, ∑ m ∈ .Icc 0 M, f (n, m) := Finset.sum_product _ _ _
+      _ ≤ ∑ n ∈ .Icc 0 N, ((fun m ↦ f (n, m)):Series).sum := by
         apply Finset.sum_le_sum; intro n _
         convert Series.partial_le_sum_of_nonneg (hnon n) (hconv n) M
         simp [Series.partial]
@@ -191,8 +183,7 @@ theorem sum_of_sum_of_AbsConvergent {f:ℕ × ℕ → ℝ} (hf:AbsConvergent f)
     by_cases h: m ≥ 0 <;> simp [h, HSub.hSub, Sub.sub]
     . solve_by_elim
     convert hfminus_conv' n.toNat
-  have := hf
-  obtain ⟨ g, hg, _ ⟩ := this
+  have ⟨ g, hg, _ ⟩ := hf
   have h1 := Sum.eq hg (hf.comp hg)
   have hplus := Sum.eq hg (hfplus_conv.comp hg)
   have hminus := Sum.eq hg (hfminus_conv.comp hg)
@@ -206,8 +197,7 @@ theorem sum_of_sum_of_AbsConvergent' {f:ℕ × ℕ → ℝ} (hf:AbsConvergent f)
   (fun m ↦ ((fun n ↦ f (n, m)):Series).sum:Series).convergesTo (Sum f) := by
   set π: ℕ × ℕ → ℕ × ℕ := fun p ↦ (p.2, p.1)
   have hπ: Function.Bijective π := Function.Involutive.bijective (congrFun rfl)
-  have := hf
-  obtain ⟨ g, hg, hconv ⟩ := this
+  have ⟨ g, hg, hconv ⟩ := hf
   convert sum_of_sum_of_AbsConvergent (f := f ∘ π) _ using 2
   . exact (Sum.of_comp hf hπ).2
   refine ⟨ π ∘ g, Function.Bijective.comp hπ hg, ?_ ⟩
@@ -228,35 +218,26 @@ abbrev AbsConvergent' {X:Type} (f: X → ℝ) : Prop := BddAbove ( (fun A ↦ 
 
 theorem AbsConvergent'.of_finite {X:Type} [Finite X] (f:X → ℝ) : AbsConvergent' f := by
   have _ := Fintype.ofFinite X
-  simp [bddAbove_def]
-  use ∑ x, |f x|; intro A
-  apply Finset.sum_le_univ_sum_of_nonneg; simp
+  simp [bddAbove_def]; use ∑ x, |f x|; intro A; apply Finset.sum_le_univ_sum_of_nonneg; simp
 
 /-- Not in textbook, but should have been included. -/
 theorem AbsConvergent'.of_countable {X:Type} (hX:CountablyInfinite X) {f:X → ℝ} :
   AbsConvergent' f ↔ AbsConvergent f := by
   constructor
-  . intro hf
-    simp [bddAbove_def] at hf
-    obtain ⟨ L, hL ⟩ := hf
-    obtain ⟨ g, hg ⟩ := hX.symm
-    refine ⟨ g, hg, ?_ ⟩
+  . intro hf; simp [bddAbove_def] at hf; obtain ⟨ L, hL ⟩ := hf
+    obtain ⟨ g, hg ⟩ := hX.symm; refine ⟨ g, hg, ?_ ⟩
     unfold Series.absConverges
     rw [Series.converges_of_nonneg_iff]
-    . use L; intro N
-      by_cases hN: N ≥ 0
+    . use L; intro N; by_cases hN: N ≥ 0
       . lift N to ℕ using hN
         set g':= Function.Embedding.mk g hg.1
         convert hL (Finset.map g' (Finset.Icc 0 N))
         simp [Series.partial]; rfl
       convert hL ∅
-      simp
-      apply Series.partial_of_lt
-      simp; contrapose! hN; assumption
+      simp; apply Series.partial_of_lt; simp; contrapose! hN; assumption
     simp [Series.nonneg]
     intro n; by_cases h: n ≥ 0 <;> simp [h]
-  intro hf
-  rwa [AbsConvergent.iff hX f] at hf
+  intro hf; rwa [AbsConvergent.iff hX f] at hf
 
 /-- Lemma 8.2.5 / Exercise 8.2.2-/
 theorem AbsConvergent'.countable_supp {X:Type} {f:X → ℝ} (hf: AbsConvergent' f) :
@@ -267,10 +248,8 @@ theorem AbsConvergent'.countable_supp {X:Type} {f:X → ℝ} (hf: AbsConvergent'
 theorem AbsConvergent'.subtype {X:Type} {f:X → ℝ} (hf: AbsConvergent' f) (A: Set X) :
   AbsConvergent' (fun x:A ↦ f x) := by
   apply BddAbove.mono _ hf
-  intro z hz; simp at hz ⊢
-  obtain ⟨ A, hA ⟩ := hz
-  use Finset.map (Function.Embedding.subtype _) A
-  simp [hA]
+  intro z hz; simp at hz ⊢; obtain ⟨ A, hA ⟩ := hz
+  use A.map (Function.Embedding.subtype _); simp [hA]
 
 /-- A generalized sum.  Note that this will give junk values if `f` is not `AbsConvergent'`. -/
 noncomputable abbrev Sum' {X:Type} (f: X → ℝ) : ℝ := Sum (fun x : { x | f x ≠ 0 } ↦ f x)
@@ -281,7 +260,7 @@ theorem Sum'.of_finsupp {X:Type} {f:X → ℝ} {A: Finset X} (h: ∀ x ∉ A, f
   unfold Sum'
   set E := { x | f x ≠ 0 }
   have hE : E ⊆ A := by intro x; simp [E]; by_contra!; specialize h x this.2; tauto
-  have hfin : Finite E := Finite.Set.subset _ hE
+  have hfin : Finite E := .Set.subset _ hE
   set E' := E.toFinite.toFinset
   rw [Sum.of_finite (fun x:E ↦ f x), ←Finset.sum_subtype E' (by simp [E'])]
   replace hE : E' ⊆ A := by aesop
@@ -309,35 +288,30 @@ theorem Sum'.of_countable_supp {X:Type} {f:X → ℝ} {A: Set X} (hA: CountablyI
   set ι : E' → E := fun ⟨ n, hn ⟩ ↦ ⟨ (g n).val, by aesop ⟩
   have hι: Function.Bijective ι := by
     constructor
-    . intro ⟨ n, hn ⟩ ⟨ m, hm ⟩ h
-      simp [ι, E', Subtype.val_inj] at hn hm h ⊢; exact hg.1 h
-    . intro ⟨ x, hx ⟩
-      obtain ⟨ n, hn ⟩ := hg.2 ⟨ x, hE hx ⟩
-      use ⟨ n, by aesop ⟩
-      simp [ι, hn]
+    . intro ⟨ n, hn ⟩ ⟨ m, hm ⟩ h; simp [ι, E', Subtype.val_inj] at hn hm h ⊢; exact hg.1 h
+    . intro ⟨ x, hx ⟩; obtain ⟨ n, hn ⟩ := hg.2 ⟨ x, hE hx ⟩; use ⟨ n, by aesop ⟩; simp [ι, hn]
   -- The cases of infinite and finite E' are handled separately.
   rcases Nat.atMostCountable_subset E' with hE' | hE'
   . --   use Nat.monotone_enum_of_infinite to enumerate E'
     --   show the partial sums of E' are a subsequence of the partial sums of A
     set hinf : Infinite E' := hE'.toInfinite
     obtain ⟨ a, ha_bij, ha_mono ⟩ := (Nat.monotone_enum_of_infinite E').exists
-    have : Filter.Tendsto (Nat.cast ∘ Subtype.val ∘ a: ℕ → ℤ) Filter.atTop Filter.atTop := by
+    have : Filter.Tendsto (Nat.cast ∘ Subtype.val ∘ a: ℕ → ℤ) .atTop .atTop := by
       apply tendsto_natCast_atTop_atTop.comp
       apply StrictMono.tendsto_atTop
-      intro n m hnm
-      simp [ha_mono hnm]
+      intro n m hnm; simp [ha_mono hnm]
     replace hsum := hsum.comp this
     apply tendsto_nhds_unique  _ hsum
     have hconv'' : AbsConvergent (fun x:E ↦ f x) := by
       rw [←AbsConvergent'.of_countable]
       . exact hconv.subtype E
       apply (CountablyInfinite.equiv _).mp hE'; use ι
-    replace := Sum.eq (hι.comp ha_bij) (AbsConvergent.comp (hι.comp ha_bij) hconv'')
+    replace := Sum.eq (hι.comp ha_bij) (hconv''.comp (hι.comp ha_bij))
     replace := this.comp tendsto_natCast_atTop_atTop
     convert this using 1; ext N
     simp [Series.partial, ι]
     calc
-      _ = ∑ x ∈ Finset.image (Subtype.val ∘ a) (Finset.Icc 0 N), f ↑(g x) := by
+      _ = ∑ x ∈ .image (Subtype.val ∘ a) (.Icc 0 N), f ↑(g x) := by
         apply (Finset.sum_subset _ _).symm
         . intro m hm; simp at hm ⊢
           obtain ⟨ n, hn, rfl ⟩ := hm
@@ -356,8 +330,8 @@ theorem Sum'.of_countable_supp {X:Type} {f:X → ℝ} {A: Set X} (hA: CountablyI
   -- When E' is finite, we show that all sufficiently large partial sums of A are equal to
   -- the sum of E'.
   let hEfin : Finite E := hι.finite_iff.mp hE'
-  let hE'fintype : Fintype E' := Fintype.ofFinite _
-  let hEfintype : Fintype E := Fintype.ofFinite _
+  let hE'fintype : Fintype E' := .ofFinite _
+  let hEfintype : Fintype E := .ofFinite _
   apply Series.convergesTo_uniq _ hsum
   simp [Sum.of_finite, Series.convergesTo]
   apply tendsto_nhds_of_eventually_eq
@@ -372,13 +346,9 @@ theorem Sum'.of_countable_supp {X:Type} {f:X → ℝ} {A: Set X} (hA: CountablyI
     _ = ∑ n ∈ E', f ↑(g n) := by
       apply (Finset.sum_subset _ _).symm
       . intro x hx; simp at hx ⊢; linarith [hN x hx]
-      intro _ _ hx'
-      simpa [E',E] using hx'
-    _ = ∑ n:E', f ↑(g ↑n) := by
-      convert (Finset.sum_set_coe _).symm
-    _ = ∑ n, f ↑(ι n) := by
-      apply Finset.sum_congr rfl
-      intros; simp [ι]
+      intro _ _ hx'; simpa [E',E] using hx'
+    _ = ∑ n:E', f ↑(g ↑n) := by convert (Finset.sum_set_coe _).symm
+    _ = ∑ n, f ↑(ι n) := by apply Finset.sum_congr rfl; intros; simp [ι]
     _ = _ := hι.sum_comp (g := fun x ↦ f ↑x)
 
 /-- Connection with Mathlib's `Summable` property. Some version of this might be suitable
@@ -399,7 +369,7 @@ theorem AbsConvergent'.iff_Summable {X:Type} (f:X → ℝ) : AbsConvergent' f 
       apply ConditionallyCompleteLattice.le_csSup _ _ h _
       simp [s]; use T ∪ S; exact Finset.sum_union hT
     linarith
-  intro h; specialize h 1 (by norm_num); obtain ⟨ S, hS ⟩ := h
+  intro h; obtain ⟨ S, hS ⟩ := h 1 (by norm_num)
   rw [bddAbove_def]
   use ∑ x ∈ S, |f x| + 1; simp; intro T
   calc
@@ -411,7 +381,7 @@ theorem AbsConvergent'.iff_Summable {X:Type} (f:X → ℝ) : AbsConvergent' f 
 
 /-- Maybe suitable for porting to Mathlib?-/
 theorem Filter.Eventually.int_natCast_atTop (p: ℤ → Prop) :
-  (∀ᶠ n in Filter.atTop, p n) ↔ ∀ᶠ n:ℕ in Filter.atTop, p ↑n := by
+  (∀ᶠ n in .atTop, p n) ↔ ∀ᶠ n:ℕ in .atTop, p ↑n := by
   refine ⟨ Filter.Eventually.natCast_atTop, ?_ ⟩
   simp [Filter.eventually_atTop]
   intro N hN; use N; intro n hn
@@ -419,7 +389,7 @@ theorem Filter.Eventually.int_natCast_atTop (p: ℤ → Prop) :
   simp at hn; solve_by_elim
 
 theorem Filter.Tendsto.int_natCast_atTop {R:Type} (f: ℤ → R) (l: Filter R) :
-Filter.Tendsto f Filter.atTop l ↔ Filter.Tendsto (f ∘ Nat.cast) Filter.atTop l := by
+Filter.Tendsto f .atTop l ↔ Filter.Tendsto (f ∘ Nat.cast) .atTop l := by
   simp [Filter.tendsto_iff_eventually]
   peel with p h
   simp [←Filter.eventually_atTop]
@@ -482,7 +452,7 @@ theorem Sum'.of_disjoint_union {X:Type} {f:X → ℝ} (hf: AbsConvergent' f) {X
 /-- This technical claim, the analogue of `tsum_univ`, is required due to the way Mathlib handles
     sets.-/
 theorem Sum'.of_univ {X:Type} {f:X → ℝ} (hf: AbsConvergent' f) :
-  Sum' (fun x: (Set.univ : Set X) ↦ f x) = Sum' f := by
+  Sum' (fun x: (.univ : Set X) ↦ f x) = Sum' f := by
   sorry
 
 theorem Sum'.of_comp {X Y:Type} {f:X → ℝ} (hf: AbsConvergent' f) {φ: Y → X}
@@ -531,7 +501,7 @@ theorem Series.permute_convergesTo_of_divergent {a: ℕ → ℝ} (ha: (a:Series)
   have h_case_I : Infinite { j | ∑ i:Fin j, n' i > L } := by sorry
   have h_case_II : Infinite { j | ∑ i:Fin j, n' i ≤ L } := by sorry
   have hn'_surj : Function.Surjective n' := by sorry
-  have hconv : Filter.Tendsto (a ∘ n') Filter.atTop (nhds 0) := by sorry
+  have hconv : Filter.Tendsto (a ∘ n') .atTop (nhds 0) := by sorry
   have hsum : (a ∘ n':Series).convergesTo L := by sorry
   use n'
   refine ⟨ ⟨ hn'_inj, hn'_surj ⟩, ?_ ⟩; convert hsum
@@ -539,12 +509,12 @@ theorem Series.permute_convergesTo_of_divergent {a: ℕ → ℝ} (ha: (a:Series)
 /-- Exercise 8.2.6 -/
 theorem Series.permute_diverges_of_divergent {a: ℕ → ℝ} (ha: (a:Series).converges)
   (ha': ¬ (a:Series).absConverges)  :
-  ∃ f : ℕ → ℕ,  Function.Bijective f ∧ Filter.Tendsto (fun N ↦ ((a ∘ f:Series).partial N : EReal)) Filter.atTop (nhds ⊤) := by
+  ∃ f : ℕ → ℕ,  Function.Bijective f ∧ Filter.Tendsto (fun N ↦ ((a ∘ f:Series).partial N : EReal)) .atTop (nhds ⊤) := by
   sorry
 
 theorem Series.permute_diverges_of_divergent' {a: ℕ → ℝ} (ha: (a:Series).converges)
   (ha': ¬ (a:Series).absConverges)  :
-  ∃ f : ℕ → ℕ,  Function.Bijective f ∧ Filter.Tendsto (fun N ↦ ((a ∘ f:Series).partial N : EReal)) Filter.atTop (nhds ⊥) := by
+  ∃ f : ℕ → ℕ,  Function.Bijective f ∧ Filter.Tendsto (fun N ↦ ((a ∘ f:Series).partial N : EReal)) .atTop (nhds ⊥) := by
   sorry
 
 end Chapter8
diff --git a/analysis/Analysis/Section_8_3.lean b/analysis/Analysis/Section_8_3.lean
index 9d8ec37..8656f12 100644
--- a/analysis/Analysis/Section_8_3.lean
+++ b/analysis/Analysis/Section_8_3.lean
@@ -67,7 +67,7 @@ theorem Uncountable.real : Uncountable ℝ := by
   set a : ℕ → ℝ := fun n ↦ (10:ℝ)^(-(n:ℝ))
   set f : Set ℕ → ℝ := fun A ↦ ∑' n:A, a n
   have hsummable (A: Set ℕ) : Summable (fun n:A ↦ a n) := by
-    apply Summable.subtype (f := fun n:ℕ ↦ a n)
+    apply Summable.subtype (f := a)
     convert summable_geometric_of_lt_one (show 0 ≤ (1/10:ℝ) by norm_num) (by norm_num) using 2 with n
     unfold a
     rw [one_div_pow, Real.rpow_neg (by norm_num), one_div]; simp
@@ -76,38 +76,34 @@ theorem Uncountable.real : Uncountable ℝ := by
     . rw [hC]
     . rw [Set.disjoint_iff_inter_eq_empty]; ext n; simp [hAB n]
     all_goals exact hsummable _
-  have h_nonneg (A:Set ℕ) : ∑' n:A, a n ≥ 0 := by
-    simp [a]; positivity
+  have h_nonneg (A:Set ℕ) : ∑' n:A, a n ≥ 0 := by simp [a]; positivity
   have h_congr {A B: Set ℕ} (hAB: A = B) : ∑' n:A, a n = ∑' n:B, a n  := by rw [hAB]
   have : Function.Injective f := by
     intro A B hAB; by_contra!
     rw [←Set.symmDiff_nonempty] at this
     replace this := Nat.min_spec this
     set n₀ := Nat.min (symmDiff A B)
-    simp [symmDiff] at this
-    obtain ⟨ h1, h2 ⟩ := this
+    simp [symmDiff] at this; obtain ⟨ h1, h2 ⟩ := this
     wlog h : n₀ ∈ A ∧ n₀ ∉ B generalizing A B
     . simp [h] at h1
       exact this hAB.symm
         (by simp [symmDiff_comm]; tauto)
         (by intro n hn; specialize h2 n (by tauto); simp [symmDiff_comm, n₀, h2])
-        (by simp [symmDiff_comm]; assumption)
+        (by simpa [symmDiff_comm])
     replace h2 {n:ℕ} (hn: n < n₀) : n ∈ A ↔ n ∈ B := by contrapose! hn; exact h2 n (by tauto)
     have : (0:ℝ) > 0 := calc
       _ = f A - f B := by linarith
       _ = ∑' n:A, a n - ∑' n:B, a n := rfl
       _ = (∑' n:{n ∈ A|n ≤ n₀}, a n + ∑' n:{n ∈ A|n > n₀}, a n) -
           (∑' n:{n ∈ B|n ≤ n₀}, a n + ∑' n:{n ∈ B|n > n₀}, a n) := by
-        congr
-        all_goals {
+        congr; all_goals {
           apply h_decomp
           . ext n; simp; rw [←not_le]; tauto
           intro n hn; simp at hn; linarith
         }
       _ = ((∑' n:{n ∈ A|n < n₀}, a n + ∑' n:{n ∈ A|n = n₀}, a n) + ∑' n:{n ∈ A|n > n₀}, a n) -
           ((∑' n:{n ∈ B|n < n₀}, a n + ∑' n:{n ∈ B|n = n₀}, a n) + ∑' n:{n ∈ B|n > n₀}, a n) := by
-        congr
-        all_goals {
+        congr; all_goals {
           apply h_decomp
           . ext n; simp [le_iff_lt_or_eq]
           intro n hn; simp at hn; linarith
@@ -124,18 +120,15 @@ theorem Uncountable.real : Uncountable ℝ := by
       _ = (∑' n:{n ∈ A|n < n₀}, a n - ∑' n:{n ∈ B|n < n₀}, a n) + a n₀ +
           ∑' n:{n ∈ A|n > n₀}, a n - ∑' n:{n ∈ B|n > n₀}, a n := by abel
       _ = 0 + a n₀ + ∑' n:{n ∈ A|n > n₀}, a n - ∑' n:{n ∈ B|n > n₀}, a n := by
-        congr; rw [sub_eq_zero]; apply tsum_congr_set_coe
-        ext n; simp; intro hn; exact h2 hn
+        congr; rw [sub_eq_zero]; apply tsum_congr_set_coe; ext; simpa using h2
       _ ≥ 0 + a n₀ + 0 - ∑' n:{n|n > n₀}, a n := by
-        gcongr
-        . positivity
+        gcongr; positivity
         calc
           _ = ∑' (n : {n ∈ B|n > n₀}), a n + ∑' (n : {n ∉ B|n > n₀}), a n := by
             apply h_decomp
             . ext n; simp; tauto
             intro n hn; simp at hn; tauto
-          _ ≥ ∑' (n : {n ∈ B|n > n₀}), a n + 0 := by
-            gcongr; solve_by_elim
+          _ ≥ ∑' (n : {n ∈ B|n > n₀}), a n + 0 := by gcongr; solve_by_elim
           _ = _ := by simp
       _ = 0 + (10:ℝ)^(-(n₀:ℝ)) + 0 - (1 / (9:ℝ)) * (10:ℝ)^(-(n₀:ℝ)) := by
         congr
@@ -144,7 +137,7 @@ theorem Uncountable.real : Uncountable ℝ := by
           constructor
           . intro j k hjk; simpa [ι] using hjk
           intro ⟨ n, hn ⟩; simp [ι] at hn ⊢; use n - n₀ - 1; omega
-        rw [←Equiv.tsum_eq (Equiv.ofBijective ι hι)]
+        rw [←(Equiv.ofBijective ι hι).tsum_eq]
         simp [ι,a]
         calc
           _ = ∑' j:ℕ, (10:ℝ)^(-1-n₀:ℝ) * (1/(10:ℝ))^j := by
@@ -166,7 +159,7 @@ theorem Uncountable.real : Uncountable ℝ := by
   replace : EqualCard (Set ℕ) (Set.range f) := by
     use (Equiv.ofInjective _ this).toFun
     exact (Equiv.ofInjective _ this).bijective
-  replace := (Uncountable.equiv this).mp power_set_nat
+  replace := (equiv this).mp power_set_nat
   contrapose this
   rw [not_uncountable_iff] at this ⊢
   exact SetCoe.countable _
@@ -218,20 +211,4 @@ abbrev CardOrder : Preorder Type := {
 example (X:Type) : ¬ CountablyInfinite (Set X) := by
   sorry
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
 end Chapter8
diff --git a/analysis/Analysis/Section_8_4.lean b/analysis/Analysis/Section_8_4.lean
index b098887..eecbc6a 100644
--- a/analysis/Analysis/Section_8_4.lean
+++ b/analysis/Analysis/Section_8_4.lean
@@ -52,15 +52,15 @@ def CartesianProduct.equiv {I U: Type} (X : I → Set U) :
 def Function.equiv {I X:Type} : (∀ _:I, X) ≃ (I → X) := {
   toFun f := f
   invFun f := f
-  left_inv f := by rfl
-  right_inv f := by rfl
+  left_inv f := rfl
+  right_inv f := rfl
 }
 
 def product_zero_equiv {X: Fin 0 → Type} : (∀ i:Fin 0, X i) ≃ PUnit := {
   toFun f := PUnit.unit
   invFun x i := nomatch i
   left_inv f := by aesop
-  right_inv f := by rfl
+  right_inv f := rfl
 }
 
 def product_one_equiv {X: Fin 1 → Type} : (∀ i:Fin 1, X i) ≃ X 0 := {
@@ -91,15 +91,14 @@ def product_three_equiv {X: Fin 3 → Type} : (∀ i:Fin 3, X i) ≃ (X 0 × X 1
 
 /-- Axiom 8.1 (Choice) -/
 theorem axiom_of_choice {I: Type} {X: I → Type} (h : ∀ i, Nonempty (X i)) :
-  Nonempty (∀ i, X i) := by
-  use fun i ↦ (h i).some
+  Nonempty (∀ i, X i) := by use fun i ↦ (h i).some
 
 theorem axiom_of_countable_choice {I: Type} {X: I → Type} [Countable I] (h : ∀ i, Nonempty (X i)) :
   Nonempty (∀ i, X i) := axiom_of_choice h
 
 /-- Lemma 8.4.5 -/
 theorem exist_tendsTo_sup {E: Set ℝ} (hnon: E.Nonempty) (hbound: BddAbove E) :
-  ∃ a : ℕ → ℝ, (∀ n, a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E)) := by
+  ∃ a : ℕ → ℝ, (∀ n, a n ∈ E) ∧ Filter.Tendsto a .atTop (nhds (sSup E)) := by
   -- This proof is written to follow the structure of the original text.
   set X : ℕ → Set ℝ := fun n ↦ { x ∈ E | sSup E - 1 / (n+1:ℝ) ≤ x ∧ x ≤ sSup E }
   have hX : ∀ n, Nonempty (X n) := by
@@ -113,15 +112,14 @@ theorem exist_tendsTo_sup {E: Set ℝ} (hnon: E.Nonempty) (hbound: BddAbove E) :
   constructor
   . intro n; have := (a n).property; unfold X at this; simp_all
   apply Filter.Tendsto.squeeze (g := fun n:ℕ ↦ sSup E - 1/(n+1:ℝ)) (h := fun n:ℕ ↦ sSup E)
-  . convert Filter.Tendsto.sub (a := sSup E) (b := 0) tendsto_const_nhds _
-    . simp
+  . convert Filter.Tendsto.sub (a := sSup E) (b := 0) tendsto_const_nhds _; simp
     exact tendsto_one_div_add_atTop_nhds_zero_nat
   . exact tendsto_const_nhds
   all_goals intro n; have := (a n).property; unfold X at this; simp_all
 
 /-- Remark 8.4.6.  This special case of Lemma 8.4.5 avoids (countable) choice. -/
 theorem exist_tendsTo_sup_of_closed {E: Set ℝ} (hnon: E.Nonempty) (hbound: BddAbove E) (hclosed: IsClosed E) :
-  ∃ a : ℕ → ℝ, (∀ n, a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E)) := by
+  ∃ a : ℕ → ℝ, (∀ n, a n ∈ E) ∧ Filter.Tendsto a .atTop (nhds (sSup E)) := by
   set X : ℕ → Set ℝ := fun n ↦ { x ∈ E | sSup E - 1 / (n+1:ℝ) ≤ x ∧ x ≤ sSup E }
   have hX : ∀ n, Nonempty (X n) := by
     intro n
@@ -139,8 +137,7 @@ theorem exist_tendsTo_sup_of_closed {E: Set ℝ} (hnon: E.Nonempty) (hbound: Bdd
   constructor
   . simp [X] at ha; aesop
   apply Filter.Tendsto.squeeze (g := fun n:ℕ ↦ sSup E - 1/(n+1:ℝ)) (h := fun n:ℕ ↦ sSup E)
-  . convert Filter.Tendsto.sub (a := sSup E) (b := 0) tendsto_const_nhds _
-    . simp
+  . convert Filter.Tendsto.sub (a := sSup E) (b := 0) tendsto_const_nhds _;  simp
     exact tendsto_one_div_add_atTop_nhds_zero_nat
   . exact tendsto_const_nhds
   all_goals intro n; specialize ha n; simp [X] at ha; simp_all
@@ -154,8 +151,7 @@ theorem exists_function {X Y : Type} {P : X → Y → Prop} (h: ∀ x, ∃ y, P
 from `exists_function`, avoiding previous results that relied more explicitly
 on the axiom of choice. -/
 theorem axiom_of_choice_from_exists_function {I: Type} {X: I → Type} (h : ∀ i, Nonempty (X i)) :
-  Nonempty (∀ i, X i) := by
-  use fun i ↦ (h i).some
+  Nonempty (∀ i, X i) := by use fun i ↦ (h i).some
 
 /-- Exercise 8.4.2 -/
 theorem exists_set_singleton_intersect {I U:Type} {X: I → Set U} (h: Set.PairwiseDisjoint Set.univ X)
@@ -168,12 +164,12 @@ from `exists_set_singleton_intersect`, avoiding previous results that relied mor
 on the axiom of choice. -/
 theorem axiom_of_choice_from_exists_set_singleton_intersect {I: Type} {X: I → Type} (h : ∀ i, Nonempty (X i)) :
   Nonempty (∀ i, X i) := by
-  use fun i ↦ (h i).some
+  sorry
 
 /-- Exercise 8.4.3 -/
 theorem Function.Injective.inv_surjective {A B:Type} {g: B → A} (hg: Function.Surjective g) :
   ∃ f : A → B, Function.Injective f ∧ Function.RightInverse f g := by
-    sorry
+  sorry
 
 /-- Exercise 8.4.3.  The spirit of the question here is to establish this result directly
 from `Function.Injective.inv_surjective`, avoiding previous results that relied more explicitly
diff --git a/analysis/Analysis/Section_8_5.lean b/analysis/Analysis/Section_8_5.lean
index cbb474d..9f4d2f1 100644
--- a/analysis/Analysis/Section_8_5.lean
+++ b/analysis/Analysis/Section_8_5.lean
@@ -101,20 +101,14 @@ theorem WellFoundedLT.iff (X:Type) [LinearOrder X] :
   WellFoundedLT X ↔ ∀ A:Set X, A.Nonempty → ∃ x:A, IsMin x := by
   unfold WellFoundedLT IsMin
   rw [isWellFounded_iff, WellFounded.wellFounded_iff_has_min]
-  constructor <;> intro h A hA <;> specialize h A hA
-  . obtain ⟨ x, hxA, h ⟩ := h
-    use ⟨ x, hxA ⟩; intro ⟨ y, hy ⟩ this
-    specialize h y hy
+  peel with A hA; constructor
+  . intro ⟨ x, hxA, h ⟩; use ⟨ x, hxA ⟩; intro ⟨ y, hy ⟩ this; specialize h y hy
     simp at this ⊢; order
-  obtain ⟨ ⟨ x, hx ⟩, h ⟩ := h
-  refine ⟨ _, hx, ?_ ⟩
-  intro y hy; specialize h (b := ⟨ _, hy ⟩)
+  intro ⟨ ⟨ x, hx ⟩, h ⟩; refine ⟨ _, hx, ?_ ⟩; intro y hy; specialize h (b := ⟨ _, hy ⟩)
   simp at h; contrapose! h; simp [h]; order
 
 theorem WellFoundedLT.iff' {X:Type} [PartialOrder X] (h: IsTotal X) :
-  WellFoundedLT X ↔ ∀ A:Set X, A.Nonempty → ∃ x:A, IsMin x := by
-  let _lin := LinearOrder.mk h
-  exact iff X
+  WellFoundedLT X ↔ ∀ A:Set X, A.Nonempty → ∃ x:A, IsMin x := @iff X (LinearOrder.mk h)
 
 /-- Example 8.5.9 -/
 example : WellFoundedLT ℕ := by
@@ -141,13 +135,10 @@ example {X:Type} [LinearOrder X] [WellFoundedLT X] (A: Set X) : WellFoundedLT A
 theorem WellFoundedLT.subset {X:Type} [PartialOrder X] {A B: Set X} (hA: IsTotal A) [hwell: WellFoundedLT A] (hAB: B ⊆ A) : WellFoundedLT B := by
   set hAlin : LinearOrder A := LinearOrder.mk hA
   set hBlin : LinearOrder B := LinearOrder.mk (hA.subset hAB)
-  rw [iff] at hwell ⊢
-  intro C hC
-  specialize hwell ((Set.embeddingOfSubset _ _ hAB) '' C) (by aesop)
-  obtain ⟨ ⟨ ⟨ x, hx ⟩, hx' ⟩, hmin ⟩ := hwell; simp at hx'
-  obtain ⟨ y, hy, hyC, this ⟩ := hx'; use ⟨ _, hyC ⟩
-  simp_all [IsMin, Set.embeddingOfSubset]; subst this
-  intros; aesop
+  rw [iff] at hwell ⊢; intro C hC
+  obtain ⟨ ⟨ ⟨ x, hx ⟩, hx' ⟩, hmin ⟩ := hwell ((Set.embeddingOfSubset _ _ hAB) '' C) (by aesop)
+  simp at hx'; obtain ⟨ y, hy, hyC, this ⟩ := hx'; use ⟨ _, hyC ⟩
+  simp_all [IsMin, Set.embeddingOfSubset]; subst this; intros; aesop
 
 /-- Proposition 8.5.10 / Exercise 8.5.10 -/
 theorem WellFoundedLT.strong_induction {X:Type} [LinearOrder X] [WellFoundedLT X] {P:X → Prop}
@@ -160,8 +151,7 @@ abbrev IsUpperBound {X:Type} [PartialOrder X] (A:Set X) (x:X) : Prop :=
 
 /-- Connection with Mathlib's `upperBounds` -/
 theorem IsUpperBound.iff {X:Type} [PartialOrder X] (A:Set X) (x:X) :
-  IsUpperBound A x ↔ x ∈ upperBounds A := by
-    simp [IsUpperBound, upperBounds]
+  IsUpperBound A x ↔ x ∈ upperBounds A := by simp [IsUpperBound, upperBounds]
 
 abbrev IsStrictUpperBound {X:Type} [PartialOrder X] (A:Set X) (x:X) : Prop :=
   IsUpperBound A x ∧ x ∉ A
@@ -184,19 +174,16 @@ theorem IsMin.iff_lowerbound {X:Type} [PartialOrder X] {Y: Set X} (hY: IsTotal Y
   constructor
   . rintro ⟨ hx₀, hmin ⟩
     simp [IsMin, hx₀] at hmin ⊢
-    intro x hx; specialize hmin x hx; specialize hY ⟨ _, hx ⟩ ⟨ _, hx₀ ⟩
-    aesop
+    peel hmin with x hx hmin; specialize hY ⟨ _, hx ⟩ ⟨ _, hx₀ ⟩; aesop
   intro h; use h.1; simp [IsMin]; aesop
 
 theorem IsMin.iff_lowerbound' {X:Type} [PartialOrder X] {Y: Set X} (hY: IsTotal Y) : (∃ x₀ : Y, IsMin x₀) ↔ ∃ x₀, x₀ ∈ Y ∧ ∀ x ∈ Y, x₀ ≤ x := by
   constructor
   . intro ⟨ ⟨ x₀, hx₀ ⟩, hmin ⟩
     have : ∃ (hx₀ : x₀ ∈ Y), IsMin (⟨ _, hx₀ ⟩:Y) := by use hx₀
-    rw [iff_lowerbound hY x₀] at this
-    use x₀
+    rw [iff_lowerbound hY x₀] at this; use x₀
   intro ⟨ x₀, hx₀, hmin ⟩
-  have := (iff_lowerbound hY x₀).mpr ⟨ hx₀, hmin ⟩
-  obtain ⟨ hx₀, hmin' ⟩ := this; use ⟨ _, hx₀ ⟩
+  obtain ⟨ hx₀, hmin' ⟩ := (iff_lowerbound hY x₀).mpr ⟨ hx₀, hmin ⟩; use ⟨ _, hx₀ ⟩
 
 /-- Exercise 8.5.11 -/
 example {X:Type} [PartialOrder X] {Y Y':Set X} (hY: IsTotal Y) (hY': IsTotal Y') (hY_well: WellFoundedLT Y) (hY'_well: WellFoundedLT Y') (hYY': IsTotal (Y ∪ Y': Set X)) : WellFoundedLT (Y ∪ Y': Set X) := by sorry
@@ -215,8 +202,8 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
     obtain ⟨ hx₀, hmin ⟩ := hY.2.2; refine ⟨ hY.2.1, ⟨ ?_, hstrict ⟩ ⟩
     rw [IsMin.iff_lowerbound hY.1 x₀]; tauto
   by_contra! hs
-  let s : Ω₀ → X := fun Y ↦ (hs ↑Y Y.property).choose
-  replace hs (Y:Ω₀) : IsStrictUpperBound Y (s Y) := (hs ↑Y Y.property).choose_spec
+  let s : Ω₀ → X := fun Y ↦ (hs Y Y.property).choose
+  replace hs (Y:Ω₀) : IsStrictUpperBound Y (s Y) := (hs Y Y.property).choose_spec
 
   have hpt: {x₀} ∈ Ω₀ := by
     have htotal : IsTotal ({x₀}: Set X) := by simp [IsTotal]
@@ -236,8 +223,7 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
       . intro ⟨ a, ha ⟩ ⟨ b, hb ⟩; simp; solve_by_elim [hY.1]
       intro y; simp; tauto
     obtain ⟨ hx₀, hmin ⟩ := hY.2.2
-    simp [IsMin] at hmin hxy ⊢
-    have := hmin _ hxy.1
+    simp [IsMin] at hmin hxy ⊢; have := hmin _ hxy.1
     exact ⟨ ⟨ hx₀, by contrapose! hxy; order ⟩, by intros; solve_by_elim ⟩
   classical
   let F : Ω₀ → X → Ω₀ := fun Y x ↦ if hxy : x ∈ Y.val \ {x₀} then ⟨ {y ∈ (Y:Set X) | y < x}, hF Y.property hxy ⟩ else pt
@@ -250,7 +236,7 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
     sorry
 
   -- Exercise 8.5.13
-  have ex_8_5_13 {Y Y':Ω} (x:X) (h: x ∈ (Y':Set X) \ Y) : IsStrictUpperBound (Y:Set X) x := by
+  have ex_8_5_13 {Y Y':Ω} (x:X) (h: x ∈ (Y':Set X) \ Y) : IsStrictUpperBound Y x := by
     sorry
 
   have : IsTotal Ω := by
@@ -262,12 +248,9 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
     have h1 : IsStrictUpperBound Y x₂ := by solve_by_elim
     have h2 : IsStrictUpperBound Y' x₁ := by solve_by_elim
     simp [IsStrictUpperBound.iff] at h1 h2
-    specialize h1 _ hx₁
-    specialize h2 _ hx₂
-    order
-  set Y_infty : Set X := ⋃ Y:Ω, (Y:Set X)
-  have hmem : x₀ ∈ Y_infty := by
-    simp [Y_infty]; use pt; simp [pt, hpt, hΩ]
+    specialize h1 _ hx₁; specialize h2 _ hx₂; order
+  set Y_infty : Set X := ⋃ Y:Ω, Y
+  have hmem : x₀ ∈ Y_infty := by simp [Y_infty]; use pt; simp [pt, hpt, hΩ]
   have hmin {x:X} (hx: x ∈ Y_infty) : x₀ ≤ x := by
     sorry
   have htotal : IsTotal Y_infty := by
@@ -277,23 +260,17 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
     specialize this ⟨ _, hYΩ ⟩ ⟨ _, hY'Ω ⟩
     simp at this ⊢
     rcases this with this | this
-    . simp [Ω₀] at hY'Ω₀
-      replace hY'Ω₀ := hY'Ω₀.1 ⟨ _, this hxY ⟩ ⟨ _, hxY' ⟩
-      simpa using hY'Ω₀
-    simp [Ω₀] at hYΩ₀
-    replace hYΩ₀ := hYΩ₀.1 ⟨ _, hxY ⟩ ⟨ _, this hxY' ⟩
-    simpa using hYΩ₀
+    . simp [Ω₀] at hY'Ω₀; replace hY'Ω₀ := hY'Ω₀.1 ⟨ _, this hxY ⟩ ⟨ _, hxY' ⟩; simpa using hY'Ω₀
+    simp [Ω₀] at hYΩ₀; replace hYΩ₀ := hYΩ₀.1 ⟨ _, hxY ⟩ ⟨ _, this hxY' ⟩; simpa using hYΩ₀
   have hwell : WellFoundedLT Y_infty := by
     rw [iff' htotal]; intro A ⟨ ⟨a, ha⟩, haA ⟩
-    simp [Y_infty] at ha
-    obtain ⟨ Y, ⟨hYΩ₀, hYΩ⟩, haY ⟩ := ha
+    simp [Y_infty] at ha; obtain ⟨ Y, ⟨hYΩ₀, hYΩ⟩, haY ⟩ := ha
     simp [Ω₀, iff' hYΩ₀.1] at hYΩ₀
     obtain ⟨ b, hb, hbY, hbmin ⟩ := hYΩ₀.2.1 {x:Y | ∃ x':A, (x:X) = x'} (by use ⟨ _, haY ⟩; simp [ha, haA])
     simp at hbY; obtain ⟨ hbY_infty, hbA ⟩ := hbY
     rw [IsMin.iff_lowerbound' (IsTotal.subtype htotal)]
     use ⟨ _, hbY_infty ⟩, hbA; intro ⟨ x, hx ⟩ hxA
-    simp [Y_infty] at hx ⊢
-    obtain ⟨ Y', ⟨ hY'Ω₀, hY'Ω ⟩, hxY' ⟩ := hx
+    simp [Y_infty] at hx ⊢; obtain ⟨ Y', ⟨ hY'Ω₀, hY'Ω ⟩, hxY' ⟩ := hx
     sorry
   have hY_inftyΩ₀ : Y_infty ∈ Ω₀ := by
     sorry
@@ -310,11 +287,9 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
   simp [IsStrictUpperBound.iff] at hs
   have hYs_Ω : ⟨ _, hYs_Ω₀ ⟩ ∈ Ω := by
     simp only [Ω, Set.mem_setOf_eq, Set.mem_diff, Set.union_singleton, Set.mem_insert_iff, Set.mem_singleton_iff]
-    intro x ⟨ hx, hxx₀ ⟩
-    rcases hx with rfl | hx
+    rintro x ⟨ (rfl | hx), hxx₀ ⟩
     . unfold sY_infty; congr 1
-      apply (Subtype.val_injective _).symm
-      convert hF _
+      apply (Subtype.val_injective _).symm; convert hF _
       . ext y; simp; constructor
         . intro h; simp [h]; solve_by_elim
         rintro ⟨ h1 | h1, h2 ⟩
@@ -327,16 +302,14 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
     convert hYΩ _ hxY hxx₀ using 2
     apply Subtype.val_injective
     rw [hF, hF]
-    . ext y; simp [Y_infty]; intro hyx
-      constructor
-      . intro h
-        rcases h with rfl | ⟨ Y', ⟨hY'Ω₀, hY'Ω⟩, hyY' ⟩
+    . ext y; simp [Y_infty]; intro hyx; constructor
+      . rintro (rfl | ⟨ Y', ⟨hY'Ω₀, hY'Ω⟩, hyY' ⟩)
         . specialize hs _ hx'; order
         by_contra!
         specialize ex_8_5_13 (Y := ⟨_, hYΩ'⟩) (Y' := ⟨_, hY'Ω⟩) y (by simp [hyY', this])
         rw [IsStrictUpperBound.iff] at ex_8_5_13
         specialize ex_8_5_13 x (by simp [hxY]); order
-      intro hyY; right; refine ⟨ _, ⟨hYΩ₀, hYΩ'⟩, hyY ⟩
+      intro hyY; right; exact ⟨ _, ⟨hYΩ₀, hYΩ'⟩, hyY ⟩
     all_goals simp [hxY, hx', hxx₀]
   have hs_mem : sY_infty ∈ Y_infty := Set.mem_iUnion_of_mem ⟨ _, hYs_Ω ⟩ (by simp)
   specialize hs _ hs_mem; order
diff --git a/analysis/Analysis/Section_9_1.lean b/analysis/Analysis/Section_9_1.lean
index 113392d..994d72c 100644
--- a/analysis/Analysis/Section_9_1.lean
+++ b/analysis/Analysis/Section_9_1.lean
@@ -120,21 +120,16 @@ theorem closure_of_Ioo {a b:ℝ} (h:a < b) : closure (Set.Ioo a b) = Set.Icc a b
     rcases le_or_gt a x with h' | h'
     . specialize h h'
       use x-b, by linarith
-      intro y ⟨ h1, h2 ⟩
-      apply lt_of_lt_of_le _ (le_abs_self _)
-      linarith
+      intro y ⟨ h1, h2 ⟩; observe : x-y ≤ |x-y|; linarith
     use a-x, by linarith
-    intro y ⟨ h1, h2 ⟩
-    apply lt_of_lt_of_le _ (neg_le_abs _)
-    linarith
+    intro y ⟨ h1, h2 ⟩; observe : -(x-y) ≤ |x-y|; linarith
   intro ⟨ h1, h2 ⟩
   by_cases ha : x = a
   . sorry
   by_cases hb : x = b
   . sorry
   intro ε hε
-  use x, ⟨ by contrapose! ha; linarith, by contrapose! hb; linarith ⟩
-  simp [le_of_lt hε]
+  use x, ⟨ by contrapose! ha; linarith, by contrapose! hb; linarith ⟩; simp; order
 
 theorem closure_of_Ioc {a b:ℝ} (h:a < b) : closure (Set.Ioc a b) = Set.Icc a b := by
   sorry
@@ -176,22 +171,18 @@ theorem closure_of_Q :
 
 /-- Lemma 9.1.14 / Exercise 9.1.5 -/
 theorem limit_of_AdherentPt (X: Set ℝ) (x:ℝ) :
-  AdherentPt x X ↔ ∃ a : ℕ → ℝ, (∀ n, a n ∈ X) ∧ Filter.Tendsto a Filter.atTop (nhds x) := by
+  AdherentPt x X ↔ ∃ a : ℕ → ℝ, (∀ n, a n ∈ X) ∧ Filter.Tendsto a .atTop (nhds x) := by
     sorry
 
 theorem AdherentPt.of_mem {X: Set ℝ} {x: ℝ} (h: x ∈ X) : AdherentPt x X := by
-  rw [limit_of_AdherentPt]
-  use fun _ ↦ x
-  simp [h]
+  rw [limit_of_AdherentPt]; use fun _ ↦ x; simp [h]
 
 /-- Definition 9.1.15.  Here we use the Mathlib definition. -/
 theorem isClosed_def (X:Set ℝ): IsClosed X ↔ closure X = X :=
   closure_eq_iff_isClosed.symm
 
 theorem isClosed_def' (X:Set ℝ): IsClosed X ↔ ∀ x, AdherentPt x X → x ∈ X := by
-  simp [isClosed_def, subset_antisymm_iff, subset_closure]
-  simp [closure_def]
-  rfl
+  simp [isClosed_def, subset_antisymm_iff, subset_closure]; simp [closure_def]; rfl
 
 /-- Examples 9.1.16 -/
 theorem Icc_closed {a b:ℝ} : IsClosed (Set.Icc a b) := by sorry
@@ -231,17 +222,11 @@ theorem Q_not_closed : ¬ IsClosed ((fun n:ℚ ↦ (n:ℝ)) '' Set.univ) := by s
 
 /-- Corollary 9.1.17 -/
 theorem isClosed_iff_limits_mem (X: Set ℝ) :
-  IsClosed X ↔ ∀ (a:ℕ → ℝ) (L:ℝ), (∀ n, a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds L) → L ∈ X := by
+  IsClosed X ↔ ∀ (a:ℕ → ℝ) (L:ℝ), (∀ n, a n ∈ X) → Filter.Tendsto a .atTop (nhds L) → L ∈ X := by
   rw [isClosed_def']
   constructor
-  . intro h _ L _ _
-    apply h L
-    rw [limit_of_AdherentPt]
-    solve_by_elim
-  intro _ _ hx
-  rw [limit_of_AdherentPt] at hx
-  obtain ⟨ _, _, _ ⟩ := hx
-  solve_by_elim
+  . intro h _ L _ _; apply h L; rw [limit_of_AdherentPt]; solve_by_elim
+  intro _ _ hx; rw [limit_of_AdherentPt] at hx; obtain ⟨ _, _, _ ⟩ := hx; solve_by_elim
 
 /-- Definition 9.1.18 (Limit points) -/
 abbrev LimitPt (x:ℝ) (X: Set ℝ) := AdherentPt x (X \ {x})
@@ -262,7 +247,7 @@ example : IsolatedPt 3 ((Set.Ioo 1 2) ∪ {3}) := by sorry
 
 /-- Remark 9.1.20 -/
 theorem LimitPt.iff_limit (x:ℝ) (X: Set ℝ) :
-  LimitPt x X ↔ ∃ a : ℕ → ℝ, (∀ n, a n ∈ X \ {x}) ∧ Filter.Tendsto a Filter.atTop (nhds x) := by
+  LimitPt x X ↔ ∃ a : ℕ → ℝ, (∀ n, a n ∈ X \ {x}) ∧ Filter.Tendsto a .atTop (nhds x) := by
   simp [limit_of_AdherentPt]
 
 
@@ -281,24 +266,20 @@ theorem mem_Icc_isLimit {a b x:ℝ} (h: a < b) (hx: x ∈ Set.Icc a b) : LimitPt
   -- This proof is written to follow the structure of the original text, with some slight simplifications.
   simp at hx
   rw [LimitPt.iff_limit]
-  rcases le_iff_lt_or_eq.1 hx.2 with hxb | hxb
+  obtain hxb | hxb := le_iff_lt_or_eq.1 hx.2
   . use (fun n:ℕ ↦ (x + 1/(n+(b-x)⁻¹)))
     constructor
     . intro n; simp
       have : b - x > 0 := by linarith
       have : (b - x)⁻¹ > 0 := by positivity
       have : n + (b - x)⁻¹ > 0 := by linarith
-      refine ⟨ ⟨ ?_, ?_⟩, by linarith ⟩
-      . have : (n+(b - x)⁻¹)⁻¹ > 0 := by positivity
-        linarith
+      have : (n+(b - x)⁻¹)⁻¹ > 0 := by positivity
       have : (b-x)⁻¹ ≤ n + (b - x)⁻¹ := by linarith
       have : (n + (b - x)⁻¹)⁻¹ ≤ b-x := by rwa [inv_le_comm₀ (by positivity) (by positivity)]
-      linarith
-    convert Filter.Tendsto.const_add x (c := 0) _
-    . simp
+      refine ⟨ ⟨ ?_, ?_⟩, ?_ ⟩ <;> linarith
+    convert Filter.Tendsto.const_add x (c := 0) _; simp
     convert Filter.Tendsto.comp (f := fun (k:ℕ) ↦ (k:ℝ)) (g := fun k ↦ 1/(k+(b-x)⁻¹)) _ tendsto_natCast_atTop_atTop
-    convert tendsto_mul_add_inv_atTop_nhds_zero 1 (b - x)⁻¹ (by norm_num) using 2 with n
-    simp
+    convert tendsto_mul_add_inv_atTop_nhds_zero 1 (b - x)⁻¹ (by norm_num) using 2 with n; simp
   sorry
 
 
@@ -333,21 +314,11 @@ theorem mem_R_isLimit {x:ℝ} : LimitPt x (Set.univ) := by
 theorem isBounded_def (X: Set ℝ) : Bornology.IsBounded X ↔ ∃ M > 0, X ⊆ Set.Icc (-M) M := by
   simp [isBounded_iff_forall_norm_le]
   constructor
-  . intro ⟨ C, hC ⟩
-    use (max C 1)
-    constructor
-    . apply lt_of_lt_of_le _ (le_max_right _ _)
-      norm_num
-    intro x hx; specialize hC x hx
-    rw [abs_le'] at hC
-    simp [hC.1, hC.2]
-    have := le_max_left C 1
-    linarith
-  intro ⟨ M, hM, hXM ⟩; use M; intro x hx
-  replace hXM := hXM hx
-  simp [abs_le'] at hXM ⊢
-  simp [hXM]
-  linarith [hXM.1]
+  . intro ⟨ C, hC ⟩; use (max C 1)
+    refine ⟨ lt_of_lt_of_le (by norm_num) (le_max_right _ _), ?_ ⟩
+    peel hC with x hx hC; rw [abs_le'] at hC; simp [hC.1, hC.2]; linarith [le_max_left C 1]
+  intro ⟨ M, hM, hXM ⟩; use M; intro x hx; specialize hXM hx
+  simp [abs_le'] at hXM ⊢; simp [hXM]; linarith [hXM.1]
 
 /-- Example 9.1.23 -/
 theorem Icc_bounded (a b:ℝ) : Bornology.IsBounded (Set.Icc a b) := by sorry
@@ -371,7 +342,7 @@ theorem R_unbounded (a: ℝ) : ¬ Bornology.IsBounded (Set.univ: Set ℝ) := by
 theorem Heine_Borel (X: Set ℝ) :
   IsClosed X ∧ Bornology.IsBounded X ↔ ∀ a : ℕ → ℝ, (∀ n, a n ∈ X) →
   (∃ n : ℕ → ℕ, StrictMono n
-    ∧ ∃ L ∈ X, Filter.Tendsto (fun j ↦ a (n j)) Filter.atTop (nhds L)) := by
+    ∧ ∃ L ∈ X, Filter.Tendsto (fun j ↦ a (n j)) .atTop (nhds L)) := by
   sorry
 
 /-- Exercise 9.1.4 -/
diff --git a/analysis/Analysis/Section_9_10.lean b/analysis/Analysis/Section_9_10.lean
index e32bcc2..6c0a56a 100644
--- a/analysis/Analysis/Section_9_10.lean
+++ b/analysis/Analysis/Section_9_10.lean
@@ -43,19 +43,19 @@ theorem BddBelow.unbounded_iff' (X:Set ℝ) : ¬ BddBelow X ↔ sInf ((fun x:ℝ
   aesop
 
 /-- Definition 9.10.13 (Limit at infinity) -/
-theorem Filter.Tendsto.AtTop.iff {X: Set ℝ} (f:ℝ → ℝ) (L:ℝ) : Filter.Tendsto f (Filter.atTop ⊓ Filter.principal X) (nhds L) ↔ ∀ ε > (0:ℝ), ∃ M, ∀ x ∈ X ∩ Set.Ici M, |f x - L| < ε := by
+theorem Filter.Tendsto.AtTop.iff {X: Set ℝ} (f:ℝ → ℝ) (L:ℝ) : Filter.Tendsto f (.atTop ⊓ Filter.principal X) (nhds L) ↔ ∀ ε > (0:ℝ), ∃ M, ∀ x ∈ X ∩ Set.Ici M, |f x - L| < ε := by
   rw [LinearOrderedAddCommGroup.tendsto_nhds]
   peel with ε hε
   simp [Filter.eventually_inf_principal, Filter.eventually_atTop]
   aesop
 
 /-- Exercise 9.10.4 -/
-example : Filter.Tendsto (fun x:ℝ ↦ 1/x) (Filter.atTop ⊓ Filter.principal (Set.Ioi 0)) (nhds 0) := by
+example : Filter.Tendsto (fun x:ℝ ↦ 1/x) (.atTop ⊓ Filter.principal (Set.Ioi 0)) (nhds 0) := by
   sorry
 
 open Classical in
 /-- Exercise 9.10.1 -/
-example (a:ℕ → ℝ) (L:ℝ) : Filter.Tendsto (fun x:ℝ ↦ (if h:(∃ n:ℕ, x = n) then a h.choose else 0)) (Filter.atTop ⊓ Filter.principal ((fun n:ℕ ↦ (n:ℝ)) '' Set.univ)) (nhds L) ↔ Filter.Tendsto a Filter.atTop (nhds L) := by
+example (a:ℕ → ℝ) (L:ℝ) : Filter.Tendsto (fun x:ℝ ↦ (if h:(∃ n:ℕ, x = n) then a h.choose else 0)) (.atTop ⊓ Filter.principal ((fun n:ℕ ↦ (n:ℝ)) '' Set.univ)) (nhds L) ↔ Filter.Tendsto a .atTop (nhds L) := by
   sorry
 
 end Chapter9
diff --git a/analysis/Analysis/Section_9_3.lean b/analysis/Analysis/Section_9_3.lean
index 4778a0b..9828aa8 100644
--- a/analysis/Analysis/Section_9_3.lean
+++ b/analysis/Analysis/Section_9_3.lean
@@ -69,17 +69,16 @@ theorem Convergesto.iff (X:Set ℝ) (f: ℝ → ℝ) (L:ℝ) (x₀:ℝ) :
   rw [Filter.eventually_inf_principal]
   simp [Filter.Eventually, mem_nhds_iff_exists_Ioo_subset]
   constructor
-  . intro ⟨ δ, hpos, hδ ⟩; use (x₀-δ), (x₀+δ), ⟨by linarith, by linarith⟩; intro x
-    simp; exact fun h1 h2 hX ↦ hδ x hX h1 h2
+  . intro ⟨ δ, hpos, hδ ⟩; use (x₀-δ), (x₀+δ), ⟨by linarith, by linarith⟩
+    intro x; simp; intro h1 h2 hX; exact hδ x hX h1 h2
   intro ⟨ l, u, ⟨ h1, h2 ⟩, h ⟩
   have h1' : 0 < x₀ - l := by linarith
   have h2' : 0 < u - x₀ := by linarith
   set δ := min (x₀ - l) (u - x₀)
   have hδ1 : δ ≤ x₀ - l := min_le_left _ _
   have hδ2 : δ ≤ u - x₀ := min_le_right _ _
-  use δ, (by positivity)
-  intro x hxX _ _
-  specialize h (show x ∈ Set.Ioo l u by simp; exact ⟨by linarith, by linarith⟩)
+  use δ, (by positivity); intro x hxX _ _
+  specialize h (show x ∈ Set.Ioo l u by simp; constructor <;> linarith)
   simpa [hxX] using h
 
 /-- Example 9.3.8 -/
@@ -89,14 +88,13 @@ example: Convergesto (Set.Icc 1 3) (fun x ↦ x^2) 4 2 := by
 /-- Proposition 9.3.9 / Exercise 9.3.1 -/
 theorem Convergesto.iff_conv {E:Set ℝ} (f: ℝ → ℝ) (L:ℝ) {x₀:ℝ} (h: AdherentPt x₀ E) :
   Convergesto E f L x₀ ↔ ∀ a:ℕ → ℝ, (∀ n:ℕ, a n ∈ E) →
-  Filter.Tendsto a Filter.atTop (nhds x₀) →
-  Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L) := by
+  Filter.Tendsto a .atTop (nhds x₀) →
+  Filter.Tendsto (fun n ↦ f (a n)) .atTop (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.Tendsto a Filter.atTop (nhds x₀)) :
-  Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds L) := by
-  rw [iff_conv f L h] at hf
-  solve_by_elim
+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.Tendsto a .atTop (nhds x₀)) :
+  Filter.Tendsto (fun n ↦ f (a n)) .atTop (nhds L) := by
+  rw [iff_conv f L h] 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.
 
@@ -113,9 +111,7 @@ theorem Convergesto.add {E:Set ℝ} {f g: ℝ → ℝ} {L M:ℝ} {x₀:ℝ} (h:
   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 ⊢
-    intro a ha hconv
-    specialize hf a ha hconv
-    specialize hg a ha hconv
+    intro a ha hconv; specialize hf a ha hconv; specialize hg a ha hconv
     convert Filter.Tendsto.add hf hg using 1
 
 /-- Proposition 9.3.14 (Limit laws for functions) / Exercise 9.3.2 -/
@@ -209,9 +205,9 @@ open Classical in
 /-- Example 9.3.21 -/
 noncomputable abbrev f_9_3_21 : ℝ → ℝ := fun x ↦ if x ∈ (fun q:ℚ ↦ (q:ℝ)) '' Set.univ then 1 else 0
 
-example : Filter.Tendsto (fun n ↦ f_9_3_21 (1/n:ℝ)) Filter.atTop (nhds 1) := by sorry
+example : Filter.Tendsto (fun n ↦ f_9_3_21 (1/n:ℝ)) .atTop (nhds 1) := by sorry
 
-example : Filter.Tendsto (fun n ↦ f_9_3_21 ((Real.sqrt 2)/n:ℝ)) Filter.atTop (nhds 0) := by sorry
+example : Filter.Tendsto (fun n ↦ f_9_3_21 ((Real.sqrt 2)/n:ℝ)) .atTop (nhds 0) := by sorry
 
 example : ¬ ∃ L, Convergesto Set.univ f_9_3_21 L 0 := by sorry
 
diff --git a/analysis/Analysis/Section_9_4.lean b/analysis/Analysis/Section_9_4.lean
index a5ad5ae..89db4b2 100644
--- a/analysis/Analysis/Section_9_4.lean
+++ b/analysis/Analysis/Section_9_4.lean
@@ -61,7 +61,7 @@ example : ContinuousWithinAt f_9_4_6 (Set.Ici 0) 0 := by sorry
 theorem ContinuousWithinAt.tfae (X:Set ℝ) (f: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) :
   [
     ContinuousWithinAt f X x₀,
-    ∀ a:ℕ → ℝ, (∀ n, a n ∈ X) → Filter.Tendsto a Filter.atTop (nhds x₀) → Filter.Tendsto (fun n ↦  f (a n)) Filter.atTop (nhds (f x₀)),
+    ∀ a:ℕ → ℝ, (∀ n, a n ∈ X) → Filter.Tendsto a .atTop (nhds x₀) → Filter.Tendsto (fun n ↦  f (a n)) .atTop (nhds (f x₀)),
     ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x-x₀| < δ → |f x - f x₀| < ε
   ].TFAE := by
   sorry
@@ -69,8 +69,8 @@ theorem ContinuousWithinAt.tfae (X:Set ℝ) (f: ℝ → ℝ) {x₀:ℝ} (h : x
 /-- Remark 9.4.8 --/
 theorem Filter.Tendsto.comp_of_continuous {X:Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h : x₀ ∈ X)
   (h_cont: ContinuousWithinAt f X x₀) {a: ℕ → ℝ} (ha: ∀ n, a n ∈ X)
-  (hconv: Filter.Tendsto a Filter.atTop (nhds x₀)):
-  Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds (f x₀)) := by
+  (hconv: Filter.Tendsto a .atTop (nhds x₀)):
+  Filter.Tendsto (fun n ↦ f (a n)) .atTop (nhds (f x₀)) := by
   have := (ContinuousWithinAt.tfae X f h).out 0 1
   rw [this] at h_cont; solve_by_elim
 
@@ -78,41 +78,35 @@ theorem Filter.Tendsto.comp_of_continuous {X:Set ℝ} {f: ℝ → ℝ} {x₀:ℝ
 theorem ContinuousWithinAt.add {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (f + g) X x₀ := by
-  rw [ContinuousWithinAt.iff] at hf hg ⊢
-  convert Convergesto.add (AdherentPt.of_mem h) hf hg using 1
+  rw [iff] at hf hg ⊢; convert hf.add (AdherentPt.of_mem h) hg using 1
 
 
 theorem ContinuousWithinAt.sub {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (f - g) X x₀ := by
-  rw [ContinuousWithinAt.iff] at hf hg ⊢
-  convert Convergesto.sub (AdherentPt.of_mem h) hf hg using 1
+  rw [iff] at hf hg ⊢; convert hf.sub (AdherentPt.of_mem h) hg using 1
 
 theorem ContinuousWithinAt.max {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (max f g) X x₀ := by
-  rw [ContinuousWithinAt.iff] at hf hg ⊢
-  convert Convergesto.max (AdherentPt.of_mem h) hf hg using 1
+  rw [iff] at hf hg ⊢; convert hf.max (AdherentPt.of_mem h) hg using 1
 
 
 theorem ContinuousWithinAt.min {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (min f g) X x₀ := by
-  rw [ContinuousWithinAt.iff] at hf hg ⊢
-  convert Convergesto.min (AdherentPt.of_mem h) hf hg using 1
+  rw [iff] at hf hg ⊢; convert hf.min (AdherentPt.of_mem h) hg using 1
 
 
 theorem ContinuousWithinAt.mul' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X)
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (f * g) X x₀ := by
-  rw [ContinuousWithinAt.iff] at hf hg ⊢
-  convert Convergesto.mul (AdherentPt.of_mem h) hf hg using 1
+  rw [iff] at hf hg ⊢; convert hf.mul (AdherentPt.of_mem h) hg using 1
 
 theorem ContinuousWithinAt.div' {X:Set ℝ} (f g: ℝ → ℝ) {x₀:ℝ} (h : x₀ ∈ X) (hM: g x₀ ≠ 0)
   (hf: ContinuousWithinAt f X x₀) (hg: ContinuousWithinAt g X x₀) :
   ContinuousWithinAt (f / g) X x₀ := by
-  rw [ContinuousWithinAt.iff] at hf hg ⊢
-  convert Convergesto.div (AdherentPt.of_mem h) hM hf hg using 1
+  rw [iff] at hf hg ⊢; convert hf.div (AdherentPt.of_mem h) 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
diff --git a/analysis/Analysis/Section_9_5.lean b/analysis/Analysis/Section_9_5.lean
index 44997a6..8590a6d 100644
--- a/analysis/Analysis/Section_9_5.lean
+++ b/analysis/Analysis/Section_9_5.lean
@@ -19,30 +19,30 @@ Main constructions and results of this section:
 namespace Chapter9
 
 /-- Definition 9.5.1.  We give left and right limits the "junk" value of 0 if the limit does not exist. -/
-abbrev RightLimitExists (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := ∃ L, Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)
+abbrev RightLimitExists (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := ∃ L, Filter.Tendsto f ((nhds x₀) ⊓ .principal (X ∩ .Ioi x₀)) (nhds L)
 
 open Classical in
 noncomputable abbrev right_limit (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : ℝ := if h : RightLimitExists X f x₀ then h.choose else 0
 
-abbrev LeftLimitExists (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := ∃ L, Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds L)
+abbrev LeftLimitExists (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : Prop := ∃ L, Filter.Tendsto f ((nhds x₀) ⊓ .principal (X ∩ .Iio x₀)) (nhds L)
 
 open Classical in
 noncomputable abbrev left_limit (X: Set ℝ) (f: ℝ → ℝ) (x₀:ℝ) : ℝ := if h: LeftLimitExists X f x₀ then h.choose else 0
 
 theorem right_limit.eq {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} {L:ℝ} (had: AdherentPt x₀ (X ∩ Set.Ioi x₀))
-  (h: Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal (X ∩ Set.Ioi x₀)) (nhds L)) : RightLimitExists X f x₀ ∧ right_limit X f x₀ = L := by
+  (h: Filter.Tendsto f ((nhds x₀) ⊓ .principal (X ∩ .Ioi x₀)) (nhds L)) : RightLimitExists X f x₀ ∧ right_limit X f x₀ = L := by
   have h' : RightLimitExists X f x₀ := by use L
   simp [right_limit, h']
-  have hne : (nhds x₀ ⊓ Filter.principal (X ∩ Set.Ioi x₀)).NeBot := by
+  have hne : (nhds x₀ ⊓ .principal (X ∩ .Ioi x₀)).NeBot := by
     rwa [←nhdsWithin.eq_1, ←mem_closure_iff_nhdsWithin_neBot, closure_def']
   exact tendsto_nhds_unique h'.choose_spec h
 
 theorem left_limit.eq {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} {L:ℝ} (had: AdherentPt x₀ (X ∩ Set.Iio x₀))
-  (h: Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal (X ∩ Set.Iio x₀))
+  (h: Filter.Tendsto f ((nhds x₀) ⊓ .principal (X ∩ Set.Iio x₀))
   (nhds L)) : LeftLimitExists X f x₀ ∧ left_limit X f x₀ = L := by
   have h' : LeftLimitExists X f x₀ := by use L
   simp [left_limit, h']
-  have hne : (nhds x₀ ⊓ Filter.principal (X ∩ Set.Iio x₀)).NeBot := by
+  have hne : (nhds x₀ ⊓ .principal (X ∩ .Iio x₀)).NeBot := by
     rwa [←nhdsWithin.eq_1, ←mem_closure_iff_nhdsWithin_neBot, closure_def']
   exact tendsto_nhds_unique h'.choose_spec h
 
@@ -51,35 +51,35 @@ theorem right_limit.eq' {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h: RightLimitE
   simp [right_limit, h]; exact h.choose_spec
 
 theorem left_limit.eq' {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h: LeftLimitExists X f x₀) :
-  Filter.Tendsto f ((nhds x₀) ⊓ Filter.principal (X ∩ Set.Iio x₀)) (nhds (left_limit X f x₀)) := by
+  Filter.Tendsto f ((nhds x₀) ⊓ .principal (X ∩ .Iio x₀)) (nhds (left_limit X f x₀)) := by
   simp [left_limit, h]; exact h.choose_spec
 
 /-- Example 9.5.2.  The second part of this example is no longer operative as we assign "junk" values to our functions instead of leaving them undefined. -/
-example : right_limit Set.univ Real.sign 0 = 1 := by sorry
+example : right_limit .univ Real.sign 0 = 1 := by sorry
 
-example : left_limit Set.univ Real.sign 0 = -1 := by sorry
+example : left_limit .univ Real.sign 0 = -1 := by sorry
 
-theorem right_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentPt x₀ (X ∩ Set.Ioi x₀))
+theorem right_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentPt x₀ (X ∩ .Ioi x₀))
   (h: RightLimitExists X f x₀)
-  (a:ℕ → ℝ) (ha: ∀ n, a n ∈ X ∩ Set.Ioi x₀)
-  (hconv: Filter.Tendsto a Filter.atTop (nhds x₀)) :
-  Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds (right_limit X f x₀)) := by
+  (a:ℕ → ℝ) (ha: ∀ n, a n ∈ X ∩ .Ioi x₀)
+  (hconv: Filter.Tendsto a .atTop (nhds x₀)) :
+  Filter.Tendsto (fun n ↦ f (a n)) .atTop (nhds (right_limit X f x₀)) := by
   obtain ⟨ L, hL ⟩ := h
   apply Convergesto.comp had _ ha hconv
-  rwa [Convergesto.iff, (right_limit.eq had hL).2]
+  rwa [Convergesto.iff, (eq had hL).2]
 
-theorem left_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentPt x₀ (X ∩ Set.Iio x₀))
+theorem left_limit.conv {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (had: AdherentPt x₀ (X ∩ .Iio x₀))
   (h: LeftLimitExists X f x₀)
-  (a:ℕ → ℝ) (ha: ∀ n, a n ∈ X ∩ Set.Iio x₀)
-  (hconv: Filter.Tendsto a Filter.atTop (nhds x₀)) :
-  Filter.Tendsto (fun n ↦ f (a n)) Filter.atTop (nhds (left_limit X f x₀)) := by
+  (a:ℕ → ℝ) (ha: ∀ n, a n ∈ X ∩ .Iio x₀)
+  (hconv: Filter.Tendsto a .atTop (nhds x₀)) :
+  Filter.Tendsto (fun n ↦ f (a n)) .atTop (nhds (left_limit X f x₀)) := by
   obtain ⟨ L, hL ⟩ := h
   apply Convergesto.comp had _ ha hconv
-  rwa [Convergesto.iff, (left_limit.eq had hL).2]
+  rwa [Convergesto.iff, (eq had hL).2]
 
 /-- Proposition 9.5.3 -/
 theorem ContinuousAt.iff_eq_left_right_limit {X: Set ℝ} {f: ℝ → ℝ} {x₀:ℝ} (h: x₀ ∈ X)
-  (had_left: AdherentPt x₀ (X ∩ Set.Iio x₀)) (had_right: AdherentPt x₀ (X ∩ Set.Ioi x₀)) :
+  (had_left: AdherentPt x₀ (X ∩ .Iio x₀)) (had_right: AdherentPt x₀ (X ∩ .Ioi x₀)) :
   ContinuousWithinAt f X x₀ ↔ (RightLimitExists X f x₀ ∧ right_limit X f x₀ = f x₀) ∧ (LeftLimitExists X f x₀ ∧ left_limit X f x₀ = f x₀) := by
   -- This proof is written to follow the structure of the original text.
   constructor
@@ -94,8 +94,8 @@ theorem ContinuousAt.iff_eq_left_right_limit {X: Set ℝ} {f: ℝ → ℝ} {x₀
   rw [hright, ←Convergesto.iff] at hre
   rw [lheft, ←Convergesto.iff] at hle
   simp [Convergesto, Real.CloseNear, Real.CloseFn] at hre hle
-  specialize hre ε hε; obtain ⟨ δ_plus, hδ_plus, hre ⟩ := hre
-  specialize hle ε hε; obtain ⟨ δ_minus, hδ_minus, hle ⟩ := hle
+  obtain ⟨ δ_plus, hδ_plus, hre ⟩ := hre ε hε
+  obtain ⟨ δ_minus, hδ_minus, hle ⟩ := hle ε hε
   use min δ_plus δ_minus, (by positivity)
   intro x hx hxx₀
   rcases lt_trichotomy x x₀ with hlt | heq | hgt
diff --git a/analysis/Analysis/Section_9_6.lean b/analysis/Analysis/Section_9_6.lean
index 9f490b4..0c26cc3 100644
--- a/analysis/Analysis/Section_9_6.lean
+++ b/analysis/Analysis/Section_9_6.lean
@@ -107,7 +107,7 @@ theorem IsMaxOn.of_continuous_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf
   obtain ⟨ n, hn, ⟨ xmax, hmax, hconv⟩ ⟩ := (Heine_Borel (Set.Icc a b)).mp ⟨ hclosed, hbounded⟩ x hx
   use xmax, hmax
   have hn_lower (j:ℕ) : n j ≥ j := why_7_6_3 hn j
-  have hconv' : Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds (f xmax)) :=
+  have hconv' : Filter.Tendsto (fun j ↦ f (x (n j))) .atTop (nhds (f xmax)) :=
     Filter.Tendsto.comp_of_continuous hmax (hf.continuousWithinAt hmax) (fun j ↦ hx (n j)) hconv
   have hlower (j:ℕ) : m - 1/(j+1:ℝ) < f (x (n j)) := by
     apply lt_of_le_of_lt _ (hfx (n j))
@@ -116,7 +116,7 @@ theorem IsMaxOn.of_continuous_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf
   have hupper (j:ℕ) : f (x (n j)) ≤ m := by
     apply claim1
     simp only [Set.mem_image, E]; use x (n j), hx (n j)
-  have hconvm : Filter.Tendsto (fun j ↦ f (x (n j))) Filter.atTop (nhds m) := by
+  have hconvm : Filter.Tendsto (fun j ↦ f (x (n j))) .atTop (nhds m) := by
     apply Filter.Tendsto.squeeze (g := fun j ↦ m - 1/(j+1:ℝ)) (h := fun j ↦ m) (f := fun j ↦ f (x (n j)))
     . convert Filter.Tendsto.const_sub m (c:=0) _
       . simp
diff --git a/analysis/Analysis/Section_9_7.lean b/analysis/Analysis/Section_9_7.lean
index 44f007e..9b72b89 100644
--- a/analysis/Analysis/Section_9_7.lean
+++ b/analysis/Analysis/Section_9_7.lean
@@ -51,7 +51,7 @@ theorem intermediate_value {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: Continuou
       set x := fun n ↦ (hxe n).choose
       have hx1 (n:ℕ) : x n ∈ E := (hxe n).choose_spec.1
       have hx2 (n:ℕ) : c - 1/(n+1:ℝ) < x n := (hxe n).choose_spec.2
-      have : Filter.Tendsto x Filter.atTop (nhds c) := by
+      have : Filter.Tendsto x .atTop (nhds c) := by
         apply Filter.Tendsto.squeeze (g := fun j ↦ c - 1/(j+1:ℝ)) (h := fun j ↦ c) (f := x)
         . convert Filter.Tendsto.const_sub c tendsto_one_div_add_atTop_nhds_zero_nat
           simp
@@ -92,12 +92,12 @@ theorem intermediate_value {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: Continuou
         have := hmem n hn
         simp only [Set.mem_Icc] at this
         tauto
-      have hconv : Filter.Tendsto (fun n:ℕ ↦ c + 1/(n+1:ℝ)) Filter.atTop (nhds c) := by
+      have hconv : Filter.Tendsto (fun n:ℕ ↦ c + 1/(n+1:ℝ)) .atTop (nhds c) := by
         convert Filter.Tendsto.const_add c tendsto_one_div_add_atTop_nhds_zero_nat
         simp
       replace hf := (hf.continuousWithinAt hc).tendsto
       rw [nhdsWithin.eq_1] at hf
-      have hconv' : Filter.Tendsto (fun n:ℕ ↦ c + 1/(n+1:ℝ)) Filter.atTop (Filter.principal (Set.Icc a b)) := by
+      have hconv' : Filter.Tendsto (fun n:ℕ ↦ c + 1/(n+1:ℝ)) .atTop (Filter.principal (Set.Icc a b)) := by
         simp only [Filter.tendsto_principal, Filter.eventually_atTop]; use N
       replace hconv' := Filter.tendsto_inf.mpr ⟨ hconv, hconv' ⟩
       apply ge_of_tendsto (Filter.Tendsto.comp hf hconv') _
diff --git a/analysis/Analysis/Section_9_9.lean b/analysis/Analysis/Section_9_9.lean
index 4533cde..bc571d9 100644
--- a/analysis/Analysis/Section_9_9.lean
+++ b/analysis/Analysis/Section_9_9.lean
@@ -97,7 +97,7 @@ theorem Chapter6.Sequence.equiv_iff_rat (a b: Sequence) :
 
 /-- Lemma 9.9.7 / Exercise 9.9.1 -/
 theorem Chapter6.Sequence.equiv_iff (a b: Sequence) :
-  Sequence.equiv a b ↔ Filter.Tendsto (fun n ↦ a n - b n) Filter.atTop (nhds 0) := by
+  Sequence.equiv a b ↔ Filter.Tendsto (fun n ↦ a n - b n) .atTop (nhds 0) := by
   sorry
 
 
@@ -113,7 +113,7 @@ theorem UniformContinuousOn.iff_preserves_equiv {X:Set ℝ} (f: ℝ → ℝ) :
   sorry
 
 /-- Remark 9.9.9 -/
-theorem Chapter6.Sequence.equiv_const (x₀: ℝ) (x:ℕ → ℝ) : Filter.Tendsto x Filter.atTop (nhds x₀) ↔
+theorem Chapter6.Sequence.equiv_const (x₀: ℝ) (x:ℕ → ℝ) : Filter.Tendsto x .atTop (nhds x₀) ↔
   Sequence.equiv (x:Sequence) (fun n:ℕ ↦ x₀:Sequence) := by
   sorry
 
@@ -206,17 +206,17 @@ theorem UniformContinuousOn.of_continuousOn {a b:ℝ} {f:ℝ → ℝ}
   replace hcont := ContinuousOn.continuousWithinAt hcont hL
   have hconv' := Filter.Tendsto.comp_of_continuous hL hcont (fun k ↦ hxmem (j k)) hconv
   rw [Sequence.equiv_iff] at hequiv
-  replace hequiv : Filter.Tendsto (fun k ↦ x (n (j k)) - y (n (j k))) Filter.atTop (nhds 0) := by
-    have hj' : Filter.Tendsto j Filter.atTop Filter.atTop := StrictMono.tendsto_atTop hj
-    have hn' : Filter.Tendsto n Filter.atTop Filter.atTop := StrictMono.tendsto_atTop hmono
-    have hcoe : Filter.Tendsto (fun n:ℕ ↦ (n:ℤ)) Filter.atTop Filter.atTop := tendsto_natCast_atTop_atTop
+  replace hequiv : Filter.Tendsto (fun k ↦ x (n (j k)) - y (n (j k))) .atTop (nhds 0) := by
+    have hj' : Filter.Tendsto j .atTop .atTop := StrictMono.tendsto_atTop hj
+    have hn' : Filter.Tendsto n .atTop .atTop := StrictMono.tendsto_atTop hmono
+    have hcoe : Filter.Tendsto (fun n:ℕ ↦ (n:ℤ)) .atTop .atTop := tendsto_natCast_atTop_atTop
     exact hequiv.comp (hcoe.comp (hn'.comp hj'))
-  have hyconv : Filter.Tendsto (fun k ↦ y (n (j k))) Filter.atTop (nhds L) := by
+  have hyconv : Filter.Tendsto (fun k ↦ y (n (j k))) .atTop (nhds L) := by
     convert Filter.Tendsto.sub hconv hequiv with k
     . abel
     simp
   replace hyconv := Filter.Tendsto.comp_of_continuous hL hcont (fun k ↦ hymem (j k)) hyconv
-  have : Filter.Tendsto (fun k ↦ f (x (n (j k))) - f (y (n (j k)))) Filter.atTop (nhds 0) := by
+  have : Filter.Tendsto (fun k ↦ f (x (n (j k))) - f (y (n (j k)))) .atTop (nhds 0) := by
     convert Filter.Tendsto.sub hconv' hyconv
     simp
   sorry