refactor(logic/basic): refactor logic theorems

algebra/big_operators.lean

@@ -11,8 +11,6 @@ import algebra.group data.list data.list.comb algebra.group_power data.set.finit
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-@[simp] lemma exists_false {α : Sort u} : ¬ (∃a:α, false) := assume ⟨a, h⟩, h
-
 namespace list
 -- move to list.sum, needs to match exactly, otherwise transport fails
 definition prod [has_mul α] [has_one α] : list α → α := list.foldl (*) 1
@@ -277,7 +275,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 [bexists_def, bexists_def, exists_mem_insert_iff],
+  rw [bex_def, bex_def, exists_mem_insert_iff],
   simp [mul_eq_zero_iff_eq_zero_or_eq_zero] {contextual := tt}
 end
 

data/finset/basic.lean

@@ -11,13 +11,6 @@ open list subtype nat
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-@[simp] lemma or_self_or (a b : Prop) : a ∨ a ∨ b ↔ a ∨ b :=
-calc a ∨ a ∨ b ↔ (a ∨ a) ∨ b : or.assoc.symm
-  ... ↔ _ : by rw [or_self]
-
-theorem perm_insert_cons_of_not_mem [decidable_eq α] {a : α} {l : list α} (h : a ∉ l) : perm (list.insert a l) (a :: l) :=
-have list.insert a l = a :: l, from if_neg h, by rw this
-
 def nodup_list (α : Type u) := {l : list α // nodup l}
 
 def to_nodup_list_of_nodup {l : list α} (n : nodup l) : nodup_list α :=
@@ -138,8 +131,8 @@ quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ h₁ h₂, h₁ h₂)
 theorem subset.antisymm {s₁ s₂ : finset α} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ :=
 ext (λ x, iff.intro (λ H, mem_of_subset_of_mem H₁ H) (λ H, mem_of_subset_of_mem H₂ H))
 
-theorem subset_of_forall {s₁ s₂ : finset α} : (∀x, x ∈ s₁ → x ∈ s₂) → s₁ ⊆ s₂ :=
-quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ H, H)
+theorem subset_iff {s₁ s₂ : finset α} : s₁ ⊆ s₂ ↔ (∀x, x ∈ s₁ → x ∈ s₂) :=
+⟨λ s a, mem_of_subset_of_mem s, quotient.induction_on₂ s₁ s₂ (λ l₁ l₂ H, H)⟩
 
 end subset
 
