chore(*): clean up uses of zorn

analysis/metric_space.lean

@@ -654,7 +654,7 @@ instance complete_of_proper {α : Type u} [metric_space α] [proper_space α] :
   intros f hf,
   /-We want to show that the Cauchy filter `f` is converging. It suffices to find a closed
   ball (therefore compact by properness) where it is nontrivial.-/
-  have A : ∃ t ∈ f.sets, ∀ x y ∈ t, dist x y < 1 := (cauchy_of_metric.1 hf).2 1 (by norm_num),
+  have A : ∃ t ∈ f.sets, ∀ x y ∈ t, dist x y < 1 := (cauchy_of_metric.1 hf).2 1 zero_lt_one,
   rcases A with ⟨t, ⟨t_fset, ht⟩⟩,
   rcases inhabited_of_mem_sets hf.1 t_fset with ⟨x, xt⟩,
   have : t ⊆ closed_ball x 1 := by intros y yt; simp [dist_comm]; apply le_of_lt (ht x y xt yt),

analysis/topology/topological_space.lean

@@ -696,24 +696,20 @@ let ⟨r, hrs, hruv⟩ := H u v hu hv ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩ in
 
 theorem exists_irreducible (s : set α) (H : is_irreducible s) :
   ∃ t : set α, is_irreducible t ∧ s ⊆ t ∧ ∀ u, is_irreducible u → t ⊆ u → u = t :=
-let ⟨⟨m, hsm, hm⟩, hm_max⟩ := @zorn.zorn { t | s ⊆ t ∧ is_irreducible t } (subrel (⊆) _)
-  (λ c hchain, classical.by_cases
-    (assume hc : c = ∅, ⟨⟨s, set.subset.refl s, H⟩, λ ⟨t, hsx, hx⟩,
-      hc.symm ▸ false.elim⟩)
-    (assume hc : c ≠ ∅, let ⟨⟨x, hsx, hx⟩, hxc⟩ := exists_mem_of_ne_empty hc in
-      ⟨⟨⋃ t ∈ c, subtype.val t, λ z hz, mem_bUnion hxc (hsx hz), λ u v hu hv ⟨y, hy, hyu⟩ ⟨z, hz, hzv⟩,
-        let ⟨p, hpc, hyp⟩ := mem_bUnion_iff.1 hy,
-            ⟨q, hqc, hzq⟩ := mem_bUnion_iff.1 hz in
-        or.cases_on (zorn.chain.total hchain hpc hqc)
-          (assume hpq : p.1 ⊆ q.1, let ⟨x, hxp, hxuv⟩ := q.2.2 u v hu hv
-              ⟨y, hpq hyp, hyu⟩ ⟨z, hzq, hzv⟩ in
-            ⟨x, mem_bUnion hqc hxp, hxuv⟩)
-          (assume hqp : q.1 ⊆ p, let ⟨x, hxp, hxuv⟩ := p.2.2 u v hu hv
-              ⟨y, hyp, hyu⟩ ⟨z, hqp hzq, hzv⟩ in
-            ⟨x, mem_bUnion hpc hxp, hxuv⟩)⟩,
-      λ ⟨p, hsp, hp⟩ hpc z hzp, mem_bUnion hpc hzp⟩))
-  (λ _ _ _, set.subset.trans) in
-⟨m, hm, hsm, λ u hu hmu, subset.antisymm (hm_max ⟨_, set.subset.trans hsm hmu, hu⟩ hmu) hmu⟩
+let ⟨m, hm, hsm, hmm⟩ := zorn.zorn_subset₀ { t : set α | is_irreducible t }
+  (λ c hc hcc hcn, let ⟨t, htc⟩ := exists_mem_of_ne_empty hcn in
+    ⟨⋃₀ c, λ u v hu hv ⟨y, hy, hyu⟩ ⟨z, hz, hzv⟩,
+      let ⟨p, hpc, hyp⟩ := mem_sUnion.1 hy,
+          ⟨q, hqc, hzq⟩ := mem_sUnion.1 hz in
+      or.cases_on (zorn.chain.total hcc hpc hqc)
+        (assume hpq : p ⊆ q, let ⟨x, hxp, hxuv⟩ := hc hqc u v hu hv
+            ⟨y, hpq hyp, hyu⟩ ⟨z, hzq, hzv⟩ in
+          ⟨x, mem_sUnion_of_mem hxp hqc, hxuv⟩)
+        (assume hqp : q ⊆ p, let ⟨x, hxp, hxuv⟩ := hc hpc u v hu hv
+            ⟨y, hyp, hyu⟩ ⟨z, hqp hzq, hzv⟩ in
+          ⟨x, mem_sUnion_of_mem hxp hpc, hxuv⟩),
+    λ x hxc, set.subset_sUnion_of_mem hxc⟩) s H in
+⟨m, hm, hsm, λ u hu hmu, hmm _ hu hmu⟩
 
 def irreducible_component (x : α) : set α :=
 classical.some (exists_irreducible {x} is_irreducible_singleton)

