fix(*): fix wrt changes in lean

algebra/lattice/bounded_lattice.lean

@@ -58,7 +58,7 @@ instance bounded_lattice_Prop : bounded_lattice Prop :=
   bot_le       := @false.elim }
 
 section logic
-variable [pre_order α]
+variable [preorder α]
 
 theorem monotone_and {p q : α → Prop} (m_p : monotone p) (m_q : monotone q) :
   monotone (λx, p x ∧ q x) :=

algebra/lattice/complete_lattice.lean

@@ -55,12 +55,12 @@ Sup_le (assume a, assume ha : a ∈ s, le_Sup $ h ha)
 theorem Inf_le_Inf (h : s ⊆ t) : Inf t ≤ Inf s :=
 le_Inf (assume a, assume ha : a ∈ s, Inf_le $ h ha)
 
-@[simp] theorem le_Sup_iff : Sup s ≤ a ↔ (∀b ∈ s, b ≤ a) :=
+@[simp] theorem Sup_le_iff : Sup s ≤ a ↔ (∀b ∈ s, b ≤ a) :=
 ⟨assume : Sup s ≤ a, assume b, assume : b ∈ s,
   le_trans (le_Sup ‹b ∈ s›) ‹Sup s ≤ a›,
   Sup_le⟩
 
-@[simp] theorem Inf_le_iff : a ≤ Inf s ↔ (∀b ∈ s, a ≤ b) :=
+@[simp] theorem le_Inf_iff : a ≤ Inf s ↔ (∀b ∈ s, a ≤ b) :=
 ⟨assume : a ≤ Inf s, assume b, assume : b ∈ s,
   le_trans ‹a ≤ Inf s› (Inf_le ‹b ∈ s›),
   le_Inf⟩
@@ -72,7 +72,9 @@ by have := le_Sup h; finish
 
 -- TODO: it is weird that we have to add union_def
 theorem Sup_union {s t : set α} : Sup (s ∪ t) = Sup s ⊔ Sup t :=
-le_antisymm (by finish) (by finish [union_def])
+le_antisymm 
+  (by finish) 
+  (sup_le (Sup_le_Sup $ subset_union_left _ _) (Sup_le_Sup $ subset_union_right _ _))
 
 /- old proof:
 le_antisymm
@@ -87,7 +89,9 @@ by finish
 -/
 
 theorem Inf_union {s t : set α} : Inf (s ∪ t) = Inf s ⊓ Inf t :=
-le_antisymm (by finish [union_def]) (by finish)
+le_antisymm 
+  (le_inf (Inf_le_Inf $ subset_union_left _ _) (Inf_le_Inf $ subset_union_right _ _))
+  (by finish)
 
 /- old proof:
 le_antisymm
@@ -116,25 +120,19 @@ le_antisymm (by finish) (le_Sup ⟨⟩) -- finish fails because ⊤ ≤ a simpli
 @[simp] theorem Inf_univ : Inf univ = (⊥ : α) :=
 le_antisymm (Inf_le ⟨⟩) bot_le
 
+-- TODO(Jeremy): get this automatically
 @[simp] theorem Sup_insert {a : α} {s : set α} : Sup (insert a s) = a ⊔ Sup s :=
-le_antisymm (by finish) (by finish [insert_def])
-
-/- old proof
 have Sup {b | b = a} = a,
   from le_antisymm (Sup_le $ assume b b_eq, b_eq ▸ le_refl _) (le_Sup rfl),
 calc Sup (insert a s) = Sup {b | b = a} ⊔ Sup s : Sup_union
                   ... = a ⊔ Sup s : by rw [this]
--/
 
 @[simp] theorem Inf_insert {a : α} {s : set α} : Inf (insert a s) = a ⊓ Inf s :=
-le_antisymm (by finish [insert_def]) (by finish)
-
-/- old proof
 have Inf {b | b = a} = a,
   from le_antisymm (Inf_le rfl) (le_Inf $ assume b b_eq, b_eq ▸ le_refl _),
 calc Inf (insert a s) = Inf {b | b = a} ⊓ Inf s : Inf_union
                   ... = a ⊓ Inf s : by rw [this]
