From 243423f4c1ed625ac5960d0640b7e78857c97b75 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Mon, 11 May 2026 13:20:46 -0400 Subject: [PATCH 1/3] chore: extract API from #38807 prepared with Claude code --- Mathlib/Order/Bounds/Basic.lean | 22 ++++++++++++++++++ Mathlib/Order/DirSupClosed.lean | 41 ++++++++++++--------------------- 2 files changed, 37 insertions(+), 26 deletions(-) diff --git a/Mathlib/Order/Bounds/Basic.lean b/Mathlib/Order/Bounds/Basic.lean index 8a02a3889b5de2..53294bdd62dfa0 100644 --- a/Mathlib/Order/Bounds/Basic.lean +++ b/Mathlib/Order/Bounds/Basic.lean @@ -132,6 +132,10 @@ lemma DirectedOn.isCofinalFor_fst_image_prod_snd_image {β : Type*} [Preorder β obtain ⟨z, hz, hxz, hyz⟩ := hs _ hx _ hy exact ⟨z, hz, hxz.1, hyz.2⟩ +@[to_dual] +lemma IsCofinalFor.nonempty (h : IsCofinalFor s t) (hs : s.Nonempty) : t.Nonempty := + let ⟨_, ha⟩ := hs; let ⟨b, hb, _⟩ := h ha; ⟨b, hb⟩ + theorem IsCofinalFor.union_left (hc : IsCofinalFor s t) : IsCofinalFor (s ∪ t) t := by rintro a (has | hat) · exact hc has @@ -148,6 +152,17 @@ theorem DirectedOn.of_isCofinalFor (hd : DirectedOn (· ≤ ·) t) obtain ⟨w, hw, hzw⟩ := hc hz exact ⟨w, hw, hxz.trans hzw, hyz.trans hzw⟩ +/-- If `b` is not an upper bound of a directed set `s`, then the elements of `s` not below `b` +form a cofinal subset of `s`. -/ +@[to_dual /-- If `b` is not a lower bound of a coinitially-directed set `s`, then the elements of +`s` not above `b` form a coinitial subset of `s`. -/] +theorem DirectedOn.isCofinalFor_sdiff_Iic (hd : DirectedOn (· ≤ ·) s) (hb : b ∉ upperBounds s) : + IsCofinalFor s (s \ Iic b) := by + obtain ⟨w, hw, hwb⟩ : ∃ w ∈ s, ¬ w ≤ b := by simpa [upperBounds] using hb + intro x hx + obtain ⟨z, hz, hxz, hwz⟩ := hd x hx w hw + exact ⟨z, ⟨hz, fun hzb ↦ hwb (hwz.trans hzb)⟩, hxz⟩ + theorem isCofinalFor_or_isCofinalFor_of_directedOn_union (h : DirectedOn (· ≤ ·) (s ∪ t)) : IsCofinalFor t s ∨ IsCofinalFor s t := by rw [or_iff_not_imp_left] @@ -226,6 +241,13 @@ theorem IsLUB.of_subset_of_superset {s t p : Set α} (hs : IsLUB s a) (hp : IsLU (htp : t ⊆ p) : IsLUB t a := ⟨upperBounds_mono_set htp hp.1, lowerBounds_mono_set (upperBounds_mono_set hst) hs.2⟩ +/-- The least upper bound of a set is also the least upper bound of any cofinal subset. -/ +@[to_dual /-- The greatest lower bound of a set is also the greatest lower bound of any +coinitial subset. -/] +theorem IsLUB.of_isCofinalFor {s t : Set α} (hs : IsLUB s a) (hts : t ⊆ s) + (hst : IsCofinalFor s t) : IsLUB t a := + ⟨upperBounds_mono_set hts hs.1, fun _b hb ↦ hs.2 (upperBounds_mono_of_isCofinalFor hst hb)⟩ + @[to_dual] theorem IsLeast.mono (ha : IsLeast s a) (hb : IsLeast t b) (hst : s ⊆ t) : b ≤ a := hb.2 (hst ha.1) diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index 55a1f0824831de..f6ecf14b555c28 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -179,24 +179,16 @@ theorem DirSupClosedOn.union (hDL : IsLowerSet D) obtain ⟨hds, hn⟩ := h by_cases had : a ∈ lowerBounds (upperBounds (d ∩ s)) · exact .inl <| hs (hDL inter_subset_left hD) inter_subset_right hn hds - ⟨fun b hb ↦ ha.1 hb.1, had⟩ - · simp only [lowerBounds, mem_setOf_eq, not_forall] at had - obtain ⟨b, hb, hb'⟩ := had - have key : {x ∈ d | ¬ x ≤ b} ⊆ d ∩ t := fun a ⟨had, hab⟩ ↦ - ⟨had, (hdu had).resolve_left fun has ↦ hab <| hb ⟨had, has⟩⟩ - obtain ⟨w, hw⟩ : {x ∈ d | ¬ x ≤ b}.Nonempty := by - contrapose! hb' - apply ha.2 - aesop - refine Or.inr <| ht (hDL inter_subset_left hD) (key.trans inter_subset_right) - ⟨w, hw⟩ (fun x hx y hy ↦ ?_) ?_ - · obtain ⟨z, hz, hz'⟩ := hd₁ _ (.inr (key hx)) _ (.inr (key hy)) - exact ⟨z, ⟨⟨hdst ▸ hz, mt hz'.1.trans hx.2⟩, hz'⟩⟩ - · refine ⟨fun x hx ↦ ha.1 hx.1, fun x hx ↦ ha.2 fun y hy ↦ ?_⟩ - by_cases hyb : y ≤ b - · obtain ⟨z, hz, hxz, hyz⟩ := hd₁ _ (hdst ▸ hy) _ (.inr (key hw)) - exact hxz.trans (hx ⟨hdst ▸ hz, fun hzb ↦ hw.2 (hyz.trans hzb)⟩) - exact hx ⟨hy, hyb⟩ + ⟨upperBounds_mono_set inter_subset_left ha.1, had⟩ + · obtain ⟨b, hb, hb'⟩ : ∃ b ∈ upperBounds (d ∩ s), ¬ a ≤ b := by + simpa [lowerBounds] using had + have hdd : DirectedOn (· ≤ ·) d := hdst ▸ hd₁ + have hcof : IsCofinalFor d (d \ Iic b) := + hdd.isCofinalFor_sdiff_Iic fun h ↦ hb' (ha.2 h) + have hsub : d \ Iic b ⊆ d ∩ t := by grind [mem_upperBounds] + exact .inr <| ht (hDL diff_subset hD) (hsub.trans inter_subset_right) + (hcof.nonempty (hdst ▸ hd₀)) (hdd.of_isCofinalFor diff_subset hcof) + (ha.of_isCofinalFor diff_subset hcof) theorem DirSupInaccOn.inter (hDL : IsLowerSet D) (hs : DirSupInaccOn D s) (ht : DirSupInaccOn D t) : DirSupInaccOn D (s ∩ t) := by @@ -232,14 +224,11 @@ theorem dirSupInaccOn_iff_inter_subset (hDL : IsLowerSet D) : choose f hf using H have := ht₀.to_subtype have hft : range f ⊆ t := by grind - apply (h (hDL hft hD) (range_nonempty f) _ _ has).ne_empty - · aesop - · intro a ha b hb - obtain ⟨c, hc, _, _⟩ := ht₁ _ (hft ha) _ (hft hb) - have := hf ⟨c, hc⟩ - grind - · exact ⟨upperBounds_mono_set hft ha.1, - fun b hb ↦ ha.2 fun c hc ↦ (hf ⟨c, hc⟩).1.trans (hb <| by simp)⟩ + have hcof : IsCofinalFor t (range f) := fun c hc ↦ + ⟨f ⟨c, hc⟩, ⟨_, rfl⟩, (hf ⟨c, hc⟩).1⟩ + apply (h (hDL hft hD) (range_nonempty f) (ht₁.of_isCofinalFor hft hcof) + (ha.of_isCofinalFor hft hcof) has).ne_empty + aesop /-- The condition `(d ∩ s).Nonempty` in `DirSupInacc` can be replaced with the stronger `∃ b ∈ d, Ici b ∩ d ⊆ s`. -/ From 903a1c86c5923c1345a2afce0f71ee7c56d1e628 Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Mon, 11 May 2026 20:49:07 -0400 Subject: [PATCH 2/3] use directedOn_union_iff --- Mathlib/Order/Bounds/Basic.lean | 11 ----------- Mathlib/Order/DirSupClosed.lean | 24 +++++++----------------- 2 files changed, 7 insertions(+), 28 deletions(-) diff --git a/Mathlib/Order/Bounds/Basic.lean b/Mathlib/Order/Bounds/Basic.lean index 53294bdd62dfa0..c0df362d88c1ab 100644 --- a/Mathlib/Order/Bounds/Basic.lean +++ b/Mathlib/Order/Bounds/Basic.lean @@ -152,17 +152,6 @@ theorem DirectedOn.of_isCofinalFor (hd : DirectedOn (· ≤ ·) t) obtain ⟨w, hw, hzw⟩ := hc hz exact ⟨w, hw, hxz.trans hzw, hyz.trans hzw⟩ -/-- If `b` is not an upper bound of a directed set `s`, then the elements of `s` not below `b` -form a cofinal subset of `s`. -/ -@[to_dual /-- If `b` is not a lower bound of a coinitially-directed set `s`, then the elements of -`s` not above `b` form a coinitial subset of `s`. -/] -theorem DirectedOn.isCofinalFor_sdiff_Iic (hd : DirectedOn (· ≤ ·) s) (hb : b ∉ upperBounds s) : - IsCofinalFor s (s \ Iic b) := by - obtain ⟨w, hw, hwb⟩ : ∃ w ∈ s, ¬ w ≤ b := by simpa [upperBounds] using hb - intro x hx - obtain ⟨z, hz, hxz, hwz⟩ := hd x hx w hw - exact ⟨z, ⟨hz, fun hzb ↦ hwb (hwz.trans hzb)⟩, hxz⟩ - theorem isCofinalFor_or_isCofinalFor_of_directedOn_union (h : DirectedOn (· ≤ ·) (s ∪ t)) : IsCofinalFor t s ∨ IsCofinalFor s t := by rw [or_iff_not_imp_left] diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index f6ecf14b555c28..ea42e59b68a644 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -171,24 +171,14 @@ theorem DirSupClosedOn.union (hDL : IsLowerSet D) (hs : DirSupClosedOn D s) (ht : DirSupClosedOn D t) : DirSupClosedOn D (s ∪ t) := by intro d hD hdu hd₀ hd₁ a ha have hdst : d ∩ s ∪ d ∩ t = d := by grind - rw [← hdst] at hd₀ hd₁ - wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ (d ∩ s).Nonempty - · rw [union_comm] at hdu hd₀ hd₁ hdst ⊢ + wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s) + · rw [union_comm] at hdu hdst ⊢ exact this hDL ht hs hD hdu hd₀ hd₁ ha hdst <| - (directedOn_or_directedOn_of_union' hd₀ hd₁).resolve_right h - obtain ⟨hds, hn⟩ := h - by_cases had : a ∈ lowerBounds (upperBounds (d ∩ s)) - · exact .inl <| hs (hDL inter_subset_left hD) inter_subset_right hn hds - ⟨upperBounds_mono_set inter_subset_left ha.1, had⟩ - · obtain ⟨b, hb, hb'⟩ : ∃ b ∈ upperBounds (d ∩ s), ¬ a ≤ b := by - simpa [lowerBounds] using had - have hdd : DirectedOn (· ≤ ·) d := hdst ▸ hd₁ - have hcof : IsCofinalFor d (d \ Iic b) := - hdd.isCofinalFor_sdiff_Iic fun h ↦ hb' (ha.2 h) - have hsub : d \ Iic b ⊆ d ∩ t := by grind [mem_upperBounds] - exact .inr <| ht (hDL diff_subset hD) (hsub.trans inter_subset_right) - (hcof.nonempty (hdst ▸ hd₀)) (hdd.of_isCofinalFor diff_subset hcof) - (ha.of_isCofinalFor diff_subset hcof) + (directedOn_union_iff.mp (by rw [hdst]; exact hd₁)).resolve_right h + obtain ⟨hds, hcof⟩ := h + have hcof' : IsCofinalFor d (d ∩ s) := hcof.union_right.mono_left hdst.ge + exact .inl <| hs (hDL inter_subset_left hD) inter_subset_right + (hcof'.nonempty hd₀) hds (ha.of_isCofinalFor inter_subset_left hcof') theorem DirSupInaccOn.inter (hDL : IsLowerSet D) (hs : DirSupInaccOn D s) (ht : DirSupInaccOn D t) : DirSupInaccOn D (s ∩ t) := by From 7afb7a5b9ff34fa8ed56510897ec8034faec60fa Mon Sep 17 00:00:00 2001 From: Bryan Gin-ge Chen Date: Mon, 11 May 2026 21:26:21 -0400 Subject: [PATCH 3/3] golf further --- Mathlib/Order/DirSupClosed.lean | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/Mathlib/Order/DirSupClosed.lean b/Mathlib/Order/DirSupClosed.lean index ea42e59b68a644..492ebe87ca3be5 100644 --- a/Mathlib/Order/DirSupClosed.lean +++ b/Mathlib/Order/DirSupClosed.lean @@ -174,7 +174,7 @@ theorem DirSupClosedOn.union (hDL : IsLowerSet D) wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s) · rw [union_comm] at hdu hdst ⊢ exact this hDL ht hs hD hdu hd₀ hd₁ ha hdst <| - (directedOn_union_iff.mp (by rw [hdst]; exact hd₁)).resolve_right h + (directedOn_union_iff.mp (by rwa [hdst])).resolve_right h obtain ⟨hds, hcof⟩ := h have hcof' : IsCofinalFor d (d ∩ s) := hcof.union_right.mono_left hdst.ge exact .inl <| hs (hDL inter_subset_left hD) inter_subset_right @@ -210,15 +210,11 @@ theorem dirSupInaccOn_iff_inter_subset (hDL : IsLowerSet D) : mpr := .of_inter_subset mp h t hD ht₀ ht₁ a ha has := by by_contra! H - have H : ∀ b : t, ∃ c, b.1 ≤ c ∧ c ∈ t ∧ c ∉ s := by simpa [not_subset, and_assoc] using H - choose f hf using H - have := ht₀.to_subtype - have hft : range f ⊆ t := by grind - have hcof : IsCofinalFor t (range f) := fun c hc ↦ - ⟨f ⟨c, hc⟩, ⟨_, rfl⟩, (hf ⟨c, hc⟩).1⟩ - apply (h (hDL hft hD) (range_nonempty f) (ht₁.of_isCofinalFor hft hcof) - (ha.of_isCofinalFor hft hcof) has).ne_empty - aesop + have hcof : IsCofinalFor t (t \ s) := by grind [IsCofinalFor, not_subset] + obtain ⟨x, hx, hxs⟩ := h (hDL diff_subset hD) (hcof.nonempty ht₀) + (ht₁.of_isCofinalFor diff_subset hcof) + (ha.of_isCofinalFor diff_subset hcof) has + exact hx.2 hxs /-- The condition `(d ∩ s).Nonempty` in `DirSupInacc` can be replaced with the stronger `∃ b ∈ d, Ici b ∩ d ⊆ s`. -/