Merge pull request #252 from teorth:golf

some golf

analysis/Analysis/Section_11_1.lean

···
   | Ico _ b => b
 
 theorem BoundedInterval.subset_Icc (I: BoundedInterval) : I ⊆ Icc I.a I.b := match I with
-  | Ioo a b => by simp [Ioo, Icc, BoundedInterval.a, BoundedInterval.b, subset_iff, Set.Ioo_subset_Icc_self]
-  | Icc a b => by simp [Icc, BoundedInterval.a, BoundedInterval.b, subset_iff]
-  | Ioc a b => by simp [Ioc, Icc, BoundedInterval.a, BoundedInterval.b, subset_iff, Set.Ioc_subset_Icc_self]
-  | Ico a b => by simp [Ico, Icc, BoundedInterval.a, BoundedInterval.b, subset_iff, Set.Ico_subset_Icc_self]
+  | Ioo _ _ => by simp [Ioo, Icc, a, b, subset_iff, Set.Ioo_subset_Icc_self]
+  | Icc _ _ => by simp [Icc, a, b, subset_iff]
+  | Ioc _ _ => by simp [Ioc, Icc, a, b, subset_iff, Set.Ioc_subset_Icc_self]
+  | Ico _ _ => by simp [Ico, Icc, a, b, subset_iff, Set.Ico_subset_Icc_self]
 
 theorem BoundedInterval.Ioo_subset (I: BoundedInterval) : Ioo I.a I.b ⊆ I := match I with
-  | Ioo a b => by simp [Ioo, BoundedInterval.a, BoundedInterval.b, subset_iff]
-  | Icc a b => by simp [Icc, BoundedInterval.a, BoundedInterval.b, subset_iff, Set.Ioo_subset_Icc_self]
-  | Ioc a b => by simp [Ioc, Ioo, BoundedInterval.a, BoundedInterval.b, subset_iff, Set.Ioo_subset_Ioc_self]
-  | Ico a b => by simp [Ico, Ioo, BoundedInterval.a, BoundedInterval.b, subset_iff, Set.Ioo_subset_Ico_self]
+  | Ioo _ _ => by simp [Ioo, a, b, subset_iff]
+  | Icc _ _ => by simp [Icc, a, b, subset_iff, Set.Ioo_subset_Icc_self]
+  | Ioc _ _ => by simp [Ioc, Ioo, a, b, subset_iff, Set.Ioo_subset_Ioc_self]
+  | Ico _ _ => by simp [Ico, Ioo, a, b, subset_iff, Set.Ioo_subset_Ico_self]
 
 instance BoundedInterval.instTrans : IsTrans BoundedInterval (· ⊆ ·) where
-  trans I J K hIJ hJK := by
-    simp [subset_iff] at hIJ hJK ⊢
-    exact hIJ.trans hJK
+  trans I J K hIJ hJK := by simp_all [subset_iff]; exact hIJ.trans hJK
 
 @[simp]
 theorem BoundedInterval.mem_inter (I J: BoundedInterval) (x:ℝ) :
-  x ∈ (I ∩ J : BoundedInterval) ↔ x ∈ I ∧ x ∈ J := by
-  simp [inter_eq, Set.mem_inter_iff, mem_iff, mem_iff]
+  x ∈ (I ∩ J : BoundedInterval) ↔ x ∈ I ∧ x ∈ J := by simp [mem_iff]
 
 abbrev BoundedInterval.length (I: BoundedInterval) : ℝ := max (I.b - I.a) 0
 
···
 
 theorem BoundedInterval.empty_of_lt {I: BoundedInterval} (h: I.b < I.a) : (I:Set ℝ) = ∅ := by
   cases I with
-  | Ioo a b => simp [Ioo, le_of_lt h]
-  | Icc a b => simp [Icc, h]
-  | Ioc a b => simp [Ioc, le_of_lt h]
-  | Ico a b => simp [Ico, le_of_lt h]
+  | Ioo _ _ => simp [Ioo, le_of_lt h]
+  | Icc _ _ => simp [Icc, h]
+  | Ioc _ _ => simp [Ioc, le_of_lt h]
+  | Ico _ _ => simp [Ico, le_of_lt h]
 
 theorem BoundedInterval.length_of_empty {I: BoundedInterval} (hI: (I:Set ℝ) = ∅) : |I|ₗ = 0 := by
   sorry
···
 theorem BoundedInterval.dist_le_length {I:BoundedInterval} {x y:ℝ} (hx: x ∈ I) (hy: y ∈ I) : |x - y| ≤ |I|ₗ := by
   replace hx := subset_Icc I _ hx
   replace hy := subset_Icc I _ hy
-  simp [mem_iff, abs_le'] at hx hy ⊢
-  left; constructor <;> linarith
+  simp_all [mem_iff, abs_le']; left; constructor <;> linarith
 
 abbrev BoundedInterval.joins (K I J: BoundedInterval) : Prop := (I:Set ℝ) ∩ (J:Set ℝ) = ∅
   ∧ (K:Set ℝ) = (I:Set ℝ) ∪ (J:Set ℝ) ∧ |K|ₗ = |I|ₗ + |J|ₗ
···
   . ext x; simp; constructor
     . 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]
+  simp [length, 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
   and_intros
···
   . ext x; simp; constructor
     . 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]
+  simp [length, 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
   and_intros
···
   . ext x; simp; constructor
     . 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]
+  simp [length, 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
   and_intros
···
   . ext x; simp; constructor
     . 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]
+  simp [length, 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
   and_intros
···
   . ext x; simp; constructor
     . 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]
+  simp [length, 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
   and_intros
···
   . ext x; simp; constructor
     . 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]
+  simp [length, 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
   and_intros
···
   . ext x; simp; constructor
     . 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]
+  simp [length, 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
   and_intros
···
   . ext x; simp; constructor
     . 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]
+  simp [length, show a ≤ b by linarith, show b ≤ c by linarith, show a ≤ c by linarith]
 
 
 @[ext]
···
   bot := {
     intervals := {I}
     exists_unique x hx := by apply ExistsUnique.intro I <;> simp [hx]
-    contains J hJ := by simp at hJ; rw [hJ, subset_iff]
+    contains J hJ := by simp_all [subset_iff]
     }
 
 @[simp]
···
 {
   intervals := P.intervals ∪ Q.intervals
   exists_unique x hx := by
-    simp [mem_iff, h.2] at hx
-    rcases hx with hx | hx
-    . obtain ⟨ L, hLP, hxL ⟩ := (P.exists_unique x hx).exists
+    simp [mem_iff, h.2] at hx; rcases hx with hx | hx
+    . obtain ⟨ L, hLP, hxL ⟩ := (P.exists_unique _ hx).exists
       apply ExistsUnique.intro L (by aesop)
-      intro K ⟨hK, hxK⟩
-      simp at hK; rcases hK with hKP | hKQ
-      . exact (P.exists_unique x hx).unique ⟨ hKP, hxK ⟩ ⟨ hLP, hxL ⟩
-      replace hxK := (BoundedInterval.subset_iff _ _).mp (Q.contains K hKQ) hxK
-      have := congr(x ∈ $(h.1))
-      simp [hx, hxK] at this
-    obtain ⟨ L, hLQ, hxL ⟩ := (Q.exists_unique x hx).exists
+      intro K ⟨hK, hxK⟩; simp at hK; rcases hK with hKP | hKQ
+      . exact (P.exists_unique _ hx).unique ⟨ hKP, hxK ⟩ ⟨ hLP, hxL ⟩
+      replace hxK := (K.subset_iff _).mp (Q.contains _ hKQ) hxK
+      have := congr(x ∈ $(h.1)); simp [hx, hxK] at this
+    obtain ⟨ L, hLQ, hxL ⟩ := (Q.exists_unique _ hx).exists
     apply ExistsUnique.intro L (by aesop)
-    intro K ⟨hK, hxK⟩
-    simp at hK; rcases hK with hKP | hKQ
-    . replace hxK := (BoundedInterval.subset_iff _ _).mp (P.contains K hKP) hxK
-      have := congr(x ∈ $(h.1))
-      simp [hx, hxK] at this
+    intro K ⟨hK, hxK⟩; simp at hK; rcases hK with hKP | hKQ
+    . replace hxK := (K.subset_iff _).mp (P.contains _ hKP) hxK
+      have := congr(x ∈ $(h.1)); simp [hx, hxK] at this
     exact (Q.exists_unique x hx).unique ⟨ hKQ, hxK ⟩ ⟨ hLQ, hxL ⟩
   contains L hL := by
     simp at hL; rcases hL with hLP | hLQ
-    . apply (P.contains L hLP).trans
-      simp [h, subset_iff]
-    apply (Q.contains L hLQ).trans
-    simp [h, subset_iff]
+    . apply (P.contains _ hLP).trans; simp [h, subset_iff]
+    apply (Q.contains _ hLQ).trans; simp [h, subset_iff]
 }
 
 @[simp]
···
     simp [mem_iff] at hxK
   contains L hL := by
     simp at hL; rcases hL with hL | rfl
-    . exact P.contains L hL
+    . exact P.contains _ hL
     simp [subset_iff]
 }
 
