feat(library/data/{finset,set}): various basic facts

library/data/finset/basic.lean

@@ -152,6 +152,9 @@ rfl
 theorem card_singleton (a : A) : card (singleton a) = 1 :=
 rfl
 
+lemma ne_empty_of_card_eq_succ {s : finset A} {n : nat} : card s = succ n → s ≠ ∅ :=
+by intros; substvars; contradiction
+
 /- insert -/
 section insert
 variable [h : decidable_eq A]
@@ -190,6 +193,9 @@ theorem insert_eq_of_mem {a : A} {s : finset A} (H : a ∈ s) : insert a s = s :
 ext (λ x, eq.substr (mem_insert_eq x a s)
    (or_iff_right_of_imp (λH1, eq.substr H1 H)))
 
+theorem insert.comm (x y : A) (s : finset A) : insert x (insert y s) = insert y (insert x s) :=
+ext (take a, by rewrite [*mem_insert_eq, propext !or.left_comm])
+
 theorem card_insert_of_mem {a : A} {s : finset A} : a ∈ s → card (insert a s) = card s :=
 quot.induction_on s
   (λ (l : nodup_list A) (ainl : a ∈ ⟦l⟧), list.length_insert_of_mem ainl)
@@ -203,9 +209,6 @@ theorem card_insert_le (a : A) (s : finset A) :
 if H : a ∈ s then by rewrite [card_insert_of_mem H]; apply le_succ
 else by rewrite [card_insert_of_not_mem H]
 
-lemma ne_empty_of_card_eq_succ {s : finset A} {n : nat} : card s = succ n → s ≠ ∅ :=
-by intros; substvars; contradiction
-
 protected theorem induction [recursor 6] {P : finset A → Prop}
     (H1 : P empty)
     (H2 : ∀ ⦃a : A⦄, ∀{s : finset A}, a ∉ s → P s → P (insert a s)) :
@@ -285,6 +288,14 @@ quot.induction_on s (λ l bin, mem_of_mem_erase bin)
 theorem mem_erase_of_ne_of_mem {a b : A} {s : finset A} : a ≠ b → a ∈ s → a ∈ erase b s :=
 quot.induction_on s (λ l n ain, list.mem_erase_of_ne_of_mem n ain)
 