@@ -200,7 +193,7 @@ finset.induction_on_to_finset s $ assume l hl, show a ∈ insert b l ↔ (a = b
 theorem mem_insert : a ∈ insert a s := by simp
 theorem mem_insert_of_mem : a ∈ s → a ∈ insert b s := by simp {contextual := tt}
 theorem mem_of_mem_insert_of_ne (h : b ∈ insert a s) : b ≠ a → b ∈ s :=
-or_resolve_right (mem_insert_iff.mp h)
+(mem_insert_iff.1 h).resolve_left
 
 @[simp] theorem insert_eq_of_mem (h : a ∈ s) : insert a s = s :=
 ext (λ x, by rw mem_insert_iff; apply or_iff_right_of_imp; intro eq; rw eq; assumption)
@@ -215,13 +208,13 @@ ext $ by simp [mem_insert_iff]
 assume h, @not_mem_empty α a $ h ▸ by simp
 
 theorem subset_insert [h : decidable_eq α] : s ⊆ insert a s :=
-subset_of_forall (λ x h, mem_insert_of_mem h)
+subset_iff.2 (λ x h, mem_insert_of_mem h)
 
 theorem insert_subset_insert (h : s ⊆ t) : insert a s ⊆ insert a t :=
-subset_of_forall $ assume x, by simp; exact or.imp_right (mem_of_subset_of_mem h)
+subset_iff.2 $ assume x, by simp [-forall_or_distrib_left]; exact or.imp_right (subset_iff.1 h _)
 
 @[recursor 6] protected theorem induction {p : finset α → Prop}
-  (h₁ : p ∅) (h₂ : ∀⦃a : α⦄, ∀{s : finset α}, a ∉ s → p s → p (insert a s)) (s) : p s :=
+  (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α}, a ∉ s → p s → p (insert a s)) (s) : p s :=
 finset.induction_on_to_finset s $ λl, list.rec_on l
   (assume _, h₁)
   (assume a l ih hal,
@@ -231,7 +224,7 @@ finset.induction_on_to_finset s $ λl, list.rec_on l
     this ▸ @h₂ a l' (not_mem_of_nodup_cons hal) (ih _))
 
 protected theorem induction_on {p : finset α → Prop} (s : finset α)
-  (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄, ∀ {s : finset α}, a ∉ s → p s → p (insert a s)) : p s :=
+  (h₁ : p ∅) (h₂ : ∀ ⦃a : α⦄ {s : finset α}, a ∉ s → p s → p (insert a s)) : p s :=
 finset.induction h₁ h₂ s
 
 -- useful in proofs by induction
@@ -244,25 +237,19 @@ end insert
 section singleton
 variables [decidable_eq α] {a b : α} {s : finset α}
 
-@[simp] theorem mem_singleton_iff : b ∈ ({a} : finset α) ↔ (b = a) :=
+@[simp] theorem mem_singleton : b ∈ ({a} : finset α) ↔ (b = a) :=
 show b ∈ insert a ∅ ↔ b = a, by simp
 
-theorem mem_singleton : a ∈ ({a} : finset α) := mem_insert
-
-theorem mem_singleton_of_eq (h : b = a) : b ∈ ({a} : finset α) :=
-by rw h; apply mem_insert
-
-theorem eq_of_mem_singleton (h : b ∈ ({a}:finset α)) : b = a :=
-iff.mp mem_singleton_iff h
+theorem mem_singleton_self : a ∈ ({a} : finset α) := mem_insert
 
-theorem eq_of_singleton_eq (h : {a} = ({b}:finset α)) : a = b :=
-have a ∈ ({b} : finset α), by rw ←h; apply mem_singleton,
-eq_of_mem_singleton this
+theorem singleton_inj (h : {a} = ({b}:finset α)) : a = b :=
+have a ∈ ({b} : finset α), by rw ← h; apply mem_singleton_self,
+mem_singleton.1 this
 
 @[simp] theorem singleton_ne_empty : ({a} : finset α) ≠ ∅ := insert_ne_empty
 
 @[simp] theorem insert_singelton_self_eq  : ({a, a} : finset α) = {a} :=
-show insert a {a} = ({a} : finset α), by rw [insert_eq_of_mem]; apply mem_singleton
+show insert a {a} = ({a} : finset α), by rw [insert_eq_of_mem]; apply mem_singleton_self
 
 end singleton
 
@@ -444,10 +431,10 @@ theorem insert_erase (h : a ∈ s) : insert a (erase a s) = s :=
 ext $ assume x, by simp; constructor; finish
 
 theorem erase_subset_erase (h : s ⊆ t) : erase a s ⊆ erase a t :=
-subset_of_forall $ assume x, by simp; exact and_implies_right (mem_of_subset_of_mem h)
+subset_iff.2 $ assume x, by simp [-and_imp]; exact and.imp_right (mem_of_subset_of_mem h)
 
 theorem erase_subset : erase a s ⊆ s :=
-subset_of_forall $ assume x, by simp {contextual:=tt}
+subset_iff.2 $ assume x, by simp {contextual:=tt}
 
 theorem erase_eq_of_not_mem (h : a ∉ s) : erase a s = s :=
 ext $ assume b, by by_cases b = a; simp [*]

data/finset/fold.lean

@@ -13,7 +13,7 @@ variables {α : Type u} {β : Type v} {γ : Type w}
 
 namespace list
 
-@[congr] lemma map_congr {f g : α → β} : ∀{l : list α}, (∀x∈l, f x = g x) → map f l = map g l
+@[congr] lemma map_congr {f g : α → β} : ∀ {l : list α}, (∀ x ∈ l, f x = g x) → map f l = map g l
 | [] _     := rfl
 | (a::l) h :=
   have f a = g a, from h _ (mem_cons_self _ _),
@@ -80,10 +80,10 @@ calc ({a}:finset α).fold op b f = f a * (∅:finset α).fold op b f : fold_inse
   ... = f a * b : by rw [fold_empty]
 
 @[simp] lemma fold_image [decidable_eq γ] {g : γ → α} {s : finset γ} :
-  (∀x∈s, ∀y∈s, g x = g y → x = y) → (s.image g).fold op b f = s.fold op b (f ∘ g) :=
+  (∀ (x ∈ s) (y ∈ s), g x = g y → x = y) → (s.image g).fold op b f = s.fold op b (f ∘ g) :=
 finset.induction_on_to_finset s $ assume l hl hg, by rw [image_to_finset_of_nodup hl hg]; simp
 
-@[congr] lemma fold_congr {g : α → β} : (∀x∈s, f x = g x) → s.fold op b f = s.fold op b g :=
+@[congr] lemma fold_congr {g : α → β} : (∀ x ∈ s, f x = g x) → s.fold op b f = s.fold op b g :=
 finset.induction_on_to_finset s $ assume l hl (hg : ∀x∈l, f x = g x),
   by simp [-foldl_map]; rw [list.map_congr hg]
 

data/list/basic.lean

@@ -212,7 +212,7 @@ assume ainbl binl, or.elim (eq_or_mem_of_mem_cons ainbl)
   (assume : a ∈ l, this)
 
 theorem not_mem_append {a : α} {s t : list α} (h₁ : a ∉ s) (h₂ : a ∉ t) : a ∉ s++t :=
-mt mem_append.1 $ not_or_of_not_and_not ⟨h₁, h₂⟩
+mt mem_append.1 $ not_or_distrib.2 ⟨h₁, h₂⟩
 
 theorem length_pos_of_mem {a : α} : ∀ {l : list α}, a ∈ l → 0 < length l
 | (b::l) _ := zero_lt_succ _
@@ -301,7 +301,7 @@ theorem subset_app_of_subset_right (l l₁ l₂ : list α) : l ⊆ l₂ → l 
 
 theorem cons_subset_of_subset_of_mem {a : α} {l m : list α} (ainm : a ∈ m) (lsubm : l ⊆ m) :
   a::l ⊆ m :=
-λ b, or_imp_iff_and_imp.2 ⟨λ e, e.symm ▸ ainm, @lsubm _⟩
+λ b, or_imp_distrib.2 ⟨λ e, e.symm ▸ ainm, @lsubm _⟩
 
 theorem app_subset_of_subset_of_subset {l₁ l₂ l : list α} (l₁subl : l₁ ⊆ l) (l₂subl : l₂ ⊆ l) :
   l₁ ++ l₂ ⊆ l :=
@@ -398,7 +398,7 @@ assume n, if_neg n
 
 theorem index_of_eq_length {a : α} {l : list α} : index_of a l = length l ↔ a ∉ l :=
 begin
-  induction l with b l ih; simp [not_or_iff, -add_comm],
+  induction l with b l ih; simp [-add_comm],
   by_cases a = b with h; simp [h, -add_comm],
   { intro, contradiction },
   { rw ← ih, exact ⟨succ_inj, congr_arg _⟩ }

data/list/comb.lean

@@ -169,7 +169,7 @@ theorem exists_of_any_eq_tt {p : α → bool} : ∀ {l : list α}, any l p = tt
 | []     h := begin simp at h, contradiction end
 | (b::l) h := begin
                 simp [bool.bor_eq_tt] at h, cases h with h h,
-                { existsi b, simp [h]},
+                { existsi b, simp [h] },
                 cases (exists_of_any_eq_tt h) with a ha,
                 existsi a, apply (and.intro (or.inr ha.left) ha.right)
               end
@@ -203,22 +203,22 @@ iff.intro
   (λ h, forall_mem_cons h.left h.right)
 
 theorem not_exists_mem_nil (p : α → Prop) : ¬ ∃ x ∈ @nil α, p x :=
-assume h, bexists.elim h (λ a anil, absurd anil (not_mem_nil a))
+assume h, bex.elim h (λ a anil, absurd anil (not_mem_nil a))
 
 theorem exists_mem_cons_of {p : α → Prop} {a : α} (l : list α) (h : p a) :
   ∃ x ∈ a :: l, p x :=
-bexists.intro a (by simp) h
+bex.intro a (by simp) h
 
 theorem exists_mem_cons_of_exists {p : α → Prop} {a : α} {l : list α} (h : ∃ x ∈ l, p x) :
   ∃ x ∈ a :: l, p x :=
-bexists.elim h (λ x xl px, bexists.intro x (by simp [xl]) px)
+bex.elim h (λ x xl px, bex.intro x (by simp [xl]) px)
 
 theorem or_exists_of_exists_mem_cons {p : α → Prop} {a : α} {l : list α} (h : ∃ x ∈ a :: l, p x) :
   p a ∨ ∃ x ∈ l, p x :=
-bexists.elim h (λ x xal px,
+bex.elim h (λ x xal px,
   or.elim (eq_or_mem_of_mem_cons xal)
     (assume : x = a, begin rw ←this, simp [px] end)
-    (assume : x ∈ l, or.inr (bexists.intro x this px)))
+    (assume : x ∈ l, or.inr (bex.intro x this px)))
 
 @[simp] theorem exists_mem_cons_iff (p : α → Prop) (a : α) (l : list α) :
   (∃ x ∈ a :: l, p x) ↔ p a ∨ ∃ x ∈ l, p x :=

data/list/perm.lean

@@ -499,7 +499,7 @@ assume p, perm_induction_on p
               exact skip y r
             end)
           (λ xney : x ≠ y,
-            have x ∈ t₁, from or_resolve_right xinyt₁ xney,
+            have x ∈ t₁, from xinyt₁.resolve_left xney,
             have x ∈ t₂, from mem_erase_dup.1 (mem_of_perm r (mem_erase_dup.2 this)),
             have y ∉ x::t₂, from
               assume : y ∈ x::t₂, or.elim (eq_or_mem_of_mem_cons this)

data/list/set.lean

@@ -76,7 +76,7 @@ by simp [list.erase, h]
 | (x::y::xs) h := if h' : x = a then
                     by simp [h', one_add]
                   else
-                    have ainyxs : a ∈ y::xs, from or_resolve_right h $ by cc,
+                    have ainyxs : a ∈ y::xs, from h.resolve_left $ by cc,
                     by simp [h', length_erase_of_mem ainyxs, one_add]
 
 @[simp] theorem erase_of_not_mem {a : α} : ∀{l : list α}, a ∉ l → l.erase a = l
@@ -266,7 +266,7 @@ mem_union_iff.2 (or.inr h)
 
 theorem forall_mem_union {p : α → Prop} {l₁ l₂ : list α} (h₁ : ∀ x ∈ l₁, p x) (h₂ : ∀ x ∈ l₂, p x) :
   ∀ x ∈ l₁ ∪ l₂, p x :=
-by simp [or_imp_iff_and_imp, forall_and_distrib]; exact ⟨h₁, h₂⟩
+by simp [or_imp_distrib, forall_and_distrib]; exact ⟨h₁, h₂⟩
 
 theorem forall_mem_of_forall_mem_union_left {p : α → Prop} {l₁ l₂ : list α}
    (h : ∀ x ∈ l₁ ∪ l₂, p x) :

data/seq/seq.lean

@@ -50,8 +50,7 @@ theorem mem_cons_of_mem (y : α) {a : α} : ∀ {s : seq α}, a ∈ s → a ∈
 | ⟨f, al⟩ := stream.mem_cons_of_mem (some y)
 
 theorem eq_or_mem_of_mem_cons {a b : α} : ∀ {s : seq α}, a ∈ cons b s → a = b ∨ a ∈ s
-| ⟨f, al⟩ h := or_of_or_of_implies_left
-  (stream.eq_or_mem_of_mem_cons h) (λh, by injection h)
+| ⟨f, al⟩ h := (stream.eq_or_mem_of_mem_cons h).imp_left (λh, by injection h)
 
 @[simp] theorem mem_cons_iff {a b : α} {s : seq α} : a ∈ cons b s ↔ a = b ∨ a ∈ s :=
 ⟨eq_or_mem_of_mem_cons, λo, by cases o with e m;
@@ -562,10 +561,7 @@ def bind (s : seq1 α) (f : α → seq1 β) : seq1 β :=
 join (map f s)
 
 @[simp] theorem join_map_ret (s : seq α) : seq.join (seq.map ret s) = s :=
-begin
-  apply coinduction2 s, intro s, apply cases_on s; simp [ret],
-  { intros x s, exact ⟨_, rfl, rfl⟩ }
-end
+by apply coinduction2 s; intro s; apply cases_on s; simp [ret]
 
 @[simp] theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s
 | ⟨a, s⟩ := begin

data/set/basic.lean

@@ -62,9 +62,9 @@ theorem ssubset_def {s t : set α} : (s ⊂ t) = (s ⊆ t ∧ s ≠ t) := rfl
 theorem not_mem_empty (x : α) : ¬ (x ∈ (∅ : set α)) :=
 assume h : x ∈ ∅, h
 
-@[simp] lemma not_not_mem_iff {α : Type u} {a : α} {s : set α} [decidable (a ∈ s)] :
+@[simp] lemma not_not_mem {α : Type u} {a : α} {s : set α} [decidable (a ∈ s)] :
   ¬ (a ∉ s) ↔ a ∈ s :=
-not_not_iff
+not_not
 
 
 /- empty set -/
@@ -100,7 +100,7 @@ ne_empty_iff_exists_mem
 theorem subset_empty_iff (s : set α) : s ⊆ ∅ ↔ s = ∅ :=
 by finish [set_eq_def]
 
-theorem bounded_forall_empty_iff {p : α → Prop} :
+theorem ball_empty_iff {p : α → Prop} :
   (∀ x ∈ (∅ : set α), p x) ↔ true :=
 by finish [iff_def]
 
@@ -139,7 +139,7 @@ theorem mem_union.elim {x : α} {a b : set α} {P : Prop}
     (H₁ : x ∈ a ∪ b) (H₂ : x ∈ a → P) (H₃ : x ∈ b → P) : P :=
 or.elim H₁ H₂ H₃
 
-theorem mem_union_iff (x : α) (a b : set α) : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b := iff.rfl
+theorem mem_union (x : α) (a b : set α) : x ∈ a ∪ b ↔ x ∈ a ∨ x ∈ b := iff.rfl
 
 @[simp] theorem mem_union_eq (x : α) (a b : set α) : x ∈ a ∪ b = (x ∈ a ∨ x ∈ b) := rfl
 
@@ -271,16 +271,16 @@ by finish [set_eq_def, iff_def]
 /- distributivity laws -/
 
 theorem inter_distrib_left (s t u : set α) : s ∩ (t ∪ u) = (s ∩ t) ∪ (s ∩ u) :=
-ext (assume x, and_distrib _ _ _)
+ext (assume x, and_or_distrib_left)
 
 theorem inter_distrib_right (s t u : set α) : (s ∪ t) ∩ u = (s ∩ u) ∪ (t ∩ u) :=
-ext (assume x, and_distrib_right _ _ _)
+ext (assume x, or_and_distrib_right)
 
 theorem union_distrib_left (s t u : set α) : s ∪ (t ∩ u) = (s ∪ t) ∩ (s ∪ u) :=
-ext (assume x, or_distrib _ _ _)
+ext (assume x, or_and_distrib_left)
 
 theorem union_distrib_right (s t u : set α) : (s ∩ t) ∪ u = (s ∪ u) ∩ (t ∪ u) :=
-ext (assume x, or_distrib_right _ _ _)
+ext (assume x, and_or_distrib_right)
 
 /- insert -/
 
@@ -325,7 +325,7 @@ theorem forall_insert_of_forall {P : α → Prop} {a : α} {s : set α} (h : ∀
   ∀ x, x ∈ insert a s → P x :=
 by finish
 
-theorem bounded_forall_insert_iff {P : α → Prop} {a : α} {s : set α} :
+theorem ball_insert_iff {P : α → Prop} {a : α} {s : set α} :
   (∀ x ∈ insert a s, P x) ↔ P a ∧ (∀x ∈ s, P x) :=
 by finish [iff_def]
 
@@ -529,7 +529,7 @@ by safe [set_eq_def, iff_def, mem_image_eq, eq_on]
 theorem image_comp (f : β → γ) (g : α → β) (a : set α) : (f ∘ g) '' a = f '' (g '' a) :=
 begin
   safe [set_eq_def, iff_def, mem_image_eq, (∘)],
-  have h' :=  h_1 (g a_1),
+  have h' := h_2 (g a_2),
   finish
 end
 
@@ -552,11 +552,7 @@ subset.antisymm
   (subset_inter (mono_image $ inter_subset_left _ _) (mono_image $ inter_subset_right _ _))
 
 @[simp] lemma image_singleton {f : α → β} {a : α} : f '' {a} = {f a} :=
-begin
-  apply set.ext, intro x,
-  simp [image],
-  exact ⟨assume ⟨a', ha', hx⟩, hx ▸ ha' ▸ rfl, assume h, ⟨a, rfl, h.symm⟩⟩
-end
+set.ext $ λ x, by simp [image]; rw eq_comm
 
 theorem fix_set_compl (t : set α) : compl t = - t := rfl
 
@@ -565,7 +561,7 @@ theorem mem_image_compl (t : set α) (S : set (set α)) :
   t ∈ compl '' S ↔ -t ∈ S :=
 begin
   safe [mem_image_eq, iff_def, fix_set_compl],
-  have h' := h_1 (- t), clear h_1,
+  tactic.swap, have h' := h_1 (- t),
   all_goals { simp [compl_compl] at *; contradiction }
 end
 
@@ -582,11 +578,11 @@ set.ext $ assume x, ⟨assume ⟨y, (hy : p y), (h_eq : -y = x)⟩,
   show p (- x), by rw [←h_eq, compl_compl]; assumption,
   assume h : p (-x), ⟨_, h, compl_compl _⟩⟩
 
-theorem bounded_forall_image_of_bounded_forall {f : α → β} {s : set α} {p : β → Prop}
+theorem ball_image_of_ball {f : α → β} {s : set α} {p : β → Prop}
   (h : ∀ x ∈ s, p (f x)) : ∀ y ∈ f '' s, p y :=
 by finish [mem_image_eq]
 
-theorem bounded_forall_image_iff {f : α → β} {s : set α} {p : β → Prop} :
+theorem ball_image_iff {f : α → β} {s : set α} {p : β → Prop} :
   (∀ y ∈ f '' s, p y) ↔ (∀ x ∈ s, p (f x)) :=
 begin
   safe [mem_image_eq, iff_def],
@@ -681,7 +677,7 @@ eq_univ_of_univ_subset $ assume x _, h x
 lemma range_compose {g : α → β} : range (g ∘ f) = g '' range f :=
 subset.antisymm
   (forall_range_iff.mpr $ assume i, mem_image_of_mem g mem_range)
-  (bounded_forall_image_iff.mpr $ forall_range_iff.mpr $ assume i, mem_range)
+  (ball_image_iff.mpr $ forall_range_iff.mpr $ assume i, mem_range)
 end range
 
 def pairwise_on (s : set α) (r : α → α → Prop) := ∀x ∈ s, ∀y ∈ s, x ≠ y → r x y

data/set/lattice.lean

@@ -104,11 +104,11 @@ theorem subset_Inter {t : set β} {s : α → set β} (h : ∀ i, t ⊆ s i) : t
 
 @[simp] -- complete_boolean_algebra
 theorem compl_Union (s : α → set β) : - (⋃ i, s i) = (⋂ i, - s i) :=
-ext (λ x, begin simp, apply not_exists_iff end)
+ext (λ x, by simp)
 
 -- classical -- complete_boolean_algebra
 theorem compl_Inter (s : α → set β) : -(⋂ i, s i) = (⋃ i, - s i) :=
-ext (λ x, begin simp, apply classical.not_forall_iff end)
+ext (λ x, by simp [classical.not_forall])
 
 -- classical -- complete_boolean_algebra
 theorem Union_eq_comp_Inter_comp (s : α → set β) : (⋃ i, s i) = - (⋂ i, - s i) :=
@@ -333,7 +333,7 @@ instance : complete_boolean_algebra (set α) :=
       or.imp_right
         (assume hn : x ∉ s, assume i hi, or.resolve_left (h i hi) hn)
         (classical.em $ x ∈ s),
-  inf_Sup_le_supr_inf := assume s t x, show x ∈ s ∩ (⋃₀ t) → x ∈ (⋃ b ∈ t, s ∩ b), by simp; exact id }
+  inf_Sup_le_supr_inf := assume s t x, show x ∈ s ∩ (⋃₀ t) → x ∈ (⋃ b ∈ t, s ∩ b), by simp [-and_imp] }
 
 theorem union_sdiff_same {a b : set α} : a ∪ (b \ a) = a ∪ b :=
 lattice.sup_sub_same