refactor(library): cleanup proofs

Fixed proofs that broke when we tried to implement a "checkpoint" have.

library/algebra/complete_lattice.lean

@@ -256,10 +256,10 @@ have le₂ : (⨆s₁) ⊔ (⨆s₂) ≤ ⨆ (s₁ ∪ s₂), from
 le.antisymm le₁ le₂
 
 lemma Inf_empty_eq_Sup_univ : ⨅ (∅ : set A) = ⨆ univ :=
-have le₁ : ⨅ ∅ ≤ ⨆ univ, from
+have le₁ : ⨅ (∅ : set A) ≤ ⨆ univ, from
   le_Sup !mem_univ,
 have le₂ : ⨆ univ ≤ ⨅ ∅, from
-  le_Inf (take a, suppose a ∈ ∅, absurd this !not_mem_empty),
+  le_Inf (take a : A, suppose a ∈ ∅, absurd this !not_mem_empty),
 le.antisymm le₁ le₂
 
 lemma Sup_empty_eq_Inf_univ : ⨆ (∅ : set A) = ⨅ univ :=

library/algebra/module.lean

@@ -45,7 +45,7 @@ section left_module
   !add.left_cancel this
 
   proposition smul_zero (a : R) : a • (0 : M) = 0 :=
-  have a • 0 + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
+  have a • (0:M) + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
   !add.left_cancel this
 
   proposition neg_smul (a : R) (u : M) : (-a) • u = - (a • u) :=

library/data/bag.lean

@@ -291,7 +291,7 @@ private lemma max_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a
 | a (b::l) h₁ h₂ :=
   assert nodup l, from nodup_of_nodup_cons h₂,
   assert b ∉ l,   from not_mem_of_nodup_cons h₂,