--/
+
 
 @[simp] theorem Sup_singleton {a : α} : Sup {a} = a :=
 by finish [singleton_def]
@@ -532,7 +530,7 @@ instance complete_lattice_fun {α : Type u} {β : Type v} [complete_lattice β]
   le_Inf := assume s f h a, le_Inf $ assume b ⟨f', h', b_eq⟩, b_eq ▸ h _ h' a }
 
 section complete_lattice
-variables [pre_order α] [complete_lattice β]
+variables [preorder α] [complete_lattice β]
 
 theorem monotone_Sup_of_monotone {s : set (α → β)} (m_s : ∀f∈s, monotone f) : monotone (Sup s) :=
 assume x y h, Sup_le $ assume x' ⟨f, f_in, fx_eq⟩, le_Sup_of_le ⟨f, f_in, rfl⟩ $ fx_eq ▸ m_s _ f_in h

algebra/lattice/filter.lean

@@ -69,9 +69,6 @@ le_antisymm
   (le_infi $ assume t, le_infi $ assume ⟨_, h⟩, Inf_le_Inf h)
   (le_Inf $ assume b h, infi_le_of_le {b} $ infi_le_of_le (by simp [h]) $ Inf_le $ by simp)
 
-theorem Sup_le_iff {s : set α} {a : α} : Sup s ≤ a ↔ (∀x∈s, x ≤ a) :=
-⟨assume h x hx, le_trans (le_Sup hx) h, Sup_le⟩
-
 end lattice
 
 instance : monad set :=
@@ -133,7 +130,7 @@ subset.antisymm
     (prod_mono (inter_subset_left _ _) (inter_subset_left _ _))
     (prod_mono (inter_subset_right _ _) (inter_subset_right _ _)))
 
-theorem monotone_prod [pre_order α] {f : α → set β} {g : α → set γ}
+theorem monotone_prod [preorder α] {f : α → set β} {g : α → set γ}
   (hf : monotone f) (hg : monotone g) : monotone (λx, set.prod (f x) (g x)) :=
 assume a b h, prod_mono (hf h) (hg h)
 
@@ -169,7 +166,7 @@ end
 @[simp] theorem prod_mk_mem_set_prod_eq {a : α} {b : β} {s : set α} {t : set β} :
   (a, b) ∈ set.prod s t = (a ∈ s ∧ b ∈ t) := rfl
 
-theorem monotone_inter [pre_order β] {f g : β → set α}
+theorem monotone_inter [preorder β] {f g : β → set α}
   (hf : monotone f) (hg : monotone g) : monotone (λx, (f x) ∩ (g x)) :=
 assume a b h x ⟨h₁, h₂⟩, ⟨hf h h₁, hg h h₂⟩
 
@@ -192,7 +189,7 @@ image_eq_vimage_of_inverse (@prod.swap α β) (@prod.swap β α)
   begin simp; intros; trivial end
   begin simp; intros; trivial end
 
-theorem monotone_set_of [pre_order α] {p : α → β → Prop}
+theorem monotone_set_of [preorder α] {p : α → β → Prop}
   (hp : ∀b, monotone (λa, p a b)) : monotone (λa, {b | p a b}) :=
 assume a a' h b, hp b h
 
@@ -296,7 +293,7 @@ def upwards (s : set α) := ∀{x y}, x ∈ s → x ≼ y → y ∈ s
 
 end order
 
