refactor(linear_algebra/basic): move some lemmas to the right place

algebra/ring.lean

@@ -16,6 +16,13 @@ theorem mul_two (n : α) : n * 2 = n + n :=
 
 theorem bit0_eq_two_mul (n : α) : bit0 n = 2 * n :=
 (two_mul _).symm
+
+variable (α)
+lemma zero_ne_one_or_forall_eq_0 : (0 : α) ≠ 1 ∨ (∀a:α, a = 0) :=
+by haveI := classical.dec;
+   refine not_or_of_imp (λ h a, _); simpa using congr_arg ((*) a) h.symm
+variable {α}
+
 end
 
 namespace units

data/seq/computation.lean

@@ -755,7 +755,7 @@ equiv_of_mem h (ret_mem _)
 
 /-- `lift_rel R ca cb` is a generalization of `equiv` to relations other than
   equality. It asserts that if `ca` terminates with `a`, then `cb` terminates with
-  some `b` such that `R a b`, and if `cb` terminates with b` then `ca` terminates
+  some `b` such that `R a b`, and if `cb` terminates with `b` then `ca` terminates
   with some `a` such that `R a b`. -/
 def lift_rel (R : α → β → Prop) (ca : computation α) (cb : computation β) : Prop :=
 (∀ {a}, a ∈ ca → ∃ {b}, b ∈ cb ∧ R a b) ∧

data/set/basic.lean

@@ -51,7 +51,7 @@ theorem ext {a b : set α} (h : ∀ x, x ∈ a ↔ x ∈ b) : a = b :=
 funext (assume x, propext (h x))
 
 theorem ext_iff (s t : set α) : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t :=
-⟨begin intros h x, rw h end, set.ext⟩
+⟨begin intros h x, rw h end, ext⟩
 
 @[trans] theorem mem_of_mem_of_subset {α : Type u} {x : α} {s t : set α} (hx : x ∈ s) (h : s ⊆ t) : x ∈ t :=
 h hx
@@ -414,10 +414,10 @@ theorem insert_comm (a b : α) (s : set α) : insert a (insert b s) = insert b (
 ext $ by simp [or.left_comm]
 
 theorem insert_union : insert a s ∪ t = insert a (s ∪ t) :=
-set.ext $ assume a, by simp [or.comm, or.left_comm]
+ext $ assume a, by simp [or.comm, or.left_comm]
 
 @[simp] theorem union_insert : s ∪ insert a t = insert a (s ∪ t) :=
-set.ext $ assume a, by simp [or.comm, or.left_comm]
+ext $ assume a, by simp [or.comm, or.left_comm]
 
 -- TODO(Jeremy): make this automatic
 theorem insert_ne_empty (a : α) (s : set α) : insert a s ≠ ∅ :=
@@ -467,7 +467,7 @@ by finish
 ⟨λh, h (by simp), λh b e, by simp at e; simp [*]⟩
 
 theorem set_compr_eq_eq_singleton {a : α} : {b | b = a} = {a} :=
-set.ext $ by simp
+ext $ by simp
 
 @[simp] theorem union_singleton : s ∪ {a} = insert a s :=
 by simp [singleton_def]
@@ -627,10 +627,10 @@ theorem diff_eq_empty {s t : set α} : s \ t = ∅ ↔ s ⊆ t :=
   assume h, eq_empty_of_subset_empty $ assume x ⟨hx, hnx⟩, hnx $ h hx⟩
 
 @[simp] theorem diff_empty {s : set α} : s \ ∅ = s :=
-set.ext $ assume x, ⟨assume ⟨hx, _⟩, hx, assume h, ⟨h, not_false⟩⟩
+ext $ assume x, ⟨assume ⟨hx, _⟩, hx, assume h, ⟨h, not_false⟩⟩
 
 theorem diff_diff {u : set α} : s \ t \ u = s \ (t ∪ u) :=
-set.ext $ by simp [not_or_distrib, and.comm, and.left_comm]
+ext $ by simp [not_or_distrib, and.comm, and.left_comm]
 
 lemma diff_subset_iff {s t u : set α} : s \ t ⊆ u ↔ s ⊆ t ∪ u :=
 ⟨assume h x xs, classical.by_cases or.inl (assume nxt, or.inr (h ⟨xs, nxt⟩)),
@@ -640,7 +640,7 @@ lemma diff_subset_comm {s t u : set α} : s \ t ⊆ u ↔ s \ u ⊆ t :=
 by rw [diff_subset_iff, diff_subset_iff, union_comm]
 
 @[simp] theorem insert_diff (h : a ∈ t) : insert a s \ t = s \ t :=
-set.ext $ by intro; constructor; simp [or_imp_distrib, h] {contextual := tt}
+ext $ by intro; constructor; simp [or_imp_distrib, h] {contextual := tt}
 
 theorem union_diff_self {s t : set α} : s ∪ (t \ s) = s ∪ t :=
 by finish [ext_iff, iff_def]
@@ -649,7 +649,7 @@ theorem diff_union_self {s t : set α} : (s \ t) ∪ t = s ∪ t :=
 by rw [union_comm, union_diff_self, union_comm]
 
 theorem diff_inter_self {a b : set α} : (b \ a) ∩ a = ∅ :=
-set.ext $ by simp [iff_def] {contextual:=tt}
+ext $ by simp [iff_def] {contextual:=tt}
 
 theorem diff_eq_self {s t : set α} : s \ t = s ↔ t ∩ s ⊆ ∅ :=
 by finish [ext_iff, iff_def, subset_def]
@@ -661,6 +661,8 @@ diff_eq_self.2 $ by simp [singleton_inter_eq_empty.2 h]
   insert a (s \ {a}) = insert a s :=
 by simp [insert_eq, union_diff_self, -union_singleton, -singleton_union]
 
+@[simp] lemma diff_self {s : set α} : s \ s = ∅ := ext $ by simp
+
 /- powerset -/
 
 theorem mem_powerset {x s : set α} (h : x ⊆ s) : x ∈ powerset s := h
@@ -708,7 +710,7 @@ theorem preimage_comp {s : set γ} : (g ∘ f) ⁻¹' s = f ⁻¹' (g ⁻¹' s)
 theorem eq_preimage_subtype_val_iff {p : α → Prop} {s : set (subtype p)} {t : set α} :
   s = subtype.val ⁻¹' t ↔ (∀x (h : p x), (⟨x, h⟩ : subtype p) ∈ s ↔ x ∈ t) :=
 ⟨assume s_eq x h, by rw [s_eq]; simp,
- assume h, set.ext $ assume ⟨x, hx⟩, by simp [h]⟩
+ assume h, ext $ assume ⟨x, hx⟩, by simp [h]⟩
 
 end preimage
 
@@ -807,7 +809,7 @@ theorem image_univ_of_surjective {ι : Type*} {f : ι → β} (H : surjective f)
 eq_univ_of_forall $ by simp [image]; exact H
 
 @[simp] theorem image_singleton {f : α → β} {a : α} : f '' {a} = {f a} :=
-set.ext $ λ x, by simp [image]; rw eq_comm
+ext $ λ x, by simp [image]; rw eq_comm
 
 lemma inter_singleton_ne_empty {α : Type*} {s : set α} {a : α} : s ∩ {a} ≠ ∅ ↔ a ∈ s :=
 by finish  [set.inter_singleton_eq_empty]
@@ -914,7 +916,7 @@ image_subset_iff.2 (union_preimage_subset _ _ _)
 
 lemma subtype_val_image {p : α → Prop} {s : set (subtype p)} :
   subtype.val '' s = {x | ∃h : p x, (⟨x, h⟩ : subtype p) ∈ s} :=
-set.ext $ assume a,
+ext $ assume a,
 ⟨assume ⟨⟨a', ha'⟩, in_s, h_eq⟩, h_eq ▸ ⟨ha', in_s⟩,
   assume ⟨ha, in_s⟩, ⟨⟨a, ha⟩, in_s, rfl⟩⟩
 
@@ -963,7 +965,7 @@ eq_univ_iff_forall
 @[simp] theorem range_id : range (@id α) = univ := range_iff_surjective.2 surjective_id
 
 @[simp] theorem image_univ {ι : Type*} {f : ι → β} : f '' univ = range f :=
-set.ext $ by simp [image, range]
+ext $ by simp [image, range]
 
 theorem range_comp {g : α → β} : range (g ∘ f) = g '' range f :=
 subset.antisymm
@@ -982,7 +984,7 @@ end
 
 theorem image_preimage_eq_inter_range {f : α → β} {t : set β} :
   f '' preimage f t = t ∩ range f :=
-set.ext $ assume x, ⟨assume ⟨x, hx, heq⟩, heq ▸ ⟨hx, mem_range_self _⟩,
+ext $ assume x, ⟨assume ⟨x, hx, heq⟩, heq ▸ ⟨hx, mem_range_self _⟩,
   assume ⟨hx, ⟨y, h_eq⟩⟩, h_eq ▸ mem_image_of_mem f $
     show y ∈ preimage f t, by simp [preimage, h_eq, hx]⟩
 
@@ -1018,18 +1020,18 @@ theorem mem_prod_eq {p : α × β} : p ∈ set.prod s t = (p.1 ∈ s ∧ p.2 ∈
 lemma mk_mem_prod {a : α} {b : β} (a_in : a ∈ s) (b_in : b ∈ t) : (a, b) ∈ set.prod s t := ⟨a_in, b_in⟩
 
 @[simp] theorem prod_empty {s : set α} : set.prod s ∅ = (∅ : set (α × β)) :=
-set.ext $ by simp [set.prod]
+ext $ by simp [set.prod]
 
 @[simp] theorem empty_prod {t : set β} : set.prod ∅ t = (∅ : set (α × β)) :=
-set.ext $ by simp [set.prod]
+ext $ by simp [set.prod]
 
 theorem insert_prod {a : α} {s : set α} {t : set β} :
   set.prod (insert a s) t = (prod.mk a '' t) ∪ set.prod s t :=
-set.ext begin simp [set.prod, image, iff_def, or_imp_distrib] {contextual := tt}; cc end
+ext begin simp [set.prod, image, iff_def, or_imp_distrib] {contextual := tt}; cc end
 
 theorem prod_insert {b : β} {s : set α} {t : set β} :
   set.prod s (insert b t) = ((λa, (a, b)) '' s) ∪ set.prod s t :=
-set.ext begin simp [set.prod, image, iff_def, or_imp_distrib] {contextual := tt}; cc end
+ext begin simp [set.prod, image, iff_def, or_imp_distrib] {contextual := tt}; cc end
 
 theorem prod_preimage_eq {f : γ → α} {g : δ → β} :
   set.prod (preimage f s) (preimage g t) = preimage (λp, (f p.1, g p.2)) (set.prod s t) := rfl
@@ -1046,7 +1048,7 @@ subset.antisymm
     (prod_mono (inter_subset_right _ _) (inter_subset_right _ _)))
 
 theorem image_swap_prod : (λp:β×α, (p.2, p.1)) '' set.prod t s = set.prod s t :=
-set.ext $ assume ⟨a, b⟩, by simp [mem_image_eq, set.prod, and_comm]; exact
+ext $ assume ⟨a, b⟩, by simp [mem_image_eq, set.prod, and_comm]; exact
 ⟨ assume ⟨b', a', ⟨h_a, h_b⟩, h⟩, by subst a'; subst b'; assumption,
   assume h, ⟨b, a, ⟨rfl, rfl⟩, h⟩⟩
 
@@ -1055,15 +1057,15 @@ image_eq_preimage_of_inverse prod.swap_left_inverse prod.swap_right_inverse
 
 theorem prod_image_image_eq {m₁ : α → γ} {m₂ : β → δ} :
   set.prod (image m₁ s) (image m₂ t) = image (λp:α×β, (m₁ p.1, m₂ p.2)) (set.prod s t) :=
-set.ext $ by simp [-exists_and_distrib_right, exists_and_distrib_right.symm, and.left_comm, and.assoc, and.comm]
+ext $ by simp [-exists_and_distrib_right, exists_and_distrib_right.symm, and.left_comm, and.assoc, and.comm]
 
 theorem prod_range_range_eq {α β γ δ} {m₁ : α → γ} {m₂ : β → δ} :
   set.prod (range m₁) (range m₂) = range (λp:α×β, (m₁ p.1, m₂ p.2)) :=
-set.ext $ by simp [range]
+ext $ by simp [range]
 
 @[simp] theorem prod_singleton_singleton {a : α} {b : β} :
   set.prod {a} {b} = ({(a, b)} : set (α×β)) :=
-set.ext $ by simp [set.prod]
+ext $ by simp [set.prod]
 
 theorem prod_neq_empty_iff {s : set α} {t : set β} :
   set.prod s t ≠ ∅ ↔ (s ≠ ∅ ∧ t ≠ ∅) :=
@@ -1073,7 +1075,7 @@ by simp [not_eq_empty_iff_exists]
   (a, b) ∈ set.prod s t = (a ∈ s ∧ b ∈ t) := rfl
 
 @[simp] theorem univ_prod_univ : set.prod (@univ α) (@univ β) = univ :=
-set.ext $ assume ⟨a, b⟩, by simp
+ext $ assume ⟨a, b⟩, by simp
 
 lemma prod_sub_preimage_iff {W : set γ} {f : α × β → γ} :
   set.prod s t ⊆ f ⁻¹' W ↔ ∀ a b, a ∈ s → b ∈ t → f (a, b) ∈ W :=

linear_algebra/basic.lean

@@ -37,12 +37,6 @@ reserve infix `≃ₗ` : 50
 universes u v w x y
 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type y} {ι : Type x}
 
-@[simp] lemma set.diff_self {s : set α} : s \ s = ∅ :=
-set.ext $ by simp
-
-lemma zero_ne_one_or_forall_eq_0 (α : Type u) [ring α] : (0 : α) ≠ 1 ∨ (∀a:α, a = 0) :=
-not_or_of_imp $ λ h a, by simpa using congr_arg ((*) a) h.symm
-
 namespace finset
 
 lemma smul_sum [ring γ] [module γ β] {s : finset α} {a : γ} {f : α → β} :