fix(*): update to lean

analysis/topology/topological_space.lean

@@ -29,13 +29,8 @@ section topological_space
 
 variables {α : Type u} {β : Type v} {ι : Sort w} {a a₁ a₂ : α} {s s₁ s₂ : set α} {p p₁ p₂ : α → Prop}
 
-lemma topological_space_eq {f g : topological_space α} (h' : f.is_open = g.is_open) : f = g :=
-begin
-  cases f with a, cases g with b,
-  have h : a = b, assumption,
-  clear h',
-  subst h
-end
+lemma topological_space_eq : ∀ {f g : topological_space α}, f.is_open = g.is_open → f = g
+| ⟨a, _, _, _⟩ ⟨b, _, _, _⟩ rfl := rfl
 
 section
 variables [t : topological_space α]
@@ -951,7 +946,7 @@ lemma is_topological_basis_of_open_of_nhds {s : set (set α)}
     (assume u hu,
       (@is_open_iff_nhds α (generate_from _) _).mpr $ assume a hau,
         let ⟨v, hvs, hav, hvu⟩ := h_nhds a u hau hu in
-        by rw nhds_generate_from; exact (infi_le_of_le v $ infi_le_of_le ⟨hav, hvs⟩ $ by simp [hvu]))
+        by rw nhds_generate_from; exact infi_le_of_le v (infi_le_of_le ⟨hav, hvs⟩ $ by simp [hvu]))
     (generate_from_le h_open)⟩
 
 lemma mem_nhds_of_is_topological_basis {a : α} {s : set α} {b : set (set α)}

data/list/basic.lean