+theorem mem_erase_iff (a b : A) (s : finset A) : a ∈ erase b s ↔ a ∈ s ∧ a ≠ b :=
+iff.intro
+  (assume H, and.intro (mem_of_mem_erase H) (ne_of_mem_erase H))
+  (assume H, mem_erase_of_ne_of_mem (and.right H) (and.left H))
+
+theorem mem_erase_eq (a b : A) (s : finset A) : a ∈ erase b s = (a ∈ s ∧ a ≠ b) :=
+propext !mem_erase_iff
+
 open decidable
 theorem erase_insert (a : A) (s : finset A) : a ∉ s → erase a (insert a s) = s :=
 λ anins, finset.ext (λ b, by_cases
@@ -354,6 +365,12 @@ ext (λ a, by rewrite [*mem_union_eq]; exact or.comm)
 theorem union.assoc (s₁ s₂ s₃ : finset A) : (s₁ ∪ s₂) ∪ s₃ = s₁ ∪ (s₂ ∪ s₃) :=
 ext (λ a, by rewrite [*mem_union_eq]; exact or.assoc)
 
+theorem union.left_comm (s₁ s₂ s₃ : finset A) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
+!left_comm union.comm union.assoc s₁ s₂ s₃
+
+theorem union.right_comm (s₁ s₂ s₃ : finset A) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ :=
+!right_comm union.comm union.assoc s₁ s₂ s₃
+
 theorem union_self (s : finset A) : s ∪ s = s :=
 ext (λ a, iff.intro
   (λ ain, or.elim (mem_or_mem_of_mem_union ain) (λ i, i) (λ i, i))
@@ -417,6 +434,12 @@ ext (λ a, by rewrite [*mem_inter_eq]; exact and.comm)
 theorem inter.assoc (s₁ s₂ s₃ : finset A) : (s₁ ∩ s₂) ∩ s₃ = s₁ ∩ (s₂ ∩ s₃) :=
 ext (λ a, by rewrite [*mem_inter_eq]; exact and.assoc)
 
+theorem inter.left_comm (s₁ s₂ s₃ : finset A) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
+!left_comm inter.comm inter.assoc s₁ s₂ s₃
+
+theorem inter.right_comm (s₁ s₂ s₃ : finset A) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
+!right_comm inter.comm inter.assoc s₁ s₂ s₃
+
 theorem inter_self (s : finset A) : s ∩ s = s :=
 ext (λ a, iff.intro
   (λ h, mem_of_mem_inter_right h)
@@ -532,22 +555,85 @@ quot.induction_on₃ s₁ s₂ s₃ (λ l₁ l₂ l₃ h₁ h₂, list.sub.trans
 theorem mem_of_subset_of_mem {s₁ s₂ : finset A} {a : A} : s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂ :=
 quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h₁ h₂, h₁ a h₂)
 
+theorem subset.antisymm {s₁ s₂ : finset A} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ :=
+ext (take x, iff.intro (assume H, mem_of_subset_of_mem H₁ H) (assume H, mem_of_subset_of_mem H₂ H))
+
+-- alternative name
+theorem eq_of_subset_of_subset {s₁ s₂ : finset A} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ :=
+subset.antisymm H₁ H₂
+
 theorem subset_of_forall {s₁ s₂ : finset A} : (∀x, x ∈ s₁ → x ∈ s₂) → s₁ ⊆ s₂ :=
 quot.induction_on₂ s₁ s₂ (λ l₁ l₂ H, H)
 
 theorem subset_insert [h : decidable_eq A] (s : finset A) (a : A) : s ⊆ insert a s :=
 subset_of_forall (take x, suppose x ∈ s, mem_insert_of_mem _ this)
 
-theorem eq_of_subset_of_subset {s₁ s₂ : finset A} (H₁ : s₁ ⊆ s₂) (H₂ : s₂ ⊆ s₁) : s₁ = s₂ :=
-ext (take x, iff.intro (assume H, mem_of_subset_of_mem H₁ H) (assume H, mem_of_subset_of_mem H₂ H))
+theorem eq_empty_of_subset_empty {x : finset A} (H : x ⊆ ∅) : x = ∅ :=
+subset.antisymm H (empty_subset x)
+
+theorem subset_empty_iff (x : finset A) : x ⊆ ∅ ↔ x = ∅ :=
+iff.intro eq_empty_of_subset_empty (take xeq, by rewrite xeq; apply subset.refl ∅)
 
 section
 variable [decA : decidable_eq A]
 include decA
 
-theorem erase_subset_erase_of_subset {a : A} {s₁ s₂ : finset A} : s₁ ⊆ s₂ → erase a s₁ ⊆ erase a s₂ :=
-λ is_sub, subset_of_forall (λ b bin,
-  mem_erase_of_ne_of_mem (ne_of_mem_erase bin) (mem_of_subset_of_mem is_sub (mem_of_mem_erase bin)))
+theorem erase_subset_erase (a : A) {s t : finset A} (H : s ⊆ t) : erase a s ⊆ erase a t :=
+begin
+  apply subset_of_forall,
+  intro x,
+  rewrite *mem_erase_eq,
+  intro H',
+  show x ∈ t ∧ x ≠ a, from and.intro (mem_of_subset_of_mem H (and.left H')) (and.right H')
+end
+
+theorem erase_subset  (a : A) (s : finset A) : erase a s ⊆ s :=
+begin
+  apply subset_of_forall,
+  intro x,
+  rewrite mem_erase_eq,
+  intro H,
+  apply and.left H
+end
+
+theorem erase_eq_of_not_mem {a : A} {s : finset A} (anins : a ∉ s) : erase a s = s :=
+eq_of_subset_of_subset !erase_subset
+  (subset_of_forall (take x, assume xs : x ∈ s,
+    have x ≠ a, from assume H', anins (eq.subst H' xs),
+    mem_erase_of_ne_of_mem this xs))
+
+theorem erase_insert_subset (a : A) (s : finset A) : erase a (insert a s) ⊆ s :=
+decidable.by_cases
+  (assume ains : a ∈ s, by rewrite [insert_eq_of_mem ains]; apply erase_subset)
+  (assume nains : a ∉ s, by rewrite [!erase_insert nains]; apply subset.refl)
+
+theorem erase_subset_of_subset_insert {a : A} {s t : finset A} (H : s ⊆ insert a t) :
+  erase a s ⊆ t :=
+subset.trans (!erase_subset_erase H) !erase_insert_subset
+
+theorem insert_erase_subset (a : A) (s : finset A) : s ⊆ insert a (erase a s) :=
+decidable.by_cases
+  (assume ains : a ∈ s, by rewrite [!insert_erase ains]; apply subset.refl)
+  (assume nains : a ∉ s, by rewrite[erase_eq_of_not_mem nains]; apply subset_insert)
+
+theorem insert_subset_insert (a : A) {s t : finset A} (H : s ⊆ t) : insert a s ⊆ insert a t :=
+begin
+  apply subset_of_forall,
+  intro x,
+  rewrite *mem_insert_eq,
+  intro H',
+  cases H' with [xeqa, xins],
+    exact (or.inl xeqa),
+  exact (or.inr (mem_of_subset_of_mem H xins))
+end
+
+theorem subset_insert_of_erase_subset {s t : finset A} {a : A} (H : erase a s ⊆ t) :
+  s ⊆ insert a t :=
+subset.trans (insert_erase_subset a s) (!insert_subset_insert H)
+
+theorem subset_insert_iff (s t : finset A) (a : A) : s ⊆ insert a t ↔ erase a s ⊆ t :=
+iff.intro !erase_subset_of_subset_insert !subset_insert_of_erase_subset
+
 end
 
 /- upto -/

library/data/finset/comb.lean

@@ -20,6 +20,7 @@ definition image (f : A → B) (s : finset A) : finset B :=
 quot.lift_on s
   (λ l, to_finset (list.map f (elt_of l)))
   (λ l₁ l₂ p, quot.sound (perm_erase_dup_of_perm (perm_map _ p)))
+notation f `'[`:max a `]` := image f a
 
 theorem image_empty (f : A → B) : image f ∅ = ∅ :=
 rfl
@@ -27,7 +28,7 @@ rfl
 theorem mem_image_of_mem (f : A → B) {s : finset A} {a : A} : a ∈ s → f a ∈ image f s :=
 quot.induction_on s (take l, assume H : a ∈ elt_of l, mem_to_finset (mem_map f H))
 
-theorem mem_image_of_mem_of_eq {f : A → B} {s : finset A} {a : A} {b : B}
+theorem mem_image {f : A → B} {s : finset A} {a : A} {b : B}
     (H1 : a ∈ s) (H2 : f a = b) :
   b ∈ image f s :=
 eq.subst H2 (mem_image_of_mem f H1)
@@ -42,7 +43,7 @@ theorem mem_image_iff (f : A → B) {s : finset A} {y : B} : y ∈ image f s ↔
 iff.intro exists_of_mem_image
   (assume H,
     obtain x (H₁ : x ∈ s) (H₂ : f x = y), from H,
-    mem_image_of_mem_of_eq H₁ H₂)
+    mem_image H₁ H₂)
 
 theorem mem_image_eq (f : A → B) {s : finset A} {y : B} : y ∈ image f s = ∃x, x ∈ s ∧ f x = y :=
 propext (mem_image_iff f)
@@ -51,7 +52,7 @@ theorem mem_image_of_mem_image_of_subset {f : A → B} {s t : finset A} {y : B}
     (H1 : y ∈ image f s) (H2 : s ⊆ t) : y ∈ image f t :=
 obtain x (H3: x ∈ s) (H4 : f x = y), from exists_of_mem_image H1,
 have H5 : x ∈ t, from mem_of_subset_of_mem H2 H3,
-show y ∈ image f t, from mem_image_of_mem_of_eq H5 H4
+show y ∈ image f t, from mem_image H5 H4
 
 theorem image_insert [h' : decidable_eq A] (f : A → B) (s : finset A) (a : A) :
   image f (insert a s) = insert (f a) (image f s) :=
@@ -84,8 +85,30 @@ ext (take z, iff.intro
   (suppose z ∈ image f (image g s),
     obtain y (Hy : y ∈ image g s) (Hfy : f y = z), from exists_of_mem_image this,
     obtain x (Hx : x ∈ s) (Hgx : g x = y), from exists_of_mem_image Hy,
-    mem_image_of_mem_of_eq Hx (by esimp; rewrite [Hgx, Hfy])))
+    mem_image Hx (by esimp; rewrite [Hgx, Hfy])))
 
+lemma image_subset {a b : finset A} (f : A → B) (H : a ⊆ b) : f '[a] ⊆ f '[b] :=
+subset_of_forall
+  (take y, assume Hy : y ∈ f '[a],
+    obtain x (Hx₁ : x ∈ a) (Hx₂ : f x = y), from exists_of_mem_image Hy,
+    mem_image (mem_of_subset_of_mem H Hx₁) Hx₂)
+
+theorem image_union [h' : decidable_eq A] (f : A → B) (s t : finset A) :
+  image f (s ∪ t) = image f s ∪ image f t :=
+ext (take y, iff.intro
+  (assume H : y ∈ image f (s ∪ t),
+    obtain x [(xst : x ∈ s ∪ t) (fxy : f x = y)], from exists_of_mem_image H,
+    or.elim (mem_or_mem_of_mem_union xst)
+      (assume xs, mem_union_l (mem_image xs fxy))
+      (assume xt, mem_union_r (mem_image xt fxy)))
+  (assume H : y ∈ image f s ∪ image f t,
+    or.elim (mem_or_mem_of_mem_union H)
+      (assume yifs : y ∈ image f s,
+        obtain x [(xs : x ∈ s) (fxy : f x = y)], from exists_of_mem_image yifs,
+        mem_image (mem_union_l xs) fxy)
+      (assume yift : y ∈ image f t,
+        obtain x [(xt : x ∈ t) (fxy : f x = y)], from exists_of_mem_image yift,
+        mem_image (mem_union_r xt) fxy)))
 end image
 
 /- filter and set-builder notation -/
@@ -126,8 +149,12 @@ iff.intro
 
 theorem mem_filter_eq : x ∈ filter p s = (x ∈ s ∧ p x) :=
 propext !mem_filter_iff
+
 end filter
 
+theorem mem_singleton_eq' {A : Type} [deceq : decidable_eq A] (x a : A) : x ∈ '{a} = (x = a) :=
+by rewrite [mem_insert_eq, mem_empty_eq, or_false]
+
 /- set difference -/
 section diff
 variables {A : Type} [deceq : decidable_eq A]

library/data/set/basic.lean

@@ -3,8 +3,8 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad, Leonardo de Moura
 -/
-import logic
-open eq.ops
+import logic algebra.binary
+open eq.ops binary
 
 definition set [reducible] (X : Type) := X → Prop
 
@@ -29,9 +29,13 @@ theorem subset.refl (a : set X) : a ⊆ a := take x, assume H, H
 theorem subset.trans (a b c : set X) (subab : a ⊆ b) (subbc : b ⊆ c) : a ⊆ c :=
 take x, assume ax, subbc (subab ax)
 
-theorem subset.antisymm (a b : set X) (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
+theorem subset.antisymm {a b : set X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
 setext (λ x, iff.intro (λ ina, h₁ ina) (λ inb, h₂ inb))
 
+-- an alterantive name
+theorem eq_of_subset_of_subset {a b : set X} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b :=
+subset.antisymm h₁ h₂
+
 definition strict_subset (a b : set X) := a ⊆ b ∧ a ≠ b
 infix `⊂`:50 := strict_subset
 
@@ -58,6 +62,20 @@ assume H : x ∈ ∅, H
 
 theorem mem_empty_eq (x : X) : x ∈ ∅ = false := rfl
 
+theorem eq_empty_of_forall_not_mem {s : set X} (H : ∀ x, x ∉ s) : s = ∅ :=
+setext (take x, iff.intro
+  (assume xs, absurd xs (H x))
+  (assume xe, absurd xe !not_mem_empty))
+
+theorem empty_subset (s : set X) : ∅ ⊆ s :=
+take x, assume H, false.elim H
+
+theorem eq_empty_of_subset_empty {s : set X} (H : s ⊆ ∅) : s = ∅ :=
+subset.antisymm H (empty_subset s)
+
+theorem subset_empty_iff (s : set X) : s ⊆ ∅ ↔ s = ∅ :=
+iff.intro eq_empty_of_subset_empty (take xeq, by rewrite xeq; apply subset.refl ∅)
+
 /- universal set -/
 
 definition univ : set X := λx, true
@@ -94,6 +112,12 @@ setext (take x, or.comm)
 theorem union.assoc (a b c : set X) : (a ∪ b) ∪ c = a ∪ (b ∪ c) :=
 setext (take x, or.assoc)
 
+theorem union.left_comm (s₁ s₂ s₃ : set X) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
+!left_comm union.comm union.assoc s₁ s₂ s₃
+
+theorem union.right_comm (s₁ s₂ s₃ : set X) : (s₁ ∪ s₂) ∪ s₃ = (s₁ ∪ s₃) ∪ s₂ :=
+!right_comm union.comm union.assoc s₁ s₂ s₃
+
 /- intersection -/
 
 definition inter [reducible] (a b : set X) : set X := λx, x ∈ a ∧ x ∈ b
@@ -118,6 +142,12 @@ setext (take x, !and.comm)
 theorem inter.assoc (a b c : set X) : (a ∩ b) ∩ c = a ∩ (b ∩ c) :=
 setext (take x, !and.assoc)
 
+theorem inter.left_comm (s₁ s₂ s₃ : set X) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
+!left_comm inter.comm inter.assoc s₁ s₂ s₃
+
+theorem inter.right_comm (s₁ s₂ s₃ : set X) : (s₁ ∩ s₂) ∩ s₃ = (s₁ ∩ s₃) ∩ s₂ :=
+!right_comm inter.comm inter.assoc s₁ s₂ s₃
+
 theorem inter_univ (a : set X) : a ∩ univ = a :=
 setext (take x, !and_true)
 

library/data/set/function.lean

@@ -58,6 +58,23 @@ take y, assume Hy : y ∈ f '[a],
 obtain x (Hx₁ : x ∈ a) (Hx₂ : f x = y), from Hy,
 mem_image (H Hx₁) Hx₂
 
+theorem image_union (f : X → Y) (s t : set X) :
+  image f (s ∪ t) = image f s ∪ image f t :=
+setext (take y, iff.intro
+  (assume H : y ∈ image f (s ∪ t),
+    obtain x [(xst : x ∈ s ∪ t) (fxy : f x = y)], from H,
+    or.elim xst
+      (assume xs, or.inl (mem_image xs fxy))
+      (assume xt, or.inr (mem_image xt fxy)))
+  (assume H : y ∈ image f s ∪ image f t,
+    or.elim H
+      (assume yifs : y ∈ image f s,
+        obtain x [(xs : x ∈ s) (fxy : f x = y)], from yifs,
+        mem_image (or.inl xs) fxy)
+      (assume yift : y ∈ image f t,
+        obtain x [(xt : x ∈ t) (fxy : f x = y)], from yift,
+        mem_image (or.inr xt) fxy)))
+
 /- maps to -/
 
 definition maps_to [reducible] (f : X → Y) (a : set X) (b : set Y) : Prop := ∀⦃x⦄, x ∈ a → f x ∈ b

library/theories/group_theory/action.lean

@@ -66,7 +66,7 @@ lemma exists_of_orbit {b : S} : b ∈ orbit hom H a → ∃ h, h ∈ H ∧ hom h
 
 lemma orbit_of_exists {b : S} : (∃ h, h ∈ H ∧ hom h a = b) → b ∈ orbit hom H a :=
 assume Pex, obtain h PinH Phab, from Pex,
-mem_image_of_mem_of_eq (mem_image_of_mem hom PinH) Phab
+mem_image (mem_image_of_mem hom PinH) Phab
 
 lemma is_fixed_point_of_mem_fixed_points :
   a ∈ fixed_points hom H → is_fixed_point hom H a :=
@@ -266,7 +266,7 @@ variables {hom : G → perm S} [Hom : is_hom_class hom] {H : finset G} [subgH :
 include Hom subgH
 
 lemma in_orbit_refl {a : S} : a ∈ orbit hom H a :=
-mem_image_of_mem_of_eq (mem_image_of_mem_of_eq (finsubg_has_one H) (hom_map_one hom)) rfl
+mem_image (mem_image (finsubg_has_one H) (hom_map_one hom)) rfl
 
 lemma in_orbit_trans {a b c : S} :
   a ∈ orbit hom H b → b ∈ orbit hom H c → a ∈ orbit hom H c :=
@@ -339,7 +339,7 @@ ext take s, iff.intro
   (assume Pin,
    obtain Psin Ps, from iff.elim_left !mem_filter_iff Pin,
    obtain a Pa, from exists_of_mem_orbits Psin,
-   mem_image_of_mem_of_eq
+   mem_image
      (mem_filter_of_mem !mem_univ (eq.symm
        (eq_of_card_eq_of_subset (by rewrite [card_singleton, Pa, Ps])
          (subset_of_forall
@@ -543,7 +543,7 @@ ext (take (pp : perm (fin (succ n))), iff.intro
   mem_filter_of_mem !mem_univ Ppp)
   (assume Pstab,
   assert Ppp : pp maxi = maxi, from of_mem_filter Pstab,
-  mem_image_of_mem_of_eq !mem_univ (lift_lower_eq Ppp)))
+  mem_image !mem_univ (lift_lower_eq Ppp)))
 
 definition move_from_max_to (i : fin (succ n)) : perm (fin (succ n)) :=
 perm.mk (madd (i - maxi)) madd_inj
@@ -552,8 +552,8 @@ lemma orbit_max : orbit (@id (perm (fin (succ n)))) univ maxi = univ :=
 ext (take i, iff.intro
   (assume P, !mem_univ)
   (assume P, begin
-    apply mem_image_of_mem_of_eq,
-      apply mem_image_of_mem_of_eq,
+    apply mem_image,
+      apply mem_image,
         apply mem_univ (move_from_max_to i), apply rfl,
       apply sub_add_cancel
     end))

library/theories/group_theory/cyclic.lean

@@ -182,7 +182,7 @@ assume Pe, let s := image (pow a) (upto (succ n)) in
 assert Psub: cyc a ⊆ s, from subset_of_forall
   (take g, assume Pgin, obtain i Pilt Pig, from of_mem_filter Pgin, begin
   rewrite [-Pig, pow_mod Pe],
-  apply mem_image_of_mem_of_eq,
+  apply mem_image,
     apply mem_upto_of_lt (mod_lt i !zero_lt_succ),
     exact rfl end),
 #nat calc order a ≤ card s : card_le_card_of_subset Psub

library/theories/group_theory/finsubg.lean

@@ -96,7 +96,7 @@ lemma fin_lrcoset_comm {a b : A} :
 by esimp [fin_lcoset, fin_rcoset]; rewrite [-*image_compose, lmul_rmul]
 
 lemma inv_mem_fin_inv {a : A} : a ∈ H → a⁻¹ ∈ fin_inv H :=
-assume Pin, mem_image_of_mem_of_eq Pin rfl
+assume Pin, mem_image Pin rfl
 
 lemma fin_lcoset_eq (a : A) : ts (fin_lcoset H a) = a ∘> (ts H) := calc
       ts (fin_lcoset H a) = coset.l a (ts H) : to_set_image
@@ -401,11 +401,11 @@ lemma lrcoset_same_of_mem_normalizer {g : G} :
   g ∈ normalizer H → fin_lcoset H g = fin_rcoset H g :=
 assume Pg, ext take h, iff.intro
   (assume Pl, obtain j Pjin Pj, from exists_of_mem_image Pl,
-  mem_image_of_mem_of_eq (of_mem_filter Pg j Pjin)
+  mem_image (of_mem_filter Pg j Pjin)
     (calc g*j*g⁻¹*g = g*j : inv_mul_cancel_right
                 ... = h   : Pj))
   (assume Pr, obtain j Pjin Pj, from exists_of_mem_image Pr,
-  mem_image_of_mem_of_eq (of_mem_filter (finsubg_has_inv (normalizer H) Pg) j Pjin)
+  mem_image (of_mem_filter (finsubg_has_inv (normalizer H) Pg) j Pjin)
     (calc g*(g⁻¹*j*g⁻¹⁻¹) = g*(g⁻¹*j*g)   : inv_inv
                       ... = g*(g⁻¹*(j*g)) : mul.assoc
                       ... = j*g           : mul_inv_cancel_left