chore(order/zorn): Review (#12175)

Lemma renames

src/analysis/convex/basic.lean

@@ -1034,11 +1034,11 @@ Relates `convex` and `ord_connected`.
 section
 
 lemma set.ord_connected.convex_of_chain [ordered_semiring 𝕜] [ordered_add_comm_monoid E]
-  [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) (h : zorn.chain (≤) s) :
+  [module 𝕜 E] [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) (h : is_chain (≤) s) :
   convex 𝕜 s :=
 begin
   refine convex_iff_segment_subset.mpr (λ x y hx hy, _),
-  obtain hxy | hyx := h.total_of_refl hx hy,
+  obtain hxy | hyx := h.total hx hy,
   { exact (segment_subset_Icc hxy).trans (hs.out hx hy) },
   { rw segment_symm,
     exact (segment_subset_Icc hyx).trans (hs.out hy hx) }
@@ -1047,7 +1047,7 @@ end
 lemma set.ord_connected.convex [ordered_semiring 𝕜] [linear_ordered_add_comm_monoid E] [module 𝕜 E]
   [ordered_smul 𝕜 E] {s : set E} (hs : s.ord_connected) :
   convex 𝕜 s :=
-hs.convex_of_chain (zorn.chain_of_trichotomous s)
+hs.convex_of_chain $ is_chain_of_trichotomous s
 
 lemma convex_iff_ord_connected [linear_ordered_field 𝕜] {s : set 𝕜} :
   convex 𝕜 s ↔ s.ord_connected :=

src/analysis/convex/cone.lean

@@ -505,7 +505,7 @@ theorem exists_top (p : linear_pmap ℝ E ℝ)
   ∃ q ≥ p, q.domain = ⊤ ∧ ∀ x : q.domain, (x : E) ∈ s → 0 ≤ q x :=
 begin
   replace hp_nonneg : p ∈ { p | _ }, by { rw mem_set_of_eq, exact hp_nonneg },
-  obtain ⟨q, hqs, hpq, hq⟩ := zorn.zorn_nonempty_partial_order₀ _ _ _ hp_nonneg,
+  obtain ⟨q, hqs, hpq, hq⟩ := zorn_nonempty_partial_order₀ _ _ _ hp_nonneg,
   { refine ⟨q, hpq, _, hqs⟩,
     contrapose! hq,
     rcases step s q hqs _ hq with ⟨r, hqr, hr⟩,

src/analysis/inner_product_space/basic.lean

@@ -886,7 +886,7 @@ containing it. -/
 lemma exists_maximal_orthonormal {s : set E} (hs : orthonormal 𝕜 (coe : s → E)) :
   ∃ w ⊇ s, orthonormal 𝕜 (coe : w → E) ∧ ∀ u ⊇ w, orthonormal 𝕜 (coe : u → E) → u = w :=
 begin
-  rcases zorn.zorn_subset_nonempty {b | orthonormal 𝕜 (coe : b → E)} _ _ hs  with ⟨b, bi, sb, h⟩,
+  obtain ⟨b, bi, sb, h⟩ := zorn_subset_nonempty {b | orthonormal 𝕜 (coe : b → E)} _ _ hs,
   { refine ⟨b, sb, bi, _⟩,
     exact λ u hus hu, h u hu hus },
   { refine λ c hc cc c0, ⟨⋃₀ c, _, _⟩,

src/data/set/pairwise.lean

@@ -157,10 +157,19 @@ lemma pairwise_insert :
 by simp only [insert_eq, pairwise_union, pairwise_singleton, true_and,
   mem_singleton_iff, forall_eq]
 
+lemma pairwise.insert (hs : s.pairwise r) (h : ∀ b ∈ s, a ≠ b → r a b ∧ r b a) :
+  (insert a s).pairwise r :=
+pairwise_insert.2 ⟨hs, h⟩
+
 lemma pairwise_insert_of_symmetric (hr : symmetric r) :
   (insert a s).pairwise r ↔ s.pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b :=
 by simp only [pairwise_insert, hr.iff a, and_self]
 
+lemma pairwise.insert_of_symmetric (hs : s.pairwise r) (hr : symmetric r)
+  (h : ∀ b ∈ s, a ≠ b → r a b) :
+  (insert a s).pairwise r :=
+(pairwise_insert_of_symmetric hr).2 ⟨hs, h⟩
+
 lemma pairwise_pair : set.pairwise {a, b} r ↔ (a ≠ b → r a b ∧ r b a) :=
 by simp [pairwise_insert]
 

src/field_theory/adjoin.lean

@@ -673,16 +673,16 @@ noncomputable instance : inhabited (lifts F E K) := ⟨⊥⟩
 lemma lifts.eq_of_le {x y : lifts F E K} (hxy : x ≤ y) (s : x.1) :
   x.2 s = y.2 ⟨s, hxy.1 s.mem⟩ := hxy.2 s ⟨s, hxy.1 s.mem⟩ rfl
 
-lemma lifts.exists_max_two {c : set (lifts F E K)} {x y : lifts F E K} (hc : zorn.chain (≤) c)
+lemma lifts.exists_max_two {c : set (lifts F E K)} {x y : lifts F E K} (hc : is_chain (≤) c)
   (hx : x ∈ set.insert ⊥ c) (hy : y ∈ set.insert ⊥ c) :
   ∃ z : lifts F E K, z ∈ set.insert ⊥ c ∧ x ≤ z ∧ y ≤ z :=
 begin
-  cases (zorn.chain_insert hc (λ _ _ _, or.inl bot_le)).total_of_refl hx hy with hxy hyx,
+  cases (hc.insert $ λ _ _ _, or.inl bot_le).total hx hy with hxy hyx,
   { exact ⟨y, hy, hxy, le_refl y⟩ },
   { exact ⟨x, hx, le_refl x, hyx⟩ },
 end
 
-lemma lifts.exists_max_three {c : set (lifts F E K)} {x y z : lifts F E K} (hc : zorn.chain (≤) c)
+lemma lifts.exists_max_three {c : set (lifts F E K)} {x y z : lifts F E K} (hc : is_chain (≤) c)
   (hx : x ∈ set.insert ⊥ c) (hy : y ∈ set.insert ⊥ c) (hz : z ∈ set.insert ⊥ c) :
   ∃ w  : lifts F E K, w ∈ set.insert ⊥ c ∧ x ≤ w ∧ y ≤ w ∧ z ≤ w :=
 begin
@@ -692,7 +692,7 @@ begin
 end
 
 /-- An upper bound on a chain of lifts -/
-def lifts.upper_bound_intermediate_field {c : set (lifts F E K)} (hc : zorn.chain (≤) c) :
+def lifts.upper_bound_intermediate_field {c : set (lifts F E K)} (hc : is_chain (≤) c) :
   intermediate_field F E :=
 { carrier := λ s, ∃ x : (lifts F E K), x ∈ set.insert ⊥ c ∧ (s ∈ x.1 : Prop),
   zero_mem' := ⟨⊥, set.mem_insert ⊥ c, zero_mem ⊥⟩,
@@ -710,7 +710,7 @@ def lifts.upper_bound_intermediate_field {c : set (lifts F E K)} (hc : zorn.chai
   algebra_map_mem' := λ s, ⟨⊥, set.mem_insert ⊥ c, algebra_map_mem ⊥ s⟩ }
 
 /-- The lift on the upper bound on a chain of lifts -/
-noncomputable def lifts.upper_bound_alg_hom {c : set (lifts F E K)} (hc : zorn.chain (≤) c) :
+noncomputable def lifts.upper_bound_alg_hom {c : set (lifts F E K)} (hc : is_chain (≤) c) :
   lifts.upper_bound_intermediate_field hc →ₐ[F] K :=
 { to_fun := λ s, (classical.some s.mem).2 ⟨s, (classical.some_spec s.mem).2⟩,
   map_zero' := alg_hom.map_zero _,
@@ -732,11 +732,11 @@ noncomputable def lifts.upper_bound_alg_hom {c : set (lifts F E K)} (hc : zorn.c
   commutes' := λ _, alg_hom.commutes _ _ }
 
 /-- An upper bound on a chain of lifts -/
-noncomputable def lifts.upper_bound {c : set (lifts F E K)} (hc : zorn.chain (≤) c) :
+noncomputable def lifts.upper_bound {c : set (lifts F E K)} (hc : is_chain (≤) c) :
   lifts F E K :=
 ⟨lifts.upper_bound_intermediate_field hc, lifts.upper_bound_alg_hom hc⟩
 
-lemma lifts.exists_upper_bound (c : set (lifts F E K)) (hc : zorn.chain (≤) c) :
+lemma lifts.exists_upper_bound (c : set (lifts F E K)) (hc : is_chain (≤) c) :
   ∃ ub, ∀ a ∈ c, a ≤ ub :=
 ⟨lifts.upper_bound hc,
 begin
@@ -786,7 +786,7 @@ lemma alg_hom_mk_adjoin_splits
   (hK : ∀ s ∈ S, is_integral F (s : E) ∧ (minpoly F s).splits (algebra_map F K)) :
   nonempty (adjoin F S →ₐ[F] K) :=
 begin
-  obtain ⟨x : lifts F E K, hx⟩ := zorn.zorn_partial_order lifts.exists_upper_bound,
+  obtain ⟨x : lifts F E K, hx⟩ := zorn_partial_order lifts.exists_upper_bound,
   refine ⟨alg_hom.mk (λ s, x.2 ⟨s, adjoin_le_iff.mpr (λ s hs, _) s.mem⟩) x.2.map_one (λ s t,
     x.2.map_mul ⟨s, _⟩ ⟨t, _⟩) x.2.map_zero (λ s t, x.2.map_add ⟨s, _⟩ ⟨t, _⟩) x.2.commutes⟩,
   rcases (x.exists_lift_of_splits (hK s hs).1 (hK s hs).2) with ⟨y, h1, h2⟩,

src/field_theory/is_alg_closed/basic.lean

@@ -179,7 +179,7 @@ variables {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [algebra K
 
 variables (K L M)
 include hL
-open zorn subalgebra alg_hom function
+open subalgebra alg_hom function
 
 /-- This structure is used to prove the existence of a homomorphism from any algebraic extension
 into an algebraic closure -/
@@ -215,7 +215,7 @@ instance : preorder (subfield_with_hom K L M hL) :=
 open lattice
 
 lemma maximal_subfield_with_hom_chain_bounded (c : set (subfield_with_hom K L M hL))
-  (hc : chain (≤) c) :
+  (hc : is_chain (≤) c) :
   ∃ ub : subfield_with_hom K L M hL, ∀ N, N ∈ c → N ≤ ub :=
 if hcn : c.nonempty then
 let ub : subfield_with_hom K L M hL :=
@@ -246,7 +246,7 @@ variables (hL M)
 
 lemma exists_maximal_subfield_with_hom : ∃ E : subfield_with_hom K L M hL,
   ∀ N, E ≤ N → N ≤ E :=
-zorn.exists_maximal_of_chains_bounded
+exists_maximal_of_chains_bounded
   maximal_subfield_with_hom_chain_bounded (λ _ _ _, le_trans)
 
 /-- The maximal `subfield_with_hom`. We later prove that this is equal to `⊤`. -/

src/group_theory/sylow.lean

@@ -73,11 +73,11 @@ end sylow
   Every `p`-subgroup is contained in a Sylow `p`-subgroup. -/
 lemma is_p_group.exists_le_sylow {P : subgroup G} (hP : is_p_group p P) :
   ∃ Q : sylow p G, P ≤ Q :=
-exists.elim (zorn.zorn_nonempty_partial_order₀ {Q : subgroup G | is_p_group p Q} (λ c hc1 hc2 Q hQ,
+exists.elim (zorn_nonempty_partial_order₀ {Q : subgroup G | is_p_group p Q} (λ c hc1 hc2 Q hQ,
 ⟨ { carrier := ⋃ (R : c), R,
     one_mem' := ⟨Q, ⟨⟨Q, hQ⟩, rfl⟩, Q.one_mem⟩,
     inv_mem' := λ g ⟨_, ⟨R, rfl⟩, hg⟩, ⟨R, ⟨R, rfl⟩, R.1.inv_mem hg⟩,
-    mul_mem' := λ g h ⟨_, ⟨R, rfl⟩, hg⟩ ⟨_, ⟨S, rfl⟩, hh⟩, (hc2.total_of_refl R.2 S.2).elim
+    mul_mem' := λ g h ⟨_, ⟨R, rfl⟩, hg⟩ ⟨_, ⟨S, rfl⟩, hh⟩, (hc2.total R.2 S.2).elim
       (λ T, ⟨S, ⟨S, rfl⟩, S.1.mul_mem (T hg) hh⟩) (λ T, ⟨R, ⟨R, rfl⟩, R.1.mul_mem hg (T hh)⟩) },
   λ ⟨g, _, ⟨S, rfl⟩, hg⟩, by
   { refine exists_imp_exists (λ k hk, _) (hc1 S.2 ⟨g, hg⟩),

src/linear_algebra/linear_independent.lean

@@ -805,7 +805,7 @@ begin
   let indep : set ι → Prop := λ I, linear_independent R (s ∘ coe : I → M),
   let X := { I : set ι // indep I },
   let r : X → X → Prop := λ I J, I.1 ⊆ J.1,
-  have key : ∀ c : set X, zorn.chain r c → indep (⋃ (I : X) (H : I ∈ c), I),
+  have key : ∀ c : set X, is_chain r c → indep (⋃ (I : X) (H : I ∈ c), I),
   { intros c hc,
     dsimp [indep],
     rw [linear_independent_comp_subtype],
@@ -818,7 +818,7 @@ begin
     exact linear_independent_comp_subtype.mp I.2 f hI hsum },
   have trans : transitive r := λ I J K, set.subset.trans,
   obtain ⟨⟨I, hli : indep I⟩, hmax : ∀ a, r ⟨I, hli⟩ a → r a ⟨I, hli⟩⟩ :=
-    @zorn.exists_maximal_of_chains_bounded _ r
+    @exists_maximal_of_chains_bounded _ r
     (λ c hc, ⟨⟨⋃ I ∈ c, (I : set ι), key c hc⟩, λ I, set.subset_bUnion_of_mem⟩) trans,
   exact ⟨I, hli, λ J hsub hli, set.subset.antisymm hsub (hmax ⟨J, hli⟩ hsub)⟩,
 end
@@ -1171,7 +1171,7 @@ by rw [linear_independent_fin_succ, linear_independent_unique_iff, range_unique,
 lemma exists_linear_independent_extension (hs : linear_independent K (coe : s → V)) (hst : s ⊆ t) :
   ∃b⊆t, s ⊆ b ∧ t ⊆ span K b ∧ linear_independent K (coe : b → V) :=
 begin
-  rcases zorn.zorn_subset_nonempty {b | b ⊆ t ∧ linear_independent K (coe : b → V)} _ _
+  rcases zorn_subset_nonempty {b | b ⊆ t ∧ linear_independent K (coe : b → V)} _ _
     ⟨hst, hs⟩ with ⟨b, ⟨bt, bi⟩, sb, h⟩,
   { refine ⟨b, bt, sb, λ x xt, _, bi⟩,
     by_contra hn,

src/measure_theory/covering/vitali.lean

@@ -72,7 +72,7 @@ begin
     ∧ ∀ a ∈ t, ∀ b ∈ u, set.nonempty (a ∩ b) → ∃ c ∈ u, (a ∩ c).nonempty ∧ δ a ≤ τ * δ c},
   -- By Zorn, choose a maximal family in the good set `T` of disjoint families.
   obtain ⟨u, uT, hu⟩ : ∃ u ∈ T, ∀ v ∈ T, u ⊆ v → v = u,
-  { refine zorn.zorn_subset _ (λ U UT hU, _),
+  { refine zorn_subset _ (λ U UT hU, _),
     refine ⟨⋃₀ U, _, λ s hs, subset_sUnion_of_mem hs⟩,
     simp only [set.sUnion_subset_iff, and_imp, exists_prop, forall_exists_index,
                 set.mem_set_of_eq],

src/order/compactly_generated.lean

@@ -341,16 +341,15 @@ begin
   exact ⟨λ x, ⟨{x}, ⟨λ x _, h x, Sup_singleton⟩⟩⟩,
 end
 
-/-- A compact element `k` has the property that any `b < `k lies below a "maximal element below
+/-- A compact element `k` has the property that any `b < k` lies below a "maximal element below
 `k`", which is to say `[⊥, k]` is coatomic. -/
 theorem Iic_coatomic_of_compact_element {k : α} (h : is_compact_element k) :
   is_coatomic (set.Iic k) :=
 ⟨λ ⟨b, hbk⟩, begin
   by_cases htriv : b = k,
   { left, ext, simp only [htriv, set.Iic.coe_top, subtype.coe_mk], },
   right,
-  rcases zorn.zorn_nonempty_partial_order₀ (set.Iio k) _ b (lt_of_le_of_ne hbk htriv)
-    with ⟨a, a₀, ba, h⟩,
+  obtain ⟨a, a₀, ba, h⟩ := zorn_nonempty_partial_order₀ (set.Iio k) _ b (lt_of_le_of_ne hbk htriv),
   { refine ⟨⟨a, le_of_lt a₀⟩, ⟨ne_of_lt a₀, λ c hck, by_contradiction $ λ c₀, _⟩, ba⟩,
     cases h c.1 (lt_of_le_of_ne c.2 (λ con, c₀ (subtype.ext con))) hck.le,
     exact lt_irrefl _ hck, },
@@ -410,7 +409,7 @@ end, λ _, and.left⟩⟩
 /-- See Theorem 6.6, Călugăreanu -/
 theorem is_complemented_of_Sup_atoms_eq_top (h : Sup {a : α | is_atom a} = ⊤) : is_complemented α :=
 ⟨λ b, begin
-  obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := zorn.zorn_subset
+  obtain ⟨s, ⟨s_ind, b_inf_Sup_s, s_atoms⟩, s_max⟩ := zorn_subset
     {s : set α | complete_lattice.set_independent s ∧ b ⊓ Sup s = ⊥ ∧ ∀ a ∈ s, is_atom a} _,
   { refine ⟨Sup s, le_of_eq b_inf_Sup_s, _⟩,
     rw [← h, Sup_le_iff],

src/order/extension.lean

@@ -25,7 +25,7 @@ theorem extend_partial_order {α : Type u} (r : α → α → Prop) [is_partial_
   ∃ (s : α → α → Prop) (_ : is_linear_order α s), r ≤ s :=
 begin
   let S := {s | is_partial_order α s},
-  have hS : ∀ c, c ⊆ S → zorn.chain (≤) c → ∀ y ∈ c, (∃ ub ∈ S, ∀ z ∈ c, z ≤ ub),
+  have hS : ∀ c, c ⊆ S → is_chain (≤) c → ∀ y ∈ c, (∃ ub ∈ S, ∀ z ∈ c, z ≤ ub),
   { rintro c hc₁ hc₂ s hs,
     haveI := (hc₁ hs).1,
     refine ⟨Sup c, _, λ z hz, le_Sup hz⟩,
@@ -35,16 +35,16 @@ begin
     { rintro x y z ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩,
       haveI : is_partial_order _ _ := hc₁ h₁s₁,
       haveI : is_partial_order _ _ := hc₁ h₁s₂,
-      cases hc₂.total_of_refl h₁s₁ h₁s₂,
+      cases hc₂.total h₁s₁ h₁s₂,
       { exact ⟨s₂, h₁s₂, trans (h _ _ h₂s₁) h₂s₂⟩ },
       { exact ⟨s₁, h₁s₁, trans h₂s₁ (h _ _ h₂s₂)⟩ } },
     { rintro x y ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩,
       haveI : is_partial_order _ _ := hc₁ h₁s₁,
       haveI : is_partial_order _ _ := hc₁ h₁s₂,
-      cases hc₂.total_of_refl h₁s₁ h₁s₂,
+      cases hc₂.total h₁s₁ h₁s₂,
       { exact antisymm (h _ _ h₂s₁) h₂s₂ },
       { apply antisymm h₂s₁ (h _ _ h₂s₂) } } },
-  obtain ⟨s, hs₁ : is_partial_order _ _, rs, hs₂⟩ := zorn.zorn_nonempty_partial_order₀ S hS r ‹_›,
+  obtain ⟨s, hs₁ : is_partial_order _ _, rs, hs₂⟩ := zorn_nonempty_partial_order₀ S hS r ‹_›,
   resetI,
   refine ⟨s, { total := _ }, rs⟩,
   intros x y,

src/order/filter/ultrafilter.lean

@@ -22,7 +22,7 @@ In this file we define
 universes u v
 variables {α : Type u} {β : Type v}
 
-open set zorn filter function
+open set filter function
 open_locale classical filter
 
 /-- An ultrafilter is a minimal (maximal in the set order) proper filter. -/
@@ -195,13 +195,13 @@ begin
   let r : τ → τ → Prop := λt₁ t₂, t₂.val ≤ t₁.val,
   haveI                := nonempty_of_ne_bot f,
   let top : τ          := ⟨f, h, le_refl f⟩,
-  let sup : Π(c:set τ), chain r c → τ :=
+  let sup : Π(c:set τ), is_chain r c → τ :=
     λc hc, ⟨⨅a:{a:τ // a ∈ insert top c}, a.1,
       infi_ne_bot_of_directed
-        (directed_of_chain $ chain_insert hc $ λ ⟨b, _, hb⟩ _ _, or.inl hb)
+        (is_chain.directed $ hc.insert $ λ ⟨b, _, hb⟩ _ _, or.inl hb)
         (assume ⟨⟨a, ha, _⟩, _⟩, ha),
       infi_le_of_le ⟨top, mem_insert _ _⟩ le_rfl⟩,
-  have : ∀c (hc: chain r c) a (ha : a ∈ c), r a (sup c hc),
+  have : ∀ c (hc : is_chain r c) a (ha : a ∈ c), r a (sup c hc),
     from assume c hc a ha, infi_le_of_le ⟨a, mem_insert_of_mem _ ha⟩ le_rfl,
   have : (∃ (u : τ), ∀ (a : τ), r u a → r a u),
     from exists_maximal_of_chains_bounded (assume c hc, ⟨sup c hc, this c hc⟩)