-  or.elim h₁
+  or.elim (eq_or_mem_of_mem_cons h₁)
   (suppose a = b,
     have a ∉ l, by rewrite this; assumption,
     assert a ∉ max_count l₁ l₂ l, from not_mem_max_count_of_not_mem l₁ l₂ this,
@@ -305,8 +305,9 @@ private lemma max_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a
        rewrite [if_neg i, list.count_append, count_gen, max_eq_right_of_lt (lt_of_not_ge i), count_eq_zero_of_not_mem `a ∉ max_count l₁ l₂ l`]
      end))
   (suppose a ∈ l,
-    assert a ≠ b, from suppose a = b, by subst b; contradiction,
-    assert ih : list.count a (max_count l₁ l₂ l) = max (list.count a l₁) (list.count a l₂), from max_count_eq `a ∈ l` `nodup l`,
+    assert a ≠ b, from suppose a = b, begin subst b, contradiction end,
+    assert ih : list.count a (max_count l₁ l₂ l) = max (list.count a l₁) (list.count a l₂), from
+       max_count_eq `a ∈ l` `nodup l`,
     by_cases
     (suppose i : list.count b l₁ ≥ list.count b l₂, begin
        unfold max_count,
@@ -337,7 +338,7 @@ private lemma min_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a
 | a (b::l) h₁ h₂ :=
   assert nodup l, from nodup_of_nodup_cons h₂,
   assert b ∉ l,   from not_mem_of_nodup_cons h₂,
-  or.elim h₁
+  or.elim (eq_or_mem_of_mem_cons h₁)
   (suppose a = b,
     have a ∉ l, by rewrite this; assumption,
     assert a ∉ min_count l₁ l₂ l, from not_mem_min_count_of_not_mem l₁ l₂ this,

library/data/equiv.lean

@@ -35,7 +35,7 @@ lemma eq_of_to_fun_eq {A B : Type} : ∀ {e₁ e₂ : equiv A B}, fn e₁ = fn e
   assert f₁ = f₂, from h,
   assert g₁ = g₂, from funext (λ x,
     assert f₁ (g₁ x) = f₂ (g₂ x), from eq.trans (r₁ x) (eq.symm (r₂ x)),
-    have f₁ (g₁ x) = f₁ (g₂ x),   by rewrite [-h at this]; exact this,
+    have f₁ (g₁ x) = f₁ (g₂ x),   begin subst f₂, exact this end,
     show g₁ x = g₂ x,             from injective_of_left_inverse l₁ this),
   by congruence; repeat assumption
 

library/data/finset/basic.lean

@@ -237,11 +237,11 @@ quot.induction_on s
       (assume nodup_l, H1)
       (take a l',
         assume IH nodup_al',
-        have a ∉ l', from not_mem_of_nodup_cons nodup_al',
-        assert e : list.insert a l' = a :: l', from insert_eq_of_not_mem this,
+        assert aux₁: a ∉ l', from not_mem_of_nodup_cons nodup_al',
+        assert e : list.insert a l' = a :: l', from insert_eq_of_not_mem aux₁,
         assert nodup l', from nodup_of_nodup_cons nodup_al',
         assert P (quot.mk (subtype.tag l' this)), from IH this,
-        assert P (insert a (quot.mk (subtype.tag l' _))), from H2 `a ∉ l'` this,
+        assert P (insert a (quot.mk (subtype.tag l' _))), from H2 aux₁ this,
         begin
           revert nodup_al',
           rewrite [-e],

library/data/finset/partition.lean

@@ -101,7 +101,10 @@ assume Pds, inter_eq_empty (take a, assume Pa nPa,
   obtain t Ptin Paint, from iff.elim_left !mem_Union_iff nPa,
   assert s ≠ t,
     from assume Peq, absurd (Peq ▸ of_mem_sep Psin) (of_mem_sep Ptin),
-  Pds s t (mem_of_mem_sep Psin) (mem_of_mem_sep Ptin) `s ≠ t` ▸ mem_inter Pains Paint)
+  have e₁ : s ∩ t = empty, from Pds s t (mem_of_mem_sep Psin) (mem_of_mem_sep Ptin) `s ≠ t`,
+  have a ∈ s ∩ t,     from mem_inter Pains Paint,
+  have a ∈ empty,     from e₁ ▸ this,
+  absurd this !not_mem_empty)
 
 section
 variables {B: Type} [deceqB : decidable_eq B]

library/data/fintype/card.lean

@@ -26,8 +26,8 @@ lemma card_le_of_inj (A : Type) [finA : fintype A] [deceqA : decidable_eq A]
    (∃ f : A → B, injective f) → card A ≤ card B :=
 assume Pex, obtain f Pinj, from Pex,
 assert Pinj_on_univ : _, from iff.mp !set.injective_iff_inj_on_univ Pinj,
-assert Pinj_ts : _, from to_set_univ⁻¹ ▸ Pinj_on_univ,
-assert Psub : (image f univ) ⊆ univ, from !subset_univ,
+assert Pinj_ts : set.inj_on f (ts univ), from to_set_univ⁻¹ ▸ Pinj_on_univ,
+assert Psub : (image f univ) ⊆ univ,     from !subset_univ,
 finset.card_le_of_inj_on univ univ (exists.intro f (and.intro Pinj_ts Psub))
 
 -- used to prove that inj ∧ eq card => surj

library/data/nat/power.lean

@@ -59,11 +59,11 @@ theorem pow_cancel_left : ∀ {a b c : nat}, a > 1 → a ^ b = a ^ c → b = c
 | a 0        0        h₁ h₂ := rfl
 | a (succ b) 0        h₁ h₂ :=
   assert a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right h₂),
-  assert 1 < 1, by rewrite [this at h₁]; exact h₁,
+  assert (1:nat) < 1, by rewrite [this at h₁]; exact h₁,
   absurd `1 <[nat] 1` !lt.irrefl
 | a 0        (succ c) h₁ h₂ :=
   assert a = 1, by rewrite [pow_succ at h₂, pow_zero at h₂]; exact (eq_one_of_mul_eq_one_right (eq.symm h₂)),
-  assert 1 < 1, by rewrite [this at h₁]; exact h₁,
+  assert (1:nat) < 1, by rewrite [this at h₁]; exact h₁,
   absurd `1 <[nat] 1` !lt.irrefl
 | a (succ b) (succ c) h₁ h₂ :=
   assert a ≠ 0, from assume aeq0, by rewrite [aeq0 at h₁]; exact (absurd h₁ dec_trivial),

library/theories/number_theory/irrational_roots.lean

@@ -31,7 +31,7 @@ section
     from even_of_even_pow this,
   assert 2 ∣ gcd a b,
     from dvd_gcd (dvd_of_even `even a`) (dvd_of_even `even b`),
-  have 2 ∣ 1,
+  have (2:nat) ∣ 1,
     begin rewrite [gcd_eq_one_of_coprime co at this], exact this end,
   show false, from absurd `2 ∣ 1` dec_trivial
 end
@@ -97,12 +97,12 @@ section
     from ne_of_gt (denom_pos q),
   have bnz : b ≠ (0 : ℚ),
     from assume H, `b ≠ 0` (of_int.inj H),
-  have bnnz : ((b : rat)^n ≠ 0),
-    from assume bneqz, bnz (eq_zero_of_pow_eq_zero bneqz),
-  have a^n /[rat] b^n = c,
+  have bnnz : (b : rat)^n ≠ 0,
+    from assume bneqz, bnz (_root_.eq_zero_of_pow_eq_zero bneqz),
+  have a^n /[rat] (b:rat)^n = c,
     using bnz, begin rewrite [*of_int_pow, -div_pow, -eq_num_div_denom, -H] end,
-  have (a^n : rat) = c *[rat] b^n,
-    from eq.symm (!mul_eq_of_eq_div bnnz this⁻¹),
+  have (a^n : rat) = c * (b:rat)^n,
+    from eq.symm (!mul_eq_of_eq_div bnnz (eq.symm this)),
   have a^n = c * b^n,  -- int version
     using this, by rewrite [-of_int_pow at this, -of_int_mul at this]; exact of_int.inj this,
   have (abs a)^n = abs c * (abs b)^n,