@@ -2352,7 +2352,8 @@ theorem forall_mem_pw_filter (neg_trans : ∀ {x y z}, R x z → R x y ∨ R y z
   { rw [pw_filter_cons_of_neg h],
     refine λ H, ⟨_, IH H⟩,
     cases e : find (λ y, ¬ R x y) (pw_filter R l) with k,
-    { exact h.elim (ball.imp_right (λ_ _, not_not.1) (find_eq_none.1 e)) },
+    { refine h.elim (ball.imp_right _ (find_eq_none.1 e)),
+      exact λ y _, not_not.1 },
     { have := find_some e,
       exact (neg_trans (H k (find_mem e))).resolve_right this } }
 end, ball.imp_left (pw_filter_subset l)⟩

data/nat/basic.lean

@@ -238,10 +238,10 @@ theorem mul_self_inj {n m : ℕ} : n * n = m * m ↔ n = m :=
 le_antisymm_iff.trans (le_antisymm_iff.trans
   (and_congr mul_self_le_mul_self_iff mul_self_le_mul_self_iff)).symm
 
-instance decidable_ball_lt (n : nat) (P : Π k < n, Prop)
-  [H : ∀ n h, decidable (P n h)] : decidable (∀ n h, P n h) :=
+instance decidable_ball_lt (n : nat) (P : Π k < n, Prop) :
+  ∀ [H : ∀ n h, decidable (P n h)], decidable (∀ n h, P n h) :=
 begin
-  induction n with n IH; resetI,
+  induction n with n IH; intro; resetI,
   { exact is_true (λ n, dec_trivial) },
   cases IH (λ k h, P k (lt_succ_of_lt h)) with h,
   { refine is_false (mt _ h), intros hn k h, apply hn },

data/seq/computation.lean

@@ -333,7 +333,7 @@ get_eq_of_mem _ $ (thinkN_mem _).2 (get_mem _)
 theorem get_promises : s ~> get s := λ a, get_eq_of_mem _
 
 theorem mem_of_promises {a} (p : s ~> a) : a ∈ s :=
-by cases h with a' h; rw p h; exact h
+by unfreezeI; cases h with a' h; rw p h; exact h
 
 theorem get_eq_of_promises {a} : s ~> a → get s = a :=
 get_eq_of_mem _ ∘ mem_of_promises _

data/set/countable.lean

@@ -118,7 +118,7 @@ lemma countable_insert {s : set α} {a : α} (h : countable s) : countable (inse
 by rw [set.insert_eq]; from countable_union countable_singleton h
 
 lemma countable_finite {s : set α} : finite s → countable s
-| ⟨h⟩ := by haveI := (trunc_encodable_of_fintype s).out; apply countable_encodable'
+| ⟨h⟩ := by resetI; haveI := (trunc_encodable_of_fintype s).out; apply countable_encodable'
 
 lemma countable_set_of_finite_subset {s : set α} (h : countable s) :
   countable {t | finite t ∧ t ⊆ s } :=

data/set/finite.lean

@@ -96,7 +96,7 @@ finset.ext.mpr $ by simp
 @[elab_as_eliminator]
 theorem finite.induction_on {C : set α → Prop} {s : set α} (h : finite s)
   (H0 : C ∅) (H1 : ∀ {a s}, a ∉ s → finite s → C s → C (insert a s)) : C s :=
-let ⟨t⟩ := h in by exact
+let ⟨t⟩ := h in by exactI
 match s.to_finset, @mem_to_finset _ s _ with
 | ⟨l, nd⟩, al := begin
     change ∀ a, a ∈ l ↔ a ∈ s at al,
@@ -202,7 +202,7 @@ instance fintype_prod (s : set α) (t : set β) [fintype s] [fintype t] : fintyp
 fintype_of_finset (s.to_finset.product t.to_finset) $ by simp
 
 lemma finite_prod {s : set α} {t : set β} : finite s → finite t → finite (set.prod s t)
-| ⟨hs⟩ ⟨ht⟩ := by exact ⟨set.fintype_prod s t⟩
+| ⟨hs⟩ ⟨ht⟩ := by exactI ⟨set.fintype_prod s t⟩
 
 end set
 

order/order_iso.lean

@@ -83,22 +83,22 @@ protected theorem is_total : ∀ (f : r ≼o s) [is_total β s], is_total α r
 | ⟨f, o⟩ ⟨H⟩ := ⟨λ a b, (or_congr o o).2 (H _ _)⟩
 
 protected theorem is_preorder : ∀ (f : r ≼o s) [is_preorder β s], is_preorder α r
-| f H := by exact {..f.is_refl, ..f.is_trans}
+| f H := by exactI {..f.is_refl, ..f.is_trans}
 
 protected theorem is_partial_order : ∀ (f : r ≼o s) [is_partial_order β s], is_partial_order α r
-| f H := by exact {..f.is_preorder, ..f.is_antisymm}
+| f H := by exactI {..f.is_preorder, ..f.is_antisymm}
 
 protected theorem is_linear_order : ∀ (f : r ≼o s) [is_linear_order β s], is_linear_order α r
-| f H := by exact {..f.is_partial_order, ..f.is_total}
+| f H := by exactI {..f.is_partial_order, ..f.is_total}
 
 protected theorem is_strict_order : ∀ (f : r ≼o s) [is_strict_order β s], is_strict_order α r
-| f H := by exact {..f.is_irrefl, ..f.is_trans}
+| f H := by exactI {..f.is_irrefl, ..f.is_trans}
 
 protected theorem is_trichotomous : ∀ (f : r ≼o s) [is_trichotomous β s], is_trichotomous α r
 | ⟨f, o⟩ ⟨H⟩ := ⟨λ a b, (or_congr o (or_congr f.inj'.eq_iff.symm o)).2 (H _ _)⟩
 
 protected theorem is_strict_total_order' : ∀ (f : r ≼o s) [is_strict_total_order' β s], is_strict_total_order' α r
-| f H := by exact {..f.is_trichotomous, ..f.is_strict_order}
+| f H := by exactI {..f.is_trichotomous, ..f.is_strict_order}
 
 protected theorem acc (f : r ≼o s) (a : α) : acc s (f a) → acc r a :=
 begin
@@ -111,7 +111,7 @@ protected theorem well_founded : ∀ (f : r ≼o s) (h : well_founded s), well_f
 | f ⟨H⟩ := ⟨λ a, f.acc _ (H _)⟩
 
 protected theorem is_well_order : ∀ (f : r ≼o s) [is_well_order β s], is_well_order α r
-| f H := by exact {wf := f.well_founded H.wf, ..f.is_strict_total_order'}
+| f H := by exactI {wf := f.well_founded H.wf, ..f.is_strict_total_order'}
 
 /-- It suffices to prove `f` is monotone between strict orders
   to show it is an order embedding. -/

set_theory/cardinal.lean

@@ -610,7 +610,7 @@ lt_omega.trans ⟨λ ⟨n, e⟩, begin
   rw [← lift_mk_fin n] at e,
   cases quotient.exact e with f,
   exact ⟨fintype.of_equiv _ f.symm⟩
-end, λ ⟨_⟩, by exact ⟨_, fintype_card _⟩⟩
+end, λ ⟨_⟩, by exactI ⟨_, fintype_card _⟩⟩
 
 theorem lt_omega_iff_finite {α} {S : set α} : mk S < omega ↔ finite S :=
 lt_omega_iff_fintype
@@ -633,10 +633,10 @@ end
 /-- König's theorem -/
 theorem sum_lt_prod {ι} (f g : ι → cardinal) (H : ∀ i, f i < g i) : sum f < prod g :=
 lt_of_not_ge $ λ ⟨F⟩, begin
-  haveI : inhabited (Π (i : ι), (g i).out),
+  have : inhabited (Π (i : ι), (g i).out),
   { refine ⟨λ i, classical.choice $ ne_zero_iff_nonempty.1 _⟩,
     rw mk_out,
-    exact ne_of_gt (lt_of_le_of_lt (zero_le _) (H i)) },
+    exact ne_of_gt (lt_of_le_of_lt (zero_le _) (H i)) }, resetI,
   let G := inv_fun F,
   have sG : surjective G := inv_fun_surjective F.2,
   have : ∀ i, ¬ ∀ b, ∃ a, G ⟨i, a⟩ i = b,

set_theory/cofinality.lean

@@ -51,7 +51,7 @@ namespace ordinal
   interesting on limit ordinals (when it is an infinite cardinal). -/
 def cof (o : ordinal.{u}) : cardinal.{u} :=
 quot.lift_on o (λ ⟨α, r, _⟩,
-  @order.cof α (λ x y, ¬ r y x) ⟨λ a, by apply irrefl⟩) $
+  @order.cof α (λ x y, ¬ r y x) ⟨λ a, by resetI; apply irrefl⟩) $
 λ ⟨α, r, _⟩ ⟨β, s, _⟩ ⟨⟨f, hf⟩⟩, begin
   show @order.cof α (λ x y, ¬ r y x) ⟨_⟩ = @order.cof β (λ x y, ¬ s y x) ⟨_⟩,
   refine cardinal.lift_inj.1 (@order_iso.cof _ _ _ _ ⟨_⟩ ⟨_⟩ _),
@@ -85,7 +85,7 @@ theorem ord_cof_eq (r : α → α → Prop) [is_well_order α r] :
 let ⟨S, hS, e⟩ := cof_eq r, ⟨s, _, e'⟩ := cardinal.ord_eq S,
     T : set α := {a | ∃ aS : a ∈ S, ∀ b : S, s b ⟨_, aS⟩ → r b a} in
 begin
-  suffices,
+  resetI, suffices,
   { refine ⟨T, this,
       le_antisymm _ (cardinal.ord_le.2 $ cof_type_le T this)⟩,
     rw [← e, e'],
@@ -129,6 +129,7 @@ end
 
 theorem cof_le_card (o) : cof o ≤ card o :=
 induction_on o $ λ α r _, begin
+  resetI,
   have : mk (@set.univ α) = card (type r) :=
     quotient.sound ⟨equiv.set.univ _⟩,
   rw ← this, exact cof_type_le set.univ (λ a, ⟨a, ⟨⟩, irrefl a⟩)
@@ -141,7 +142,7 @@ by simpa using cof_le_card c.ord
 le_antisymm (by simpa using cof_le_card 0) (cardinal.zero_le _)
 
 @[simp] theorem cof_eq_zero {o} : cof o = 0 ↔ o = 0 := 
-⟨induction_on o $ λ α r _ z, by exact
+⟨induction_on o $ λ α r _ z, by exactI
   let ⟨S, hl, e⟩ := cof_eq r in type_eq_zero_iff_empty.2 $
   λ ⟨a⟩, let ⟨b, h, _⟩ := hl a in
   ne_zero_iff_nonempty.2 (by exact ⟨⟨_, h⟩⟩) (e.trans z),
@@ -163,6 +164,7 @@ end
 
 @[simp] theorem cof_eq_one_iff_is_succ {o} : cof.{u} o = 1 ↔ ∃ a, o = succ a := 
 ⟨induction_on o $ λ α r _ z, begin
+  resetI,
   rcases cof_eq r with ⟨S, hl, e⟩, rw z at e,
   cases ne_zero_iff_nonempty.1 (by rw e; exact one_ne_zero) with a,
   refine ⟨typein r a, eq.symm $ quotient.sound
@@ -185,6 +187,7 @@ end, λ ⟨a, e⟩, by simp [e]⟩
 
 @[simp] theorem cof_add (a b : ordinal) : b ≠ 0 → cof (a + b) = cof b :=
 induction_on a $ λ α r _, induction_on b $ λ β s _ b0, begin
+  resetI,
   change cof (type _) = _,
   refine eq_of_forall_le_iff (λ c, _),
   rw [le_cof_type, le_cof_type],
@@ -210,7 +213,7 @@ end
 
 @[simp] theorem cof_cof (o : ordinal) : cof (cof o).ord = cof o :=
 le_antisymm (le_trans (cof_le_card _) (by simp)) $
-induction_on o $ λ α r _, by exact
+induction_on o $ λ α r _, by exactI
 let ⟨S, hS, e₁⟩ := ord_cof_eq r,
     ⟨T, hT, e₂⟩ := cof_eq (subrel r S) in begin
   rw e₁ at e₂, rw ← e₂,