···
   intervals := P.intervals.filter (fun J ↦ (J:Set ℝ).Nonempty)
   exists_unique x hx := by
     obtain ⟨ J, hJP, hxJ ⟩ := (P.exists_unique x hx).exists
-    apply ExistsUnique.intro J (by
-      simp [hxJ, hJP]; simp [mem_iff] at hxJ; exact Set.nonempty_of_mem hxJ )
+    apply ExistsUnique.intro J (by simp_all [mem_iff]; exact Set.nonempty_of_mem hxJ )
     intro K ⟨ hK, hxK ⟩; simp at hK
     exact (P.exists_unique x hx).unique ⟨ hK.1, hxK ⟩ ⟨ hJP, hxJ ⟩
-  contains L hL := by
-    simp at hL; exact P.contains L hL.1
+  contains L hL := by simp at hL; exact P.contains _ hL.1
 }
 
 @[simp]
···
   simp [Partition.add_empty, Finset.union_empty]
 
 example : ∃ P:Partition (Icc 1 8),
-  P.intervals = {Icc 1 1, Ioo 1 3, Ico 3 5,
-                 Icc 5 5, Ioc 5 8, ∅} := by
+  P.intervals = {Icc 1 1, Ioo 1 3, Ico 3 5, Icc 5 5, Ioc 5 8, ∅} := by
   set P1 : Partition (Icc 1 1) := ⊥
-  set P2 : Partition (Ico 1 3) := P1.join (⊥:Partition (Ioo 1 3))
-                                  (BoundedInterval.join_Icc_Ioo (by norm_num) (by norm_num) )
-  set P3 : Partition (Ico 1 5) := P2.join (⊥:Partition (Ico 3 5))
-                                  (BoundedInterval.join_Ico_Ico (by norm_num) (by norm_num) )
-  set P4 : Partition (Icc 1 5) := P3.join (⊥:Partition (Icc 5 5))
-                                  (BoundedInterval.join_Ico_Icc (by norm_num) (by norm_num) )
-  set P5 : Partition (Icc 1 8) := P4.join (⊥:Partition (Ioc 5 8))
-                                  (BoundedInterval.join_Icc_Ioc (by norm_num) (by norm_num) )
+  set P2 : Partition (Ico 1 3) := P1.join (⊥:Partition (Ioo 1 3)) (join_Icc_Ioo (by norm_num) (by norm_num) )
+  set P3 : Partition (Ico 1 5) := P2.join (⊥:Partition (Ico 3 5)) (join_Ico_Ico (by norm_num) (by norm_num) )
+  set P4 : Partition (Icc 1 5) := P3.join (⊥:Partition (Icc 5 5)) (join_Ico_Icc (by norm_num) (by norm_num) )
+  set P5 : Partition (Icc 1 8) := P4.join (⊥:Partition (Ioc 5 8)) (join_Icc_Ioc (by norm_num) (by norm_num) )
   use P5.add_empty
   simp [P5, P4, P3, P2, P1]
   aesop
 
-example : ∃ P:Partition (Icc 1 8),
-  P.intervals = {Icc 1 1, Ioo 1 3, Ico 3 5,
-                 Icc 5 5, Ioc 5 8} := by
+example : ∃ P:Partition (Icc 1 8), P.intervals = {Icc 1 1, Ioo 1 3, Ico 3 5, Icc 5 5, Ioc 5 8} := by
   sorry
 
-example : ¬ ∃ P:Partition (Icc 1 5),
-  P.intervals = {Icc 1 4, Icc 3 5} := by
+example : ¬ ∃ P:Partition (Icc 1 5), P.intervals = {Icc 1 4, Icc 3 5} := by
   sorry
 
-example : ¬ ∃ P:Partition (Ioo 1 5),
-  P.intervals = {Ioo 1 3, Ioo 3 5} := by
+example : ¬ ∃ P:Partition (Ioo 1 5), P.intervals = {Ioo 1 3, Ioo 3 5} := by
   sorry
 
-example : ¬ ∃ P:Partition (Ioo 1 5),
-  P.intervals = {Ioo 0 3, Ico 3 5} := by
+example : ¬ ∃ P:Partition (Ioo 1 5), P.intervals = {Ioo 0 3, Ico 3 5} := by
   sorry
 
 
···
   : ∃ c ∈ Set.Ico I.a I.b, Ioo c I.b ∈ P ∨ Ico c I.b ∈ P := by
   sorry
 
-/-- Theorem 11.1.13 (Length is finitely additive).
-Due to the excessive case analysis, `simp only` is used in place of `simp` in some places
-to speed up elaboration. -/
+/-- Theorem 11.1.13 (Length is finitely additive). -/
 theorem Partition.sum_of_length  (I: BoundedInterval) (P: Partition I) :
   ∑ J ∈ P.intervals, |J|ₗ = |I|ₗ := by
   -- This proof is written to follow the structure of the original text.
···
   . rw [Finset.card_eq_zero] at hcard
     have : (I:Set ℝ) = ∅ := by
       sorry
-    replace this := length_of_empty this
-    simp only [hcard, Finset.sum_empty, this]
+    simp [hcard, length_of_empty this]
   -- the proof in the book treats the n=1 case separately, but this is unnecessary
   by_cases h : Subsingleton (I:Set ℝ)
   . have (J: BoundedInterval) (hJ: J ∈ P) : Subsingleton (J:Set ℝ) := by
       sorry
     simp_rw [length_of_subsingleton] at h this
