chore: use to_dual for SupClosed/InfClosed (leanprover-community#40175)

This PR tags lemmas about `SupClosed` with the `to_dual` attribute.

Co-authored-by: Remy Degenne <remydegenne@gmail.com>

Author: RemyDegenne

Mathlib/Order/SupClosed.lean

@@ -44,51 +44,65 @@ variable {ι : Sort*} {S : Set (Set α)} {f : ι → Set α} {s t : Set α} {a :
 open Set
 
 /-- A set `s` is *sup-closed* if `a ⊔ b ∈ s` for all `a ∈ s`, `b ∈ s`. -/
+@[to_dual /-- A set `s` is *inf-closed* if `a ⊓ b ∈ s` for all `a ∈ s`, `b ∈ s`. -/]
 def SupClosed (s : Set α) : Prop := ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ⊔ b ∈ s
 
-@[simp] lemma supClosed_empty : SupClosed (∅ : Set α) := by simp [SupClosed]
-@[simp] lemma supClosed_singleton : SupClosed ({a} : Set α) := by simp [SupClosed]
+@[to_dual (attr := simp)] lemma supClosed_empty : SupClosed (∅ : Set α) := by simp [SupClosed]
+@[to_dual (attr := simp)] lemma supClosed_singleton : SupClosed ({a} : Set α) := by simp [SupClosed]
 
-@[simp] lemma supClosed_univ : SupClosed (univ : Set α) := by simp [SupClosed]
+@[to_dual (attr := simp)] lemma supClosed_univ : SupClosed (univ : Set α) := by simp [SupClosed]
+
+@[to_dual]
 lemma SupClosed.inter (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ∩ t) :=
   fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
 
+@[to_dual]
 lemma supClosed_sInter (hS : ∀ s ∈ S, SupClosed s) : SupClosed (⋂₀ S) :=
   fun _a ha _b hb _s hs ↦ hS _ hs (ha _ hs) (hb _ hs)
 
+@[to_dual]
 lemma supClosed_iInter (hf : ∀ i, SupClosed (f i)) : SupClosed (⋂ i, f i) :=
   supClosed_sInter <| forall_mem_range.2 hf
 
+@[to_dual InfClosed.codirectedOn]
 lemma SupClosed.directedOn (hs : SupClosed s) : DirectedOn (· ≤ ·) s :=
   fun _a ha _b hb ↦ ⟨_, hs ha hb, le_sup_left, le_sup_right⟩
 
+@[to_dual]
 lemma IsUpperSet.supClosed (hs : IsUpperSet s) : SupClosed s := fun _a _ _b ↦ hs le_sup_right
 
+@[to_dual]
 lemma SupClosed.preimage [FunLike F β α] [SupHomClass F β α] (hs : SupClosed s) (f : F) :
     SupClosed (f ⁻¹' s) :=
   fun a ha b hb ↦ by simpa [map_sup] using hs ha hb
 
+@[to_dual]
 lemma SupClosed.image [FunLike F α β] [SupHomClass F α β] (hs : SupClosed s) (f : F) :
     SupClosed (f '' s) := by
   rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
   rw [← map_sup]
   exact Set.mem_image_of_mem _ <| hs ha hb
 
+@[to_dual]
 lemma supClosed_range [FunLike F α β] [SupHomClass F α β] (f : F) : SupClosed (Set.range f) := by
   simpa using supClosed_univ.image f
 
+@[to_dual]
 lemma SupClosed.prod {t : Set β} (hs : SupClosed s) (ht : SupClosed t) : SupClosed (s ×ˢ t) :=
   fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
 
+@[to_dual]
 lemma supClosed_pi {ι : Type*} {α : ι → Type*} [∀ i, SemilatticeSup (α i)] {s : Set ι}
     {t : ∀ i, Set (α i)} (ht : ∀ i ∈ s, SupClosed (t i)) : SupClosed (s.pi t) :=
   fun _a ha _b hb _i hi ↦ ht _ hi (ha _ hi) (hb _ hi)
 
+@[to_dual]
 lemma SupClosed.insert_upperBounds {s : Set α} {a : α} (hs : SupClosed s) (ha : a ∈ upperBounds s) :
     SupClosed (insert a s) := by
   rw [SupClosed]
   aesop
 
+@[to_dual]
 lemma SupClosed.insert_lowerBounds {s : Set α} {a : α} (h : SupClosed s) (ha : a ∈ lowerBounds s) :
     SupClosed (insert a s) := by
   rw [SupClosed]
@@ -101,93 +115,19 @@ section Finset
 variable {ι : Type*} {f : ι → α} {s : Set α} {t : Finset ι} {a : α}
 open Finset
 
+@[to_dual]
 lemma SupClosed.finsetSup'_mem (hs : SupClosed s) (ht : t.Nonempty) :
     (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ s :=
   sup'_induction _ _ hs
 
+@[to_dual]
 lemma SupClosed.finsetSup_mem [OrderBot α] (hs : SupClosed s) (ht : t.Nonempty) :
     (∀ i ∈ t, f i ∈ s) → t.sup f ∈ s :=
   sup'_eq_sup ht f ▸ hs.finsetSup'_mem ht
 
 end Finset
 end SemilatticeSup
 
-section SemilatticeInf
-variable [SemilatticeInf α] [SemilatticeInf β]
-
-section Set
-variable {ι : Sort*} {S : Set (Set α)} {f : ι → Set α} {s t : Set α} {a : α}
-open Set
-
-/-- A set `s` is *inf-closed* if `a ⊓ b ∈ s` for all `a ∈ s`, `b ∈ s`. -/
-def InfClosed (s : Set α) : Prop := ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ⊓ b ∈ s
-
-@[simp] lemma infClosed_empty : InfClosed (∅ : Set α) := by simp [InfClosed]
-@[simp] lemma infClosed_singleton : InfClosed ({a} : Set α) := by simp [InfClosed]
-
-@[simp] lemma infClosed_univ : InfClosed (univ : Set α) := by simp [InfClosed]
-lemma InfClosed.inter (hs : InfClosed s) (ht : InfClosed t) : InfClosed (s ∩ t) :=
-  fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
-
-lemma infClosed_sInter (hS : ∀ s ∈ S, InfClosed s) : InfClosed (⋂₀ S) :=
-  fun _a ha _b hb _s hs ↦ hS _ hs (ha _ hs) (hb _ hs)
-
-lemma infClosed_iInter (hf : ∀ i, InfClosed (f i)) : InfClosed (⋂ i, f i) :=
-  infClosed_sInter <| forall_mem_range.2 hf
-
-lemma InfClosed.codirectedOn (hs : InfClosed s) : DirectedOn (· ≥ ·) s :=
-  fun _a ha _b hb ↦ ⟨_, hs ha hb, inf_le_left, inf_le_right⟩
-
-lemma IsLowerSet.infClosed (hs : IsLowerSet s) : InfClosed s := fun _a _ _b ↦ hs inf_le_right
-
-lemma InfClosed.preimage [FunLike F β α] [InfHomClass F β α] (hs : InfClosed s) (f : F) :
-    InfClosed (f ⁻¹' s) :=
-  fun a ha b hb ↦ by simpa [map_inf] using hs ha hb
-
-lemma InfClosed.image [FunLike F α β] [InfHomClass F α β] (hs : InfClosed s) (f : F) :
-    InfClosed (f '' s) := by
-  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩
-  rw [← map_inf]
-  exact Set.mem_image_of_mem _ <| hs ha hb
-
-lemma infClosed_range [FunLike F α β] [InfHomClass F α β] (f : F) : InfClosed (Set.range f) := by
-  simpa using infClosed_univ.image f
-
-lemma InfClosed.prod {t : Set β} (hs : InfClosed s) (ht : InfClosed t) : InfClosed (s ×ˢ t) :=
-  fun _a ha _b hb ↦ ⟨hs ha.1 hb.1, ht ha.2 hb.2⟩
-
-lemma infClosed_pi {ι : Type*} {α : ι → Type*} [∀ i, SemilatticeInf (α i)] {s : Set ι}
-    {t : ∀ i, Set (α i)} (ht : ∀ i ∈ s, InfClosed (t i)) : InfClosed (s.pi t) :=
-  fun _a ha _b hb _i hi ↦ ht _ hi (ha _ hi) (hb _ hi)
-
-lemma InfClosed.insert_upperBounds {s : Set α} {a : α} (hs : InfClosed s) (ha : a ∈ upperBounds s) :
-    InfClosed (insert a s) := by
-  rw [InfClosed]
-  have ha' : ∀ b ∈ s, b ≤ a := fun _ a ↦ ha a
-  aesop
-
-lemma InfClosed.insert_lowerBounds {s : Set α} {a : α} (h : InfClosed s) (ha : a ∈ lowerBounds s) :
-    InfClosed (insert a s) := by
-  rw [InfClosed]
-  aesop
-
-end Set
-
-section Finset
-variable {ι : Type*} {f : ι → α} {s : Set α} {t : Finset ι} {a : α}
-open Finset
-
-lemma InfClosed.finsetInf'_mem (hs : InfClosed s) (ht : t.Nonempty) :
-    (∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ s :=
-  inf'_induction _ _ hs
-
-lemma InfClosed.finsetInf_mem [OrderTop α] (hs : InfClosed s) (ht : t.Nonempty) :
-    (∀ i ∈ t, f i ∈ s) → t.inf f ∈ s :=
-  inf'_eq_inf ht f ▸ hs.finsetInf'_mem ht
-
-end Finset
-end SemilatticeInf
-
 open Finset OrderDual
 
 section Lattice