remove a simp lemma and swap an equality

analysis/Analysis/Section_11_2.lean

···
   sorry
 
 /-- Example 11.2.6 -/
-theorem PiecewiseConstantOn.of_const {f:ℝ → ℝ} {I: BoundedInterval} (h: ConstantOn f (I:Set ℝ)) :
+theorem ConstantOn.piecewiseConstantOn {f:ℝ → ℝ} {I: BoundedInterval} (h: ConstantOn f (I:Set ℝ)) :
   PiecewiseConstantOn f I := by sorry
 
 /-- Lemma 11.2.7 / Exercise 11.2.1 -/
···
   ℝ := ∑ J ∈ P.intervals, constant_value_on f (J:Set ℝ) * |J|ₗ
 
 theorem PiecewiseConstantWith.integ_congr {f g:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
-  (h: ∀ x ∈ (I:Set ℝ), f x = g x) : PiecewiseConstantWith.integ f P = PiecewiseConstantWith.integ g P := by
+  (h: ∀ x ∈ (I:Set ℝ), f x = g x) : integ f P = integ g P := by
   simp only [integ, Subtype.forall]
   apply Finset.sum_congr rfl; intro J hJ; congr 1; apply constant_value_on_congr; intros
   have := P.contains _ hJ; rw [subset_iff] at this
···
   simp [integ, h']; exact PiecewiseConstantWith.integ_eq h'.choose_spec h
 
 theorem PiecewiseConstantOn.integ_congr {f g:ℝ → ℝ} {I: BoundedInterval}
-  (h: ∀ x ∈ (I:Set ℝ), f x = g x) : PiecewiseConstantOn.integ f I = PiecewiseConstantOn.integ g I := by
+  (h: ∀ x ∈ (I:Set ℝ), f x = g x) : integ f I = integ g I := by
   by_cases hf : PiecewiseConstantOn f I
   <;> have hg := hf <;> rw [congr h] at hg <;> simp [integ, hf, hg]
   rw [PiecewiseConstantWith.integ_congr h, ←integ_def hg.choose_spec, ←integ_def ?_]

analysis/Analysis/Section_11_3.lean

···
   simp
   refine ⟨ fun _ ↦ M , ⟨ ⟨ ?_, ?_, ⟩, PiecewiseConstantOn.integ_const M I ⟩ ⟩
   . peel h with _ _ h'; simp [abs_le'] at h'; simp [h'.1]
-  exact PiecewiseConstantOn.of_const (ConstantOn.of_const (c := M) (by simp))
+  exact (ConstantOn.of_const (c := M) (by simp)).piecewiseConstantOn
 
 lemma integral_bound_lower_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) : -M * |I|ₗ ∈ (fun g ↦ PiecewiseConstantOn.integ g I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} := by
   simp
   refine ⟨ fun _ ↦ -M , ⟨ ⟨ ?_, ?_, ⟩, by convert PiecewiseConstantOn.integ_const (-M) I using 1; simp ⟩ ⟩
   . peel h with _ _ h'; simp [abs_le'] at h'; simp; linarith