-theorem directed_of_chain {α : Type u} {β : Type v} [pre_order β] {f : α → β} {c : set α}
+theorem directed_of_chain {α : Type u} {β : Type v} [preorder β] {f : α → β} {c : set α}
   (h : @zorn.chain α (λa b, f b ≤ f a) c) :
   directed (≤) (λx:{a:α // a ∈ c}, f (x.val)) :=
 assume ⟨a, ha⟩ ⟨b, hb⟩, classical.by_cases
@@ -503,8 +500,8 @@ instance : alternative filter :=
   failure := λα, ⊥,
   orelse  := λα x y, x ⊔ y }
 
-def at_top [pre_order α] : filter α := ⨅ a, principal {b | a ≤ b}
-def at_bot [pre_order α] : filter α := ⨅ a, principal {b | b ≤ a}
+def at_top [preorder α] : filter α := ⨅ a, principal {b | a ≤ b}
+def at_bot [preorder α] : filter α := ⨅ a, principal {b | b ≤ a}
 
 /- lattice equations -/
 
@@ -981,7 +978,7 @@ le_antisymm
   (infi_le_of_le s $ infi_le _ $ subset.refl _)
   (le_infi $ assume t, le_infi $ assume hi, hg hi)
 
-theorem monotone_lift [pre_order γ] {f : γ → filter α} {g : γ → set α → filter β}
+theorem monotone_lift [preorder γ] {f : γ → filter α} {g : γ → set α → filter β}
   (hf : monotone f) (hg : monotone g) : monotone (λc, (f c).lift (g c)) :=
 assume a b h, lift_mono (hf h) (hg h)
 
@@ -1054,7 +1051,7 @@ theorem principal_le_lift' {t : set β} (hh : ∀s∈f.sets, t ⊆ h s) :
   principal t ≤ f.lift' h :=
 le_infi $ assume s, le_infi $ assume hs, principal_mono.mpr (hh s hs)
 
-theorem monotone_lift' [pre_order γ] {f : γ → filter α} {g : γ → set α → set β}
+theorem monotone_lift' [preorder γ] {f : γ → filter α} {g : γ → set α → set β}
   (hf : monotone f) (hg : monotone g) : monotone (λc, (f c).lift' (g c)) :=
 assume a b h, lift'_mono (hf h) (hg h)
 

algebra/lattice/fixed_points.lean

@@ -11,7 +11,7 @@ import algebra.lattice.complete_lattice
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-theorem ge_of_eq [pre_order α] {a b : α} : a = b → a ≥ b :=
+theorem ge_of_eq [preorder α] {a b : α} : a = b → a ≥ b :=
 λ h, h ▸ le_refl a
 
 namespace lattice

algebra/order.lean

@@ -11,7 +11,7 @@ universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
 section monotone
-variables [pre_order α] [pre_order β] [pre_order γ]
+variables [preorder α] [preorder β] [preorder γ]
 
 def monotone (f : α → β) := ∀{{a b}}, a ≤ b → f a ≤ f b
 
@@ -48,14 +48,14 @@ end
 
 /- order instances -/
 
-instance pre_order_fun [pre_order β] : pre_order (α → β) :=
+instance preorder_fun [preorder β] : preorder (α → β) :=
 { le := λx y, ∀b, x b ≤ y b,
   le_refl := λf b, le_refl (f b),
   le_trans := λf g h h1 h2 b, le_trans (h1 b) (h2 b),
 }
 
 instance partial_order_fun [partial_order β] : partial_order (α → β) :=
-{ pre_order_fun with
+{ preorder_fun with
   le_antisymm := λf g h1 h2, funext (λb, le_antisymm (h1 b) (h2 b))
 }
 
@@ -66,16 +66,16 @@ def weak_order_dual (wo : partial_order α) : partial_order α :=
   le_antisymm := assume a b h₁ h₂, le_antisymm h₂ h₁ }
 
 theorem le_dual_eq_le {α : Type} (wo : partial_order α) (a b : α) :
-  @has_le.le _ (@pre_order.to_has_le _ (@partial_order.to_pre_order _ (weak_order_dual wo))) a b =
-  @has_le.le _ (@pre_order.to_has_le _ (@partial_order.to_pre_order _ wo)) b a :=
+  @has_le.le _ (@preorder.to_has_le _ (@partial_order.to_preorder _ (weak_order_dual wo))) a b =
+  @has_le.le _ (@preorder.to_has_le _ (@partial_order.to_preorder _ wo)) b a :=
 rfl
 
-theorem comp_le_comp_left_of_monotone [pre_order α] [pre_order β] [pre_order γ]
+theorem comp_le_comp_left_of_monotone [preorder α] [preorder β] [preorder γ]
   {f : β → α} {g h : γ → β} (m_f : monotone f) (le_gh : g ≤ h) : has_le.le.{max w u} (f ∘ g) (f ∘ h) :=
 assume x, m_f (le_gh x)
 
 section monotone
-variables [pre_order α] [pre_order γ]
+variables [preorder α] [preorder γ]
 
 theorem monotone_lam {f : α → β → γ} (m : ∀b, monotone (λa, f a b)) : monotone f :=
 assume a a' h b, m b h

data/num/lemmas.lean

@@ -245,7 +245,7 @@ namespace pos_num
   -- TODO(Mario): Prove these using transfer tactic
   instance : decidable_linear_order pos_num :=
   { lt              := (<),
-    lt_iff_le_not_le := λ a b, @pre_order.lt_iff_le_not_le ℕ _ _ _,
+    lt_iff_le_not_le := λ a b, @preorder.lt_iff_le_not_le ℕ _ _ _,
     le              := (≤),
     le_refl         := λa, @le_refl nat _ _,
     le_trans        := λa b c, @le_trans nat _ _ _ _,
@@ -336,7 +336,7 @@ namespace num
       have := congr_arg (coe : num → nat) h, revert this,
       transfer_rw, apply add_right_cancel },
     lt                         := (<),
-    lt_iff_le_not_le := λ a b, @pre_order.lt_iff_le_not_le ℕ _ _ _,
+    lt_iff_le_not_le := λ a b, @preorder.lt_iff_le_not_le ℕ _ _ _,
     le                         := (≤),
     le_refl                    := λa, @le_refl nat _ _,
     le_trans                   := λa b c, @le_trans nat _ _ _ _,

data/set/basic.lean

@@ -19,8 +19,7 @@ theorem set_eq_def (s t : set α) : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t :=
 
 /- mem and set_of -/
 
--- TODO(Jeremy): I had to add ematch here
-@[simp, ematch] theorem mem_set_of_eq {a : α} {p : α → Prop} : a ∈ {a | p a} = p a := rfl
+@[simp] theorem mem_set_of_eq {a : α} {p : α → Prop} : a ∈ {a | p a} = p a := rfl
 
 @[simp] theorem nmem_set_of_eq {a : α} {P : α → Prop} : a ∉ {a : α | P a} = ¬ P a := rfl
 
@@ -64,12 +63,10 @@ theorem empty_def : (∅ : set α) = {x | false} := rfl
 @[simp] theorem set_of_false : {a : α | false} = ∅ := rfl
 
 theorem eq_empty_of_forall_not_mem {s : set α} (h : ∀ x, x ∉ s) : s = ∅ :=
-ext (assume x, iff.intro
-  (assume xs, absurd xs (h x))
-  (assume xe, absurd xe (not_mem_empty _)))
+by apply ext; finish
 
 theorem ne_empty_of_mem {s : set α} {x : α} (h : x ∈ s) : s ≠ ∅ :=
-  begin intro hs, rewrite hs at h, apply not_mem_empty _ h end
+by { intro hs, rewrite hs at h, apply not_mem_empty _ h }
 
 @[simp] theorem empty_subset (s : set α) : ∅ ⊆ s :=
 assume x, assume h, false.elim h

tactic/alias.lean

@@ -35,10 +35,10 @@ input theorem has the form A_iff_B or A_iff_B_left etc.
 import data.buffer.parser data.list.basic
 
 open lean.parser tactic interactive parser
-
+    
 namespace tactic.alias
 
-@[user_attribute] def alias_attr : user_attribute :=
+@[user_attribute] meta def alias_attr : user_attribute :=
 { name := `alias, descr := "This definition is an alias of another." }
 
 meta def alias_direct (d : declaration) (doc : string) (al : name) : tactic unit :=

topology/uniform_space.lean

@@ -26,7 +26,7 @@ def comp_rel {α : Type u} (r₁ r₂ : set (α×α)) :=
 @[simp] theorem swap_id_rel : prod.swap '' id_rel = @id_rel α :=
 set.ext $ assume ⟨a, b⟩, by simp [image_swap_eq_vimage_swap]; exact eq_comm
 
-theorem monotone_comp_rel [pre_order β] {f g : β → set (α×α)}
+theorem monotone_comp_rel [preorder β] {f g : β → set (α×α)}
   (hf : monotone f) (hg : monotone g) : monotone (λx, comp_rel (f x) (g x)) :=
 assume a b h p ⟨z, h₁, h₂⟩, ⟨z, hf h h₁, hg h h₂⟩