feat(*): working on list/basic, robusting simp proofs

Author: digama0

algebra/big_operators.lean

@@ -5,15 +5,13 @@ Authors: Johannes Hölzl
 
 Some big operators for lists and finite sets.
 -/
-import data.list data.list.comb data.list.perm data.set.finite data.finset
+import data.list data.list.perm data.set.finite data.finset
   algebra.group algebra.ordered_monoid algebra.group_power
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
 namespace list
--- move to list.sum, needs to match exactly, otherwise transport fails
-definition prod [has_mul α] [has_one α] : list α → α := list.foldl (*) 1
 
 section monoid
 variables [monoid α] {l l₁ l₂ : list α} {a : α}
@@ -31,12 +29,9 @@ calc (l₁ ++ l₂).prod = foldl (*) (foldl (*) 1 l₁ * 1) l₂ : by simp [list
 @[simp] theorem prod_join {l : list (list α)} : l.join.prod = (l.map list.prod).prod :=
 by induction l; simp [list.join, *] at *
 
-@[simp] theorem prod_replicate {n : ℕ} : (list.replicate n a).prod = a ^ n :=
-begin
-  induction n with n ih,
-  { show [].prod = (1:α), refl },
-  { show (a :: list.replicate n a).prod = a ^ (n+1), simp [pow_succ, ih] }
-end
+@[simp] theorem prod_repeat : ∀ (n : ℕ), (list.repeat a n).prod = a ^ n
+| 0 := rfl
+| (n+1) := by simp [pow_succ, prod_repeat n]
 
 end monoid
 
@@ -45,10 +40,10 @@ open list
 variable [comm_monoid α]
 
 lemma prod_eq_of_perm {l₁ l₂ : list α} (h : perm l₁ l₂) : l₁.prod = l₂.prod :=
-by induction h; repeat { simp [*] }
+by induction h; simp *
 
 lemma prod_reverse {l : list α} : l.reverse.prod = l.prod :=
-prod_eq_of_perm $ perm.perm_rev_simp l
+prod_eq_of_perm $ reverse_perm l
 
 end comm_monoid
 
@@ -57,7 +52,7 @@ end list
 namespace finset
 variables {s s₁ s₂ : finset α} {a : α} {f g : α → β}
 
-protected definition prod [comm_monoid β] (s : finset α) (f : α → β) : β := s.fold (*) 1 f
+protected def prod [comm_monoid β] (s : finset α) (f : α → β) : β := s.fold (*) 1 f
 
 variables [decidable_eq α]
 
@@ -106,7 +101,7 @@ s.induction_on (by simp) $
       from assume h₁ y hys hy₂,
       have ha : a ∈ t x ∩ t y, by simp [*],
       have t x ∩ t y = ∅,
-        from hd _ mem_insert _ (mem_insert_of_mem hys) $ assume h, hxs $ h.symm ▸ hys,
+        from hd _ mem_insert_self _ (mem_insert_of_mem hys) $ assume h, hxs $ h.symm ▸ hys,
       by rwa [this] at ha,
   by simp [hxs, prod_union this, ih hd'] {contextual := tt}
 
@@ -250,9 +245,9 @@ section ordered_cancel_comm_monoid
 variables [ordered_cancel_comm_monoid β]
 
 lemma sum_le_sum : (∀x∈s, f x ≤ g x) → s.sum f ≤ s.sum g :=
-s.induction_on (by simp; refl) $ assume a s ha ih h,
+s.induction_on (by simp) $ assume a s ha ih h,
   have f a + s.sum f ≤ g a + s.sum g,
-    from add_le_add (h _ mem_insert) (ih $ assume x hx, h _ $ mem_insert_of_mem hx),
+    from add_le_add (h _ mem_insert_self) (ih $ assume x hx, h _ $ mem_insert_of_mem hx),
   by simp [*]
 
 lemma zero_le_sum (h : ∀x∈s, 0 ≤ f x) : 0 ≤ s.sum f := le_trans (by simp) (sum_le_sum h)
@@ -286,7 +281,7 @@ lemma prod_eq_zero_iff : s.prod f = 0 ↔ (∃a∈s, f a = 0) :=
 s.induction_on (by simp)
 begin
   intros a s,
-  rw [bex_def, bex_def, exists_mem_insert_iff],
+  rw [bex_def, bex_def, exists_mem_insert],
   simp [mul_eq_zero_iff_eq_zero_or_eq_zero] {contextual := tt}
 end
 
@@ -298,7 +293,7 @@ variables [ordered_comm_monoid β] [∀a b : β, decidable (a ≤ b)]
 lemma sum_le_sum' : (∀x∈s, f x ≤ g x) → s.sum f ≤ s.sum g :=
 s.induction_on (by simp; refl) $ assume a s ha ih h,
   have f a + s.sum f ≤ g a + s.sum g,
-    from add_le_add' (h _ mem_insert) (ih $ assume x hx, h _ $ mem_insert_of_mem hx),
+    from add_le_add' (h _ mem_insert_self) (ih $ assume x hx, h _ $ mem_insert_of_mem hx),
   by simp [*]
 
 lemma zero_le_sum' (h : ∀x∈s, 0 ≤ f x) : 0 ≤ s.sum f := le_trans (by simp) (sum_le_sum' h)

algebra/field.lean

@@ -9,6 +9,14 @@ open set
 universe u
 variables {α : Type u}
 
+section division_ring
+variables [division_ring α] {a b : α}
+
+lemma division_ring.neg_inv (h : a ≠ 0) : - a⁻¹ = (- a)⁻¹ :=
+by rwa [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
+
+end division_ring
+
 section
 variables [discrete_field α] {a b c : α}
 
@@ -38,14 +46,14 @@ lemma lt_div_iff (h : 0 < c) : a < b / c ↔ a * c < b :=
 
 lemma ivl_translate : (λx, x + c) '' {r:α | a ≤ r ∧ r ≤ b } = {r:α | a + c ≤ r ∧ r ≤ b + c} :=
 calc (λx, x + c) '' {r | a ≤ r ∧ r ≤ b } = (λx, x - c) ⁻¹' {r | a ≤ r ∧ r ≤ b } :
-    congr_fun (image_eq_preimage_of_inverse _ _
+    congr_fun (image_eq_preimage_of_inverse
       (assume a, add_sub_cancel a c) (assume b, sub_add_cancel b c)) _
   ... = {r | a + c ≤ r ∧ r ≤ b + c} :
     set.ext $ by simp [-sub_eq_add_neg, le_sub_iff_add_le, sub_le_iff_le_add]
 
 lemma ivl_stretch (hc : 0 < c) : (λx, x * c) '' {r | a ≤ r ∧ r ≤ b } = {r | a * c ≤ r ∧ r ≤ b * c} :=
 calc (λx, x * c) '' {r | a ≤ r ∧ r ≤ b } = (λx, x / c) ⁻¹' {r | a ≤ r ∧ r ≤ b } :
-    congr_fun (image_eq_preimage_of_inverse _ _
+    congr_fun (image_eq_preimage_of_inverse
       (assume a, mul_div_cancel _ $ ne_of_gt hc) (assume b, div_mul_cancel _ $ ne_of_gt hc)) _
   ... = {r | a * c ≤ r ∧ r ≤ b * c} :
     set.ext $ by simp [le_div_iff_mul_le_of_pos, div_le_iff_le_mul_of_pos, hc]

algebra/functions.lean

@@ -26,6 +26,15 @@ lemma lt_min_iff : a < min b c ↔ (a < b ∧ a < c) :=
 ⟨assume h, ⟨lt_of_lt_of_le h (min_le_left _ _), lt_of_lt_of_le h (min_le_right _ _)⟩,
   assume ⟨h₁, h₂⟩, lt_min h₁ h₂⟩
 
+lemma lt_max_iff : a < max b c ↔ a < b ∨ a < c :=
+⟨assume h, (le_total c b).imp
+  (assume hcb, lt_of_lt_of_le h $ max_le (le_refl _) hcb)
+  (assume hbc, lt_of_lt_of_le h $ max_le hbc (le_refl _)),
+  (assume h, match h with
+    | or.inl h := lt_of_lt_of_le h (le_max_left _ _)
+    | or.inr h := lt_of_lt_of_le h (le_max_right _ _)
+    end)⟩
+
 end
 
 section decidable_linear_ordered_comm_group

analysis/ennreal.lean

@@ -403,7 +403,7 @@ suffices ∀r, 0 ≤ r → of_real r > b → a ≤ of_real r,
 assume r hr hrb,
 let ⟨p, hp, b_eq, hpr⟩ := lt_iff_exists_of_real.mp hrb in
 have p < r, by simp [hp, hr] at hpr; assumption,
-have pos : 0 < r - p, from lt_sub_iff.mpr $ begin simp [this] end,
+have pos : 0 < r - p, from lt_sub_iff.mpr $ by simp [this],
 calc a ≤ b + of_real (r - p) : h _ pos (by simp [b_eq])
   ... = of_real r :
     by simp [-sub_eq_add_neg, le_of_lt pos, hp, hr, b_eq]; simp [sub_eq_add_neg]
@@ -414,7 +414,7 @@ have ∀r, 0 ≤ r → (∃ (i : ℚ), 0 ≤ i ∧ of_real r < of_real (of_rat i
   from assume r hr,
   let ⟨q, hq⟩ := exists_lt_of_rat r in
   have 0 < of_rat q, from lt_of_le_of_lt hr hq,
-  ⟨q, le_of_lt $ of_rat_lt_of_rat.mp this, of_real_lt_of_real_iff_cases.mpr ⟨this, hq⟩⟩,
+  ⟨q, le_of_lt $ of_rat_lt.mp this, of_real_lt_of_real_iff_cases.mpr ⟨this, hq⟩⟩,
 have h₁ : ∀a, a < ∞ ↔ ∃ (i : ℚ), 0 ≤ i ∧ a < of_real (of_rat i),
   from forall_ennreal.mpr $ by simp [this] {contextual := tt},
 have ∀r p, 0 ≤ r → 0 ≤ p →
@@ -424,7 +424,7 @@ have ∀r p, 0 ≤ r → 0 ≤ p →
       let ⟨q, hrq, hqp⟩ := exists_lt_of_rat_of_rat_gt hrp in
       have 0 < of_rat q, from lt_of_le_of_lt hr hrq,
       have hp' : 0 < p, from lt_of_le_of_lt hr hrp,
-      ⟨q, le_of_lt $ of_rat_lt_of_rat.mp this,
+      ⟨q, le_of_lt $ of_rat_lt.mp this,
         by simp [of_real_lt_of_real_iff_cases, this, hrq, hqp, hp']⟩)
     (assume ⟨q, hq, hrq, hqp⟩, (of_real_lt_of_real_iff hr hp).mp $ lt_trans hrq hqp),
 have h₂ : ∀a r, 0 ≤ r →
@@ -443,7 +443,7 @@ assume x hx, le_infty
 
 lemma of_real_mem_upper_bounds {s : set real} (hs : ∀x∈s, (0:real) ≤ x) (hr : 0 ≤ r) :
   of_real r ∈ upper_bounds (of_real '' s) ↔ r ∈ upper_bounds s :=
-by simp [upper_bounds, ball_image_iff, *] {contextual := tt}
+by simp [upper_bounds, ball_image_iff, -mem_image, *] {contextual := tt}
 
 lemma is_lub_of_real {s : set real} (hs : ∀x∈s, (0:real) ≤ x) (hr : 0 ≤ r) (h : s ≠ ∅) :
   is_lub (of_real '' s) (of_real r) ↔ is_lub s r :=
@@ -801,7 +801,7 @@ s.induction_on (by simp) $ assume a s ha ih,
   have ∀ (i j : ι), ∃ (k : ι), f k a + s.sum (f k) ≤ f i a + s.sum (f j),
     from assume i j,
     let ⟨k, hk⟩ := h (insert a s) i j in
-    ⟨k, add_le_add' (hk a finset.mem_insert).left $ finset.sum_le_sum' $
+    ⟨k, add_le_add' (hk a finset.mem_insert_self).left $ finset.sum_le_sum' $
       assume a ha, (hk _ $ finset.mem_insert_of_mem ha).right⟩,
   by simp [ha, ih.symm, infi_add_infi this]
 
@@ -1000,14 +1000,14 @@ protected lemma tsum_le_tsum (h : ∀a, f a ≤ g a) : (∑a, f a) ≤ (∑a, g
 tsum_le_tsum h ennreal.has_sum ennreal.has_sum
 
 protected lemma tsum_eq_supr_nat {f : ℕ → ennreal} :
-  (∑i:ℕ, f i) = (⨆i:ℕ, (finset.upto i).sum f) :=
+  (∑i:ℕ, f i) = (⨆i:ℕ, (finset.range i).sum f) :=
 calc _ = (⨆s:finset ℕ, s.sum f) : ennreal.tsum_eq_supr_sum
-  ... = (⨆i:ℕ, (finset.upto i).sum f) : le_antisymm
+  ... = (⨆i:ℕ, (finset.range i).sum f) : le_antisymm
     (supr_le_supr2 $ assume s,
-      have ∃n, s ⊆ finset.upto n, from finset.exists_nat_subset_upto,
+      have ∃n, s ⊆ finset.range n, from finset.exists_nat_subset_range,
       let ⟨n, hn⟩ := this in
       ⟨n, finset.sum_le_sum_of_subset hn⟩)
-    (supr_le_supr2 $ assume i, ⟨finset.upto i, le_refl _⟩)
+    (supr_le_supr2 $ assume i, ⟨finset.range i, le_refl _⟩)
 
 protected lemma le_tsum {a : α} : f a ≤ (∑a, f a) :=
 calc f a = ({a} : finset α).sum f : by simp

analysis/limits.lean

@@ -16,7 +16,7 @@ infix ` ^ ` := pow_nat
 section real
 
 lemma has_sum_of_absolute_convergence {f : ℕ → ℝ}
-  (hf : ∃r, tendsto (λn, (upto n).sum (λi, abs (f i))) at_top (nhds r)) : has_sum f :=
+  (hf : ∃r, tendsto (λn, (range n).sum (λi, abs (f i))) at_top (nhds r)) : has_sum f :=
 let f' := λs:finset ℕ, s.sum (λi, abs (f i)) in
 suffices cauchy (map (λs:finset ℕ, s.sum f) at_top),
   from complete_space.complete this,
@@ -25,46 +25,46 @@ assume s hs,
 let ⟨ε, hε, hsε⟩ := mem_uniformity_dist.mp hs, ⟨r, hr⟩ := hf in
 have hε' : {p : ℝ × ℝ | dist p.1 p.2 < ε / 2} ∈ (@uniformity ℝ _).sets,
   from mem_uniformity_dist.mpr ⟨ε / 2, div_pos_of_pos_of_pos hε two_pos, assume a b h, h⟩,
-have cauchy (at_top.map $ λn, f' (upto n)),
+have cauchy (at_top.map $ λn, f' (range n)),
   from cauchy_downwards cauchy_nhds (map_ne_bot at_top_ne_bot) hr,
-have ∃n, ∀{n'}, n ≤ n' → dist (f' (upto n)) (f' (upto n')) < ε / 2,
+have ∃n, ∀{n'}, n ≤ n' → dist (f' (range n)) (f' (range n')) < ε / 2,
   by simp [cauchy_iff, mem_at_top_iff] at this;
   from let ⟨t, ht, u, hu⟩ := this _ hε' in
     ⟨u, assume n' hn, ht $ prod_mk_mem_set_prod_eq.mpr ⟨hu _ (le_refl _), hu _ hn⟩⟩,
 let ⟨n, hn⟩ := this in
-have ∀{s}, upto n ⊆ s → abs ((s \ upto n).sum f) < ε / 2,
+have ∀{s}, range n ⊆ s → abs ((s \ range n).sum f) < ε / 2,
   from assume s hs,
-  let ⟨n', hn'⟩ := @exists_nat_subset_upto s in
-  have upto n ⊆ upto n', from subset.trans hs hn',
-  have f'_nn : 0 ≤ f' (upto n' \ upto n), from zero_le_sum $ assume _ _, abs_nonneg _,
-  calc abs ((s \ upto n).sum f) ≤ f' (s \ upto n) : abs_sum_le_sum_abs
-    ... ≤ f' (upto n' \ upto n) : sum_le_sum_of_subset_of_nonneg
+  let ⟨n', hn'⟩ := @exists_nat_subset_range s in
+  have range n ⊆ range n', from subset.trans hs hn',
+  have f'_nn : 0 ≤ f' (range n' \ range n), from zero_le_sum $ assume _ _, abs_nonneg _,
+  calc abs ((s \ range n).sum f) ≤ f' (s \ range n) : abs_sum_le_sum_abs
+    ... ≤ f' (range n' \ range n) : sum_le_sum_of_subset_of_nonneg
       (finset.sdiff_subset_sdiff hn' (finset.subset.refl _))
       (assume _ _ _, abs_nonneg _)
-    ... = abs (f' (upto n' \ upto n)) : (abs_of_nonneg f'_nn).symm
-    ... = abs (f' (upto n') - f' (upto n)) :
-      by simp [f', (sum_sdiff ‹upto n ⊆ upto n'›).symm]
-    ... = abs (f' (upto n) - f' (upto n')) : abs_sub _ _
-    ... < ε / 2 : hn $ upto_subset_upto_iff.mp this,
-have ∀{s t}, upto n ⊆ s → upto n ⊆ t → dist (s.sum f) (t.sum f) < ε,
+    ... = abs (f' (range n' \ range n)) : (abs_of_nonneg f'_nn).symm
+    ... = abs (f' (range n') - f' (range n)) :
+      by simp [f', (sum_sdiff ‹range n ⊆ range n'›).symm]
+    ... = abs (f' (range n) - f' (range n')) : abs_sub _ _
+    ... < ε / 2 : hn $ range_subset.mp this,
+have ∀{s t}, range n ⊆ s → range n ⊆ t → dist (s.sum f) (t.sum f) < ε,
   from assume s t hs ht,
-  calc abs (s.sum f - t.sum f) = abs ((s \ upto n).sum f + - (t \ upto n).sum f) :
+  calc abs (s.sum f - t.sum f) = abs ((s \ range n).sum f + - (t \ range n).sum f) :
       by rw [←sum_sdiff hs, ←sum_sdiff ht]; simp
-    ... ≤ abs ((s \ upto n).sum f) + abs ((t \ upto n).sum f) :
+    ... ≤ abs ((s \ range n).sum f) + abs ((t \ range n).sum f) :
       le_trans (abs_add_le_abs_add_abs _ _) $ by rw [abs_neg]; exact le_refl _
     ... < ε / 2 + ε / 2 : add_lt_add (this hs) (this ht)
     ... = ε : by rw [←add_div, add_self_div_two],
-⟨(λs:finset ℕ, s.sum f) '' {s | upto n ⊆ s}, image_mem_map $ mem_at_top (upto n),
+⟨(λs:finset ℕ, s.sum f) '' {s | range n ⊆ s}, image_mem_map $ mem_at_top (range n),
   assume ⟨a, b⟩ ⟨⟨t, ht, ha⟩, ⟨s, hs, hb⟩⟩, by simp at ha hb; exact ha ▸ hb ▸ hsε _ _ (this ht hs)⟩
 
 lemma is_sum_iff_tendsto_nat_of_nonneg {f : ℕ → ℝ} {r : ℝ} (hf : ∀n, 0 ≤ f n) :
-  is_sum f r ↔ tendsto (λn, (upto n).sum f) at_top (nhds r) :=
+  is_sum f r ↔ tendsto (λn, (range n).sum f) at_top (nhds r) :=
 ⟨tendsto_sum_nat_of_is_sum,
   assume hr,
-  have tendsto (λn, (upto n).sum (λn, abs (f n))) at_top (nhds r),
+  have tendsto (λn, (range n).sum (λn, abs (f n))) at_top (nhds r),
     by simp [(λi, abs_of_nonneg (hf i)), hr],
   let ⟨p, h⟩ := has_sum_of_absolute_convergence ⟨r, this⟩ in
-  have hp : tendsto (λn, (upto n).sum f) at_top (nhds p), from tendsto_sum_nat_of_is_sum h,
+  have hp : tendsto (λn, (range n).sum f) at_top (nhds p), from tendsto_sum_nat_of_is_sum h,
   have p = r, from tendsto_nhds_unique at_top_ne_bot hp hr,
   this ▸ h⟩
 
@@ -138,13 +138,13 @@ by_cases
     tendsto_cong this $ univ_mem_sets' $ assume a, by simp [*, pow_inv])
 
 lemma sum_geometric' {r : ℝ} (h : r ≠ 0) :
-  ∀{n}, (upto n).sum (λi, (r + 1) ^ i) = ((r + 1) ^ n - 1) / r
+  ∀{n}, (finset.range n).sum (λi, (r + 1) ^ i) = ((r + 1) ^ n - 1) / r
 | 0     := by simp [zero_div]
 | (n+1) := by simp [@sum_geometric' n, h, pow_succ, add_div_eq_mul_add_div, add_mul]
 
 lemma sum_geometric {r : ℝ} {n : ℕ} (h : r ≠ 1) :
-  (upto n).sum (λi, r ^ i) = (r ^ n - 1) / (r - 1) :=
-calc (upto n).sum (λi, r ^ i) = (upto n).sum (λi, ((r - 1) + 1) ^ i) :
+  (range n).sum (λi, r ^ i) = (r ^ n - 1) / (r - 1) :=
+calc (range n).sum (λi, r ^ i) = (range n).sum (λi, ((r - 1) + 1) ^ i) :
     by simp
   ... = (((r - 1) + 1) ^ n - 1) / (r - 1) :
     sum_geometric' $ by simp [sub_eq_iff_eq_add, -sub_eq_add_neg, h]

analysis/measure_theory/borel_space.lean

@@ -57,7 +57,7 @@ le_antisymm
               have u ∈ (nhds a).sets, from mem_nhds_sets (ht' _ hu) hau,
               let ⟨u', hu', hau', hu'u⟩ := mem_nhds_of_is_topological_basis hb₃ this in
               have u' ∈ b', from ⟨hu', subset.trans hu'u (subset_sUnion_of_mem hu), u, hu, hu'u⟩,
-              by simp; exact ⟨⟨u', this⟩, (hv u' this).right hau'⟩)
+              by simp; exact ⟨u', this, (hv u' this).right hau'⟩)
             (Union_subset $ assume ⟨u', hu'⟩, subset_sUnion_of_mem $ (hv u' hu').left),
         have h_encode : encodable {u // u ∈ b'},
           from (countable.to_encodable $ countable_subset (by simp [subset_def] {contextual := tt}) hb₁),
@@ -181,13 +181,13 @@ is_topological_basis_of_open_of_nhds
         from ne_empty_iff_exists_mem.mp $ by simp [t₁₂.symm, h],
       let ⟨c, hc₁, hc₂⟩ := this in
       have of_rat (max a₁ a₂) < of_rat (min b₁ b₂), from lt_trans hc₁ hc₂,
-      of_rat_lt_of_rat.mp this,
+      of_rat_lt.mp this,
     by simp [t₁₂]; exact ⟨max a₁ a₂, min b₁ b₂, this, rfl⟩)
   (suffices ∀r, ∃(t : set ℝ), r ∈ t ∧ ∃a b, t = Ioo (of_rat a) (of_rat b) ∧ a < b,
       by simpa,
     assume r,
     let ⟨a, ha⟩ := exists_gt_of_rat r, ⟨b, hb⟩ := exists_lt_of_rat r in
-    ⟨Ioo (of_rat a) (of_rat b), ⟨ha, hb⟩, a, b, rfl, of_rat_lt_of_rat.mp $ lt_trans ha hb⟩)
+    ⟨Ioo (of_rat a) (of_rat b), ⟨ha, hb⟩, a, b, rfl, of_rat_lt.mp $ lt_trans ha hb⟩)
   begin simp [is_open_Ioo] {contextual:=tt} end
   (assume a v hav hv,
     let
@@ -196,7 +196,7 @@ is_topological_basis_of_open_of_nhds
       ⟨p, hap, hpu⟩ := exists_lt_of_rat_of_rat_gt hu
     in
     ⟨Ioo (of_rat q) (of_rat p),
-      begin simp; exact ⟨q, p, of_rat_lt_of_rat.mp $ lt_trans hqa hap, rfl⟩ end,
+      begin simp; exact ⟨q, p, of_rat_lt.mp $ lt_trans hqa hap, rfl⟩ end,
       ⟨hqa, hap⟩, assume a' ⟨hqa', ha'p⟩, h _ (lt_trans hlq hqa') (lt_trans ha'p hpu)⟩)
 
 instance : second_countable_topology ℝ :=
@@ -222,11 +222,11 @@ have ∀a b, a < b → g.is_measurable (Ioo (of_rat a) (of_rat b)),
   have (⋃c>a, - Iio (of_rat c)) ∩ Iio (of_rat b) = Ioo (of_rat a) (of_rat b),
     from set.ext $ assume x,
     have h₁ : x < of_rat b → ∀p, of_rat p ≤ x → p > a → of_rat a < x,
-      from assume hxb p hpx hpa, lt_of_lt_of_le (of_rat_lt_of_rat.mpr hpa) hpx,
+      from assume hxb p hpx hpa, lt_of_lt_of_le (of_rat_lt.mpr hpa) hpx,
     have h₂ : x < of_rat b → of_rat a < x → (∃ (i : ℚ), of_rat i ≤ x ∧ i > a),
       from assume hxb hax,
       let ⟨c, hac, hcx⟩ := exists_lt_of_rat_of_rat_gt hax in
-      ⟨c, le_of_lt hcx, of_rat_lt_of_rat.mp hac⟩,
+      ⟨c, le_of_lt hcx, of_rat_lt.mp hac⟩,
     by simp [iff_def, Iio, Ioo] {contextual := tt}; exact ⟨h₁, h₂⟩,
   this ▸ @is_measurable_inter _ g _ _
     (@is_measurable_bUnion _ _ g _ _ countable_encodable $ assume b hb, hgc b)