refactor(order/well_founded): ditch well_founded_iff_has_min' and well_founded_iff_has_max' (#15071)

vihdzp · vihdzp · commit 210657c4ea4a · 2023-03-31T22:20:08.000Z
The predicate `x ≤ y → y = x` is no more convenient than `¬ x &lt; y`. For this reason, we ditch `well_founded.well_founded_iff_has_min'` and `well_founded.well_founded_iff_has_max'` in favor of `well_founded.well_founded_iff_has_min` (or in some cases, just `well_founded.has_min`. We also remove the misplaced lemma `well_founded.eq_iff_not_lt_of_le`, and we golf the theorems that used the removed theorems.

The lemma `well_founded.well_founded_iff_has_min` has a misleading name when applied on `well_founded (&gt;)`, and mildly screws over dot notation and rewriting by virtue of using `&gt;`, but a future refactor will fix this.
diff --git a/src/algebra/lie/engel.lean b/src/algebra/lie/engel.lean
@@ -259,14 +259,11 @@ begin
     exact nontrivial_max_triv_of_is_nilpotent R K (L' ⧸ K.to_lie_submodule), },
   haveI _i5 : is_noetherian R L' :=
     is_noetherian_of_surjective L _ (linear_map.range_range_restrict (to_endomorphism R L M)),
-  obtain ⟨K, hK₁, hK₂⟩ :=
-    well_founded.well_founded_iff_has_max'.mp (lie_subalgebra.well_founded_of_noetherian R L') s hs,
+  obtain ⟨K, hK₁, hK₂⟩ := (lie_subalgebra.well_founded_of_noetherian R L').has_min s hs,
   have hK₃ : K = ⊤,
   { by_contra contra,
     obtain ⟨K', hK'₁, hK'₂⟩ := this K hK₁ contra,
-    specialize hK₂ K' hK'₁ (le_of_lt hK'₂),
-    replace hK'₂ := (ne_of_lt hK'₂).symm,
-    contradiction, },
+    exact hK₂ K' hK'₁ hK'₂, },
   exact hK₃ ▸ hK₁,
 end
 
diff --git a/src/linear_algebra/free_module/pid.lean b/src/linear_algebra/free_module/pid.lean
@@ -59,21 +59,21 @@ variables {ι : Type*} (b : basis ι R M)
 open submodule.is_principal submodule
 
 lemma eq_bot_of_generator_maximal_map_eq_zero (b : basis ι R M) {N : submodule R M}
-  {ϕ : M →ₗ[R] R} (hϕ : ∀ (ψ : M →ₗ[R] R), N.map ϕ ≤ N.map ψ → N.map ψ = N.map ϕ)
+  {ϕ : M →ₗ[R] R} (hϕ : ∀ (ψ : M →ₗ[R] R), ¬ N.map ϕ < N.map ψ)
   [(N.map ϕ).is_principal] (hgen : generator (N.map ϕ) = (0 : R)) : N = ⊥ :=
 begin
   rw submodule.eq_bot_iff,
   intros x hx,
   refine b.ext_elem (λ i, _),
   rw (eq_bot_iff_generator_eq_zero _).mpr hgen at hϕ,
   rw [linear_equiv.map_zero, finsupp.zero_apply],
-  exact (submodule.eq_bot_iff _).mp (hϕ ((finsupp.lapply i) ∘ₗ ↑b.repr) bot_le) _ ⟨x, hx, rfl⟩
+  exact (submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 $ hϕ ((finsupp.lapply i) ∘ₗ ↑b.repr)) _
+    ⟨x, hx, rfl⟩
 end
 
 lemma eq_bot_of_generator_maximal_submodule_image_eq_zero {N O : submodule R M} (b : basis ι R O)
   (hNO : N ≤ O)
-  {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ϕ.submodule_image N ≤ ψ.submodule_image N →
-    ψ.submodule_image N = ϕ.submodule_image N)
+  {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ¬ ϕ.submodule_image N < ψ.submodule_image N)
   [(ϕ.submodule_image N).is_principal] (hgen : generator (ϕ.submodule_image N) = 0) :
   N = ⊥ :=
 begin
@@ -82,7 +82,7 @@ begin
   refine congr_arg coe (show (⟨x, hNO hx⟩ : O) = 0, from b.ext_elem (λ i, _)),
   rw (eq_bot_iff_generator_eq_zero _).mpr hgen at hϕ,
   rw [linear_equiv.map_zero, finsupp.zero_apply],
-  refine (submodule.eq_bot_iff _).mp (hϕ ((finsupp.lapply i) ∘ₗ ↑b.repr) bot_le) _ _,
+  refine (submodule.eq_bot_iff _).mp (not_bot_lt_iff.1 $ hϕ ((finsupp.lapply i) ∘ₗ ↑b.repr)) _ _,
   exact (linear_map.mem_submodule_image_of_le hNO).mpr ⟨x, hx, rfl⟩
 end
 
@@ -115,8 +115,7 @@ variables {M : Type*} [add_comm_group M] [module R M] {b : ι → M}
 open submodule.is_principal
 
 lemma generator_maximal_submodule_image_dvd {N O : submodule R M} (hNO : N ≤ O)
-  {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ϕ.submodule_image N ≤ ψ.submodule_image N →
-    ψ.submodule_image N = ϕ.submodule_image N)
+  {ϕ : O →ₗ[R] R} (hϕ : ∀ (ψ : O →ₗ[R] R), ¬ ϕ.submodule_image N < ψ.submodule_image N)
   [(ϕ.submodule_image N).is_principal]
   (y : M) (yN : y ∈ N) (ϕy_eq : ϕ ⟨y, hNO yN⟩ = generator (ϕ.submodule_image N))
   (ψ : O →ₗ[R] R) : generator (ϕ.submodule_image N) ∣ ψ ⟨y, hNO yN⟩ :=
@@ -144,7 +143,7 @@ begin
   refine le_antisymm (this.trans (le_of_eq _))
     (ideal.span_singleton_le_span_singleton.mpr d_dvd_left),
   rw span_singleton_generator,
-  refine hϕ ψ' (le_trans _ this),
+  apply (le_trans _ this).eq_of_not_gt (hϕ ψ'),
   rw [← span_singleton_generator (ϕ.submodule_image N)],
   exact ideal.span_singleton_le_span_singleton.mpr d_dvd_left,
   { exact subset_span (mem_insert _ _) }
@@ -175,8 +174,7 @@ lemma submodule.basis_of_pid_aux [finite ι] {O : Type*} [add_comm_group O] [mod
 begin
   -- Let `ϕ` be a maximal projection of `M` onto `R`, in the sense that there is
   -- no `ψ` whose image of `N` is larger than `ϕ`'s image of `N`.
-  have : ∃ ϕ : M →ₗ[R] R, ∀ (ψ : M →ₗ[R] R),
-    ϕ.submodule_image N ≤ ψ.submodule_image N → ψ.submodule_image N = ϕ.submodule_image N,
+  have : ∃ ϕ : M →ₗ[R] R, ∀ (ψ : M →ₗ[R] R), ¬ ϕ.submodule_image N < ψ.submodule_image N,
   { obtain ⟨P, P_eq, P_max⟩ := set_has_maximal_iff_noetherian.mpr
         (infer_instance : is_noetherian R R) _
         (show (set.range (λ ψ : M →ₗ[R] R, ψ.submodule_image N)).nonempty,
diff --git a/src/order/basic.lean b/src/order/basic.lean
@@ -227,6 +227,9 @@ le_iff_lt_or_eq.trans or.comm
 lemma lt_iff_le_and_ne [partial_order α] {a b : α} : a < b ↔ a ≤ b ∧ a ≠ b :=
 ⟨λ h, ⟨le_of_lt h, ne_of_lt h⟩, λ ⟨h1, h2⟩, h1.lt_of_ne h2⟩
 
+lemma eq_iff_not_lt_of_le {α} [partial_order α] {x y : α} : x ≤ y → y = x ↔ ¬ x < y :=
+by rw [lt_iff_le_and_ne, not_and, not_not, eq_comm]
+
 -- See Note [decidable namespace]
 protected lemma decidable.eq_iff_le_not_lt [partial_order α] [@decidable_rel α (≤)]
   {a b : α} : a = b ↔ a ≤ b ∧ ¬ a < b :=
diff --git a/src/order/compactly_generated.lean b/src/order/compactly_generated.lean
@@ -190,18 +190,16 @@ end
 
 lemma well_founded.is_Sup_finite_compact (h : well_founded ((>) : α → α → Prop)) :
   is_Sup_finite_compact α :=
-begin
-  intros s,
-  let p : set α := { x | ∃ (t : finset α), ↑t ⊆ s ∧ t.sup id = x },
-  have hp : p.nonempty, { use [⊥, ∅], simp, },
-  obtain ⟨m, ⟨t, ⟨ht₁, ht₂⟩⟩, hm⟩ := well_founded.well_founded_iff_has_max'.mp h p hp,
-  use t, simp only [ht₁, ht₂, true_and], apply le_antisymm,
-  { apply Sup_le, intros y hy, classical,
-    have hy' : (insert y t).sup id ∈ p,
-    { use insert y t, simp, rw set.insert_subset, exact ⟨hy, ht₁⟩, },
-    have hm' : m ≤ (insert y t).sup id, { rw ← ht₂, exact finset.sup_mono (t.subset_insert y), },
-    rw ← hm _ hy' hm', simp, },
-  { rw [← ht₂, finset.sup_id_eq_Sup], exact Sup_le_Sup ht₁, },
+λ s, begin
+  obtain ⟨m, ⟨t, ⟨ht₁, rfl⟩⟩, hm⟩ := well_founded.well_founded_iff_has_min.mp h
+    {x | ∃ t : finset α, ↑t ⊆ s ∧ t.sup id = x} ⟨⊥, ∅, by simp⟩,
+  refine ⟨t, ht₁, (Sup_le (λ y hy, _)).antisymm _⟩,
+  { classical,
+    rw eq_of_le_of_not_lt (finset.sup_mono (t.subset_insert y))
+      (hm _ ⟨insert y t, by simp [set.insert_subset, hy, ht₁]⟩),
+    simp },
+  { rw finset.sup_id_eq_Sup,
+    exact Sup_le_Sup ht₁ },
 end
 
 lemma is_Sup_finite_compact.is_sup_closed_compact (h : is_Sup_finite_compact α) :
diff --git a/src/order/order_iso_nat.lean b/src/order/order_iso_nat.lean
@@ -226,17 +226,9 @@ a (monotonic_sequence_limit_index a)
 lemma well_founded.supr_eq_monotonic_sequence_limit [complete_lattice α]
   (h : well_founded ((>) : α → α → Prop)) (a : ℕ →o α) : supr a = monotonic_sequence_limit a :=
 begin
-  suffices : (⨆ (m : ℕ), a m) ≤ monotonic_sequence_limit a,
-  { exact le_antisymm this (le_supr a _), },
-  apply supr_le,
-  intros m,
-  by_cases hm : m ≤ monotonic_sequence_limit_index a,
-  { exact a.monotone hm, },
-  { replace hm := le_of_not_le hm,
-    let S := { n | ∀ m, n ≤ m → a n = a m },
-    have hInf : Inf S ∈ S,
-    { refine nat.Inf_mem _, rw well_founded.monotone_chain_condition at h, exact h a, },
-    change Inf S ≤ m at hm,
-    change a m ≤ a (Inf S),
-    rw hInf m hm, },
+  apply (supr_le (λ m, _)).antisymm (le_supr a _),
+  cases le_or_lt m (monotonic_sequence_limit_index a) with hm hm,
+  { exact a.monotone hm },
+  { cases well_founded.monotone_chain_condition'.1 h a with n hn,
+    exact (nat.Inf_mem ⟨n, λ k hk, (a.mono hk).eq_of_not_lt (hn k hk)⟩ m hm.le).ge }
 end
diff --git a/src/order/well_founded.lean b/src/order/well_founded.lean
@@ -72,26 +72,6 @@ begin
   exact hm' y hy' hy
 end
 
-lemma eq_iff_not_lt_of_le {α} [partial_order α] {x y : α} : x ≤ y → y = x ↔ ¬ x < y :=
-begin
-  split,
-  { intros xle nge,
-    cases le_not_le_of_lt nge,
-    rw xle left at nge,
-    exact lt_irrefl x nge },
-  { intros ngt xle,
-    contrapose! ngt,
-    exact lt_of_le_of_ne xle (ne.symm ngt) }
-end
-
-theorem well_founded_iff_has_max' [partial_order α] : (well_founded ((>) : α → α → Prop) ↔
-  ∀ (p : set α), p.nonempty → ∃ m ∈ p, ∀ x ∈ p, m ≤ x → x = m) :=
-by simp only [eq_iff_not_lt_of_le, well_founded_iff_has_min]
-
-theorem well_founded_iff_has_min' [partial_order α] : (well_founded (has_lt.lt : α → α → Prop)) ↔
-  ∀ (p : set α), p.nonempty → ∃ m ∈ p, ∀ x ∈ p, x ≤ m → x = m :=
-@well_founded_iff_has_max' αᵒᵈ _
-
 open set
 /-- The supremum of a bounded, well-founded order -/
 protected noncomputable def sup {r : α → α → Prop} (wf : well_founded r) (s : set α)
diff --git a/src/ring_theory/artinian.lean b/src/ring_theory/artinian.lean
@@ -181,12 +181,11 @@ end
 /-- A module is Artinian iff every nonempty set of submodules has a minimal submodule among them.
 -/
 theorem set_has_minimal_iff_artinian :
-  (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, I ≤ M' → I = M') ↔
-  is_artinian R M :=
-by rw [is_artinian_iff_well_founded, well_founded.well_founded_iff_has_min']
+  (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬ I < M') ↔ is_artinian R M :=
+by rw [is_artinian_iff_well_founded, well_founded.well_founded_iff_has_min]
 
 theorem is_artinian.set_has_minimal [is_artinian R M] (a : set $ submodule R M) (ha : a.nonempty) :
-  ∃ M' ∈ a, ∀ I ∈ a, I ≤ M' → I = M' :=
+  ∃ M' ∈ a, ∀ I ∈ a, ¬ I < M' :=
 set_has_minimal_iff_artinian.mpr ‹_› a ha
 
 /-- A module is Artinian iff every decreasing chain of submodules stabilizes. -/
@@ -414,19 +413,19 @@ begin
     simpa only [this, top_smul, ideal.zero_eq_bot] using hJ },
   by_contradiction hJ, change J ≠ ⊤ at hJ,
   rcases is_artinian.set_has_minimal {J' : ideal R | J < J'} ⟨⊤, hJ.lt_top⟩
-    with ⟨J', hJJ' : J < J', hJ' : ∀ I, J < I → I ≤ J' → I = J'⟩,
+    with ⟨J', hJJ' : J < J', hJ' : ∀ I, J < I → ¬ I < J'⟩,
   rcases set_like.exists_of_lt hJJ' with ⟨x, hxJ', hxJ⟩,
   obtain rfl : J ⊔ ideal.span {x} = J',
-  { refine hJ' (J ⊔ ideal.span {x}) _ _,
+  { apply eq_of_le_of_not_lt _ (hJ' (J ⊔ ideal.span {x}) _),
+    { exact (sup_le hJJ'.le (span_le.2 (singleton_subset_iff.2 hxJ'))) },
     { rw set_like.lt_iff_le_and_exists,
-      exact ⟨le_sup_left, ⟨x, mem_sup_right (mem_span_singleton_self x), hxJ⟩⟩ },
-    { exact (sup_le hJJ'.le (span_le.2 (singleton_subset_iff.2 hxJ'))) } },
+      exact ⟨le_sup_left, ⟨x, mem_sup_right (mem_span_singleton_self x), hxJ⟩⟩ } },
   have : J ⊔ Jac • ideal.span {x} ≤ J ⊔ ideal.span {x},
     from sup_le_sup_left (smul_le.2 (λ _ _ _, submodule.smul_mem _ _)) _,
   have : Jac * ideal.span {x} ≤ J, --Need version 4 of Nakayamas lemma on Stacks
   { classical, by_contradiction H,
     refine H (smul_sup_le_of_le_smul_of_le_jacobson_bot
-      (fg_span_singleton _) le_rfl (hJ' _ _ this).ge),
+      (fg_span_singleton _) le_rfl (this.eq_of_not_lt (hJ' _ _)).ge),
     exact lt_of_le_of_ne le_sup_left (λ h, H $ h.symm ▸ le_sup_right) },
   have : ideal.span {x} * Jac ^ (n + 1) ≤ ⊥,
     calc ideal.span {x} * Jac ^ (n + 1) = ideal.span {x} * Jac * Jac ^ n :
diff --git a/src/ring_theory/ideal/associated_prime.lean b/src/ring_theory/ideal/associated_prime.lean
@@ -95,7 +95,7 @@ begin
     rw [smul_comm, hc, smul_zero] },
   have H₂ : (submodule.span R {a • y}).annihilator ≠ ⊤,
   { rwa [ne.def, submodule.annihilator_eq_top_iff, submodule.span_singleton_eq_bot] },
-  rwa [← h₃ (R ∙ a • y).annihilator ⟨l.trans H₁, H₂, _, rfl⟩ H₁,
+  rwa [H₁.eq_of_not_lt (h₃ (R ∙ a • y).annihilator ⟨l.trans H₁, H₂, _, rfl⟩),
     submodule.mem_annihilator_span_singleton, smul_comm, smul_smul]
 end
 
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
@@ -253,20 +253,20 @@ begin
   { intro H,
     constructor,
     intro N,
-    obtain ⟨⟨N₀, h₁⟩, e : N₀ ≤ N, h₂⟩ := well_founded.well_founded_iff_has_max'.mp
+    obtain ⟨⟨N₀, h₁⟩, e : N₀ ≤ N, h₂⟩ := well_founded.has_min
       H { N' : α | N'.1 ≤ N } ⟨⟨⊥, submodule.fg_bot⟩, bot_le⟩,
     convert h₁,
     refine (e.antisymm _).symm,
     by_contra h₃,
     obtain ⟨x, hx₁ : x ∈ N, hx₂ : x ∉ N₀⟩ := set.not_subset.mp h₃,
     apply hx₂,
-    have := h₂ ⟨(R ∙ x) ⊔ N₀, _⟩ _ _,
+    have := eq_of_le_of_not_lt _ (h₂ ⟨(R ∙ x) ⊔ N₀, _⟩ _),
     { injection this with eq,
-      rw ← eq,
+      rw eq,
       exact (le_sup_left : (R ∙ x) ≤ (R ∙ x) ⊔ N₀) (submodule.mem_span_singleton_self _) },
     { exact submodule.fg.sup ⟨{x}, by rw [finset.coe_singleton]⟩ h₁ },
-    { exact sup_le ((submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e },
-    { show N₀ ≤ (R ∙ x) ⊔ N₀, from le_sup_right } }
+    { show N₀ ≤ (R ∙ x) ⊔ N₀, from le_sup_right },
+    { exact sup_le ((submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e } }
 end
 
 variables (R M)
@@ -280,14 +280,12 @@ variables {R M}
 /-- A module is Noetherian iff every nonempty set of submodules has a maximal submodule among them.
 -/
 theorem set_has_maximal_iff_noetherian :
-  (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, M' ≤ I → I = M') ↔
-  is_noetherian R M :=
-by rw [is_noetherian_iff_well_founded, well_founded.well_founded_iff_has_max']
+  (∀ a : set $ submodule R M, a.nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬ M' < I) ↔ is_noetherian R M :=
+by rw [is_noetherian_iff_well_founded, well_founded.well_founded_iff_has_min]
 
 /-- A module is Noetherian iff every increasing chain of submodules stabilizes. -/
 theorem monotone_stabilizes_iff_noetherian :
-  (∀ (f : ℕ →o submodule R M), ∃ n, ∀ m, n ≤ m → f n = f m)
-    ↔ is_noetherian R M :=
+  (∀ (f : ℕ →o submodule R M), ∃ n, ∀ m, n ≤ m → f n = f m) ↔ is_noetherian R M :=
 by rw [is_noetherian_iff_well_founded, well_founded.monotone_chain_condition]
 
 /-- If `∀ I > J, P I` implies `P J`, then `P` holds for all submodules. -/