linear_algebra/basic.lean

@@ -7,7 +7,7 @@ Basics of linear algebra. This sets up the "categorical/lattice structure" of
 modules, submodules, and linear maps.
 -/
 
-import algebra.pi_instances order.zorn data.set.finite data.finsupp order.order_iso
+import algebra.pi_instances data.finsupp order.order_iso
 
 open function lattice
 

linear_algebra/basis.lean

@@ -21,7 +21,7 @@ We define the following concepts:
 * `is_basis.constr s g`: constructs a `linear_map` by extending `g` from the basis `s`
 
 -/
-import linear_algebra.lc
+import linear_algebra.lc order.zorn
 noncomputable theory
 
 open function lattice set submodule

logic/schroeder_bernstein.lean

@@ -92,36 +92,27 @@ end antisymm
 section wo
 parameters {ι : Type u} {β : ι → Type v}
 
-private def sets := {s : set (∀ i, β i) //
+@[reducible] private def sets := {s : set (∀ i, β i) |
   ∀ (x ∈ s) (y ∈ s) i, (x : ∀ i, β i) i = y i → x = y}
 
-private def sets.partial_order : partial_order sets :=
-{ le          := λ s t, s.1 ⊆ t.1,
-  le_refl     := λ s, subset.refl _,
-  le_trans    := λ s t u, subset.trans,
-  le_antisymm := λ s t h₁ h₂, subtype.eq (subset.antisymm h₁ h₂) }
-
-local attribute [instance] sets.partial_order
-
 theorem injective_min (I : nonempty ι) : ∃ i, nonempty (∀ j, β i ↪ β j) :=
-let ⟨⟨s, hs⟩, ms⟩ := show ∃s:sets, ∀a, s ≤ a → a = s, from
-  zorn.zorn_partial_order $ λ c hc,
-    ⟨⟨⋃₀ (subtype.val '' c),
-    λ x ⟨_, ⟨⟨s, hs⟩, sc, rfl⟩, xs⟩ y ⟨_, ⟨⟨t, ht⟩, tc, rfl⟩, yt⟩,
-      (hc.total sc tc).elim (λ h, ht _ (h xs) _ yt) (λ h, hs _ xs _ (h yt))⟩,
-    λ ⟨s, hs⟩ sc x h, ⟨s, ⟨⟨s, hs⟩, sc, rfl⟩, h⟩⟩ in
+let ⟨s, hs, ms⟩ := show ∃s∈sets, ∀a∈sets, s ⊆ a → a = s, from
+  zorn.zorn_subset sets (λ c hc hcc, ⟨⋃₀ c,
+    λ x ⟨p, hpc, hxp⟩ y ⟨q, hqc, hyq⟩ i hi,
+      (hcc.total hpc hqc).elim (λ h, hc hqc x (h hxp) y hyq i hi) (λ h, hc hpc x hxp y (h hyq) i hi),
+  λ _, subset_sUnion_of_mem⟩) in
 let ⟨i, e⟩ := show ∃ i, ∀ y, ∃ x ∈ s, (x : ∀ i, β i) i = y, from
   classical.by_contradiction $ λ h,
   have h : ∀ i, ∃ y, ∀ x ∈ s, (x : ∀ i, β i) i ≠ y,
-    by simpa [classical.not_forall] using h,
+    by simpa only [not_exists, classical.not_forall] using h,
   let ⟨f, hf⟩ := axiom_of_choice h in
-  have f ∈ (⟨s, hs⟩:sets).1, from
-    let s' : sets := ⟨insert f s, λ x hx y hy, begin
+  have f ∈ s, from
+    have insert f s ∈ sets := λ x hx y hy, begin
       cases hx; cases hy, {simp [hx, hy]},
       { subst x, exact λ i e, (hf i y hy e.symm).elim },
       { subst y, exact λ i e, (hf i x hx e).elim },
       { exact hs x hx y hy }
-    end⟩ in ms s' (subset_insert f s) ▸ mem_insert _ _,
+    end, ms _ this (subset_insert f s) ▸ mem_insert _ _,
   let ⟨i⟩ := I in hf i f this rfl in
 let ⟨f, hf⟩ := axiom_of_choice e in
 ⟨i, ⟨λ j, ⟨λ a, f a j, λ a b e',

order/order_iso.lean

@@ -289,18 +289,6 @@ instance (r : α → α → Prop) [is_well_order α r]
   (p : set α) : is_well_order p (subrel r p) :=
 order_embedding.is_well_order (subrel.order_embedding r p)
 
-instance [preorder α] (p : set α) : preorder p :=
-⟨subrel (≤) p, subrel (<) p, λ _, le_refl _, λ _ _ _, le_trans,
-λ _ _, lt_iff_le_not_le⟩
-
-instance [partial_order α] (p : set α) : partial_order p :=
-{ le_antisymm := λ _ _ hab hba, subtype.eq $ le_antisymm hab hba,
-  .. (infer_instance : preorder p) }
-
-instance [linear_order α] (p : set α) : linear_order p :=
-{ le_total := λ _ _, le_total _ _,
-  .. (infer_instance : partial_order p) }
-
 end subrel
 
 /-- Restrict the codomain of an order embedding -/

order/zorn.lean

@@ -225,19 +225,26 @@ theorem zorn_partial_order {α : Type u} [partial_order α]
 let ⟨m, hm⟩ := @zorn α (≤) h (assume a b c, le_trans) in
 ⟨m, assume a ha, le_antisymm (hm a ha) ha⟩
 
-theorem zorn_partial_order₀ {α : Type u} [partial_order α]
-  (s : set α) (x : α) (hxs : x ∈ s)
-  (ih : ∀ c ⊆ s, zorn.chain (≤) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) :
-  ∃ m ∈ s, ∀ z ∈ s, m ≤ z → z = m :=
-let ⟨m, hm⟩ := @zorn.zorn_partial_order s (subrel.partial_order s)
-  (λ c hc, classical.by_cases
-    (assume hce : c = ∅, hce.symm ▸ ⟨⟨x, hxs⟩, λ _, false.elim⟩)
-    (assume hce : c ≠ ∅, let ⟨m, hmc⟩ := set.exists_mem_of_ne_empty hce in
-      let ⟨ub, hubs, hub⟩ := ih (subtype.val '' c) (set.image_subset_iff.2 $ λ z hz, z.2)
-      (by rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq;
-        exact hc p hpc q hqc (mt (by rintro rfl; refl) hpq)) m.1 ⟨m, hmc, rfl⟩ in
-      ⟨⟨ub, hubs⟩, λ a hac, hub a.1 ⟨a, hac, rfl⟩⟩)) in
-⟨m.1, m.2, λ z hz hmz, congr_arg subtype.val $ hm ⟨z, hz⟩ hmz⟩
+theorem zorn_partial_order₀ {α : Type u} [partial_order α] (s : set α)
+  (ih : ∀ c ⊆ s, chain (≤) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub)
+  (x : α) (hxs : x ∈ s) : ∃ m ∈ s, x ≤ m ∧ ∀ z ∈ s, m ≤ z → z = m :=
+let ⟨⟨m, hms, hxm⟩, h⟩ := @zorn_partial_order {m // m ∈ s ∧ x ≤ m} _ (λ c hc, classical.by_cases
+  (assume hce : c = ∅, hce.symm ▸ ⟨⟨x, hxs, le_refl _⟩, λ _, false.elim⟩)
+  (assume hce : c ≠ ∅, let ⟨m, hmc⟩ := set.exists_mem_of_ne_empty hce in
+    let ⟨ub, hubs, hub⟩ := ih (subtype.val '' c) (image_subset_iff.2 $ λ z hzc, z.2.1)
+    (by rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq;
+      exact hc p hpc q hqc (mt (by rintro rfl; refl) hpq)) m.1 (mem_image_of_mem _ hmc) in
+    ⟨⟨ub, hubs, le_trans m.2.2 $ hub m.1 $ mem_image_of_mem _ hmc⟩, λ a hac, hub a.1 ⟨a, hac, rfl⟩⟩)) in
+⟨m, hms, hxm, λ z hzs hmz, congr_arg subtype.val $ h ⟨z, hzs, le_trans hxm hmz⟩ hmz⟩
+
+/-let ⟨m, hm⟩ := @zorn.zorn_partial_order s _ (λ c hc, classical.by_cases
+  (assume hce : c = ∅, hce.symm ▸ ⟨⟨x, hxs⟩, λ _, false.elim⟩)
+  (assume hce : c ≠ ∅, let ⟨m, hmc⟩ := set.exists_mem_of_ne_empty hce in
+    let ⟨ub, hubs, hub⟩ := ih (subtype.val '' c) (set.image_subset_iff.2 $ λ z hz, z.2)
+    (by rintro _ ⟨p, hpc, rfl⟩ _ ⟨q, hqc, rfl⟩ hpq;
+      exact hc p hpc q hqc (mt (by rintro rfl; refl) hpq)) m.1 ⟨m, hmc, rfl⟩ in
+    ⟨⟨ub, hubs⟩, λ a hac, hub a.1 ⟨a, hac, rfl⟩⟩)) in
+⟨m.1, m.2, λ z hz hmz, congr_arg subtype.val $ hm ⟨z, hz⟩ hmz⟩-/
 
 theorem zorn_subset {α : Type u} (S : set (set α))
   (h : ∀c ⊆ S, chain (⊆) c → ∃ub ∈ S, ∀ s ∈ c, s ⊆ ub) :

ring_theory/ideal_operations.lean

@@ -280,14 +280,12 @@ theorem radical_eq_Inf (I : ideal R) :
   radical I = Inf { J : ideal R | I ≤ J ∧ is_prime J } :=
 le_antisymm (le_Inf $ λ J hJ, hJ.2.radical_le_iff.2 hJ.1) $
 λ r hr, classical.by_contradiction $ λ hri,
-let S := { J | I ≤ J ∧ is_prime J } in
-let ⟨m, ⟨him, hrm⟩, hm⟩ := zorn.zorn_partial_order₀ { K | I ≤ K ∧ r ∉ radical K } I ⟨le_refl _, hri⟩
-  (λ c hc1 hc2 y hyc, ⟨Sup c, ⟨le_Sup_of_le hyc (hc1 hyc).1, λ ⟨n, hrnc⟩,
-    let ⟨y, hyc, hrny⟩ := submodule.mem_Sup_of_directed hrnc y hyc hc2.directed_on in
-    (hc1 hyc).2 ⟨n, hrny⟩⟩, λ _, le_Sup⟩) in
+let ⟨m, (hrm : r ∉ radical m), him, hm⟩ := zorn.zorn_partial_order₀ {K : ideal R | r ∉ radical K}
+  (λ c hc hcc y hyc, ⟨Sup c, λ ⟨n, hrnc⟩, let ⟨y, hyc, hrny⟩ :=
+      submodule.mem_Sup_of_directed hrnc y hyc hcc.directed_on in hc hyc ⟨n, hrny⟩,
+    λ z, le_Sup⟩) I hri in
 have ∀ x ∉ m, r ∈ radical (m ⊔ span {x}) := λ x hxm, classical.by_contradiction $ λ hrmx, hxm $
-  have _ := hm (m ⊔ span {x}) ⟨le_trans him le_sup_left, hrmx⟩ le_sup_left,
-  this ▸ (le_sup_right : _ ≤ m ⊔ span {x}) (subset_span $ set.mem_singleton _),
+  hm (m ⊔ span {x}) hrmx le_sup_left ▸ (le_sup_right : _ ≤ m ⊔ span {x}) (subset_span $ set.mem_singleton _),
 have is_prime m, from ⟨by rintro rfl; rw radical_top at hrm; exact hrm trivial,
   λ x y hxym, classical.or_iff_not_imp_left.2 $ λ hxm, classical.by_contradiction $ λ hym,
   let ⟨n, hrn⟩ := this _ hxm, ⟨p, hpm, q, hq, hpqrn⟩ := submodule.mem_sup.1 hrn, ⟨c, hcxq⟩ := mem_span_singleton'.1 hq in

ring_theory/ideals.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Chris Hughes, Mario Carneiro
 -/
-import tactic.ring linear_algebra.basic ring_theory.associated
+import linear_algebra.basic ring_theory.associated order.zorn
 
 universes u v
 variables {α : Type u} {β : Type v} [comm_ring α] {a b : α}
@@ -133,22 +133,13 @@ instance is_maximal.is_prime' (I : ideal α) : ∀ [H : I.is_maximal], I.is_prim
 theorem exists_le_maximal (I : ideal α) (hI : I ≠ ⊤) :
   ∃ M : ideal α, M.is_maximal ∧ I ≤ M :=
 begin
-  let C : set (set α) := {s | ∃ J:ideal α, J ≠ ⊤ ∧ ↑J = s},
-  rcases zorn.zorn_subset₀ C _ _ ⟨I, hI, rfl⟩ with ⟨_, ⟨M, M0, rfl⟩, IM, h⟩,
+  rcases zorn.zorn_partial_order₀ { J : ideal α | J ≠ ⊤ } _ I hI with ⟨M, M0, IM, h⟩,
   { refine ⟨M, ⟨M0, λ J hJ, by_contradiction $ λ J0, _⟩, IM⟩,
-    cases lt_iff_le_not_le.1 hJ with hJ₁ hJ₂,
-    exact hJ₂ (le_of_eq (h _ ⟨_, J0, rfl⟩ hJ₁) : _) },
-  { intros S SC cC S0,
-    choose I hp using show ∀ x : S, ↑x ∈ C, from λ ⟨x, xs⟩, SC xs,
-    refine ⟨_, ⟨⨆ s:S, span s, _, rfl⟩, _⟩,
-    rw [ne_top_iff_one, submodule.mem_supr_of_directed
-      (coe_nonempty_iff_ne_empty.2 S0), not_exists],
-    { rintro ⟨_, xs⟩, rcases SC xs with ⟨J, J0, rfl⟩,
-      simp, exact J.ne_top_iff_one.1 J0 },
-    { rintro ⟨i, iS⟩ ⟨j, jS⟩,
-      rcases cC.directed iS jS with ⟨k, kS, ik, jk⟩,
-      exact ⟨⟨_, kS⟩, span_mono ik, span_mono jk⟩ },
-    { exact λ s ss, span_le.1 (le_supr (λ s:S, span (s:set α)) ⟨s, ss⟩) } },
+    cases h J J0 (le_of_lt hJ), exact lt_irrefl _ hJ },
+  { intros S SC cC I IS,
+    refine ⟨Sup S, λ H, _, λ _, le_Sup⟩,
+    rcases submodule.mem_Sup_of_directed ((eq_top_iff_one _).1 H) I IS cC.directed_on with ⟨J, JS, J0⟩,
+    exact SC JS ((eq_top_iff_one _).2 J0) }
 end
 
 end ideal