diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean index ba389f600..3c2710ac4 100644 --- a/library/data/set/basic.lean +++ b/library/data/set/basic.lean @@ -6,7 +6,7 @@ Author: Jeremy Avigad, Leonardo de Moura import logic.connectives logic.identities algebra.binary open eq.ops binary -definition set [reducible] (X : Type) := X → Prop +definition set (X : Type) := X → Prop namespace set @@ -14,7 +14,7 @@ variable {X : Type} /- membership and subset -/ -definition mem [reducible] (x : X) (a : set X) := a x +definition mem (x : X) (a : set X) := a x infix ∈ := mem notation a ∉ b := ¬ mem a b @@ -24,7 +24,7 @@ funext (take x, propext (H x)) definition subset (a b : set X) := ∀⦃x⦄, x ∈ a → x ∈ b infix ⊆ := subset -definition superset [reducible] (s t : set X) : Prop := t ⊆ s +definition superset (s t : set X) : Prop := t ⊆ s infix ⊇ := superset theorem subset.refl (a : set X) : a ⊆ a := take x, assume H, H @@ -66,7 +66,7 @@ exists.intro x (and.intro xs Px) /- empty set -/ -definition empty [reducible] : set X := λx, false +definition empty : set X := λx, false notation `∅` := empty theorem not_mem_empty (x : X) : ¬ (x ∈ ∅) := @@ -112,7 +112,7 @@ ext (take x, iff.intro (assume H', trivial) (assume H', H x)) /- union -/ -definition union [reducible] (a b : set X) : set X := λx, x ∈ a ∨ x ∈ b +definition union (a b : set X) : set X := λx, x ∈ a ∨ x ∈ b notation a ∪ b := union a b theorem mem_union_left {x : X} {a : set X} (b : set X) : x ∈ a → x ∈ a ∪ b := @@ -167,7 +167,7 @@ theorem union_subset {s t r : set X} (sr : s ⊆ r) (tr : t ⊆ r) : s ∪ t ⊆ /- intersection -/ -definition inter [reducible] (a b : set X) : set X := λx, x ∈ a ∧ x ∈ b +definition inter (a b : set X) : set X := λx, x ∈ a ∧ x ∈ b notation a ∩ b := inter a b theorem mem_inter_iff (x : X) (a b : set X) : x ∈ a ∩ b ↔ x ∈ a ∧ x ∈ b := !iff.refl @@ -234,7 +234,7 @@ ext (take x, !or.right_distrib) /- set-builder notation -/ -- {x : X | P} -definition set_of [reducible] (P : X → Prop) : set X := P +definition set_of (P : X → Prop) : set X := P notation `{` binder ` | ` r:(scoped:1 P, set_of P) `}` := r -- {x ∈ s | P} diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index 99ba0f5a3..ef7ae9f77 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -241,6 +241,8 @@ exists.intro x (have x ∈ X ∧ ¬ b ≤ x, by rewrite [-not_implies_iff_and_not]; apply Hx, and.intro (and.left this) (lt_of_not_ge (and.right this))) +section +local attribute mem [quasireducible] -- TODO: is there a better place to put this? proposition image_neg_eq (X : set ℝ) : (λ x, -x) '[X] = {x | -x ∈ X} := set.ext (take x, iff.intro @@ -290,7 +292,7 @@ have HX : X = {x | -x ∈ negX}, from set.ext (take x, by rewrite [↑set_of, ↑mem, +neg_neg]), show inf {x | -x ∈ X} = - sup X, using HX Hb' nonempty_negX, by rewrite [HX at {2}, sup_neg nonempty_negX Hb', neg_neg] - +end end /- limits under pointwise operations -/ diff --git a/library/theories/group_theory/hom.lean b/library/theories/group_theory/hom.lean index e13ae3f9f..e32fe09a8 100644 --- a/library/theories/group_theory/hom.lean +++ b/library/theories/group_theory/hom.lean @@ -116,17 +116,19 @@ variable {H : set A} variable [is_subgH : is_subgroup H] include is_subgH +section mem_reducible +local attribute mem [reducible] theorem hom_map_subgroup : is_subgroup (f '[H]) := - have Pone : 1 ∈ f '[H], from mem_image subg_has_one (hom_map_one f), - have Pclosed : mul_closed_on (f '[H]), from hom_map_mul_closed f H subg_mul_closed, - assert Pinv : ∀ b, b ∈ f '[H] → b⁻¹ ∈ f '[H], from - assume b, assume Pimg, - obtain a (Pa : a ∈ H ∧ f a = b), from Pimg, - assert Painv : a⁻¹ ∈ H, from subg_has_inv a (and.left Pa), - assert Pfainv : (f a)⁻¹ ∈ f '[H], from mem_image Painv (hom_map_inv f a), - and.right Pa ▸ Pfainv, - is_subgroup.mk Pone Pclosed Pinv - + have Pone : 1 ∈ f '[H], from mem_image subg_has_one (hom_map_one f), + have Pclosed : mul_closed_on (f '[H]), from hom_map_mul_closed f H subg_mul_closed, + assert Pinv : ∀ b, b ∈ f '[H] → b⁻¹ ∈ f '[H], from + assume b, assume Pimg, + obtain a (Pa : a ∈ H ∧ f a = b), from Pimg, + assert Painv : a⁻¹ ∈ H, from subg_has_inv a (and.left Pa), + assert Pfainv : (f a)⁻¹ ∈ f '[H], from mem_image Painv (hom_map_inv f a), + and.right Pa ▸ Pfainv, + is_subgroup.mk Pone Pclosed Pinv +end mem_reducible end section hom_theorem diff --git a/library/theories/group_theory/subgroup.lean b/library/theories/group_theory/subgroup.lean index 288392140..2ff001b14 100644 --- a/library/theories/group_theory/subgroup.lean +++ b/library/theories/group_theory/subgroup.lean @@ -205,7 +205,8 @@ include s variable {H : set A} variable [is_subg : is_subgroup H] include is_subg - +section set_reducible +local attribute set [reducible] lemma subg_has_one : H (1 : A) := @is_subgroup.has_one A s H is_subg lemma subg_mul_closed : mul_closed_on H := @is_subgroup.mul_closed A s H is_subg lemma subg_has_inv : subgroup.has_inv H := @is_subgroup.has_inv A s H is_subg @@ -240,6 +241,7 @@ lemma subg_in_coset_refl (a : A) : a ∈ a ∘> H ∧ a ∈ H <∘ a := assert PHinvaa : H (a⁻¹*a), from (eq.symm (mul.left_inv a)) ▸ PH1, assert PHainva : H (a*a⁻¹), from (eq.symm (mul.right_inv a)) ▸ PH1, and.intro PHinvaa PHainva +end set_reducible lemma subg_in_lcoset_same_lcoset (a b : A) : in_lcoset H a b → same_lcoset H a b := assume Pa_in_b : H (b⁻¹*a), have Pbinva : b⁻¹*a ∘> H = H, from subgroup_lcoset_id (b⁻¹*a) Pa_in_b, diff --git a/tests/lean/run/congr_tac2.lean b/tests/lean/run/congr_tac2.lean index 8036aaece..c4f2f107b 100644 --- a/tests/lean/run/congr_tac2.lean +++ b/tests/lean/run/congr_tac2.lean @@ -30,6 +30,7 @@ example (A : Type) (s₁ s₂ : set A) [fxs₁ : finite_set s₁] [fxs₂ : fini begin intros, congruence, + unfold set at *, assumption end