diff --git a/analysis/Analysis/Appendix_A_7.lean b/analysis/Analysis/Appendix_A_7.lean
index 30efc0e..95044f8 100644
--- a/analysis/Analysis/Appendix_A_7.lean
+++ b/analysis/Analysis/Appendix_A_7.lean
@@ -59,7 +59,7 @@ def equality_as_equiv_relation (X:Type) : Setoid X := {
 open Real in
 /-- Example A.7.1 -/
 example {x y:ℝ} (h:x = y) : 2*x = 2*y ∧ sin x = sin y ∧ ∀ z, x + z = y + z := by
-  refine ⟨ ?_, ?_, ?_ ⟩
+  and_intros
   . rw [h]
   . rw [h]
   intro z
diff --git a/analysis/Analysis/Section_11_1.lean b/analysis/Analysis/Section_11_1.lean
index bf683e7..b10f242 100644
--- a/analysis/Analysis/Section_11_1.lean
+++ b/analysis/Analysis/Section_11_1.lean
@@ -182,90 +182,74 @@ abbrev BoundedInterval.joins (K I J: BoundedInterval) : Prop := (I:Set ℝ) ∩
   ∧ (K:Set ℝ) = (I:Set ℝ) ∪ (J:Set ℝ) ∧ |K|ₗ = |I|ₗ + |J|ₗ
 
 theorem BoundedInterval.join_Icc_Ioc {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Icc a c).joins (Icc a b) (Ioc b c) := by
-  refine ⟨ ?_, ?_, ?_ ⟩
+  and_intros
   . rw [Set.eq_empty_iff_forall_notMem]; intros; simp; intros; linarith
   . ext x; simp; constructor
-    . intro ⟨ h1, h2 ⟩; simp [h1, h2]; exact le_or_lt x b
-    rintro (h1 | h2)
-    . exact ⟨ h1.1, by linarith ⟩
-    exact ⟨ by linarith, h2.2 ⟩
+    . intro ⟨ _, _ ⟩; simp_all [le_or_lt x b]
+    rintro (_ | _) <;> and_intros <;> linarith
   simp [length, BoundedInterval.a, BoundedInterval.b,
         show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
 
 theorem BoundedInterval.join_Icc_Ioo {a b c:ℝ} (hab: a ≤ b) (hbc: b < c) : (Ico a c).joins (Icc a b) (Ioo b c) := by
-  refine ⟨ ?_, ?_, ?_ ⟩
+  and_intros
   . rw [Set.eq_empty_iff_forall_notMem]; intros; simp; intros; linarith
   . ext x; simp; constructor
-    . intro ⟨ h1, h2 ⟩; simp [h1, h2]; exact le_or_lt x b
-    rintro (h1 | h2)
-    . exact ⟨ h1.1, by linarith ⟩
-    exact ⟨ by linarith, h2.2 ⟩
+    . intro ⟨ _, _ ⟩; simp_all [le_or_lt x b]
+    rintro (_ | _) <;> and_intros <;> linarith
   simp [length, BoundedInterval.a, BoundedInterval.b,
         show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
 
 theorem BoundedInterval.join_Ioc_Ioc {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Ioc a c).joins (Ioc a b) (Ioc b c) := by
-  refine ⟨ ?_, ?_, ?_ ⟩
+  and_intros
   . rw [Set.eq_empty_iff_forall_notMem]; intros; simp; intros; linarith
   . ext x; simp; constructor
-    . intro ⟨ h1, h2 ⟩; simp [h1, h2]; exact le_or_lt x b
-    rintro (h1 | h2)
-    . exact ⟨ h1.1, by linarith ⟩
-    exact ⟨ by linarith, h2.2 ⟩
+    . intro ⟨ _, _ ⟩; simp_all [le_or_lt x b]
+    rintro (_ | _) <;> and_intros <;> linarith
   simp [length, BoundedInterval.a, BoundedInterval.b,
         show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
 
 theorem BoundedInterval.join_Ioc_Ioo {a b c:ℝ} (hab: a ≤ b) (hbc: b < c) : (Ioo a c).joins (Ioc a b) (Ioo b c) := by
-  refine ⟨ ?_, ?_, ?_ ⟩
+  and_intros
   . rw [Set.eq_empty_iff_forall_notMem]; intros; simp; intros; linarith
   . ext x; simp; constructor
-    . intro ⟨ h1, h2 ⟩; simp [h1, h2]; exact le_or_lt x b
-    rintro (h1 | h2)
-    . exact ⟨ h1.1, by linarith ⟩
-    exact ⟨ by linarith, h2.2 ⟩
+    . intro ⟨ _, _ ⟩; simp_all [le_or_lt x b]
+    rintro (_ | _) <;> and_intros <;> linarith
   simp [length, BoundedInterval.a, BoundedInterval.b,
         show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
 
 theorem BoundedInterval.join_Ico_Icc {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Icc a c).joins (Ico a b) (Icc b c) := by
-  refine ⟨ ?_, ?_, ?_ ⟩
+  and_intros
   . rw [Set.eq_empty_iff_forall_notMem]; intros; simp; intros; linarith
   . ext x; simp; constructor
-    . intro ⟨ h1, h2 ⟩; simp [h1, h2]; exact lt_or_le x b
-    rintro (h1 | h2)
-    . exact ⟨ h1.1, by linarith ⟩
-    exact ⟨ by linarith, h2.2 ⟩
+    . intro ⟨ _, _ ⟩; simp_all [lt_or_le x b]
+    rintro (_ | _) <;> and_intros <;> linarith
   simp [length, BoundedInterval.a, BoundedInterval.b,
         show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
 
 theorem BoundedInterval.join_Ico_Ico {a b c:ℝ} (hab: a ≤ b) (hbc: b ≤ c) : (Ico a c).joins (Ico a b) (Ico b c) := by
-  refine ⟨ ?_, ?_, ?_ ⟩
+  and_intros
   . rw [Set.eq_empty_iff_forall_notMem]; intros; simp; intros; linarith
   . ext x; simp; constructor
-    . intro ⟨ h1, h2 ⟩; simp [h1, h2]; exact lt_or_le x b
-    rintro (h1 | h2)
-    . exact ⟨ h1.1, by linarith ⟩
-    exact ⟨ by linarith, h2.2 ⟩
+    . intro ⟨ _, _ ⟩; simp_all [lt_or_le x b]
+    rintro (_ | _) <;> and_intros <;> linarith
   simp [length, BoundedInterval.a, BoundedInterval.b,
         show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
 
 theorem BoundedInterval.join_Ioo_Icc {a b c:ℝ} (hab: a < b) (hbc: b ≤ c) : (Ioc a c).joins (Ioo a b) (Icc b c) := by
-  refine ⟨ ?_, ?_, ?_ ⟩
+  and_intros
   . rw [Set.eq_empty_iff_forall_notMem]; intros; simp; intros; linarith
   . ext x; simp; constructor
-    . intro ⟨ h1, h2 ⟩; simp [h1, h2]; exact lt_or_le x b
-    rintro (h1 | h2)
-    . exact ⟨ h1.1, by linarith ⟩
-    exact ⟨ by linarith, h2.2 ⟩
+    . intro ⟨ _, _ ⟩; simp_all [lt_or_le x b]
+    rintro (_ | _) <;> and_intros <;> linarith
   simp [length, BoundedInterval.a, BoundedInterval.b,
         show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
 
 theorem BoundedInterval.join_Ioo_Ico {a b c:ℝ} (hab: a < b) (hbc: b ≤ c) : (Ioo a c).joins (Ioo a b) (Ico b c) := by
-  refine ⟨ ?_, ?_, ?_ ⟩
+  and_intros
   . rw [Set.eq_empty_iff_forall_notMem]; intros; simp; intros; linarith
   . ext x; simp; constructor
-    . intro ⟨ h1, h2 ⟩; simp [h1, h2]; exact lt_or_le x b
-    rintro (h1 | h2)
-    . exact ⟨ h1.1, by linarith ⟩
-    exact ⟨ by linarith, h2.2 ⟩
+    . intro ⟨ _, _ ⟩; simp_all [lt_or_le x b]
+    rintro (_ | _) <;> and_intros <;> linarith
   simp [length, BoundedInterval.a, BoundedInterval.b,
         show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
 
diff --git a/analysis/Analysis/Section_3_1.lean b/analysis/Analysis/Section_3_1.lean
index 165bed1..0860f46 100644
--- a/analysis/Analysis/Section_3_1.lean
+++ b/analysis/Analysis/Section_3_1.lean
@@ -224,9 +224,11 @@ theorem SetTheory.Set.singleton_uniq (a:Object) : ∃! (X:Set), ∀ x, x ∈ X 
 theorem SetTheory.Set.pair_uniq (a b:Object) : ∃! (X:Set), ∀ x, x ∈ X ↔ x = a ∨ x = b := by sorry
 
 /-- Remark 3.1.8 -/
+@[simp]
 theorem SetTheory.Set.pair_comm (a b:Object) : ({a,b}:Set) = {b,a} := by sorry
 
 /-- Remark 3.1.8 -/
+@[simp]
 theorem SetTheory.Set.pair_self (a:Object) : ({a,a}:Set) = {a} := by
   sorry
 
@@ -289,14 +291,17 @@ theorem SetTheory.Set.union_assoc (A B C:Set) : (A ∪ B) ∪ C = A ∪ (B ∪ C
   sorry
 
 /-- Proposition 3.1.27(c) -/
+@[simp]
 theorem SetTheory.Set.union_self (A:Set) : A ∪ A = A := by
   sorry
 
 /-- Proposition 3.1.27(a) -/
+@[simp]
 theorem SetTheory.Set.union_empty (A:Set) : A ∪ ∅ = A := by
   sorry
 
 /-- Proposition 3.1.27(a) -/
+@[simp]
 theorem SetTheory.Set.empty_union (A:Set) : ∅ ∪ A = A := by
   sorry
 
@@ -338,9 +343,11 @@ theorem SetTheory.Set.ssubset_def (X Y:Set) : X ⊂ Y ↔ (X ⊆ Y ∧ X ≠ Y)
 theorem SetTheory.Set.subset_congr_left {A A' B:Set} (hAA':A = A') (hAB: A ⊆ B) : A' ⊆ B := by sorry
 
 /-- Examples 3.1.16 -/
+@[simp]
 theorem SetTheory.Set.subset_self (A:Set) : A ⊆ A := by sorry
 
 /-- Examples 3.1.16 -/
+@[simp]
 theorem SetTheory.Set.empty_subset (A:Set) : ∅ ⊆ A := by sorry
 
 /-- Proposition 3.1.17 (Partial ordering by set inclusion) -/
@@ -407,6 +414,7 @@ lemma SetTheory.Set.coe_inj (A:Set) (x y:A) : x.val = y.val ↔ x = y := Subtype
 -/
 def SetTheory.Set.subtype_mk (A:Set) {x:Object} (hx:x ∈ A) : A := ⟨ x, hx ⟩
 
+@[simp]
 lemma SetTheory.Set.subtype_mk_coe {A:Set} {x:Object} (hx:x ∈ A) : A.subtype_mk hx = x := by rfl
 
 
@@ -423,6 +431,7 @@ theorem SetTheory.Set.specification_axiom' {A:Set} (P: A → Prop) (x:A) :
   (SetTheory.specification_axiom A P).2 x
 
 /-- Axiom 3.6 (axiom of specification) -/
+@[simp]
 theorem SetTheory.Set.specification_axiom'' {A:Set} (P: A → Prop) (x:Object) :
     x ∈ A.specify P ↔ ∃ h:x ∈ A, P ⟨ x, h ⟩ := by
   constructor
@@ -476,6 +485,7 @@ theorem SetTheory.Set.subset_union {A X: Set} (hAX: A ⊆ X) : A ∪ X = X := by
 theorem SetTheory.Set.union_subset {A X: Set} (hAX: A ⊆ X) : X ∪ A = X := by sorry
 
 /-- Proposition 3.1.27(c) -/
+@[simp]
 theorem SetTheory.Set.inter_self (A:Set) : A ∩ A = A := by
   sorry
 
@@ -543,6 +553,7 @@ abbrev SetTheory.Set.replace (A:Set) {P: A → Object → Prop}
   (hP : ∀ x y y', P x y ∧ P x y' → y = y') : Set := SetTheory.replace A P hP
 
 /-- Axiom 3.7 (Axiom of replacement) -/
+@[simp]
 theorem SetTheory.Set.replacement_axiom {A:Set} {P: A → Object → Prop}
   (hP: ∀ x y y', P x y ∧ P x y' → y = y') (y:Object) :
     y ∈ A.replace hP ↔ ∃ x, P x y := SetTheory.replacement_axiom A P hP y
@@ -718,6 +729,7 @@ theorem SetTheory.Set.inter_subset_right (A B:Set) : A ∩ B ⊆ B := by
   sorry
 
 /-- Exercise 3.1.7 -/
+@[simp]
 theorem SetTheory.Set.subset_inter_iff (A B C:Set) : C ⊆ A ∩ B ↔ C ⊆ A ∧ C ⊆ B := by
   sorry
 
@@ -730,13 +742,16 @@ theorem SetTheory.Set.subset_union_right (A B:Set) : B ⊆ A ∪ B := by
   sorry
 
 /-- Exercise 3.1.7 -/
+@[simp]
 theorem SetTheory.Set.union_subset_iff (A B C:Set) : A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C := by
   sorry
 
 /-- Exercise 3.1.8 -/
+@[simp]
 theorem SetTheory.Set.inter_union_cancel (A B:Set) : A ∩ (A ∪ B) = A := by sorry
 
 /-- Exercise 3.1.8 -/
+@[simp]
 theorem SetTheory.Set.union_inter_cancel (A B:Set) : A ∪ (A ∩ B) = A := by sorry
 
 /-- Exercise 3.1.9 -/
diff --git a/analysis/Analysis/Section_3_4.lean b/analysis/Analysis/Section_3_4.lean
index 2ef6d5e..4c887dd 100644
--- a/analysis/Analysis/Section_3_4.lean
+++ b/analysis/Analysis/Section_3_4.lean
@@ -49,17 +49,16 @@ theorem SetTheory.Set.image_eq_image {X Y:Set} (f:X → Y) (S: Set):
 
 theorem SetTheory.Set.image_in_codomain {X Y:Set} (f:X → Y) (S: Set) :
     image f S ⊆ Y := by
-  intro _ h; rw [mem_image] at h; obtain ⟨ x', hx', hf ⟩ := h
-  rw [← hf]; exact (f x').property
+  intro _ h; rw [mem_image] at h; obtain ⟨ x', hx', rfl ⟩ := h
+  exact (f x').property
 
 /-- Example 3.4.2 -/
 abbrev f_3_4_2 : nat → nat := fun n ↦ (2*n:ℕ)
 
 theorem SetTheory.Set.image_f_3_4_2 : image f_3_4_2 {1,2,3} = {2,4,6} := by
-  rw [ext_iff]
-  intros; simp only [mem_image, mem_triple, f_3_4_2]
+  rw [ext_iff]; intros; simp only [mem_image, mem_triple, f_3_4_2]
   constructor
-  · rintro ⟨_, (h | h | h), rfl⟩
+  · rintro ⟨x, (h | h | h), rfl⟩
     map_tacs [left; (right;left); (right;right)]
     all_goals simp_all
   rintro (h | h | h)
@@ -79,12 +78,11 @@ theorem SetTheory.Set.mem_image_of_eval_counter :
   Definition 3.4.4 (inverse images).
   Again, it is not required that U be a subset of Y.
 -/
-abbrev SetTheory.Set.preimage {X Y:Set} (f:X → Y) (U: Set) : Set :=
-  X.specify (P := fun x ↦ (f x).val ∈ U)
+abbrev SetTheory.Set.preimage {X Y:Set} (f:X → Y) (U: Set) : Set := X.specify (P := fun x ↦ (f x).val ∈ U)
 
+@[simp]
 theorem SetTheory.Set.mem_preimage {X Y:Set} (f:X → Y) (U: Set) (x:X) :
-    x.val ∈ preimage f U ↔ (f x).val ∈ U := by
-  rw [specification_axiom']
+    x.val ∈ preimage f U ↔ (f x).val ∈ U := by rw [specification_axiom']
 
 /--
   A version of mem_preimage that does not require x to be of type X.
@@ -92,14 +90,10 @@ theorem SetTheory.Set.mem_preimage {X Y:Set} (f:X → Y) (U: Set) (x:X) :
 theorem SetTheory.Set.mem_preimage' {X Y:Set} (f:X → Y) (U: Set) (x:Object) :
     x ∈ preimage f U ↔ ∃ x': X, x'.val = x ∧ (f x').val ∈ U := by
   constructor
-  . intro h
-    by_cases hx: x ∈ X
-    . use ⟨ x, hx ⟩
-      have := mem_preimage f U ⟨ x, hx ⟩; simp_all
-    . rw [preimage] at h
-      simp_all [X.specification_axiom h]
-  . intro ⟨ x', hx', hfx' ⟩
-    rwa [← hx', mem_preimage]
+  . intro h; by_cases hx: x ∈ X
+    . use ⟨ x, hx ⟩; have := mem_preimage f U ⟨ x, hx ⟩; simp_all
+    . simp_all [X.specification_axiom h]
+  . rintro ⟨ x', rfl, hfx' ⟩; rwa [mem_preimage]
 
 /-- Connection with Mathlib's notion of preimage. -/
 theorem SetTheory.Set.preimage_eq {X Y:Set} (f:X → Y) (U: Set) :
@@ -112,8 +106,7 @@ theorem SetTheory.Set.preimage_eq {X Y:Set} (f:X → Y) (U: Set) :
   rintro ⟨x', hy, rfl⟩; simp only [_root_.Set.mem_setOf] at hy; use x'
 
 theorem SetTheory.Set.preimage_in_domain {X Y:Set} (f:X → Y) (U: Set) :
-    (preimage f U) ⊆ X := by
-  intro x h; rw [preimage] at h; exact specification_axiom h
+    (preimage f U) ⊆ X := by intro x h; simp at h; tauto
 
 /-- Example 3.4.6 -/
 theorem SetTheory.Set.preimage_f_3_4_2 : preimage f_3_4_2 {2,4,6} = {1,2,3} := by
@@ -121,13 +114,10 @@ theorem SetTheory.Set.preimage_f_3_4_2 : preimage f_3_4_2 {2,4,6} = {1,2,3} := b
   intro x
   simp only [mem_preimage', mem_triple, f_3_4_2]
   constructor
-  · rintro ⟨x, rfl, (h | h | h)⟩
-    · left; simp_all
-    · right; left; simp_all; omega
-    · right; right; simp_all; omega
-  rintro (h | h | h)
+  · rintro ⟨x, rfl, (h | h | h)⟩ <;> simp_all <;> omega
+  rintro (rfl | rfl | rfl)
   map_tacs [use 1; use 2; use 3]
-  all_goals simp_all
+  all_goals simp
 
 theorem SetTheory.Set.image_preimage_f_3_4_2 :
     image f_3_4_2 (preimage f_3_4_2 {1,2,3}) ≠ {1,2,3} := by sorry
@@ -137,10 +127,8 @@ example : (fun n:ℤ ↦ n^2) ⁻¹' {0,1,4} = {-2,-1,0,1,2} := by
   ext x
   refine ⟨ ?_, by aesop ⟩
   rintro (h | h | h)
-  · aesop
-  · aesop
-  have : 2 ^ 2 = (4:ℤ) := by norm_num
-  rw [←h, sq_eq_sq_iff_eq_or_eq_neg] at this; aesop
+  on_goal 3 => have : 2 ^ 2 = (4:ℤ) := (by norm_num); rw [←h, sq_eq_sq_iff_eq_or_eq_neg] at this
+  all_goals aesop
 
 example : (fun n:ℤ ↦ n^2) ⁻¹' ((fun n:ℤ ↦ n^2) '' {-1,0,1,2}) ≠ {-1,0,1,2} := by sorry
 
@@ -161,6 +149,7 @@ theorem SetTheory.Set.coe_of_fun_inj {X Y:Set} (f g:X → Y) : (f:Object) = (g:O
   simp [coe_of_fun]
 
 /-- Axiom 3.11 (Power set axiom) --/
+@[simp]
 theorem SetTheory.Set.powerset_axiom {X Y:Set} (F:Object) :
     F ∈ (X ^ Y) ↔ ∃ f: Y → X, f = F := SetTheory.powerset_axiom X Y F
 
@@ -181,26 +170,23 @@ theorem SetTheory.Set.example_3_4_9 (F:Object) :
     F ∈ ({0,1}:Set) ^ ({4,7}:Set) ↔ F = f_3_4_9_a
     ∨ F = f_3_4_9_b ∨ F = f_3_4_9_c ∨ F = f_3_4_9_d := by
   rw [powerset_axiom]
-  constructor
-  · rintro ⟨f, rfl⟩
-    unfold f_3_4_9_a f_3_4_9_b f_3_4_9_c f_3_4_9_d
-    simp [coe_of_fun_inj, mem_pair] at *
-    have := (f ⟨4, by simp⟩).property
-    have := (f ⟨7, by simp⟩).property
-    by_cases (f ⟨4, by simp⟩).val = (0: Object) <;>
-    by_cases (f ⟨7, by simp⟩).val = (0: Object)
-    map_tacs [left; (right;left); (right;right;left); (right;right;right)]
-    all_goals ext ⟨_, hx⟩; simp [mem_pair] at hx; aesop
-  rintro (h | h | h | h)
-  map_tacs [use f_3_4_9_a; use f_3_4_9_b; use f_3_4_9_c; use f_3_4_9_d]
-  all_goals exact h.symm
+  refine ⟨?_, by aesop ⟩
+  rintro ⟨f, rfl⟩
+  unfold f_3_4_9_a f_3_4_9_b f_3_4_9_c f_3_4_9_d
+  have h1 := (f ⟨4, by simp⟩).property
+  have h2 := (f ⟨7, by simp⟩).property
+  simp [coe_of_fun_inj, mem_pair] at *
+  rcases h1 with _ | _ <;> rcases h2 with _ | _
+  map_tacs [(right;right;right); (right;right;left); (right;left); left]
+  all_goals ext ⟨_, hx⟩; simp [mem_pair] at hx; aesop
 
 /-- Exercise 3.4.6 (i). One needs to provide a suitable definition of the power set here. -/
-abbrev SetTheory.Set.powerset (X:Set) : Set :=
+def SetTheory.Set.powerset (X:Set) : Set :=
   (({0,1} ^ X): Set).replace (P := sorry) (by sorry)
 
 open Classical in
 /-- Exercise 3.4.6 (i) -/
+@[simp]
 theorem SetTheory.Set.mem_powerset {X:Set} (x:Object) :
     x ∈ powerset X ↔ ∃ Y:Set, x = Y ∧ Y ⊆ X := by sorry
 
@@ -256,12 +242,10 @@ abbrev SetTheory.Set.iUnion (I: Set) (A: I → Set) : Set :=
 
 theorem SetTheory.Set.mem_iUnion {I:Set} (A: I → Set) (x:Object) :
     x ∈ iUnion I A ↔ ∃ α:I, x ∈ A α := by
-  rw [union_axiom]
-  constructor
+  rw [union_axiom]; constructor
   . intro ⟨ _, _, hS ⟩; rw [replacement_axiom] at hS; obtain ⟨ α, hα ⟩ := hS
     simp_all; use α.val, α.property
-  intro ⟨ α, hx ⟩; refine ⟨ A α, hx, ?_ ⟩
-  rw [replacement_axiom]; use α
+  intro ⟨ α, hx ⟩; refine ⟨ A α, hx, by rw [replacement_axiom]; use α ⟩
 
 open Classical in
 noncomputable abbrev SetTheory.Set.index_example : ({1,2,3}:Set) → Set :=
@@ -361,8 +345,7 @@ lemma SetTheory.Set.mem_powerset' {S S' : Set} : (S': Object) ∈ S.powerset ↔
 lemma SetTheory.Set.mem_union_powerset_replace_iff {S : Set} {P : S.powerset → Object → Prop} {hP : _} {x : Object} :
     x ∈ union (S.powerset.replace (P := P) hP) ↔
     ∃ (S' : S.powerset) (U : Set), P S' U ∧ x ∈ U := by
-  simp only [union_axiom, replacement_axiom]
-  tauto
+  simp only [union_axiom, replacement_axiom]; tauto
 
 /-- Exercise 3.4.7 -/
 theorem SetTheory.Set.partial_functions {X Y:Set} :
diff --git a/analysis/Analysis/Section_3_5.lean b/analysis/Analysis/Section_3_5.lean
index 158903d..8089426 100644
--- a/analysis/Analysis/Section_3_5.lean
+++ b/analysis/Analysis/Section_3_5.lean
@@ -37,6 +37,7 @@ structure OrderedPair where
 #check OrderedPair.ext
 
 /-- Definition 3.5.1 (Ordered pair) -/
+@[simp]
 theorem OrderedPair.eq (x y x' y' : Object) :
     (⟨ x, y ⟩ : OrderedPair) = (⟨ x', y' ⟩ : OrderedPair) ↔ x = x' ∧ y = y' := by aesop
 
@@ -53,20 +54,15 @@ instance OrderedPair.inst_coeObject : Coe OrderedPair Object where
   the full Cartesian product
 -/
 abbrev SetTheory.Set.slice (x:Object) (Y:Set) : Set :=
-  Y.replace (P := fun y z ↦ z = (⟨x, y⟩:OrderedPair)) (by
-    intro y z z' ⟨ hz, hz'⟩
-    simp_all
-  )
+  Y.replace (P := fun y z ↦ z = (⟨x, y⟩:OrderedPair)) (by intros; simp_all)
 
+@[simp]
 theorem SetTheory.Set.mem_slice (x z:Object) (Y:Set) :
     z ∈ (SetTheory.Set.slice x Y) ↔ ∃ y:Y, z = (⟨x, y⟩:OrderedPair) := replacement_axiom _ _
 
 /-- Definition 3.5.2 (Cartesian product) -/
 abbrev SetTheory.Set.cartesian (X Y:Set) : Set :=
-  union (X.replace (P := fun x z ↦ z = slice x Y) (by
-    intro x z z' ⟨ hz, hz' ⟩
-    simp_all
-  ))
+  union (X.replace (P := fun x z ↦ z = slice x Y) (by intros; simp_all))
 
 /-- This instance enables the ×ˢ notation for Cartesian product. -/
 instance SetTheory.Set.inst_SProd : SProd Set Set Set where
@@ -74,73 +70,47 @@ instance SetTheory.Set.inst_SProd : SProd Set Set Set where
 
 example (X Y:Set) : X ×ˢ Y = SetTheory.Set.cartesian X Y := rfl
 
+@[simp]
 theorem SetTheory.Set.mem_cartesian (z:Object) (X Y:Set) :
     z ∈ X ×ˢ Y ↔ ∃ x:X, ∃ y:Y, z = (⟨x, y⟩:OrderedPair) := by
-  simp only [SProd.sprod, union_axiom]
-  constructor
-  . intro h
-    obtain ⟨ S, hz, hS ⟩ := h
-    rw [replacement_axiom] at hS
-    obtain ⟨ x, hx ⟩ := hS
-    simp at hx
-    rw [hx, mem_slice] at hz
-    obtain ⟨ y, rfl ⟩ := hz
-    use x, y
-  intro h
-  obtain ⟨ x, y, rfl ⟩ := h
-  use slice x Y
-  constructor
-  . rw [mem_slice]
-    use y
-  rw [replacement_axiom]
-  use x
+  simp only [SProd.sprod, union_axiom]; constructor
+  . intro ⟨ S, hz, hS ⟩; rw [replacement_axiom] at hS; obtain ⟨ x, hx ⟩ := hS
+    use x; simp_all
+  rintro ⟨ x, y, rfl ⟩; use slice x Y; refine ⟨ by simp, ?_ ⟩
+  rw [replacement_axiom]; use x
 
 abbrev SetTheory.Set.curry {X Y Z:Set} (f: X ×ˢ Y → Z) : X → Y → Z :=
-  fun x y ↦ f ⟨ (⟨ x, y ⟩:OrderedPair), by rw [mem_cartesian]; use x, y ⟩
+  fun x y ↦ f ⟨ (⟨ x, y ⟩:OrderedPair), by simp ⟩
 
 noncomputable abbrev SetTheory.Set.fst {X Y:Set} (z:X ×ˢ Y) : X :=
-  (show ∃ x:X, ∃ y:Y, z.val = (⟨ x, y ⟩:OrderedPair)
-  by exact (mem_cartesian _ _ _).mp z.property).choose
+  ((mem_cartesian _ _ _).mp z.property).choose
 
 noncomputable abbrev SetTheory.Set.snd {X Y:Set} (z:X ×ˢ Y) : Y :=
-  (show ∃ y:Y, ∃ x:X, z.val = (⟨ x, y ⟩:OrderedPair)
-  by rw [exists_comm]; exact (mem_cartesian _ _ _).mp z.property).choose
+  (exists_comm.mp ((mem_cartesian _ _ _).mp z.property)).choose
 
 theorem SetTheory.Set.pair_eq_fst_snd {X Y:Set} (z:X ×ˢ Y) :
     z.val = (⟨ fst z, snd z ⟩:OrderedPair) := by
-  obtain ⟨ y, hy ⟩ := ((mem_cartesian _ _ _).mp z.property).choose_spec
-  obtain ⟨ x, hx ⟩ := (exists_comm.mp ((mem_cartesian _ _ _).mp z.property)).choose_spec
-  change z.val = (⟨ fst z, y ⟩:OrderedPair) at hy
-  change z.val = (⟨ x, snd z ⟩:OrderedPair) at hx
-  simp only [hx, EmbeddingLike.apply_eq_iff_eq, OrderedPair.eq] at hy ⊢
-  simp [hy.1]
+  have := (mem_cartesian _ _ _).mp z.property
+  obtain ⟨ y, hy: z.val = (⟨ fst z, y ⟩:OrderedPair)⟩ := this.choose_spec
+  obtain ⟨ x, hx: z.val = (⟨ x, snd z ⟩:OrderedPair)⟩ := (exists_comm.mp this).choose_spec
+  simp_all [EmbeddingLike.apply_eq_iff_eq]
 
 def SetTheory.Set.mk_cartesian {X Y:Set} (x:X) (y:Y) : X ×ˢ Y :=
-  ⟨(⟨ x, y ⟩:OrderedPair), by rw [mem_cartesian]; use x, y⟩
+  ⟨(⟨ x, y ⟩:OrderedPair), by simp⟩
 
 @[simp]
 theorem SetTheory.Set.fst_of_mk_cartesian {X Y:Set} (x:X) (y:Y) :
     fst (mk_cartesian x y) = x := by
-  let z := mk_cartesian x y
-  obtain ⟨ y', hy ⟩ := ((mem_cartesian _ _ _).mp z.property).choose_spec
-  change z.val = (⟨ fst z, y' ⟩:OrderedPair) at hy
-  unfold z at hy
-  rw [mk_cartesian] at hy ⊢
-  rw [EmbeddingLike.apply_eq_iff_eq, OrderedPair.eq] at hy
-  rw [Subtype.val_inj] at hy
-  rw [← hy.1]
+  let z := mk_cartesian x y; have := (mem_cartesian _ _ _).mp z.property
+  obtain ⟨ y', hy: z.val = (⟨ fst z, y' ⟩:OrderedPair) ⟩ := this.choose_spec
+  simp [z, mk_cartesian, Subtype.val_inj] at hy ⊢; rw [←hy.1]
 
 @[simp]
 theorem SetTheory.Set.snd_of_mk_cartesian {X Y:Set} (x:X) (y:Y) :
     snd (mk_cartesian x y) = y := by
-  let z := mk_cartesian x y
-  obtain ⟨ x', hx ⟩ := (exists_comm.mp ((mem_cartesian _ _ _).mp z.property)).choose_spec
-  change z.val = (⟨ x', snd z ⟩:OrderedPair) at hx
-  unfold z at hx
-  rw [mk_cartesian] at hx ⊢
-  rw [EmbeddingLike.apply_eq_iff_eq, OrderedPair.eq] at hx
-  repeat rw [Subtype.val_inj] at hx
-  rw [← hx.2]
+  let z := mk_cartesian x y; have := (mem_cartesian _ _ _).mp z.property
+  obtain ⟨ x', hx: z.val = (⟨ x', snd z ⟩:OrderedPair) ⟩ := (exists_comm.mp this).choose_spec
+  simp [z, mk_cartesian, Subtype.val_inj] at hx ⊢; rw [←hx.2]
 
 noncomputable abbrev SetTheory.Set.uncurry {X Y Z:Set} (f: X → Y → Z) : X ×ˢ Y → Z :=
   fun z ↦ f (fst z) (snd z)
@@ -181,14 +151,10 @@ abbrev SetTheory.Set.iProd {I: Set} (X: I → Set) : Set :=
 /-- Definition 3.5.7 -/
 theorem SetTheory.Set.mem_iProd {I: Set} {X: I → Set} (t:Object) :
     t ∈ iProd X ↔ ∃ a: ∀ i, X i, t = tuple a := by
-  simp only [iProd, specification_axiom'']
-  constructor
-  . intro ⟨ ht, a, h ⟩
-    use a
+  simp only [iProd, specification_axiom'']; constructor
+  . intro ⟨ ht, a, h ⟩; use a
   intro ⟨ a, ha ⟩
-  have h : t ∈ (I.iUnion X)^I := by
-    rw [powerset_axiom, ha]
-    use fun i ↦ ⟨ a i, by rw [mem_iUnion]; use i; exact (a i).property ⟩
+  have h : t ∈ (I.iUnion X)^I := by simp [ha]
   use h, a
 
 theorem SetTheory.Set.tuple_mem_iProd {I: Set} {X: I → Set} (a: ∀ i, X i) :
@@ -260,27 +226,19 @@ into the field of higher order category theory, which we will not pursue here.
 abbrev SetTheory.Set.Fin (n:ℕ) : Set := nat.specify (fun m ↦ (m:ℕ) < n)
 
 theorem SetTheory.Set.mem_Fin (n:ℕ) (x:Object) : x ∈ Fin n ↔ ∃ m, m < n ∧ x = m := by
-  rw [specification_axiom'']
-  constructor
-  . intro ⟨ h1, h2 ⟩
-    use ((⟨ x, h1 ⟩:nat):ℕ)
-    simp [h2]
+  rw [specification_axiom'']; constructor
+  . intro ⟨ h1, h2 ⟩; use ↑(⟨ x, h1 ⟩:nat); simp [h2]
     calc
       x = (⟨ x, h1 ⟩:nat) := rfl
-      _ = _ :=  by congr; simp
+      _ = _ := by congr; simp
   intro ⟨ m, hm, h ⟩
   use (by rw [h, ←SetTheory.Object.ofnat_eq]; exact (m:nat).property)
-  convert hm
-  simp [h, Equiv.symm_apply_eq]
-  rfl
+  convert hm; simp [h, Equiv.symm_apply_eq]; rfl
 
 abbrev SetTheory.Set.Fin_mk (n m:ℕ) (h: m < n): Fin n := ⟨ m, by rw [mem_Fin]; use m ⟩
 
 theorem SetTheory.Set.mem_Fin' {n:ℕ} (x:Fin n) : ∃ m, ∃ h : m < n, x = Fin_mk n m h := by
-  have := x.property
-  rw [mem_Fin] at this
-  obtain ⟨ m, hm, this ⟩ := this
-  use m, hm
+  obtain ⟨ m, hm, this ⟩ := (mem_Fin _ _).mp x.property; use m, hm
   simp [Fin_mk, ←Subtype.val_inj, this]
 
 @[coe]
@@ -290,16 +248,13 @@ noncomputable instance SetTheory.Set.Fin.inst_coeNat {n:ℕ} : CoeOut (Fin n) 
   coe := SetTheory.Set.Fin.toNat
 
 theorem SetTheory.Set.Fin.toNat_spec {n:ℕ} (i: Fin n) :
-    ∃ h : (i:ℕ) < n, i = Fin_mk n (i:ℕ) h := (mem_Fin' i).choose_spec
+    ∃ h : i < n, i = Fin_mk n i h := (mem_Fin' i).choose_spec
 
-theorem SetTheory.Set.Fin.toNat_lt {n:ℕ} (i: Fin n) : (i:ℕ) < n := (toNat_spec i).choose
+theorem SetTheory.Set.Fin.toNat_lt {n:ℕ} (i: Fin n) : i < n := (toNat_spec i).choose
 
 @[simp]
 theorem SetTheory.Set.Fin.coe_toNat {n:ℕ} (i: Fin n) : ((i:ℕ):Object) = (i:Object) := by
-  obtain ⟨ h, h' ⟩ := toNat_spec i
-  set j := (i:ℕ)
-  change i = Fin_mk n j h at h'
-  rw [h']
+  set j := (i:ℕ); obtain ⟨ h, h':i = Fin_mk n j h ⟩ := toNat_spec i; rw [h']
 
 @[simp]
 theorem SetTheory.Set.Fin.toNat_mk {n:ℕ} (m:ℕ) (h: m < n) : (Fin_mk n m h : ℕ) = m := by
@@ -307,10 +262,8 @@ theorem SetTheory.Set.Fin.toNat_mk {n:ℕ} (m:ℕ) (h: m < n) : (Fin_mk n m h :
   rwa [SetTheory.Object.natCast_inj] at this
 
 abbrev SetTheory.Set.Fin_embed (n N:ℕ) (h: n ≤ N) (i: Fin n) : Fin N := ⟨ i.val, by
-  have := i.property
-  rw [mem_Fin] at this ⊢
-  obtain ⟨ m, hm, im ⟩ := this
-  use m, by linarith
+  have := i.property; rw [mem_Fin] at this ⊢
+  obtain ⟨ m, hm, im ⟩ := this; use m, by linarith
 ⟩
 
 /--
@@ -329,43 +282,30 @@ theorem SetTheory.Set.finite_choice {n:ℕ} {X: Fin n → Set} (h: ∀ i, X i 
   -- (although it is more convenient to induct from 0 rather than 1)
   induction' n with n hn
   . have : Fin 0 = ∅ := by
-      rw [eq_empty_iff_forall_notMem]
-      intros
-      by_contra! h
-      simp [specification_axiom''] at h
+      rw [eq_empty_iff_forall_notMem]; intros; by_contra! h; simp at h
     have empty (i:Fin 0) : X i := False.elim (by rw [this] at i; exact not_mem_empty i i.property)
-    apply nonempty_of_inhabited (x := tuple empty)
-    rw [mem_iProd]
-    use empty
+    apply nonempty_of_inhabited (x := tuple empty); rw [mem_iProd]; use empty
   set X' : Fin n → Set := fun i ↦ X (Fin_embed n (n+1) (by linarith) i)
   have hX' (i: Fin n) : X' i ≠ ∅ := h _
   obtain ⟨ x'_obj, hx' ⟩ := nonempty_def (hn hX')
-  rw [mem_iProd] at hx'
-  obtain ⟨ x', rfl ⟩ := hx'
+  rw [mem_iProd] at hx'; obtain ⟨ x', rfl ⟩ := hx'
   set last : Fin (n+1) := Fin_mk (n+1) n (by linarith)
   obtain ⟨ a, ha ⟩ := nonempty_def (h last)
   set x : ∀ i, X i := by
     intro i
-    have := mem_Fin' i
     classical
     -- it is unfortunate here that classical logic is required to perform this gluing; this is
     -- because `nat` is technically not an inductive type.  There should be some workaround
     -- involving the equivalence between `nat` and `ℕ` (which is an inductive type).
     cases decEq i last with
-      | isTrue heq =>
-        rw [heq]
-        exact ⟨ a, ha ⟩
+      | isTrue heq => rw [heq]; exact ⟨ a, ha ⟩
       | isFalse heq =>
         have : ∃ m, ∃ h: m < n, X i = X' (Fin_mk n m h) := by
-          obtain ⟨ m, h, this ⟩ := this
-          have h' : m ≠ n := by
-            contrapose! heq
-            simp [this, last, heq]
+          obtain ⟨ m, h, this ⟩ := mem_Fin' i
+          have h' : m ≠ n := by contrapose! heq; simp [this, last, heq]
           replace h' : m < n := by contrapose! h'; linarith
-          use m, h'
-          simp [X']; congr
-        rw [this.choose_spec.choose_spec]
-        exact x' _
+          use m, h'; simp [X']; congr
+        rw [this.choose_spec.choose_spec]; exact x' _
   exact nonempty_of_inhabited (tuple_mem_iProd x)
 
 /-- Exercise 3.5.1, second part (requires axiom of regularity) -/
diff --git a/analysis/Analysis/Section_3_6.lean b/analysis/Analysis/Section_3_6.lean
index d5ecccb..df782b2 100644
--- a/analysis/Analysis/Section_3_6.lean
+++ b/analysis/Analysis/Section_3_6.lean
@@ -165,64 +165,36 @@ theorem SetTheory.Set.card_to_has_card (X:Set) {n: ℕ} (hn: n ≠ 0): X.card =
   contrapose! hn; simp only [card, hn, ↓reduceDIte]
 
 theorem SetTheory.Set.card_fin_eq (n:ℕ): (Fin n).has_card n := by
-  rw [has_card_iff]
-  use id
-  exact Function.bijective_id
+  rw [has_card_iff]; exact ⟨ id, Function.bijective_id ⟩
 
-theorem SetTheory.Set.Fin_card {n:ℕ}: (Fin n).card = n := by
-  exact has_card_to_card _ _ (card_fin_eq n)
+theorem SetTheory.Set.Fin_card {n:ℕ}: (Fin n).card = n := has_card_to_card _ _ (card_fin_eq n)
 
-theorem SetTheory.Set.Fin_finite {n:ℕ}: (Fin n).finite := by
-  exact ⟨n, card_fin_eq n⟩
+theorem SetTheory.Set.Fin_finite {n:ℕ}: (Fin n).finite := ⟨n, card_fin_eq n⟩
 
 theorem SetTheory.Set.EquivCard_to_has_card_eq {X Y:Set} (n: ℕ) (h: X ≈ Y): X.has_card n ↔ Y.has_card n := by
-  obtain ⟨f, hf⟩ := h
-  let e := Equiv.ofBijective f hf
+  obtain ⟨f, hf⟩ := h; let e := Equiv.ofBijective f hf
   constructor
-  . intro hX
-    rw [has_card_iff] at hX
-    obtain ⟨g, hg⟩ := hX
-    let e' := Equiv.ofBijective g hg
-    rw [has_card_iff]
-    let ec := e.symm.trans e'
-    use ec
-    exact ec.bijective
-  . intro hY
-    rw [has_card_iff] at hY
-    obtain ⟨g, hg⟩ := hY
-    let e' := Equiv.ofBijective g hg
-    rw [has_card_iff]
-    let ec := e.trans e'
-    use ec
-    exact ec.bijective
+  . intro hX; rw [has_card_iff] at hX ⊢; obtain ⟨g, hg⟩ := hX
+    use e.symm.trans (Equiv.ofBijective _ hg); apply Equiv.bijective
+  . intro hY; rw [has_card_iff] at hY ⊢; obtain ⟨g, hg⟩ := hY
+    use e.trans (Equiv.ofBijective _ hg); apply Equiv.bijective
 
 theorem SetTheory.Set.EquivCard_to_card_eq {X Y:Set} (h: X ≈ Y): X.card = Y.card := by
-  by_cases hX: X.finite
-  . by_cases hY: Y.finite
-    . rw [finite] at hX hY
-      obtain ⟨nX, hXn⟩ := hX
-      obtain ⟨nY, hYn⟩ := hY
-      have hcX := has_card_to_card _ _ hXn
-      have hcY := has_card_to_card _ _ hYn
-      rw [hcX, hcY]
-      rw [EquivCard_to_has_card_eq nX h] at hXn
-      exact card_uniq hXn hYn
-    . rw [finite] at hX hY
-      obtain ⟨nX, hXn⟩ := hX
-      push_neg at hY
-      have := EquivCard_to_has_card_eq nX h
-      rw [this] at hXn
-      specialize hY nX
-      contradiction
-  . by_cases hY: Y.finite
-    . rw [finite] at hX hY
-      obtain ⟨nY, hYn⟩ := hY
-      push_neg at hX
-      have := EquivCard_to_has_card_eq nY h
-      rw [← this] at hYn
-      specialize hX nY
-      contradiction
-    . simp [card, hX, hY]
+  by_cases hX: X.finite <;> by_cases hY: Y.finite <;> try rw [finite] at hX hY
+  . obtain ⟨nX, hXn⟩ := hX
+    obtain ⟨nY, hYn⟩ := hY
+    rw [has_card_to_card _ _ hXn, has_card_to_card _ _ hYn]
+    rw [EquivCard_to_has_card_eq nX h] at hXn
+    exact card_uniq hXn hYn
+  . obtain ⟨nX, hXn⟩ := hX; push_neg at hY
+    rw [EquivCard_to_has_card_eq nX h] at hXn
+    specialize hY nX
+    contradiction
+  . obtain ⟨nY, hYn⟩ := hY; push_neg at hX
+    rw [←EquivCard_to_has_card_eq nY h] at hYn
+    specialize hX nY
+    contradiction
+  simp [card, hX, hY]
 
 /-- Proposition 3.6.14 (a) / Exercise 3.6.4 -/
 theorem SetTheory.Set.card_insert {X:Set} (hX: X.finite) {x:Object} (hx: x ∉ X) :
diff --git a/analysis/Analysis/Section_8_5.lean b/analysis/Analysis/Section_8_5.lean
index 8bd1a09..b274ca4 100644
--- a/analysis/Analysis/Section_8_5.lean
+++ b/analysis/Analysis/Section_8_5.lean
@@ -172,8 +172,7 @@ example : IsStrictUpperBound (.Icc 1 2: Set ℝ) 3 := by sorry
 /-- A convenient way to simplify the notion of having `x₀` as a minimal element.-/
 theorem IsMin.iff_lowerbound {X:Type} [PartialOrder X] {Y: Set X} (hY: IsTotal Y) (x₀ : X) : (∃ hx₀ : x₀ ∈ Y, IsMin (⟨ x₀, hx₀ ⟩:Y)) ↔ x₀ ∈ Y ∧ ∀ x ∈ Y, x₀ ≤ x := by
   constructor
-  . rintro ⟨ hx₀, hmin ⟩
-    simp [IsMin, hx₀] at hmin ⊢
+  . rintro ⟨ hx₀, hmin ⟩; simp [IsMin, hx₀] at hmin ⊢
     peel hmin with x hx hmin; specialize hY ⟨ _, hx ⟩ ⟨ _, hx₀ ⟩; aesop
   intro h; use h.1; simp [IsMin]; aesop
 
@@ -182,8 +181,7 @@ theorem IsMin.iff_lowerbound' {X:Type} [PartialOrder X] {Y: Set X} (hY: IsTotal
   . intro ⟨ ⟨ x₀, hx₀ ⟩, hmin ⟩
     have : ∃ (hx₀ : x₀ ∈ Y), IsMin (⟨ _, hx₀ ⟩:Y) := by use hx₀
     rw [iff_lowerbound hY x₀] at this; use x₀
-  intro ⟨ x₀, hx₀, hmin ⟩
-  obtain ⟨ hx₀, hmin' ⟩ := (iff_lowerbound hY x₀).mpr ⟨ hx₀, hmin ⟩; use ⟨ _, hx₀ ⟩
+  intro ⟨ x₀, hx₀, hmin ⟩;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
@@ -197,10 +195,8 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
   -- simplify the notion of minimality.
   let Ω₀ := { Y : Set X | IsTotal Y ∧ WellFoundedLT Y ∧ x₀ ∈ Y ∧ ∀ x ∈ Y, x₀ ≤ x}
   suffices : ∃ Y ∈ Ω₀, ¬ ∃ x, IsStrictUpperBound Y x
-  . obtain ⟨ Y, hY, hstrict ⟩ := this
-    use Y, hY.1; simp [Ω₀, IsStrictUpperBound] at hY ⊢ hstrict
-    obtain ⟨ hx₀, hmin ⟩ := hY.2.2; refine ⟨ hY.2.1, ⟨ ?_, hstrict ⟩ ⟩
-    rw [IsMin.iff_lowerbound hY.1 x₀]; tauto
+  . obtain ⟨ Y, ⟨ hY, hY'⟩, hstrict ⟩ := this; use Y, hY
+    rw [IsMin.iff_lowerbound hY 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
@@ -208,27 +204,23 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
   have hpt: {x₀} ∈ Ω₀ := by
     have htotal : IsTotal ({x₀}: Set X) := by simp [IsTotal]
     let _lin : LinearOrder ({x₀}: Set X) := LinearOrder.mk htotal
-    simp [Ω₀, htotal]
-    convert WellFoundedLT.ofFinite; infer_instance
+    simp [Ω₀, htotal]; apply WellFoundedLT.ofFinite
   let pt : Ω₀ := ⟨ _, hpt ⟩
 
   -- The operation of sending a set `Y` in `Ω₀` to the smaller set `{y ∈ Y.val | y < x}`, which is also
   -- in `Ω₀` if `x ∈ Y.val \ {x₀}`, is not named explicitly in the text, but we give it a name `F` for
   -- the formalization.
   have hF {Y:Set X} (hY: Y ∈ Ω₀) {x:X} (hxy : x ∈ Y \ {x₀}) : {y ∈ Y | y < x} ∈ Ω₀ := by
-    simp [Ω₀, IsTotal] at hY ⊢
-    refine ⟨ ?_, ?_, ?_ ⟩
-    . intros; solve_by_elim [hY.1]
-    . convert WellFoundedLT.subset (hwell := hY.2.1) (B := {y ∈ Y | y < x}) _ _
-      . 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
-    exact ⟨ ⟨ hx₀, by contrapose! hxy; order ⟩, by intros; solve_by_elim ⟩
+    simp [Ω₀, IsTotal] at hY ⊢; obtain ⟨ _, hmin ⟩ := hY.2.2; simp_all [IsMin]
+    and_intros
+    . convert WellFoundedLT.subset (hwell := hY.2) (B := {y ∈ Y | y < x}) _ _
+      . intro ⟨ _, _ ⟩ ⟨ _, _ ⟩; simp; solve_by_elim [hY.1]
+      intro _; simp; tauto
+    have := hmin _ hxy.1; contrapose! hxy; order
   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
   replace hF {Y : Ω₀} {x : X} (hxy : x ∈ (Y:Set X) \ {x₀}) : F Y x = { y ∈ (Y:Set X) | y < x } := by
-    simp only [F, dif_pos hxy]
+    simp_all [F, dif_pos hxy]
 
   -- The set `Ω` captures the notion of a `good set`.
   set Ω := { Y : Ω₀ | ∀ x ∈ (Y:Set X) \ {x₀}, x = s (F Y x) }
@@ -240,11 +232,9 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
     sorry
 
   have : IsTotal Ω := by
-    unfold IsTotal; by_contra!
-    obtain ⟨ ⟨ ⟨ Y, hY1 ⟩, hY2 ⟩, ⟨ ⟨ Y', hY'1⟩, hY'2 ⟩, h1, h2 ⟩ := this
+    unfold IsTotal; by_contra!; obtain ⟨ ⟨ ⟨ Y, hY1 ⟩, hY2 ⟩, ⟨ ⟨ Y', hY'1⟩, hY'2 ⟩, h1, h2 ⟩ := this
     simp_all [Set.not_subset]
-    obtain ⟨ x₁, hx₁, hx₁' ⟩ := h1
-    obtain ⟨ x₂, hx₂, hx₂' ⟩ := h2
+    obtain ⟨ x₁, hx₁, hx₁' ⟩ := h1; obtain ⟨ x₂, hx₂, hx₂' ⟩ := h2
     have h1 : IsStrictUpperBound Y x₂ := by solve_by_elim
     have h2 : IsStrictUpperBound Y' x₁ := by solve_by_elim
     simp [IsStrictUpperBound.iff] at h1 h2
@@ -255,13 +245,11 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
     sorry
   have htotal : IsTotal Y_infty := by
     intro ⟨ x, hx ⟩ ⟨ x', hx'⟩; simp [Y_infty] at hx hx'
-    obtain ⟨ Y, ⟨ hYΩ₀, hYΩ ⟩, hxY ⟩ := hx
-    obtain ⟨ Y', ⟨ hY'Ω₀, hY'Ω ⟩, hxY' ⟩ := hx'
-    specialize this ⟨ _, hYΩ ⟩ ⟨ _, hY'Ω ⟩
-    simp at this ⊢
+    obtain ⟨ Y, ⟨ hYΩ₀, hYΩ ⟩, hxY ⟩ := hx; obtain ⟨ Y', ⟨ hY'Ω₀, hY'Ω ⟩, hxY' ⟩ := hx'
+    specialize this ⟨ _, hYΩ ⟩ ⟨ _, hY'Ω ⟩; simp [Ω₀] at this ⊢ hYΩ₀ hY'Ω₀
     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Ω₀
+    . replace hY'Ω₀ := hY'Ω₀.1 ⟨ _, this hxY ⟩ ⟨ _, hxY' ⟩; simpa using 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
@@ -286,31 +274,30 @@ theorem WellFoundedLT.partialOrder {X:Type} [PartialOrder X] (x₀ : X) : ∃ Y
   specialize hs ⟨ _, hY_inftyΩ₀ ⟩
   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]
+    simp [Ω, -Set.mem_insert_iff, -and_imp]
     rintro x ⟨ (rfl | hx), hxx₀ ⟩
     . unfold sY_infty; congr 1
-      apply (Subtype.val_injective _).symm; convert hF _
-      . ext y; simp; constructor
+      symm; apply Subtype.val_injective; convert hF _
+      . ext; simp; constructor
         . intro h; simp [h]; solve_by_elim
-        rintro ⟨ h1 | h1, h2 ⟩
+        rintro ⟨ _ | _, _ ⟩
         . order
         assumption
-      simp; replace hs := hs (y := x₀) (by simp [hmem]); order
-    have hx' := hx; simp [Y_infty] at hx
-    obtain ⟨ Y, ⟨hYΩ₀, hYΩ⟩, hxY ⟩ := hx
+      simp; specialize hs (y := x₀) (by simp [hmem]); order
+    have hx' := hx; simp [Y_infty] at hx'; obtain ⟨ Y, ⟨hYΩ₀, hYΩ⟩, hxY ⟩ := hx'
     have hYΩ' := hYΩ; simp [Ω] at hYΩ
     convert hYΩ _ hxY hxx₀ using 2
     apply Subtype.val_injective
     rw [hF, hF]
     . ext y; simp [Y_infty]; intro hyx; constructor
       . rintro (rfl | ⟨ Y', ⟨hY'Ω₀, hY'Ω⟩, hyY' ⟩)
-        . specialize hs _ hx'; order
+        . 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; exact ⟨ _, ⟨hYΩ₀, hYΩ'⟩, hyY ⟩
-    all_goals simp [hxY, hx', hxx₀]
+    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 70c62c3..f5689f8 100644
--- a/analysis/Analysis/Section_9_1.lean
+++ b/analysis/Analysis/Section_9_1.lean
@@ -79,15 +79,9 @@ example : ¬ AdherentPt 2 (.Ioo 0 1) := by sorry
 
 /-- Definition 9.1.10 (Closure).  Here we identify this definition with the Mathilb version. -/
 theorem closure_def (X:Set ℝ) : closure X = { x | AdherentPt x X } := by
-  ext x
-  simp [Real.mem_closure_iff, AdherentPt, Real.adherent']
+  ext; simp [Real.mem_closure_iff, AdherentPt, Real.adherent']
   constructor <;> intro h ε hε
-  . obtain ⟨ y, hy, hxy ⟩ := h ε hε
-    refine ⟨ y, hy, ?_ ⟩
-    rw [abs_sub_comm]; linarith
-  obtain ⟨ y, hy, hxy ⟩ := h (ε/2) (half_pos hε)
-  refine ⟨ y, hy, ?_ ⟩
-  rw [abs_sub_comm]; linarith
+  all_goals obtain ⟨ y, hy, hxy ⟩ := h (ε/2) (half_pos hε); exact ⟨ y, hy, by rw [abs_sub_comm]; linarith ⟩
 
 theorem closure_def' (X:Set ℝ) (x :ℝ) : x ∈ closure X ↔ AdherentPt x X := by
   simp [closure_def]
@@ -254,7 +248,7 @@ theorem LimitPt.iff_limit (x:ℝ) (X: Set ℝ) :
 open Filter in
 /-- This lemma is in more recent versions of Mathlib and can be deleted once Mathlib is updated. -/
 theorem tendsto_mul_add_inv_atTop_nhds_zero (a c : ℝ) (ha : a ≠ 0) :
-    Tendsto (fun x => (a * x + c)⁻¹) atTop (nhds 0) := by
+    atTop.Tendsto (fun x => (a * x + c)⁻¹) (nhds 0) := by
   obtain ha' | ha' := lt_or_gt_of_ne ha
   · exact tendsto_inv_atBot_zero.comp
       (tendsto_atBot_add_const_right _ c (tendsto_id.const_mul_atTop_of_neg ha'))
@@ -317,8 +311,7 @@ theorem isBounded_def (X: Set ℝ) : Bornology.IsBounded X ↔ ∃ M > 0, X ⊆
   . 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]
+  intro ⟨ M, hM, hXM ⟩; use M; intro x hx; specialize hXM hx; simp_all [abs_le']; linarith [hXM.1]
 
 /-- Example 9.1.23 -/
 theorem Icc_bounded (a b:ℝ) : Bornology.IsBounded (.Icc a b) := by sorry