-  exact PiecewiseConstantOn.of_const (ConstantOn.of_const (c := -M) (by simp))
+  exact (ConstantOn.of_const (c := -M) (by simp)).piecewiseConstantOn
 
 lemma integral_bound_upper_nonempty {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) : ((fun g ↦ PiecewiseConstantOn.integ g I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty := by
   obtain ⟨ _, h ⟩ := h; exact Set.nonempty_of_mem (integral_bound_upper_of_bounded h)
···
   IntegrableOn f I ∧ integ f I = 0 := by
   have _ := length_of_subsingleton.mpr hI
   have hconst : ConstantOn f I := ConstantOn.of_subsingleton
-  convert integ_of_piecewise_const (PiecewiseConstantOn.of_const hconst)
+  convert integ_of_piecewise_const hconst.piecewiseConstantOn
   simp [PiecewiseConstantOn.integ_const' hconst, hI]
 
 /-- Definition 11.3.9 (Riemann sums).  The restriction to positive length J is not needed thanks to various junk value conventions. -/

analysis/Analysis/Section_11_4.lean

···
     have : ∃ f', MinorizesOn f' f I ∧ PiecewiseConstantOn f' I ∧ integ f I - ε < PiecewiseConstantOn.integ f' I ∧ MajorizesOn f' 0 I := by
       obtain ⟨ f', hf'min, hf'const, hf'int ⟩ := gt_of_lt_lower_integral hf.1 (show integ f I - ε < lower_integral f I by linarith)
       use max f' 0
-      have hzero := PiecewiseConstantOn.of_const (ConstantOn.of_const' 0 I)
+      have hzero := (ConstantOn.of_const' 0 I).piecewiseConstantOn
       and_intros
       . peel hf_nonneg with x hx _; specialize hf'min _ hx; aesop
       . exact hf'const.max hzero
···
     have : ∃ g', MinorizesOn g' g I ∧ PiecewiseConstantOn g' I ∧ integ g I - ε < PiecewiseConstantOn.integ g' I ∧ MajorizesOn g' 0 I := by
       obtain ⟨ g', hg'min, hg'const, hg'int ⟩ := gt_of_lt_lower_integral hg.1 (show integ g I - ε < lower_integral g I by linarith)
       use max g' 0
-      have hzero := PiecewiseConstantOn.of_const (ConstantOn.of_const' 0 I)
+      have hzero := (ConstantOn.of_const' 0 I).piecewiseConstantOn
       and_intros
       . peel hg_nonneg with x hx _; specialize hg'min _ hx; aesop
       . exact hg'const.max hzero
···
     have : ∃ f'', MajorizesOn f'' f I ∧ PiecewiseConstantOn f'' I ∧ PiecewiseConstantOn.integ f'' I < integ f I + ε ∧ MinorizesOn f'' (fun _ ↦ M₁) I := by
       obtain ⟨ f'', hf''maj, hf''const, hf''int ⟩ := lt_of_gt_upper_integral hf.1 (show upper_integral f I < integ f I + ε  by linarith)
       use min f'' (fun _ ↦ M₁)
-      have hM₁_piece := PiecewiseConstantOn.of_const (ConstantOn.of_const' M₁ I)
+      have hM₁_piece := (ConstantOn.of_const' M₁ I).piecewiseConstantOn
       and_intros
       . peel hM₁ with x hx hM₁; rw [abs_le'] at hM₁
         specialize hf''maj _ hx; simp [hf''maj, hM₁.1]
···
     have : ∃ g'', MajorizesOn g'' g I ∧ PiecewiseConstantOn g'' I ∧ PiecewiseConstantOn.integ g'' I < integ g I + ε ∧ MinorizesOn g'' (fun _ ↦ M₂) I := by
       obtain ⟨ g'', hg''maj, hg''const, hg''int ⟩ := lt_of_gt_upper_integral hg.1 (show upper_integral g I < integ g I + ε  by linarith)
       use min g'' (fun _ ↦ M₂)
-      have hM₂_piece := PiecewiseConstantOn.of_const (ConstantOn.of_const' M₂ I)
+      have hM₂_piece := (ConstantOn.of_const' M₂ I).piecewiseConstantOn
       and_intros
       . peel hM₂ with x hx hM₂; rw [abs_le'] at hM₂
         specialize hg''maj _ hx; simp [hg''maj, hM₂.1]

analysis/Analysis/Section_11_5.lean

···
     have h'const : PiecewiseConstantOn h' I := by
       rw [of_join hjoin2 _]; and_intros
       . rw [of_join hjoin1 _]; and_intros
-        . exact of_const (ConstantOn.of_const h'const_left)
+        . exact (ConstantOn.of_const h'const_left).piecewiseConstantOn
         apply hhconst.congr'
         intro x hx; simp [h', hx, mem_iff]
-      exact of_const (ConstantOn.of_const h'const_right)
+      exact (ConstantOn.of_const h'const_right).piecewiseConstantOn
     have h'maj : MajorizesOn h' f I := by
       intro x hx; by_cases hxI': x ∈ I' <;> simp [h', hxI']
       . solve_by_elim
···
       and_intros
       . rw [of_join hjoin1 _]
         and_intros
-        . exact of_const (ConstantOn.of_const g'const_left)
+        . exact (ConstantOn.of_const g'const_left).piecewiseConstantOn
         apply hgconst.congr'
         intro x hx; simp [g', hx, mem_iff]
-      exact of_const (ConstantOn.of_const g'const_right)
+      exact (ConstantOn.of_const g'const_right).piecewiseConstantOn
     have g'maj : MinorizesOn g' f I := by
       intro x hx; by_cases hxI': x ∈ I' <;> simp [g', hxI']
       . solve_by_elim

analysis/Analysis/Section_11_8.lean

···
   convert hf using 1
   have h1 : .Ioo (x₀-ε) x₀ ∈ nhdsWithin x₀ (.Iio x₀) := by
     convert inter_mem_nhdsWithin (t := .Ioo (x₀-ε) (x₀+ε)) _ _
-    . ext; simp; constructor
-      . intro ⟨ h1, h2 ⟩; simp [h1, h2]; linarith
-      aesop
+    . ext; simp; exact ⟨ by intro ⟨ h1, h2 ⟩; simp [h1, h2]; linarith, by aesop ⟩
     apply Ioo_mem_nhds <;> linarith
   rw [←nhdsWithin_inter_of_mem h1]
   congr 1; simp [Set.Ioo_subset_Iio_self]
···
   (h : X ∈ nhds x₀) (hf: ContinuousWithinAt f X x₀) :
   jump f x₀ = 0 := by
   rw [mem_nhds_iff_exists_Ioo_subset] at h
-  obtain ⟨ l, u, hx₀, hX ⟩ := h
-  simp at hx₀
-  have hl : ∃ ε>0, .Ioc (x₀-ε) x₀ ⊆ X := by
-    refine ⟨ x₀-l, by linarith, Set.Subset.trans ?_ hX ⟩
-    intro x hx; simp at hx ⊢; exact ⟨ hx.1, by linarith ⟩
-  have hu : ∃ ε>0, .Ico x₀ (x₀+ε) ⊆ X := by
-    refine ⟨ u-x₀, by linarith, Set.Subset.trans ?_ hX ⟩
-    intro x hx; simp at hx ⊢; exact ⟨ by linarith, hx.2 ⟩
+  obtain ⟨ l, u, hx₀, hX ⟩ := h; simp at hx₀
+  have hl : ∃ ε>0, .Ioc (x₀-ε) x₀ ⊆ X :=
+    ⟨ x₀-l, by linarith, Set.Subset.trans (by intro _ _; simp_all; linarith) hX ⟩
+  have hu : ∃ ε>0, .Ico x₀ (x₀+ε) ⊆ X :=
+    ⟨ u-x₀, by linarith, Set.Subset.trans (by intro _ _; simp_all; linarith) hX ⟩
   simp [jump, left_lim_of_continuous hl hf, right_lim_of_continuous hu hf]
 
 /-- Right limits exist for monotone functions -/
 theorem right_lim_of_monotone {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) :
   Convergesto (.Ioi x₀) f (sInf (f '' .Ioi x₀)) x₀ := by
   rw [Convergesto.iff, ←nhdsWithin.eq_1]
-  apply MonotoneOn.tendsto_nhdsGT
-  . apply hf.monotoneOn
-  rw [bddBelow_def]
-  use f x₀; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
+  apply (hf.monotoneOn _).tendsto_nhdsGT
+  rw [bddBelow_def]; use f x₀; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
 
 theorem right_lim_of_monotone' {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) :
   right_lim f x₀ = sInf (f '' .Ioi x₀) := right_lim_def (right_lim_of_monotone x₀ hf)
···
 theorem left_lim_of_monotone {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) :
   Convergesto (.Iio x₀) f (sSup (f '' .Iio x₀)) x₀ := by
   rw [Convergesto.iff, ←nhdsWithin.eq_1]
-  apply MonotoneOn.tendsto_nhdsLT
-  . apply hf.monotoneOn
-  rw [bddAbove_def]
-  use f x₀; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
+  apply (hf.monotoneOn _).tendsto_nhdsLT
+  rw [bddAbove_def]; use f x₀; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
 
 theorem left_lim_of_monotone' {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) :
   left_lim f x₀ = sSup (f '' .Iio x₀) := left_lim_def (left_lim_of_monotone x₀ hf)
···
 theorem jump_of_monotone {f: ℝ → ℝ} (x₀:ℝ) (hf: Monotone f) :
   0 ≤ jump f x₀  := by
   simp [jump, left_lim_of_monotone' x₀ hf, right_lim_of_monotone' x₀ hf]
-  apply csSup_le (by simp)
-  intro a ha
-  apply le_csInf (by simp)
-  intro b hb; simp at ha hb
-  obtain ⟨ x, hx, rfl ⟩ := ha
-  obtain ⟨ y, hy, rfl ⟩ := hb
+  apply csSup_le (by simp); intro a ha
+  apply le_csInf (by simp); intro b hb; simp at ha hb
+  obtain ⟨ x, hx, rfl ⟩ := ha; obtain ⟨ y, hy, rfl ⟩ := hb
   apply hf; linarith
 
 theorem right_lim_le_left_lim_of_monotone {f:ℝ → ℝ} {a b:ℝ} (hab: a < b)
···
   calc
     _ ≤ f ((a+b)/2) := by
       apply ConditionallyCompleteLattice.csInf_le
-      . rw [bddBelow_def]
-        use f a; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
+      . rw [bddBelow_def]; use f a; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
       simp; use (a+b)/2; simp; linarith
     _ ≤ _ := by
       apply ConditionallyCompleteLattice.le_csSup
-      . rw [bddAbove_def]
-        use f b; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
+      . rw [bddAbove_def]; use f b; intro y hy; simp at hy; obtain ⟨ x, hx, rfl ⟩ := hy; apply hf; linarith
       simp; use (a+b)/2; simp; linarith
 
 /-- Definition 11.8.1 -/
···
   (hI : I ⊆ Ioo a b) (hα: ContinuousOn α (Ioo a b)) :
   α[I]ₗ = α I.b - α I.a := by
   have ha_left : left_lim α I.a = α I.a := by
-    apply left_lim_of_continuous _ (hα.continuousWithinAt _)
-    . refine ⟨ I.a - a, by linarith, ?_ ⟩
-      intro _; simp; intro h1 _; exact ⟨ h1, by linarith ⟩
-    simp [haa]; linarith
+    apply left_lim_of_continuous _ (hα.continuousWithinAt (by simp [haa]; linarith))
+    exact ⟨ I.a - a, by linarith, by intro _; simp; intro _ _; and_intros <;> linarith ⟩
   have ha_right : right_lim α I.a = α I.a := by
-    apply right_lim_of_continuous _ (hα.continuousWithinAt _)
-    . refine ⟨ b - I.a, by linarith, ?_ ⟩
-      intro _; simp; intro _ h2; exact ⟨ by linarith, h2 ⟩
-    simp [haa]; linarith
+    apply right_lim_of_continuous _ (hα.continuousWithinAt (by simp [haa]; linarith))
+    exact ⟨ b - I.a, by linarith, by intro _; simp; intro _ _; and_intros <;> linarith ⟩
   have hb_left : left_lim α I.b = α I.b := by
-    apply left_lim_of_continuous _ (hα.continuousWithinAt _)
-    . refine ⟨ I.b - a, by linarith, ?_ ⟩
-      intro _; simp; intro h1 _; exact ⟨ h1, by linarith ⟩
-    simp [hbb]; linarith
+    apply left_lim_of_continuous _ (hα.continuousWithinAt (by simp [hbb]; linarith))
+    exact ⟨ I.b - a, by linarith, by intro _; simp; intro _ _; and_intros <;> linarith ⟩
   have hb_right : right_lim α I.b = α I.b := by
-    apply right_lim_of_continuous _ (hα.continuousWithinAt _)
-    . refine ⟨ b - I.b, by linarith, ?_ ⟩
-      intro _; simp; intro h1 h2; exact ⟨ by linarith, h2 ⟩
-    simp [hbb]; linarith
+    apply right_lim_of_continuous _ (hα.continuousWithinAt (by simp [hbb]; linarith))
+    exact ⟨ b - I.b, by linarith, by intro _; simp; intro _ _; and_intros <;> linarith ⟩
   cases I with
   | Icc _ _ => simp [α_length, hb_right, ha_left, hab]
   | Ico _ _ => simp [α_length, hb_left, ha_left, hab]
   | Ioc _ _ => simp [α_length, hb_right, ha_right, hab]
-  | Ioo a' b' => simp [α_length, hb_left, ha_right]; intro h; simp [show a' = b' by linarith]
+  | Ioo a' b' => simp [α_length, hb_left, ha_right]; intros; simp [show a' = b' by linarith]
 
 /-- Example 11.8.2-/
 example : (fun x ↦ x^2)[Icc 2 3]ₗ = 5 := by
···
   sorry
 
 /-- An improved version of BoundedInterval.joins that also controls α-length. -/
-abbrev BoundedInterval.joins' (K I J: BoundedInterval) : Prop :=
-  K.joins I J ∧ ∀ α:ℝ → ℝ, α[K]ₗ = α[I]ₗ + α[J]ₗ
+abbrev BoundedInterval.joins' (K I J: BoundedInterval) : Prop :=  K.joins I J ∧ ∀ α:ℝ → ℝ, α[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 ⟨ join_Icc_Ioc hab hbc, ?_ ⟩
···
   ℝ := if h: PiecewiseConstantOn f I then PiecewiseConstantWith.RS_integ f h.choose α else 0
 
 theorem PiecewiseConstantOn.RS_integ_def {f:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
-  (h: PiecewiseConstantWith f P) (α:ℝ → ℝ) : PiecewiseConstantOn.RS_integ f I α = PiecewiseConstantWith.RS_integ f P α := by
+  (h: PiecewiseConstantWith f P) (α:ℝ → ℝ) : RS_integ f I α = PiecewiseConstantWith.RS_integ f P α := by
   have h' : PiecewiseConstantOn f I := by use P
-  simp [PiecewiseConstantOn.RS_integ, h']
-  exact PiecewiseConstantWith.RS_integ_eq h'.choose_spec h α
+  simp [RS_integ, h']; exact PiecewiseConstantWith.RS_integ_eq h'.choose_spec h α
 
 /-- α-length non-negative when α monotone -/
 theorem α_length_nonneg_of_monotone {α:ℝ → ℝ}  (hα: Monotone α) (I: BoundedInterval):
···
 /-- Analogue of Theorem 11.2.16 (a) (Laws of integration) / Exercise 11.8.3 -/
 theorem PiecewiseConstantOn.RS_integ_add {f g: ℝ → ℝ} {I: BoundedInterval}
   (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) {α:ℝ → ℝ} (hα: Monotone α):
-  PiecewiseConstantOn.RS_integ (f + g) I α = PiecewiseConstantOn.RS_integ f I α + PiecewiseConstantOn.RS_integ g I α := by
+  RS_integ (f + g) I α = RS_integ f I α + RS_integ g I α := by
   sorry
 
 /-- Analogue of Theorem 11.2.16 (b) (Laws of integration) / Exercise 11.8.3 -/
 theorem PiecewiseConstantOn.RS_integ_smul {f: ℝ → ℝ} {I: BoundedInterval} (c:ℝ)
   (hf: PiecewiseConstantOn f I) {α:ℝ → ℝ} (hα: Monotone α) :
-  PiecewiseConstantOn.RS_integ (c • f) I α = c * PiecewiseConstantOn.RS_integ f I α
+  RS_integ (c • f) I α = c * RS_integ f I α
    := by
   sorry
 
···
 theorem PiecewiseConstantOn.RS_integ_sub {f g: ℝ → ℝ} {I: BoundedInterval}
   {α:ℝ → ℝ} (hα: Monotone α)
   (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) :
-  PiecewiseConstantOn.RS_integ (f - g) I α = PiecewiseConstantOn.RS_integ f I α - PiecewiseConstantOn.RS_integ g I α := by
+  RS_integ (f - g) I α = RS_integ f I α - RS_integ g I α := by
   sorry
 
 /-- Theorem 11.8.8 (d) (Laws of RS integration) / Exercise 11.8.8 -/
 theorem PiecewiseConstantOn.RS_integ_of_nonneg {f: ℝ → ℝ} {I: BoundedInterval}
   {α:ℝ → ℝ} (hα: Monotone α)
   (h: ∀ x ∈ I, 0 ≤ f x) (hf: PiecewiseConstantOn f I) :
-  0 ≤ PiecewiseConstantOn.RS_integ f I α := by
+  0 ≤ RS_integ f I α := by
   sorry
 
 /-- Theorem 11.8.8 (e) (Laws of RS integration) / Exercise 11.8.8 -/
 theorem PiecewiseConstantOn.RS_integ_mono {f g: ℝ → ℝ} {I: BoundedInterval}
   {α:ℝ → ℝ} (hα: Monotone α)
   (h: ∀ x ∈ I, f x ≤ g x) (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) :
-  PiecewiseConstantOn.RS_integ f I α ≤ PiecewiseConstantOn.RS_integ g I α := by
+  RS_integ f I α ≤ RS_integ g I α := by
   sorry
 
 /-- Theorem 11.8.8 (f) (Laws of RS integration) / Exercise 11.8.8 -/
 theorem PiecewiseConstantOn.RS_integ_const (c: ℝ) (I: BoundedInterval) {α:ℝ → ℝ} (hα: Monotone α) :
-  PiecewiseConstantOn.RS_integ (fun _ ↦ c) I α = c * α[I]ₗ := by
+  RS_integ (fun _ ↦ c) I α = c * α[I]ₗ := by
   sorry
 
 /-- Theorem 11.8.8 (f) (Laws of RS integration) / Exercise 11.8.8 -/
 theorem PiecewiseConstantOn.RS_integ_const' {f:ℝ → ℝ} {I: BoundedInterval}
   {α:ℝ → ℝ} (hα: Monotone α) (h: ConstantOn f I) :
-  PiecewiseConstantOn.RS_integ f I α = (constant_value_on f I) * α[I]ₗ := by
+  RS_integ f I α = (constant_value_on f I) * α[I]ₗ := by
   sorry
 
 open Classical in
···
 /-- Theorem 11.8.8 (g) (Laws of RS integration) / Exercise 11.8.8 -/
 theorem PiecewiseConstantOn.RS_integ_of_extend {I J: BoundedInterval} (hIJ: I ⊆ J)
   {f: ℝ → ℝ} (h: PiecewiseConstantOn f I) {α:ℝ → ℝ} (hα: Monotone α):
-  PiecewiseConstantOn.RS_integ (fun x ↦ if x ∈ I then f x else 0) J α = PiecewiseConstantOn.RS_integ f I α := by
+  RS_integ (fun x ↦ if x ∈ I then f x else 0) J α = RS_integ f I α := by
   sorry
 
 /-- Theorem 11.8.8 (h) (Laws of RS integration) / Exercise 11.8.8 -/
 theorem PiecewiseConstantOn.RS_integ_of_join {I J K: BoundedInterval} (hIJK: K.joins' I J)
   {f: ℝ → ℝ} (h: PiecewiseConstantOn f K) {α:ℝ → ℝ} (hα: Monotone α):
-  PiecewiseConstantOn.RS_integ f K α = PiecewiseConstantOn.RS_integ f I α + PiecewiseConstantOn.RS_integ f J α := by
+  RS_integ f K α = RS_integ f I α + RS_integ f J α := by
   sorry
 
 /-- Analogue of Definition 11.3.2 (Uppper and lower Riemann integrals )-/
 noncomputable abbrev upper_RS_integral (f:ℝ → ℝ) (I: BoundedInterval) (α: ℝ → ℝ): ℝ :=
-  sInf ((fun g ↦ PiecewiseConstantOn.RS_integ g I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I})
+  sInf ((PiecewiseConstantOn.RS_integ · I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I})
 
 noncomputable abbrev lower_RS_integral (f:ℝ → ℝ) (I: BoundedInterval) (α: ℝ → ℝ): ℝ :=
-  sSup ((fun g ↦ PiecewiseConstantOn.RS_integ g I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I})
+  sSup ((PiecewiseConstantOn.RS_integ · I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I})
 
 lemma RS_integral_bound_upper_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval}
   (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) {α:ℝ → ℝ} (hα:Monotone α)
-  : M * α[I]ₗ ∈ (fun g ↦ PiecewiseConstantOn.RS_integ g I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} := by
-  simp
-  refine ⟨ fun _ ↦ M, ⟨ ⟨ ?_, ?_, ⟩, PiecewiseConstantOn.RS_integ_const M I hα ⟩ ⟩
-  . peel h with x hx h; simp_all [abs_le']
-  apply PiecewiseConstantOn.of_const (ConstantOn.of_const (c := M) (by simp))
+  : M * α[I]ₗ ∈ (PiecewiseConstantOn.RS_integ · I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} := by
+  simp; refine ⟨ fun _ ↦ M, ⟨ ⟨ ?_, ?_ ⟩, PiecewiseConstantOn.RS_integ_const M I hα ⟩ ⟩
+  . peel h with _ _ _; simp_all [abs_le']
+  exact (ConstantOn.of_const (c := M) (by simp)).piecewiseConstantOn
 
 
 lemma RS_integral_bound_lower_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) {α:ℝ → ℝ} (hα:Monotone α)
-  : -M * α[I]ₗ ∈ (fun g ↦ PiecewiseConstantOn.RS_integ g I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} := by
-  simp
-  refine ⟨ fun _ ↦ -M, ⟨ ⟨ ?_, ?_, ⟩, ?_ ⟩ ⟩
-  . peel h with x hx h'; simp [abs_le'] at *; linarith
-  . apply PiecewiseConstantOn.of_const (ConstantOn.of_const (c := -M) (by simp))
-  convert PiecewiseConstantOn.RS_integ_const _ _ hα using 1
-  simp
+  : -M * α[I]ₗ ∈ (PiecewiseConstantOn.RS_integ · I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I} := by
+  simp; refine ⟨ fun _ ↦ -M, ⟨ ⟨ ?_, ?_ ⟩, by convert PiecewiseConstantOn.RS_integ_const _ _ hα using 1; simp ⟩ ⟩
+  . peel h with _ _ _; simp [abs_le'] at *; linarith
+  exact (ConstantOn.of_const (c := -M) (by simp)).piecewiseConstantOn
+
 
 lemma RS_integral_bound_upper_nonempty {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I)
   {α:ℝ → ℝ} (hα: Monotone α) :
-  ((fun g ↦ PiecewiseConstantOn.RS_integ g I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty := by
-  obtain ⟨ M, h ⟩ := h
-  exact Set.nonempty_of_mem (RS_integral_bound_upper_of_bounded h hα)
+  ((PiecewiseConstantOn.RS_integ · I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty := by
+  obtain ⟨ M, h ⟩ := h; exact Set.nonempty_of_mem (RS_integral_bound_upper_of_bounded h hα)
 
 lemma RS_integral_bound_lower_nonempty {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I)
   {α:ℝ → ℝ} (hα: Monotone α) :
-  ((fun g ↦ PiecewiseConstantOn.RS_integ g I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty := by
-  obtain ⟨ M, h ⟩ := h
-  exact Set.nonempty_of_mem (RS_integral_bound_lower_of_bounded h hα)
+  ((PiecewiseConstantOn.RS_integ · I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty := by
+  obtain ⟨ M, h ⟩ := h; exact Set.nonempty_of_mem (RS_integral_bound_lower_of_bounded h hα)
 
 lemma RS_integral_bound_lower_le_upper {f:ℝ → ℝ} {I: BoundedInterval} {a b:ℝ}
   {α:ℝ → ℝ} (hα: Monotone α)
-  (ha: a ∈ (fun g ↦ PiecewiseConstantOn.RS_integ g I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I})
-  (hb: b ∈ (fun g ↦ PiecewiseConstantOn.RS_integ g I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I})
+  (ha: a ∈ (PiecewiseConstantOn.RS_integ · I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I})
+  (hb: b ∈ (PiecewiseConstantOn.RS_integ · I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I})
   : b ≤ a:= by
     obtain ⟨ g, ⟨ ⟨ hmaj, hgp⟩, hgi ⟩ ⟩ := ha
     obtain ⟨ h, ⟨ ⟨ hmin, hhp⟩, hhi ⟩ ⟩ := hb
-    rw [←hgi, ←hhi]
-    apply hhp.RS_integ_mono hα _ hgp
-    intro x hx; exact (ge_iff_le.mp (hmin _ hx)).trans (hmaj _ hx)
+    rw [←hgi, ←hhi]; apply hhp.RS_integ_mono hα _ hgp; intro _ hx; linarith [hmin _ hx, hmaj _ hx]
 
 lemma RS_integral_bound_below {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I)
   {α:ℝ → ℝ} (hα: Monotone α) :
-  BddBelow ((fun g ↦ PiecewiseConstantOn.RS_integ g I α) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) := by
-    rw [bddBelow_def]
-    use (RS_integral_bound_lower_nonempty h hα).some
+  BddBelow ((PiecewiseConstantOn.RS_integ · I α) ''
+    {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) := by
+    rw [bddBelow_def]; use (RS_integral_bound_lower_nonempty h hα).some
     intro a ha; exact RS_integral_bound_lower_le_upper hα ha (RS_integral_bound_lower_nonempty h hα).some_mem
 
 lemma RS_integral_bound_above {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I)
   {α:ℝ → ℝ} (hα: Monotone α):
-  BddAbove ((fun g ↦ PiecewiseConstantOn.RS_integ g I α) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) := by
-    rw [bddAbove_def]
-    use (RS_integral_bound_upper_nonempty h hα).some
+  BddAbove ((PiecewiseConstantOn.RS_integ · I α) ''
+    {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) := by
+    rw [bddAbove_def]; use (RS_integral_bound_upper_nonempty h hα).some
     intro b hb; exact RS_integral_bound_lower_le_upper hα (RS_integral_bound_upper_nonempty h hα).some_mem hb
 
 lemma le_lower_RS_integral {f:ℝ → ℝ} {I: BoundedInterval} {M:ℝ} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M)
   {α:ℝ → ℝ} (hα: Monotone α) :
-  -M * α[I]ₗ ≤ lower_RS_integral f I α := by
-  exact ConditionallyCompleteLattice.le_csSup _ _
+  -M * α[I]ₗ ≤ lower_RS_integral f I α :=
+  ConditionallyCompleteLattice.le_csSup _ _
     (RS_integral_bound_above (BddOn.of_bounded h) hα) (RS_integral_bound_lower_of_bounded h hα)
 
 lemma lower_RS_integral_le_upper {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I)
   {α:ℝ → ℝ} (hα: Monotone α) :
   lower_RS_integral f I α ≤ upper_RS_integral f I α := by
   apply ConditionallyCompleteLattice.csSup_le _ _ (RS_integral_bound_lower_nonempty h hα) _
-  rw [mem_upperBounds]
-  intros
+  rw [mem_upperBounds]; intros
   apply ConditionallyCompleteLattice.le_csInf _ _ (RS_integral_bound_upper_nonempty h hα) _
-  rw [mem_lowerBounds]
-  intros; solve_by_elim [RS_integral_bound_lower_le_upper]
+  rw [mem_lowerBounds]; intros; solve_by_elim [RS_integral_bound_lower_le_upper]
 
 lemma RS_upper_integral_le {f:ℝ → ℝ} {I: BoundedInterval} {M:ℝ} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M)
   {α:ℝ → ℝ} (hα: Monotone α) :
-  upper_RS_integral f I α ≤ M * α[I]ₗ := by
-  exact ConditionallyCompleteLattice.csInf_le _ _
+  upper_RS_integral f I α ≤ M * α[I]ₗ :=
+  ConditionallyCompleteLattice.csInf_le _ _
     (RS_integral_bound_below (.of_bounded h) hα) (RS_integral_bound_upper_of_bounded h hα)
 
 lemma upper_RS_integral_le_integ {f g:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
   (hfg: MajorizesOn g f I) (hg: PiecewiseConstantOn g I)
   {α:ℝ → ℝ} (hα: Monotone α) :
-  upper_RS_integral f I α ≤ PiecewiseConstantOn.RS_integ g I α := by
-  apply ConditionallyCompleteLattice.csInf_le _ _ (RS_integral_bound_below hf hα) _
-  use g; simpa [hg]
+  upper_RS_integral f I α ≤ PiecewiseConstantOn.RS_integ g I α :=
+  ConditionallyCompleteLattice.csInf_le _ _ (RS_integral_bound_below hf hα) ⟨ g, by simpa [hg] ⟩
 
 lemma integ_le_lower_RS_integral {f h:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
   (hfh: MinorizesOn h f I) (hg: PiecewiseConstantOn h I)
   {α:ℝ → ℝ} (hα: Monotone α) :
-  PiecewiseConstantOn.RS_integ h I α ≤ lower_RS_integral f I α := by
-  apply ConditionallyCompleteLattice.le_csSup _ _ (RS_integral_bound_above hf hα) _
-  use h; simpa [hg]
+  PiecewiseConstantOn.RS_integ h I α ≤ lower_RS_integral f I α :=
+  ConditionallyCompleteLattice.le_csSup _ _ (RS_integral_bound_above hf hα) ⟨ h, by simpa [hg] ⟩
 
 lemma lt_of_gt_upper_RS_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
   {α: ℝ → ℝ} (hα: Monotone α) {X:ℝ} (hX: upper_RS_integral f I α < X ) :
   ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.RS_integ g I α < X := by
-  obtain ⟨ Y, hY, hYX ⟩ := exists_lt_of_csInf_lt (RS_integral_bound_upper_nonempty hf hα) hX
+  have ⟨ Y, hY, hYX ⟩ := exists_lt_of_csInf_lt (RS_integral_bound_upper_nonempty hf hα) hX
   simp at hY; obtain ⟨ g, ⟨ hmaj, hgp ⟩, hgi ⟩ := hY; exact ⟨ g, hmaj, hgp, by rwa [hgi] ⟩
 
 lemma gt_of_lt_lower_RS_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
   {α:ℝ → ℝ} (hα: Monotone α) {X:ℝ} (hX: X < lower_RS_integral f I α) :
   ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.RS_integ h I α := by
-  obtain ⟨ Y, hY, hYX ⟩ := exists_lt_of_lt_csSup (RS_integral_bound_lower_nonempty hf hα) hX
+  have ⟨ Y, hY, hYX ⟩ := exists_lt_of_lt_csSup (RS_integral_bound_lower_nonempty hf hα) hX
   simp at hY; obtain ⟨ h, ⟨ hmin, hhp ⟩, hhi ⟩ := hY; exact ⟨ h, hmin, hhp, by rwa [hhi] ⟩
 
 /-- Analogue of Definition 11.3.4 -/
-noncomputable abbrev RS_integ (f:ℝ → ℝ) (I: BoundedInterval) (α:ℝ → ℝ) : ℝ :=
-upper_RS_integral f I α
+noncomputable abbrev RS_integ (f:ℝ → ℝ) (I: BoundedInterval) (α:ℝ → ℝ) : ℝ := upper_RS_integral f I α
 
 noncomputable abbrev RS_IntegrableOn (f:ℝ → ℝ) (I: BoundedInterval) (α: ℝ → ℝ) : Prop :=
   BddOn f I ∧ lower_RS_integral f I α = upper_RS_integral f I α

analysis/Analysis/Section_3_1.lean

···
 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 -/

analysis/Analysis/Section_3_4.lean

···
 
 /-- Definition 3.4.1.  Interestingly, the definition does not require S to be a subset of X. -/
 abbrev SetTheory.Set.image {X Y:Set} (f:X → Y) (S: Set) : Set :=
-  X.replace (P := fun x y ↦ y = f x ∧ x.val ∈ S) (by simp_all)
+  X.replace (P := fun x y ↦ f x = y ∧ x.val ∈ S) (by simp_all)
 
 /-- Definition 3.4.1 -/
 theorem SetTheory.Set.mem_image {X Y:Set} (f:X → Y) (S: Set) (y:Object) :