feat(Order/GaloisConnection/Defs): use to_dual for GaloisInsertion/GaloisCoinsertion (leanprover-community#35649)

This PR uses `to_dual` to generate declarations about `GaloisCoinsertion` from those for `GaloisInsertion`.

- An entry is added to the name translation dictionary for this particular name translation.
- One lemma in another file had to be tagged.
- Some uses of `to_dual` have been replaced with `to_dual none`, because I had written them before `to_dual none` existed.

Author: JovanGerb

Mathlib/Algebra/Group/Submonoid/Units.lean

@@ -177,7 +177,7 @@ lemma units_surjective : Function.Surjective (units (M := M)) :=
 @[to_additive]
 lemma units_left_inverse :
     Function.LeftInverse (units (M := M)) (Subgroup.ofUnits (M := M)) :=
-  ofUnits_units_gci.u_l_leftInverse
+  ofUnits_units_gci.leftInverse_u_l
 
 /-- The equivalence between the subgroup of units of `S` and the submonoid of unit
 elements of `S`. -/
@@ -299,7 +299,7 @@ lemma ofUnits_inf_units (S T : Subgroup Mˣ) : (S.ofUnits ⊓ T.ofUnits).units =
 @[to_additive]
 lemma ofUnits_right_inverse :
     Function.RightInverse (ofUnits (M := M)) (Submonoid.units (M := M)) :=
-  ofUnits_units_gci.u_l_leftInverse
+  ofUnits_units_gci.leftInverse_u_l
 
 @[to_additive]
 lemma ofUnits_strictMono : StrictMono (ofUnits (M := M)) := ofUnits_units_gci.strictMono_l

Mathlib/Order/GaloisConnection/Defs.lean

@@ -49,10 +49,10 @@ section
 
 variable [Preorder α] [Preorder β] {l : α → β} {u : β → α}
 
-@[to_dual self (reorder := α β, 3 4, l u, hu hl, hul hlu)]
-theorem monotone_intro (hu : Monotone u) (hl : Monotone l) (hul : ∀ a, a ≤ u (l a))
-    (hlu : ∀ a, l (u a) ≤ a) : GaloisConnection l u := fun _ _ =>
-  ⟨fun h => (hul _).trans (hu h), fun h => (hl h).trans (hlu _)⟩
+@[to_dual self (reorder := α β, 3 4, l u, hu hl, h_u_l h_l_u)]
+theorem monotone_intro (hu : Monotone u) (hl : Monotone l) (h_u_l : ∀ a, a ≤ u (l a))
+    (h_l_u : ∀ a, l (u a) ≤ a) : GaloisConnection l u := fun _ _ =>
+  ⟨fun h => (h_u_l _).trans (hu h), fun h => (hl h).trans (h_l_u _)⟩
 
 @[to_dual self]
 protected theorem dual {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
@@ -63,7 +63,7 @@ protected theorem dual {l : α → β} {u : β → α} (gc : GaloisConnection l
 variable (gc : GaloisConnection l u)
 include gc
 
-@[to_dual le_iff_le']
+@[to_dual none]
 theorem le_iff_le {a : α} {b : β} : l a ≤ b ↔ a ≤ u b :=
   gc _ _
 
@@ -146,7 +146,7 @@ section LinearOrder
 
 variable [LinearOrder α] [LinearOrder β] {l : α → β} {u : β → α}
 
-@[to_dual lt_iff_lt']
+@[to_dual none]
 theorem lt_iff_lt (gc : GaloisConnection l u) {a : α} {b : β} : b < l a ↔ u b < a :=
   lt_iff_lt_of_le_iff_le (gc a b)
 
@@ -209,16 +209,34 @@ structure GaloisInsertion {α β : Type*} [Preorder α] [Preorder β] (l : α 
   /-- Property of the choice function. -/
   choice_eq : ∀ a h, choice a h = l a
 
+/-- A Galois coinsertion is a Galois connection where `u ∘ l = id`. It also contains a constructive
+choice function, to give better definitional equalities when lifting order structures. Dual to
+`GaloisInsertion` -/
+@[to_dual (reorder := α β, 3 4, l u)]
+structure GaloisCoinsertion [Preorder α] [Preorder β] (l : α → β) (u : β → α) where
+  /-- A constructive choice function for images of `u`. -/
+  choice : ∀ x : β, x ≤ l (u x) → α
+  /-- The Galois connection associated to a Galois coinsertion. -/
+  gc : GaloisConnection l u
+  /-- Main property of a Galois coinsertion. -/
+  u_l_le : ∀ x, u (l x) ≤ x
+  /-- Property of the choice function. -/
+  choice_eq : ∀ a h, choice a h = u a
+
 /-- A constructor for a Galois insertion with the trivial `choice` function. -/
+@[to_dual (reorder := hu hl)
+/-- A constructor for a Galois coinsertion with the trivial `choice` function. -/]
 def GaloisInsertion.monotoneIntro {α β : Type*} [Preorder α] [Preorder β] {l : α → β} {u : β → α}
-    (hu : Monotone u) (hl : Monotone l) (hul : ∀ a, a ≤ u (l a)) (hlu : ∀ b, l (u b) = b) :
+    (hu : Monotone u) (hl : Monotone l) (h_u_l : ∀ a, a ≤ u (l a)) (h_l_u : ∀ b, l (u b) = b) :
     GaloisInsertion l u where
   choice x _ := l x
-  gc := GaloisConnection.monotone_intro hu hl hul fun b => le_of_eq (hlu b)
-  le_l_u b := le_of_eq <| (hlu b).symm
+  gc := GaloisConnection.monotone_intro hu hl h_u_l fun b => le_of_eq (h_l_u b)
+  le_l_u b := le_of_eq <| (h_l_u b).symm
   choice_eq _ _ := rfl
 
 /-- Make a `GaloisInsertion l u` from a `GaloisConnection l u` such that `∀ b, b ≤ l (u b)` -/
+@[to_dual /-- Make a `GaloisCoinsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisInsertion` between
+`α` and `β`. -/]
 def GaloisConnection.toGaloisInsertion {α β : Type*} [Preorder α] [Preorder β] {l : α → β}
     {u : β → α} (gc : GaloisConnection l u) (h : ∀ b, b ≤ l (u b)) : GaloisInsertion l u :=
   { choice := fun x _ => l x
@@ -227,7 +245,7 @@ def GaloisConnection.toGaloisInsertion {α β : Type*} [Preorder α] [Preorder 
     choice_eq := fun _ _ => rfl }
 
 /-- Lift the bottom along a Galois connection -/
-@[implicit_reducible]
+@[to_dual (attr := implicit_reducible) /-- Lift the top along a Galois connection -/]
 def GaloisConnection.liftOrderBot {α β : Type*} [Preorder α] [OrderBot α] [PartialOrder β]
     {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
     OrderBot β where
@@ -238,116 +256,53 @@ namespace GaloisInsertion
 
 variable {l : α → β} {u : β → α}
 
+@[to_dual]
 theorem l_u_eq [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) (b : β) : l (u b) = b :=
   (gi.gc.l_u_le _).antisymm (gi.le_l_u _)
 
+@[to_dual]
 theorem leftInverse_l_u [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) :
     LeftInverse l u :=
   gi.l_u_eq
 
+@[deprecated (since := "2026-03-06")]
+alias _root_.GaloisCoinsertion.u_l_leftInverse := GaloisCoinsertion.leftInverse_u_l
+
+@[to_dual]
 theorem l_top [Preorder α] [PartialOrder β] [OrderTop α] [OrderTop β]
     (gi : GaloisInsertion l u) : l ⊤ = ⊤ :=
   top_unique <| (gi.le_l_u _).trans <| gi.gc.monotone_l le_top
 
+@[to_dual]
 theorem l_surjective [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Surjective l :=
   gi.leftInverse_l_u.surjective
 
+@[to_dual]
 theorem u_injective [Preorder α] [PartialOrder β] (gi : GaloisInsertion l u) : Injective u :=
   gi.leftInverse_l_u.injective
 
+@[to_dual]
 theorem u_le_u_iff [Preorder α] [Preorder β] (gi : GaloisInsertion l u) {a b} : u a ≤ u b ↔ a ≤ b :=
   ⟨fun h => (gi.le_l_u _).trans (gi.gc.l_le h), fun h => gi.gc.monotone_u h⟩
 
+@[to_dual]
 theorem strictMono_u [Preorder α] [Preorder β] (gi : GaloisInsertion l u) : StrictMono u :=
   strictMono_of_le_iff_le fun _ _ => gi.u_le_u_iff.symm
 
 end GaloisInsertion
 
-/-- A Galois coinsertion is a Galois connection where `u ∘ l = id`. It also contains a constructive
-choice function, to give better definitional equalities when lifting order structures. Dual to
-`GaloisInsertion` -/
-structure GaloisCoinsertion [Preorder α] [Preorder β] (l : α → β) (u : β → α) where
-  /-- A constructive choice function for images of `u`. -/
-  choice : ∀ x : β, x ≤ l (u x) → α
-  /-- The Galois connection associated to a Galois coinsertion. -/
-  gc : GaloisConnection l u
-  /-- Main property of a Galois coinsertion. -/
-  u_l_le : ∀ x, u (l x) ≤ x
-  /-- Property of the choice function. -/
-  choice_eq : ∀ a h, choice a h = u a
-
 /-- Make a `GaloisInsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisCoinsertion` between `α` and
 `β`. -/
+@[to_dual /-- Make a `GaloisCoinsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisInsertion` between
+`α` and `β`. -/]
 def GaloisCoinsertion.dual [Preorder α] [Preorder β] {l : α → β} {u : β → α} :
     GaloisCoinsertion l u → GaloisInsertion (toDual ∘ u ∘ ofDual) (toDual ∘ l ∘ ofDual) :=
   fun x => ⟨x.1, x.2.dual, x.3, x.4⟩
 
-/-- Make a `GaloisCoinsertion` between `αᵒᵈ` and `βᵒᵈ` from a `GaloisInsertion` between `α` and
-`β`. -/
-def GaloisInsertion.dual [Preorder α] [Preorder β] {l : α → β} {u : β → α} :
-    GaloisInsertion l u → GaloisCoinsertion (toDual ∘ u ∘ ofDual) (toDual ∘ l ∘ ofDual) :=
-  fun x => ⟨x.1, x.2.dual, x.3, x.4⟩
-
 /-- Make a `GaloisInsertion` between `α` and `β` from a `GaloisCoinsertion` between `αᵒᵈ` and
 `βᵒᵈ`. -/
+@[to_dual /-- Make a `GaloisCoinsertion` between `α` and `β` from a `GaloisInsertion` between `αᵒᵈ`
+and `βᵒᵈ`. -/]
 def GaloisCoinsertion.ofDual [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} :
     GaloisCoinsertion l u → GaloisInsertion (ofDual ∘ u ∘ toDual) (ofDual ∘ l ∘ toDual) :=
   fun x => ⟨x.1, x.2.dual, x.3, x.4⟩
-
-/-- Make a `GaloisCoinsertion` between `α` and `β` from a `GaloisInsertion` between `αᵒᵈ` and
-`βᵒᵈ`. -/
-def GaloisInsertion.ofDual [Preorder α] [Preorder β] {l : αᵒᵈ → βᵒᵈ} {u : βᵒᵈ → αᵒᵈ} :
-    GaloisInsertion l u → GaloisCoinsertion (ofDual ∘ u ∘ toDual) (ofDual ∘ l ∘ toDual) :=
-  fun x => ⟨x.1, x.2.dual, x.3, x.4⟩
-
-/-- A constructor for a Galois coinsertion with the trivial `choice` function. -/
-def GaloisCoinsertion.monotoneIntro [Preorder α] [Preorder β] {l : α → β} {u : β → α}
-    (hu : Monotone u) (hl : Monotone l) (hlu : ∀ b, l (u b) ≤ b) (hul : ∀ a, u (l a) = a) :
-    GaloisCoinsertion l u :=
-  (GaloisInsertion.monotoneIntro hl.dual hu.dual hlu hul).ofDual
-
-/-- Make a `GaloisCoinsertion l u` from a `GaloisConnection l u` such that `∀ a, u (l a) ≤ a` -/
-def GaloisConnection.toGaloisCoinsertion {α β : Type*} [Preorder α] [Preorder β] {l : α → β}
-    {u : β → α} (gc : GaloisConnection l u) (h : ∀ a, u (l a) ≤ a) : GaloisCoinsertion l u :=
-  { choice := fun x _ => u x
-    gc
-    u_l_le := h
-    choice_eq := fun _ _ => rfl }
-
-/-- Lift the top along a Galois connection -/
-@[implicit_reducible]
-def GaloisConnection.liftOrderTop {α β : Type*} [PartialOrder α] [Preorder β] [OrderTop β]
-    {l : α → β} {u : β → α} (gc : GaloisConnection l u) :
-    OrderTop α where
-  top := u ⊤
-  le_top _ := gc.le_u <| le_top
-
-namespace GaloisCoinsertion
-
-variable {l : α → β} {u : β → α}
-
-theorem u_l_eq [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) (a : α) : u (l a) = a :=
-  gi.dual.l_u_eq a
-
-theorem u_l_leftInverse [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) :
-    LeftInverse u l :=
-  gi.u_l_eq
-
-theorem u_bot [PartialOrder α] [Preorder β] [OrderBot α] [OrderBot β] (gi : GaloisCoinsertion l u) :
-    u ⊥ = ⊥ :=
-  gi.dual.l_top
-
-theorem u_surjective [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : Surjective u :=
-  gi.dual.l_surjective
-
-theorem l_injective [PartialOrder α] [Preorder β] (gi : GaloisCoinsertion l u) : Injective l :=
-  gi.dual.u_injective
-
-theorem l_le_l_iff [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) {a b} :
-    l a ≤ l b ↔ a ≤ b :=
-  gi.dual.u_le_u_iff
-
-theorem strictMono_l [Preorder α] [Preorder β] (gi : GaloisCoinsertion l u) : StrictMono l :=
-  fun _ _ h => gi.dual.strictMono_u h
-
-end GaloisCoinsertion

Mathlib/Order/Monotone/Defs.lean

@@ -333,6 +333,7 @@ theorem antitoneOn_const [Preorder α] [Preorder β] {c : β} {s : Set α} :
     AntitoneOn (fun _ : α ↦ c) s :=
   fun _ _ _ _ _ ↦ le_rfl
 
+@[to_dual self]
 theorem strictMono_of_le_iff_le [Preorder α] [Preorder β] {f : α → β}
     (h : ∀ x y, x ≤ y ↔ f x ≤ f y) : StrictMono f :=
   fun _ _ ↦ (lt_iff_lt_of_le_iff_le' (h _ _) (h _ _)).1

Mathlib/Tactic/Translate/ToDual.lean

@@ -239,7 +239,9 @@ def abbreviationDict : Std.HashMap String String := .ofList [
   ("nhdsGT", "NhdsLT"),
   ("nhdsLE", "NhdsGE"),
   ("nhdsGE", "NhdsLE"),
-  ("neTop", "NeBot")
+  ("neTop", "NeBot"),
+  ("galoisInsertion", "GaloisCoinsertion"),
+  ("galoisCoinsertion", "GaloisInsertion"),
 ]
 
 /-- The bundle of environment extensions for `to_dual` -/

Mathlib/Topology/Order.lean

@@ -203,7 +203,7 @@ theorem generateFrom_setOf_isOpen (t : TopologicalSpace α) :
 
 theorem leftInverse_generateFrom :
     LeftInverse generateFrom fun t : TopologicalSpace α => { s | IsOpen[t] s } :=
-  (gciGenerateFrom α).u_l_leftInverse
+  (gciGenerateFrom α).leftInverse_u_l
 
 theorem generateFrom_surjective : Surjective (generateFrom : Set (Set α) → TopologicalSpace α) :=
   (gciGenerateFrom α).u_surjective