From c9d6cc525526f54ea8da2d58ec811afc5b613932 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 25 Jul 2015 13:38:24 -0400 Subject: [PATCH] feat(library/data/{finset,set}): various basic facts --- library/data/finset/basic.lean | 102 +++++++++++++++++++-- library/data/finset/comb.lean | 35 ++++++- library/data/set/basic.lean | 36 +++++++- library/data/set/function.lean | 17 ++++ library/theories/group_theory/action.lean | 12 +-- library/theories/group_theory/cyclic.lean | 2 +- library/theories/group_theory/finsubg.lean | 6 +- 7 files changed, 185 insertions(+), 25 deletions(-) diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean index 1b91a6b87..d2a991af4 100644 --- a/library/data/finset/basic.lean +++ b/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 -/ diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean index e4128cf8b..4c03587be 100644 --- a/library/data/finset/comb.lean +++ b/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] diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index 53e778e5d..461587fa6 100644 --- a/library/data/set/basic.lean +++ b/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) diff --git a/library/data/set/function.lean b/library/data/set/function.lean index 30ee2aff9..eecb840ca 100644 --- a/library/data/set/function.lean +++ b/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 diff --git a/library/theories/group_theory/action.lean b/library/theories/group_theory/action.lean index 0dd68d60a..7733eda59 100644 --- a/library/theories/group_theory/action.lean +++ 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)) diff --git a/library/theories/group_theory/cyclic.lean b/library/theories/group_theory/cyclic.lean index 0d5c7dd3b..9f5487035 100644 --- a/library/theories/group_theory/cyclic.lean +++ b/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 diff --git a/library/theories/group_theory/finsubg.lean b/library/theories/group_theory/finsubg.lean index bc0245787..92c0be801 100644 --- a/library/theories/group_theory/finsubg.lean +++ b/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