-    simp only [h]
-    apply Finset.sum_eq_zero this
-  simp only [length_of_subsingleton, length, sup_eq_right, tsub_le_iff_right, zero_add, not_le] at h
+    convert Finset.sum_eq_zero this
+  simp [length_of_subsingleton, length, -Set.subsingleton_coe] at h
   have : ∃ K L : BoundedInterval, K ∈ P ∧ I.joins L K := by
     by_cases hI' : I.b ∈ I
     . obtain ⟨ K, hK, hbK ⟩ := (P.exists_unique I.b hI').exists
       have hKI : K ⊆ I := P.contains K hK
       by_cases hsub : Subsingleton (K:Set ℝ)
-      . simp_all [mem_iff, Set.subsingleton_coe]
-        replace hbK := Set.Subsingleton.eq_singleton_of_mem hsub hbK
+      . simp_all [mem_iff]
+        replace hbK := hsub.eq_singleton_of_mem hbK
         have : K = Icc (I.b) (I.b) := by
           sorry
         subst this
         cases I with
-        | Ioo a b => simp [mem_iff, Set.mem_Ioo, lt_self_iff_false, and_false] at hI'
-        | Icc a b => use (Icc b b), hK, Ico a b
-                     exact join_Ico_Icc (le_of_lt h) (le_refl _)
-        | Ioc a b => use (Icc b b), hK, Ioo a b
-                     exact join_Ioo_Icc h (le_refl _)
-        | Ico a b => simp [mem_iff, Set.mem_Ico, lt_self_iff_false, and_false] at hI'
-      simp only [length_of_subsingleton, sup_eq_right, tsub_le_iff_right, zero_add, not_le] at hsub
+        | Ioo _ _ => simp [mem_iff] at hI'
+        | Icc a b => use (Icc b b), hK, Ico a b; apply join_Ico_Icc <;> order
+        | Ioc a b => use (Icc b b), hK, Ioo a b; apply join_Ioo_Icc <;> order
+        | Ico _ _ => simp [mem_iff] at hI'
+      simp [length_of_subsingleton, -Set.subsingleton_coe] at hsub
       have hKI' := (K.Ioo_subset.trans hKI).trans I.subset_Icc
       simp only [subset_iff] at hKI'
       have hKb : K.b = I.b := by
-        rw [le_antisymm_iff]
-        constructor
-        . replace hKI' := csSup_le_csSup bddAbove_Icc ?_ hKI'
-          . simp_all [csSup_Ioo hsub, csSup_Icc (le_of_lt h)]
-          simp [Set.nonempty_Ioo, hsub]
-        have := K.subset_Icc _ hbK
-        simp only [mem_iff, Set.mem_Icc] at this
-        exact this.2
+        rw [le_antisymm_iff]; and_intros
+        . replace hKI' := csSup_le_csSup bddAbove_Icc (by simp [hsub]) hKI'
+          simp_all [csSup_Ioo hsub, csSup_Icc (le_of_lt h)]
+        have := K.subset_Icc _ hbK; simp only [mem_iff, Set.mem_Icc] at this; exact this.2
       have hKA : I.a ≤ K.a := by
-        replace hKI' := csInf_le_csInf bddBelow_Icc ?_ hKI'
-        . simp_all [csInf_Icc (le_of_lt h), csInf_Ioo]
-        simp [Set.nonempty_Ioo, hsub]
+        replace hKI' := csInf_le_csInf bddBelow_Icc (by simp [hsub]) hKI'
+        simp_all [csInf_Icc (le_of_lt h), csInf_Ioo]
       cases I with
-      | Ioo a b => simp [mem_iff, Set.mem_Ioo, lt_self_iff_false, and_false] at hI'
-      | Icc a b =>
+      | Ioo _ _ => simp [mem_iff] at hI'
+      | Icc a₁ b₁ =>
         cases K with
-        | Ioo c b' =>
-          simp [mem_iff, subset_iff, BoundedInterval.a, BoundedInterval.b, Set.mem_Icc, Set.mem_Ioo] at *
-          linarith
-        | Icc c b' =>
-          use Icc c b', Ico a c, hK
-          simp [BoundedInterval.b] at hKb; subst hKb
-          exact join_Ico_Icc hKA (by linarith)
-        | Ioc c b' =>
-          use Ioc c b', Icc a c, hK
-          simp [BoundedInterval.b] at hKb; subst hKb
-          exact join_Icc_Ioc hKA (by linarith)
-        | Ico c b' => simp [BoundedInterval.a, BoundedInterval.b, mem_iff, Set.mem_Icc,
-          le_refl, and_true, Set.mem_Ico, subset_iff] at *; linarith
-      | Ioc a b =>
+        | Ioo _ _ => simp [mem_iff, subset_iff, a, b] at *; linarith
+        | Icc c₂ b₂ => use Icc c₂ b₂, Ico a₁ c₂, hK; simp_all [b]; apply join_Ico_Icc <;> order
+        | Ioc c₂ b₂ => use Ioc c₂ b₂, Icc a₁ c₂, hK; simp_all [b]; apply join_Icc_Ioc <;> order
+        | Ico _ _ => simp [a, b, mem_iff] at *; linarith
+      | Ioc a₁ b₁ =>
         cases K with
-        | Ioo c b' => simp_all [mem_iff, subset_iff]
-        | Icc c b' =>
-          use Icc c b', Ioo a c, hK
-          simp [BoundedInterval.b] at hKb; subst hKb
-          simp [subset_iff] at hKI
-          have : c ∈ Set.Icc c b' := by simp; linarith
+        | Ioo _ _ => simp_all [mem_iff, subset_iff]
+        | Icc c₂ b₂ =>
+          use Icc c₂ b₂, Ioo a₁ c₂, hK
+          simp_all [a,b,subset_iff]
+          have : c₂ ∈ Set.Icc c₂ b₁ := by simp; linarith
           replace this := hKI this; simp at this
-          exact join_Ioo_Icc (by linarith) (by linarith)
-        | Ioc c b' =>
-          use Ioc c b', Ioc a c, hK
-          simp [BoundedInterval.b] at hKb; subst hKb
-          exact join_Ioc_Ioc hKA (by linarith)
-        | Ico c b' =>
-          simp [mem_iff, subset_iff, BoundedInterval.a, BoundedInterval.b, Set.mem_Ioc, Set.mem_Ico] at *; linarith
-      | Ico a b => simp [mem_iff, Set.mem_Ico, lt_self_iff_false, and_false] at hI'
+          apply join_Ioo_Icc <;> tauto
+        | Ioc c₂ b₂ => use Ioc c₂ b₂, Ioc a₁ c₂, hK; simp_all [b]; apply join_Ioc_Ioc <;> order
+        | Ico _ _ => simp [mem_iff, subset_iff, a, b] at *; linarith
+      | Ico _ _ => simp [mem_iff] at hI'
     obtain ⟨ c, hc, hK ⟩ := P.exist_right h hI'
     cases I with
-    | Ioo a b =>
+    | Ioo a₁ b₁ =>
       rcases hK with hK | hK
-      . simp_all [mem_iff, subset_iff, BoundedInterval.a, BoundedInterval.b]
-        use Ioo c b, hK, Ioc a c
-        exact join_Ioc_Ioo (hc.1) (hc.2)
-      simp_all [mem_iff, subset_iff, BoundedInterval.a, BoundedInterval.b]
-      use Ico c b, hK, Ioo a c
-      replace hK := P.contains _ hK
-      simp [subset_iff] at hK
-      have : c ∈ Set.Ico c b := by simp; linarith
+      . simp_all [mem_iff, subset_iff, a, b]; use Ioo c b₁, hK, Ioc a₁ c; apply join_Ioc_Ioo <;> tauto
+      simp_all [mem_iff, subset_iff, a, b]
+      use Ico c b₁, hK, Ioo a₁ c
+      replace hK := P.contains _ hK; simp [subset_iff] at hK
+      have : c ∈ Set.Ico c b₁ := by simp; linarith
       replace this := hK this; simp at this
-      exact join_Ioo_Ico (by linarith) (by linarith)
-    | Icc a b => simp [mem_iff, subset_iff, BoundedInterval.a, BoundedInterval.b] at hI' h; linarith
-    | Ioc a b => simp [mem_iff, subset_iff, BoundedInterval.a, BoundedInterval.b] at hI' h; linarith
-    | Ico a b =>
+      apply join_Ioo_Ico <;> linarith
+    | Icc _ _ => simp [mem_iff, subset_iff, a, b] at hI' h; order
+    | Ioc _ _ => simp [mem_iff, subset_iff, a, b] at hI' h; order
+    | Ico a₁ b₁ =>
       rcases hK with hK | hK
-      . simp_all [mem_iff, subset_iff, BoundedInterval.a, BoundedInterval.b]
-        use Ioo c b, hK, Icc a c
-        exact join_Icc_Ioo (hc.1) (hc.2)
-      simp_all [mem_iff, subset_iff, BoundedInterval.a, BoundedInterval.b]
-      use Ico c b, hK, Ico a c
-      exact join_Ico_Ico (by linarith) (by linarith)
+      . simp_all [mem_iff, subset_iff, a, b]; use Ioo c b₁, hK, Icc a₁ c; apply join_Icc_Ioo <;> tauto
+      simp_all [mem_iff, subset_iff, a, b]; use Ico c b₁, hK, Ico a₁ c;  apply join_Ico_Ico <;> linarith
   obtain ⟨ K, L, hK, ⟨ h1, h2, h3 ⟩ ⟩ := this
   have : ∃ P' : Partition L, P'.intervals = P.intervals.erase K := by
     sorry
   obtain ⟨ P', hP' ⟩ := this
-  rw [h3, ←Finset.add_sum_erase _ _ hK, ←hP', add_comm]
-  congr
-  apply hn _ _ _
-  simp only [hP', Finset.card_erase_of_mem hK, hcard, add_tsub_cancel_right]
+  rw [h3, ←Finset.add_sum_erase _ _ hK, ←hP', add_comm]; congr
+  apply hn; simp [hP', Finset.card_erase_of_mem hK, hcard]
 
 /-- Definition 11.1.14 (Finer and coarser partitions) -/
 instance Partition.instLE (I: BoundedInterval) : LE (Partition I) where
···
   max P P' := {
     intervals := Finset.image₂ (fun J K ↦ J ∩ K) P.intervals P'.intervals
     exists_unique x hx := by
-      obtain ⟨ J, ⟨ hJ1, hJ2⟩, hxJ ⟩ := P.exists_unique x hx
-      obtain ⟨ K, ⟨ hK1, hK2⟩, hxK ⟩ := P'.exists_unique x hx
+      obtain ⟨ J, ⟨ hJ1, hJ2⟩, hxJ ⟩ := P.exists_unique _ hx
+      obtain ⟨ K, ⟨ hK1, hK2⟩, hxK ⟩ := P'.exists_unique _ hx
       simp [hx] at hxJ hxK
       apply ExistsUnique.intro (J ∩ K)
-      . simp; exact ⟨ ⟨ J, hJ1, K, hK1, rfl ⟩, ⟨ hJ2, hK2 ⟩ ⟩
-      simp; rintro L J' hJ' K' hK' rfl hx'; simp at hx'
-      specialize hxJ J' hJ' hx'.1
-      specialize hxK K' hK' hx'.2
-      simp [hxJ, hxK]
+      . simp_all; exact ⟨ _, hJ1, _, hK1, rfl ⟩
+      simp; rintro _ J' hJ' K' hK' rfl hx'; simp at hx'
+      simp [hxJ _ hJ' hx'.1, hxK _ hK' hx'.2]
     contains L hL := by
       simp at hL
       obtain ⟨ J, hJ, K, hK, rfl ⟩ := hL
-      replace hJ := P.contains J hJ
-      replace hK := P'.contains K hK
+      replace hJ := P.contains _ hJ
+      replace hK := P'.contains _ hK
       simp [subset_iff] at hJ hK ⊢
       exact Set.inter_subset_left.trans hJ
     }
 
 
 /-- Example 11.1.17 -/
-example : ∃ P P' : Partition (Icc 1 4),
-  P.intervals = {Ico 1 3, Icc 3 4} ∧
-  P'.intervals = {Icc 1 2, Ioc 2 4} ∧
+example : ∃ P P' : Partition (Icc 1 4), P.intervals = {Ico 1 3, Icc 3 4} ∧ P'.intervals = {Icc 1 2, Ioc 2 4} ∧
   (P' ⊔ P).intervals = {Icc 1 2, Ioo 2 3, Icc 3 4, ∅} := by
   sorry
 

analysis/Analysis/Section_11_2.lean

···
   if h: Constant f then h.choose else hY.some
 
 theorem Constant.eq {X Y:Type} {f: X → Y} [Nonempty Y] (h: Constant f) (x:X) :
-  f x = constant_value f := by
-  rw [constant_value, dif_pos h]
-  exact h.choose_spec x
+  f x = constant_value f := by simp [constant_value, h]; apply h.choose_spec
 
 theorem Constant.of_const {X Y:Type} {f:X → Y} {c:Y} (h: ∀ x, f x = c) :
   Constant f := by use c
 
 theorem Constant.const_eq {X Y:Type} {f:X → Y} [hX: Nonempty X] [Nonempty Y] {c:Y} (h: ∀ x, f x = c) :
-  constant_value f = c := by
-    rw [←eq (of_const h) hX.some, h hX.some]
+  constant_value f = c := by rw [←eq (of_const h) hX.some, h hX.some]
 
-theorem Constant.of_subsingleton {X Y:Type} [Subsingleton X] [hY: Nonempty Y] {f:X → Y} :
+theorem Constant.of_subsingleton {X Y:Type} [hs: Subsingleton X] [hY: Nonempty Y] {f:X → Y} :
   Constant f := by
   by_cases h:Nonempty X
-  . use f (h.some : X); intro x; congr; exact Subsingleton.elim x h.some
-  use hY.some; intro x; simp at h; exact IsEmpty.elim h x
+  . use f h.some; intros; congr; exact hs.elim _ h.some
+  use hY.some; intro x; simp at h; exact h.elim x
 
 abbrev ConstantOn (f: ℝ → ℝ) (X: Set ℝ) : Prop := Constant (fun x : X ↦ f ↑x)
 
···
 
 theorem ConstantOn.eq {f: ℝ → ℝ} {X: Set ℝ} (h: ConstantOn f X) {x:ℝ} (hx: x ∈ X) :
   f x = constant_value_on f X := by
-  convert Constant.eq h ⟨ x, hx ⟩
+  convert Constant.eq h ⟨ _, hx ⟩
 
 theorem ConstantOn.of_const {f:ℝ → ℝ} {X: Set ℝ} {c:ℝ} (h: ∀ x ∈ X, f x = c) :
   ConstantOn f X := by use c; rintro ⟨ x, hx ⟩; simp [h x hx]
 
 theorem ConstantOn.of_const' (c:ℝ) (X:Set ℝ): ConstantOn (fun _ ↦ c) X := by
-  apply ConstantOn.of_const (c := c)
-  simp
+  apply of_const (c := c); simp
 
 theorem ConstantOn.const_eq {f:ℝ → ℝ} {X: Set ℝ} (hX: X.Nonempty) {c:ℝ} (h: ∀ x ∈ X, f x = c) :
   constant_value_on f X = c := by
     rw [←eq (of_const h) hX.some_mem, h _ hX.some_mem]
 
 theorem ConstantOn.congr {f g: ℝ → ℝ} {X: Set ℝ} (h: ∀ x ∈ X, f x = g x) : ConstantOn f X ↔ ConstantOn g X := by
-  simp [ConstantOn]; rw [iff_iff_eq]
-  congr; ext ⟨ x, hx ⟩; simp [h x hx]
+  simp [ConstantOn]; rw [iff_iff_eq]; congr; ext ⟨ _, hx ⟩; simp [h _ hx]
 
 theorem ConstantOn.of_subsingleton {f: ℝ → ℝ} {X: Set ℝ} [Subsingleton X] :
   ConstantOn f X := Constant.of_subsingleton
 
 theorem constant_value_on_congr {f g: ℝ → ℝ} {X: Set ℝ} (h: ∀ x ∈ X, f x = g x) :
   constant_value_on f X = constant_value_on g X := by
-  simp [constant_value_on]
-  congr; ext ⟨ x, hx ⟩; simp [h x hx]
+  simp [constant_value_on]; congr; ext ⟨ _, hx ⟩; simp [h _ hx]
 
 /-- Definition 11.2.3 (Piecewise constant functions I) -/
 abbrev PiecewiseConstantWith (f:ℝ → ℝ) {I: BoundedInterval} (P: Partition I) : Prop := ∀ J ∈ P, ConstantOn f (J:Set ℝ)
···
 theorem PiecewiseConstantWith.congr {f g:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
   (h: ∀ x ∈ (I:Set ℝ), f x = g x) :
   PiecewiseConstantWith f P ↔ PiecewiseConstantWith g P := by
-  simp [PiecewiseConstantWith]
-  peel with J hJ
-  apply ConstantOn.congr; intro x hx
-  have := P.contains _ hJ; rw [subset_iff] at this
-  solve_by_elim
+  simp [PiecewiseConstantWith]; peel with J hJ
+  apply ConstantOn.congr; intros; have := P.contains _ hJ; rw [subset_iff] at this; solve_by_elim
 
 /-- Definition 11.2.5 (Piecewise constant functions I) -/
 abbrev PiecewiseConstantOn (f:ℝ → ℝ) (I: BoundedInterval) : Prop := ∃ P : Partition I, PiecewiseConstantWith f P
···
 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
   simp only [integ, Subtype.forall]
-  apply Finset.sum_congr rfl; intro J hJ; congr 1
-  apply constant_value_on_congr; intro x hx
+  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
   aesop
 
···
 
 /-- Proposition 11.2.13 (Piecewise constant integral is independent of partition) / Exercise 11.2.3 -/
 theorem PiecewiseConstantWith.integ_eq {f:ℝ → ℝ} {I: BoundedInterval} {P P': Partition I}
-  (hP: PiecewiseConstantWith f P) (hP': PiecewiseConstantWith f P') : PiecewiseConstantWith.integ f P = PiecewiseConstantWith.integ f P' := by
+  (hP: PiecewiseConstantWith f P) (hP': PiecewiseConstantWith f P') : integ f P = integ f P' := by
   sorry
 
 open Classical in
···
   ℝ := if h: PiecewiseConstantOn f I then PiecewiseConstantWith.integ f h.choose else 0
 
 theorem PiecewiseConstantOn.integ_def {f:ℝ → ℝ} {I: BoundedInterval} {P: Partition I}
-  (h: PiecewiseConstantWith f P) : PiecewiseConstantOn.integ f I = PiecewiseConstantWith.integ f P := by
+  (h: PiecewiseConstantWith f P) : integ f I = PiecewiseConstantWith.integ f P := by
   have h' : PiecewiseConstantOn f I := by use P
-  simp [PiecewiseConstantOn.integ, h']
-  exact PiecewiseConstantWith.integ_eq h'.choose_spec h
+  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
   by_cases hf : PiecewiseConstantOn f I
-  <;> have hg := hf <;> rw [PiecewiseConstantOn.congr h] at hg <;> simp [integ, hf, hg]
-  rw [PiecewiseConstantWith.integ_congr h, ←integ_def ?_, ←integ_def ?_]
-  . exact hg.choose_spec
-  rw [←PiecewiseConstantWith.congr h]
-  exact hf.choose_spec
+  <;> have hg := hf <;> rw [congr h] at hg <;> simp [integ, hf, hg]
+  rw [PiecewiseConstantWith.integ_congr h, ←integ_def hg.choose_spec, ←integ_def ?_]
+  rw [←PiecewiseConstantWith.congr h]; exact hf.choose_spec
 
 /-- Example 11.2.15 -/
 example : PiecewiseConstantOn.integ f_11_2_4 (Icc 1 6) = 10 := by
···
 /-- Theorem 11.2.16 (a) (Laws of integration) / Exercise 11.2.4 -/
 theorem PiecewiseConstantOn.integ_add {f g: ℝ → ℝ} {I: BoundedInterval}
   (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) :
-  PiecewiseConstantOn.integ (f + g) I = PiecewiseConstantOn.integ f I + PiecewiseConstantOn.integ g I := by
+  integ (f + g) I = integ f I + integ g I := by
   sorry
 
 /-- Theorem 11.2.16 (b) (Laws of integration) / Exercise 11.2.4 -/
-theorem PiecewiseConstantOn.integ_smul {f: ℝ → ℝ} {I: BoundedInterval} (c:ℝ)
-  (hf: PiecewiseConstantOn f I) :
-  PiecewiseConstantOn.integ (c • f) I = c * PiecewiseConstantOn.integ f I
+theorem PiecewiseConstantOn.integ_smul {f: ℝ → ℝ} {I: BoundedInterval} (c:ℝ) (hf: PiecewiseConstantOn f I) :
+  integ (c • f) I = c * integ f I
    := by
   sorry
 
 /-- Theorem 11.2.16 (c) (Laws of integration) / Exercise 11.2.4 -/
 theorem PiecewiseConstantOn.integ_sub {f g: ℝ → ℝ} {I: BoundedInterval}
   (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) :
-  PiecewiseConstantOn.integ (f - g) I = PiecewiseConstantOn.integ f I - PiecewiseConstantOn.integ g I
-   := by
+  integ (f - g) I = integ f I - integ g I := by
   sorry
 
 /-- Theorem 11.2.16 (d) (Laws of integration) / Exercise 11.2.4 -/
 theorem PiecewiseConstantOn.integ_of_nonneg {f: ℝ → ℝ} {I: BoundedInterval} (h: ∀ x ∈ I, 0 ≤ f x)
   (hf: PiecewiseConstantOn f I) :
-  0 ≤ PiecewiseConstantOn.integ f I := by
+  0 ≤ integ f I := by
   sorry
 
 /-- Theorem 11.2.16 (e) (Laws of integration) / Exercise 11.2.4 -/
 theorem PiecewiseConstantOn.integ_mono {f g: ℝ → ℝ} {I: BoundedInterval} (h: ∀ x ∈ I, f x ≤ g x)
   (hf: PiecewiseConstantOn f I) (hg: PiecewiseConstantOn g I) :
-  PiecewiseConstantOn.integ f I ≤ PiecewiseConstantOn.integ g I := by
+  integ f I ≤ integ g I := by
   sorry
 
 
 /-- Theorem 11.2.16 (f) (Laws of integration) / Exercise 11.2.4 -/
 theorem PiecewiseConstantOn.integ_const (c: ℝ) (I: BoundedInterval) :
-  PiecewiseConstantOn.integ (fun _ ↦ c) I = c * |I|ₗ := by
+  integ (fun _ ↦ c) I = c * |I|ₗ := by
   sorry
 
 /-- Theorem 11.2.16 (f) (Laws of integration) / Exercise 11.2.4 -/
 theorem PiecewiseConstantOn.integ_const' {f:ℝ → ℝ} {I: BoundedInterval} (h: ConstantOn f I) :
-  PiecewiseConstantOn.integ f I = (constant_value_on f I) * |I|ₗ := by
+  integ f I = (constant_value_on f I) * |I|ₗ := by
   sorry
 
 open Classical in
···
 /-- Theorem 11.2.16 (g) (Laws of integration) / Exercise 11.2.4 -/
 theorem PiecewiseConstantOn.integ_of_extend {I J: BoundedInterval} (hIJ: I ⊆ J)
   {f: ℝ → ℝ} (h: PiecewiseConstantOn f I) :
-  PiecewiseConstantOn.integ (fun x ↦ if x ∈ I then f x else 0) J = PiecewiseConstantOn.integ f I := by
+  integ (fun x ↦ if x ∈ I then f x else 0) J = integ f I := by
   sorry
 
 /-- Theorem 11.2.16 (h) (Laws of integration) / Exercise 11.2.4 -/
···
 /-- Theorem 11.2.16 (h) (Laws of integration) / Exercise 11.2.4 -/
 theorem PiecewiseConstantOn.integ_of_join {I J K: BoundedInterval} (hIJK: K.joins I J)
   {f: ℝ → ℝ} (h: PiecewiseConstantOn f K) :
-  PiecewiseConstantOn.integ f K = PiecewiseConstantOn.integ f I + PiecewiseConstantOn.integ f J := by
+  integ f K = integ f I + integ f J := by
   sorry
 
 end Chapter11

analysis/Analysis/Section_11_3.lean

···
 
 lemma integral_bound_upper_of_bounded {f:ℝ → ℝ} {M:ℝ} {I: BoundedInterval} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) : M * |I|ₗ ∈ (fun g ↦ PiecewiseConstantOn.integ g I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I} := by
   simp
-  refine ⟨ fun _ ↦ M , ⟨ ⟨ ?_, ?_, ⟩, ?_ ⟩ ⟩
-  . peel h with x hx h'
-    simp [abs_le'] at h'
-    simp [h'.1]
-  . apply PiecewiseConstantOn.of_const (ConstantOn.of_const (c := M) _)
-    simp
-  exact PiecewiseConstantOn.integ_const M I
+  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))
 
 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 , ⟨ ⟨ ?_, ?_, ⟩, ?_ ⟩ ⟩
-  . peel h with x hx h'
-    simp [abs_le'] at h'
-    simp; linarith
-  . apply PiecewiseConstantOn.of_const (ConstantOn.of_const (c := -M) _)
-    simp
-  convert PiecewiseConstantOn.integ_const (-M) I using 1
-  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))
 
 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
-  apply Set.nonempty_of_mem
-  exact integral_bound_upper_of_bounded h
+  obtain ⟨ _, h ⟩ := h; exact Set.nonempty_of_mem (integral_bound_upper_of_bounded h)
 
 lemma integral_bound_lower_nonempty {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) : ((fun g ↦ PiecewiseConstantOn.integ g I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}).Nonempty := by
-  obtain ⟨ _, h ⟩ := h
-  apply Set.nonempty_of_mem
-  exact integral_bound_lower_of_bounded h
+  obtain ⟨ _, h ⟩ := h; exact Set.nonempty_of_mem (integral_bound_lower_of_bounded h)
 
 lemma integral_bound_lower_le_upper {f:ℝ → ℝ} {I: BoundedInterval} {a b:ℝ}
   (ha: a ∈ (fun g ↦ PiecewiseConstantOn.integ g I) '' {g | MajorizesOn 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 PiecewiseConstantOn.integ_mono _ hhp hgp
-    intro x hx
-    have := hmaj x hx
-    apply (ge_iff_le.mp (hmin x hx)).trans (hmaj x hx)
+    rw [←hgi, ←hhi]; apply PiecewiseConstantOn.integ_mono _ hhp hgp
+    intro x hx; exact (ge_iff_le.mp (hmin x hx)).trans (hmaj x hx)
 
 lemma integral_bound_below {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) :
   BddBelow ((fun g ↦ PiecewiseConstantOn.integ g I) '' {g | MajorizesOn g f I ∧ PiecewiseConstantOn g I}) := by
-    rw [bddBelow_def]
-    use (integral_bound_lower_nonempty h).some
+    rw [bddBelow_def]; use (integral_bound_lower_nonempty h).some
     intro a ha; exact integral_bound_lower_le_upper ha (integral_bound_lower_nonempty h).some_mem
 
 lemma integral_bound_above {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) :
   BddAbove ((fun g ↦ PiecewiseConstantOn.integ g I) '' {g | MinorizesOn g f I ∧ PiecewiseConstantOn g I}) := by
-    rw [bddAbove_def]
-    use (integral_bound_upper_nonempty h).some
+    rw [bddAbove_def]; use (integral_bound_upper_nonempty h).some
     intro b hb; exact integral_bound_lower_le_upper (integral_bound_upper_nonempty h).some_mem hb
 
 /-- Lemma 11.3.3.  The proof has been reorganized somewhat from the textbook. -/
···
 lemma lower_integral_le_upper {f:ℝ → ℝ} {I: BoundedInterval} (h: BddOn f I) :
   lower_integral f I ≤ upper_integral f I := by
   apply ConditionallyCompleteLattice.csSup_le _ _ (integral_bound_lower_nonempty h) _
-  rw [mem_upperBounds]
-  intro b hb
+  rw [mem_upperBounds]; intro b hb
   apply ConditionallyCompleteLattice.le_csInf _ _ (integral_bound_upper_nonempty h) _
-  rw [mem_lowerBounds]
-  intro a ha
+  rw [mem_lowerBounds]; intro a ha
   exact integral_bound_lower_le_upper ha hb
 
 lemma upper_integral_le {f:ℝ → ℝ} {I: BoundedInterval} {M:ℝ} (h: ∀ x ∈ (I:Set ℝ), |f x| ≤ M) :
···
   {X:ℝ} (hX: upper_integral f I < X ) :
   ∃ g, MajorizesOn g f I ∧ PiecewiseConstantOn g I ∧ PiecewiseConstantOn.integ g I < X := by
   obtain ⟨ Y, hY, hYX ⟩ := exists_lt_of_csInf_lt (integral_bound_upper_nonempty hf) hX
-  simp at hY
-  peel hY with h hY
-  simp [hY, hYX]; tauto
+  simp at hY; peel hY with h hY; simp_all; tauto
 
 lemma gt_of_lt_lower_integral {f:ℝ → ℝ} {I: BoundedInterval} (hf: BddOn f I)
   {X:ℝ} (hX: X < lower_integral f I) :
   ∃ h, MinorizesOn h f I ∧ PiecewiseConstantOn h I ∧ X < PiecewiseConstantOn.integ h I := by
   obtain ⟨ Y, hY, hYX ⟩ := exists_lt_of_lt_csSup (integral_bound_lower_nonempty hf) hX
-  simp at hY
-  peel hY with h hY
-  simp [hY, hYX]; tauto
+  simp at hY; peel hY with h hY; simp_all; tauto
 
 /-- Definition 11.3.4 (Riemann integral)
 As we permit junk values, the simplest definition for the Riemann integral is the upper integral.-/
-noncomputable abbrev integ (f:ℝ → ℝ) (I: BoundedInterval) : ℝ :=
-upper_integral f I
+noncomputable abbrev integ (f:ℝ → ℝ) (I: BoundedInterval) : ℝ := upper_integral f I
 
 theorem integ_congr {f g:ℝ → ℝ} {I: BoundedInterval} (h: Set.EqOn f g I) :
   integ f I = integ g I := upper_integral_congr h
···
 /-- Remark 11.3.8 -/
 theorem integ_on_subsingleton {f:ℝ → ℝ} {I: BoundedInterval} (hI: |I|ₗ = 0) :
   IntegrableOn f I ∧ integ f I = 0 := by
-  have hI' := hI
-  rw [←length_of_subsingleton] at hI'
+  have _ := length_of_subsingleton.mpr hI
   have hconst : ConstantOn f I := ConstantOn.of_subsingleton
-  convert integ_of_piecewise_const _
-  . simp [PiecewiseConstantOn.integ_const' hconst, hI]
-  exact PiecewiseConstantOn.of_const hconst
+  convert integ_of_piecewise_const (PiecewiseConstantOn.of_const hconst)
+  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. -/
 noncomputable abbrev upper_riemann_sum (f:ℝ → ℝ) {I: BoundedInterval} (P: Partition I) : ℝ :=
···
   sorry
 
 theorem upper_integ_eq_inf_upper_sum {f:ℝ → ℝ} {I:BoundedInterval} (hf: BddOn f I) :
-  upper_integral f I = sInf (Set.range (fun P : Partition I ↦ upper_riemann_sum f P)) := by
+  upper_integral f I = sInf (.range (fun P : Partition I ↦ upper_riemann_sum f P)) := by
   sorry
 
 theorem lower_integ_ge_lower_sum {f:ℝ → ℝ} {I:BoundedInterval} (hf: BddOn f I)
···
   sorry
 
 theorem lower_integ_eq_sup_lower_sum {f:ℝ → ℝ} {I:BoundedInterval} (hf: BddOn f I) :
-  lower_integral f I = sSup (Set.range (fun P : Partition I ↦ lower_riemann_sum f P)) := by
+  lower_integral f I = sSup (.range (fun P : Partition I ↦ lower_riemann_sum f P)) := by
   sorry
 
 /-- Exercise 11.3.1 -/

analysis/Analysis/Section_11_4.lean

···
 lemma nonneg_of_le_const_mul_eps {x C:ℝ} (h: ∀ ε>0, x ≤ C * ε) : x ≤ 0 := by
   by_cases hC: C > 0
   . by_contra!
-    specialize h (x/(2*C)) ( by positivity)
-    convert_to x ≤ x/2 at h
+    specialize h (x/(2*C)) ( by positivity); convert_to x ≤ x/2 at h
     . field_simp; ring
     linarith
-  specialize h 1 (by norm_num)
-  simp at h hC; linarith
+  specialize h 1 (by norm_num); simp at h hC; linarith
 
 /-- Theorem 11.4.3 (Max and min preserve integrability)-/
 theorem integ_of_max {I: BoundedInterval} {f g:ℝ → ℝ} (hf: IntegrableOn f I) (hg: IntegrableOn g I) :
···
   -- This proof is written to follow the structure of the original text.
   unfold IntegrableOn at hf hg
   have hmax_bound : BddOn (max f g) I := by
-    obtain ⟨ M, hM ⟩ := hf.1
-    obtain ⟨ M', hM' ⟩ := hg.1
-    use max M M'; intro x hx
-    specialize hM x hx
-    specialize hM' x hx
+    obtain ⟨ M, hM ⟩ := hf.1; obtain ⟨ M', hM' ⟩ := hg.1
+    use max M M'; peel hM with x hx hM; specialize hM' _ hx
     simp only [Pi.sup_apply]
     apply abs_max_le_max_abs_abs.trans
     exact sup_le_sup hM hM'
···
     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)
     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)
-    obtain ⟨ f'', hf''max, hf''const, hf''int ⟩ := lt_of_gt_upper_integral hf.1 (show upper_integral f I < integ f I + ε  by linarith)
-    obtain ⟨ g'', hg''max, hg''const, hg''int ⟩ := lt_of_gt_upper_integral hg.1 (show upper_integral g I < integ g I + ε  by linarith)
+    obtain ⟨ f'', hf''max, hf''const, hf''int ⟩ := lt_of_gt_upper_integral hf.1 (show upper_integral f I < integ f I + ε by linarith)
+    obtain ⟨ g'', hg''max, hg''const, hg''int ⟩ := lt_of_gt_upper_integral hg.1 (show upper_integral g I < integ g I + ε by linarith)
     set h := (f'' - f') + (g'' - g')
     have hf'_integ := integ_of_piecewise_const hf'const
     have hg'_integ := integ_of_piecewise_const hg'const
···
     have hg''g'_integ := integ_of_sub hg''_integ.1 hg'_integ.1
     have hh_integ_eq := integ_of_add hf''f'_integ.1 hg''g'_integ.1
     have hinteg_le : integ h I ≤ 4 * ε := by linarith
-    have hf''g''_const := PiecewiseConstantOn.max hf''const hg''const
+    have hf''g''_const := hf''const.max hg''const
     have hf''g''_maj : MajorizesOn (max f'' g'') (max f g) I := by
       sorry
-    have hf'g'_const := PiecewiseConstantOn.max hf'const hg'const
+    have hf'g'_const := hf'const.max hg'const
     have hf'g'_maj : MinorizesOn (max f' g') (max f g) I := by
       sorry
     have hff'g''_ge := upper_integral_le_integ hmax_bound hf''g''_maj hf''g''_const
     have hf'g'_le := integ_le_lower_integral hmax_bound hf'g'_maj hf'g'_const
     have : MinorizesOn (max f'' g'') (max f' g' + h) I := by
-      intro x hx
-      specialize hf'min x hx
-      specialize hg'min x hx
-      specialize hf''max x hx
-      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]; constructor <;> linarith
+      peel hf'min with x hx hf'min; specialize hg'min _ hx; specialize hf''max _ hx; specialize hg''max _ hx
+      simp [h]; and_intros <;> linarith [le_max_left (f' x) (g' x), le_max_right (f' x) (g' x)]
     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
     rw [MinorizesOn.iff] at this
-    replace this := integ_mono hf''g''_integ.1 hf'g'h_integ.1 this
-    linarith
-  refine ⟨ hmax_bound, ?_ ⟩
-  replace := nonneg_of_le_const_mul_eps this
-  linarith
+    linarith [integ_mono hf''g''_integ.1 hf'g'h_integ.1 this]
+  exact ⟨ hmax_bound, by linarith [nonneg_of_le_const_mul_eps this] ⟩
+
+
 
 /-- Theorem 11.4.5 / Exercise 11.4.3.  The objective here is to create a shorter proof than the one above.-/
 theorem integ_of_min {I: BoundedInterval} {f g:ℝ → ℝ} (hf: IntegrableOn f I) (hg: IntegrableOn g I) :
···
 /-- Corollary 11.4.4 -/
 theorem integ_of_abs {I: BoundedInterval} {f:ℝ → ℝ} (hf: IntegrableOn f I) :
   IntegrableOn (abs f) I := by
-  have f_plus := integ_of_max hf (integ_of_const 0 I).1
-  have f_minus := integ_of_min hf (integ_of_const 0 I).1
-  convert (integ_of_sub f_plus f_minus).1 using 1
-  ext x
-  rcases le_or_gt (f x) 0 with h | h
+  have := (integ_of_const 0 I).1
+  convert (integ_of_sub (integ_of_max hf this) (integ_of_min hf this)).1 using 1
+  ext x; rcases le_or_gt (f x) 0 with h | h
   . simp [h]
   simp [le_of_lt h]
 
···
   swap
   . apply (integ_on_subsingleton _).1
     rw [←BoundedInterval.length_of_subsingleton]
-    rw [Set.not_nonempty_iff_eq_empty] at hI
-    simp [hI]
+    simp_all [Set.not_nonempty_iff_eq_empty]
   unfold IntegrableOn at hf hg
   obtain ⟨ M₁, hM₁ ⟩ := hf.1
   obtain ⟨ M₂, hM₂ ⟩ := hg.1
-  have hM₁pos : 0 ≤ M₁ := by
-    specialize hM₁ hI.some hI.some_mem
-    apply (abs_nonneg _).trans hM₁
-  have hM₂pos : 0 ≤ M₂ := by
-    specialize hM₂ hI.some hI.some_mem
-    apply (abs_nonneg _).trans hM₂
+  have hM₁pos : 0 ≤ M₁ := (abs_nonneg _).trans (hM₁ hI.some hI.some_mem)
+  have hM₂pos : 0 ≤ M₂ := (abs_nonneg _).trans (hM₂ hI.some hI.some_mem)
   have hmul_bound : BddOn (f * g) I := by
-    use M₁ * M₂
-    intro x hx
-    specialize hM₁ x hx
-    specialize hM₂ x hx
-    simp [abs_mul]
-    exact mul_le_mul  hM₁ hM₂ (by positivity) (by positivity)
+    use M₁ * M₂; peel hM₁ with x hx hM₁; specialize hM₂ _ hx
+    simp [abs_mul]; apply mul_le_mul hM₁ hM₂ <;> positivity
   have lower_le_upper : 0 ≤ upper_integral (f * g) I - lower_integral (f * g) I := by
     linarith [lower_integral_le_upper hmul_bound]
   have (ε:ℝ) (hε: 0 < ε) : upper_integral (f * g) I - lower_integral (f * g) I ≤ 2*(M₁+M₂)*ε := 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)
-      refine ⟨ ?_, ?_, ?_, ?_ ⟩
-      . intro x hx
-        specialize hf_nonneg x hx
-        specialize hf'min x hx
-        aesop
-      . exact PiecewiseConstantOn.max hf'const hzero
-      . apply lt_of_lt_of_le hf'int (PiecewiseConstantOn.integ_mono _ hf'const _)
-        . intro x hx; simp
-        exact PiecewiseConstantOn.max hf'const hzero
-      intro x hx; simp
+      and_intros
+      . peel hf_nonneg with x hx _; specialize hf'min _ hx; aesop
+      . exact hf'const.max hzero
+      . exact lt_of_lt_of_le hf'int (hf'const.integ_mono (by intros; simp) (hf'const.max hzero))
+      intro _ _; simp
     obtain ⟨ f', hf'min, hf'const, hf'int, hf'_nonneg ⟩ := this
     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)
-      refine ⟨ ?_, ?_, ?_, ?_ ⟩
-      . intro x hx
-        specialize hg_nonneg x hx
-        specialize hg'min x hx
-        aesop
-      . exact PiecewiseConstantOn.max hg'const hzero
-      . apply lt_of_lt_of_le hg'int (PiecewiseConstantOn.integ_mono _ hg'const _)
-        . intro x hx; simp
-        exact PiecewiseConstantOn.max hg'const hzero
-      intro x hx; simp
+      and_intros
+      . peel hg_nonneg with x hx _; specialize hg'min _ hx; aesop
+      . exact hg'const.max hzero
+      . apply lt_of_lt_of_le hg'int (hg'const.integ_mono (by intros; simp) (hg'const.max hzero))
+      intro _ _; simp
     obtain ⟨ g', hg'min, hg'const, hg'int, hg'_nonneg ⟩ := this
     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)
-      refine ⟨ ?_, ?_, ?_, ?_ ⟩
-      . intro x hx
-        specialize hM₁ x hx; rw [abs_le'] at hM₁
-        specialize hf''maj x hx
-        simp [hf''maj, hM₁.1]
-      . exact PiecewiseConstantOn.min hf''const hM₁_piece
-      . apply lt_of_le_of_lt (PiecewiseConstantOn.integ_mono _ _ hf''const) hf''int
-        . intro x hx; simp [hf''maj, hM₁_piece]
-        exact PiecewiseConstantOn.min hf''const hM₁_piece
-      intro x hx; simp
+      and_intros
+      . peel hM₁ with x hx hM₁; rw [abs_le'] at hM₁
+        specialize hf''maj _ hx; simp [hf''maj, hM₁.1]
+      . exact hf''const.min hM₁_piece
+      . apply lt_of_le_of_lt ((hf''const.min hM₁_piece).integ_mono _ hf''const) hf''int
+        intros; simp [hf''maj, hM₁_piece]
+      intro _ _; simp
     obtain ⟨ f'', hf''maj, hf''const, hf''int, hf''bound ⟩ := this
     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)
-      refine ⟨ ?_, ?_, ?_, ?_ ⟩
-      . intro x hx
-        specialize hM₂ x hx; rw [abs_le'] at hM₂
-        specialize hg''maj x hx
-        simp [hg''maj, hM₂.1]
-      . exact PiecewiseConstantOn.min hg''const hM₂_piece
-      . apply lt_of_le_of_lt (PiecewiseConstantOn.integ_mono _ _ hg''const) hg''int
-        . intro x hx; simp [hg''maj, hM₂_piece]
-        exact PiecewiseConstantOn.min hg''const hM₂_piece
-      intro x hx; simp
+      and_intros
+      . peel hM₂ with x hx hM₂; rw [abs_le'] at hM₂
+        specialize hg''maj _ hx; simp [hg''maj, hM₂.1]
+      . exact hg''const.min hM₂_piece
+      . apply lt_of_le_of_lt ((hg''const.min hM₂_piece).integ_mono _ hg''const) hg''int
+        intros; simp [hg''maj, hM₂_piece]
+      intro _ _; simp
     obtain ⟨ g'', hg''maj, hg''const, hg''int, hg''bound ⟩ := this
     have hf'g'_const := PiecewiseConstantOn.mul hf'const hg'const
     have hf'g'_maj : MinorizesOn (f' * g') (f * g) I := by
-      intro x hx
-      specialize hf'min x hx
-      specialize hg'min x hx
-      specialize hf'_nonneg x hx
-      specialize hg'_nonneg x hx
-      simp at hf'_nonneg hg'_nonneg ⊢
-      exact mul_le_mul hf'min hg'min (by positivity) (by linarith)
+      peel hf'min with x hx hf'min; specialize hg'min _ hx; specialize hf'_nonneg _ hx; specialize hg'_nonneg _ hx
+      simp at *; exact mul_le_mul hf'min hg'min (by positivity) (by linarith)
     have hf''g''_const := PiecewiseConstantOn.mul hf''const hg''const
     have hf''g''_maj : MajorizesOn (f'' * g'') (f * g) I := by
-      intro x hx
-      specialize hf''maj x hx
-      specialize hg''maj x hx
-      specialize hf''bound x hx
-      specialize hg_nonneg x hx
-      specialize hf_nonneg x hx
-      simp at hf''bound hf_nonneg hg_nonneg ⊢
-      exact mul_le_mul hf''maj hg''maj (by positivity) (by linarith)
+      peel hf''maj with x hx hf''maj; specialize hg''maj _ hx; specialize hf''bound _ hx
+      specialize hg_nonneg _ hx; specialize hf_nonneg _ hx
+      simp at *; exact mul_le_mul hf''maj hg''maj (by positivity) (by linarith)
     have hupper_le := upper_integral_le_integ hmul_bound hf''g''_maj hf''g''_const
     have hlower_ge := integ_le_lower_integral hmul_bound hf'g'_maj hf'g'_const
-    have hh_const := PiecewiseConstantOn.sub hf''g''_const hf'g'_const
-    have hh_integ := PiecewiseConstantOn.integ_sub hf''g''_const hf'g'_const
+    have hh_const := hf''g''_const.sub hf'g'_const
+    have hh_integ := hf''g''_const.integ_sub hf'g'_const
     have hhmin : MinorizesOn (f'' * g'' - f' * g') (M₁ • (g''-g') + M₂ • (f''-f')) I := by
       intro x hx
       simp only [Pi.sub_apply, Pi.mul_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul]
       calc
         _ = (f'' x) * (g'' x - g' x) + (g' x) * (f'' x - f' x) := by ring
         _ ≤ _ := by
-          specialize hg'min x hx
-          specialize hg''maj x hx
-          specialize hf''bound x hx
-          specialize hf'min x hx
-          specialize hf''maj x hx
-          specialize hg''bound x hx
-          gcongr
-          . linarith
-          . linarith
-          simp at hg''bound; linarith
-    have hg''g'_const := PiecewiseConstantOn.sub hg''const hg'const
-    have hg''g'_integ := PiecewiseConstantOn.integ_sub hg''const hg'const
-    have hM₁g''g'_const := PiecewiseConstantOn.smul M₁ hg''g'_const
-    have hM₁g''g_integ := PiecewiseConstantOn.integ_smul M₁ hg''g'_const
-    have hf''f'_const := PiecewiseConstantOn.sub hf''const hf'const
-    have hf''f_integ := PiecewiseConstantOn.integ_sub hf''const hf'const
-    have hM₂f''f'_const := PiecewiseConstantOn.smul M₂ hf''f'_const
-    have hM₂f''f_integ := PiecewiseConstantOn.integ_smul M₂ hf''f'_const
-    have hsum_const := PiecewiseConstantOn.add hM₁g''g'_const hM₂f''f'_const
-    have hsum_integ := PiecewiseConstantOn.integ_add hM₁g''g'_const hM₂f''f'_const
-    have hsum_bound := PiecewiseConstantOn.integ_mono hhmin hh_const hsum_const
+          specialize hg'min x hx; specialize hg''maj x hx; specialize hf''bound x hx
+          specialize hf'min x hx; specialize hf''maj x hx; specialize hg''bound x hx
+          simp at hg''bound; gcongr <;> linarith
+    have hg''g'_const := hg''const.sub hg'const
+    have hg''g'_integ := hg''const.integ_sub hg'const
+    have hM₁g''g'_const := hg''g'_const.smul M₁
+    have hM₁g''g_integ := hg''g'_const.integ_smul M₁
+    have hf''f'_const := hf''const.sub hf'const
+    have hf''f_integ := hf''const.integ_sub hf'const
+    have hM₂f''f'_const := hf''f'_const.smul M₂
+    have hM₂f''f_integ := hf''f'_const.integ_smul M₂
+    have hsum_const := hM₁g''g'_const.add hM₂f''f'_const
+    have hsum_integ := hM₁g''g'_const.integ_add hM₂f''f'_const
+    have hsum_bound := hh_const.integ_mono hhmin hsum_const
     calc
       _ ≤ M₁ * PiecewiseConstantOn.integ (g'' - g') I + M₂ * PiecewiseConstantOn.integ (f'' - f') I := by linarith
       _ ≤ M₁ * (2*ε) + M₂ * (2*ε) := by gcongr <;> linarith
       _ = _ := by ring
-  refine ⟨ hmul_bound, ?_ ⟩
-  replace := nonneg_of_le_const_mul_eps this
-  linarith
+  exact ⟨ hmul_bound, by linarith [nonneg_of_le_const_mul_eps this] ⟩
+
 
 theorem integ_of_mul {I: BoundedInterval} {f g:ℝ → ℝ} (hf: IntegrableOn f I) (hg: IntegrableOn g I) :
   IntegrableOn (f * g) I := by
···
   set fminus := -min f (fun _ ↦ 0)
   set gplus := max g (fun _ ↦ 0)
   set gminus := -min g (fun _ ↦ 0)
-  have hfplus_integ : IntegrableOn fplus I := integ_of_max hf (integ_of_const 0 I).1
-  have hfminus_integ : IntegrableOn fminus I := (integ_of_neg (integ_of_min hf (integ_of_const 0 I).1)).1
-  have hgplus_integ : IntegrableOn gplus I := integ_of_max hg (integ_of_const 0 I).1
-  have hgminus_integ : IntegrableOn gminus I := (integ_of_neg (integ_of_min hg (integ_of_const 0 I).1)).1
-  have hfplus_nonneg : MajorizesOn fplus 0 I := by intro x hx; simp [fplus]
-  have hfminus_nonneg : MajorizesOn fminus 0 I := by intro x hx; simp [fminus]
-  have hgplus_nonneg : MajorizesOn gplus 0 I := by intro x hx; simp [gplus]
-  have hgminus_nonneg : MajorizesOn gminus 0 I := by intro x hx; simp [gminus]
+  have := (integ_of_const 0 I).1
+  have hfplus_integ : IntegrableOn fplus I := integ_of_max hf this
+  have hfminus_integ : IntegrableOn fminus I := (integ_of_neg (integ_of_min hf this)).1
+  have hgplus_integ : IntegrableOn gplus I := integ_of_max hg this
+  have hgminus_integ : IntegrableOn gminus I := (integ_of_neg (integ_of_min hg this)).1
+  have hfplus_nonneg : MajorizesOn fplus 0 I := by intro _ _; simp [fplus]
+  have hfminus_nonneg : MajorizesOn fminus 0 I := by intro _ _; simp [fminus]
+  have hgplus_nonneg : MajorizesOn gplus 0 I := by intro _ _; simp [gplus]
+  have hgminus_nonneg : MajorizesOn gminus 0 I := by intro _ _; simp [gminus]
   have hfplusgplus := integ_of_mul_nonneg hfplus_integ hgplus_integ hfplus_nonneg hgplus_nonneg
   have hfplusgminus := integ_of_mul_nonneg hfplus_integ hgminus_integ hfplus_nonneg hgminus_nonneg
   have hfminusgplus := integ_of_mul_nonneg hfminus_integ hgplus_integ hfminus_nonneg hgplus_nonneg