chore(galois_connection): golf some proofs (#8582)

* golf some proofs
* add `galois_insertion.left_inverse_l_u` and `galois_coinsertion.left_inverse_u_l`;
* drop `galois_insertion.l_supr_of_ul_eq_self` and `galois_coinsertion.u_infi_of_lu_eq_self`: these lemmas are less general than `galois_connection.l_supr` and `galois_connection.u_infi`.

src/order/galois_connection.lean

@@ -150,17 +150,15 @@ section order_top
 variables [order_top α] [order_top β] {l : α → β} {u : β → α} (gc : galois_connection l u)
 include gc
 
-lemma u_top : u ⊤ = ⊤ :=
-(gc.is_glb_u_image is_glb_empty).unique $ by simp only [is_glb_empty, image_empty]
+lemma u_top : u ⊤ = ⊤ := top_unique $ gc.le_u le_top
 
 end order_top
 
 section order_bot
 variables [order_bot α] [order_bot β] {l : α → β} {u : β → α} (gc : galois_connection l u)
 include gc
 
-lemma l_bot : l ⊥ = ⊥ :=
-(gc.is_lub_l_image is_lub_empty).unique $ by simp only [is_lub_empty, image_empty]
+lemma l_bot : l ⊥ = ⊥ := gc.dual.u_top
 
 end order_bot
 
@@ -179,8 +177,7 @@ variables [semilattice_inf α] [semilattice_inf β] {l : α → β} {u : β →
   (gc : galois_connection l u)
 include gc
 
-lemma u_inf : u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂ :=
-(gc.is_glb_u_image is_glb_pair).unique $ by simp only [image_pair, is_glb_pair]
+lemma u_inf : u (b₁ ⊓ b₂) = u b₁ ⊓ u b₂ := gc.dual.l_sup
 
 end semilattice_inf
 
@@ -193,15 +190,12 @@ lemma l_supr {f : ι → α} : l (supr f) = (⨆i, l (f i)) :=
 eq.symm $ is_lub.supr_eq $ show is_lub (range (l ∘ f)) (l (supr f)),
   by rw [range_comp, ← Sup_range]; exact gc.is_lub_l_image (is_lub_Sup _)
 
-lemma u_infi {f : ι → β} : u (infi f) = (⨅i, u (f i)) :=
-eq.symm $ is_glb.infi_eq $ show is_glb (range (u ∘ f)) (u (infi f)),
-  by rw [range_comp, ← Inf_range]; exact gc.is_glb_u_image (is_glb_Inf _)
+lemma u_infi {f : ι → β} : u (infi f) = (⨅i, u (f i)) := gc.dual.l_supr
 
 lemma l_Sup {s : set α} : l (Sup s) = (⨆a ∈ s, l a) :=
 by simp only [Sup_eq_supr, gc.l_supr]
 
-lemma u_Inf {s : set β} : u (Inf s) = (⨅a ∈ s, u a) :=
-by simp only [Inf_eq_infi, gc.u_infi]
+lemma u_Inf {s : set β} : u (Inf s) = (⨅a ∈ s, u a) := gc.dual.l_Sup
 
 end complete_lattice
 
@@ -312,16 +306,17 @@ lemma l_u_eq [preorder α] [partial_order β] (gi : galois_insertion l u) (b : 
   l (u b) = b :=
 (gi.gc.l_u_le _).antisymm (gi.le_l_u _)
 
+lemma left_inverse_l_u [preorder α] [partial_order β] (gi : galois_insertion l u) :
+  left_inverse l u :=
+gi.l_u_eq
+
 lemma l_surjective [preorder α] [partial_order β] (gi : galois_insertion l u) :
   surjective l :=
-λ b, ⟨u b, gi.l_u_eq b⟩
+gi.left_inverse_l_u.surjective
 
 lemma u_injective [preorder α] [partial_order β] (gi : galois_insertion l u) :
   injective u :=
-λ a b h,
-calc a = l (u a) : (gi.l_u_eq a).symm
-   ... = l (u b) : congr_arg l h
-   ... = b       : gi.l_u_eq b
+gi.left_inverse_l_u.injective
 
 lemma l_sup_u [semilattice_sup α] [semilattice_sup β] (gi : galois_insertion l u) (a b : β) :
   l (u a ⊔ u b) = a ⊔ b :=
@@ -334,12 +329,6 @@ lemma l_supr_u [complete_lattice α] [complete_lattice β] (gi : galois_insertio
 calc l (⨆ (i : ι), u (f i)) = ⨆ (i : ι), l (u (f i)) : gi.gc.l_supr
                         ... = ⨆ (i : ι), f i : congr_arg _ $ funext $ λ i, gi.l_u_eq (f i)
 
-lemma l_supr_of_ul_eq_self [complete_lattice α] [complete_lattice β] (gi : galois_insertion l u)
-  {ι : Sort x} (f : ι → α) (hf : ∀ i, u (l (f i)) = f i) :
-  l (⨆ i, (f i)) = ⨆ i, l (f i) :=
-calc l (⨆ (i : ι), (f i)) = l ⨆ (i : ι), (u (l (f i))) : by simp [hf]
-                        ... = ⨆ (i : ι), l (f i) : gi.l_supr_u _
-
 lemma l_inf_u [semilattice_inf α] [semilattice_inf β] (gi : galois_insertion l u) (a b : β) :
   l (u a ⊓ u b) = a ⊓ b :=
 calc l (u a ⊓ u b) = l (u (a ⊓ b)) : congr_arg l gi.gc.u_inf.symm
@@ -492,6 +481,10 @@ lemma u_l_eq [partial_order α] [preorder β] (gi : galois_coinsertion l u) (a :
   u (l a) = a :=
 gi.dual.l_u_eq a
 
+lemma u_l_left_inverse [partial_order α] [preorder β] (gi : galois_coinsertion l u) :
+  left_inverse u l :=
+gi.u_l_eq
+
 lemma u_surjective [partial_order α] [preorder β] (gi : galois_coinsertion l u) :
   surjective u :=
 gi.dual.l_surjective
@@ -509,11 +502,6 @@ lemma u_infi_l [complete_lattice α] [complete_lattice β] (gi : galois_coinsert
   u (⨅ i, l (f i)) = ⨅ i, (f i) :=
 gi.dual.l_supr_u _
 
-lemma u_infi_of_lu_eq_self [complete_lattice α] [complete_lattice β] (gi : galois_coinsertion l u)
-  {ι : Sort x} (f : ι → β) (hf : ∀ i, l (u (f i)) = f i) :
-  u (⨅ i, (f i)) = ⨅ i, u (f i) :=
-gi.dual.l_supr_of_ul_eq_self _ hf
-
 lemma u_sup_l [semilattice_sup α] [semilattice_sup β] (gi : galois_coinsertion l u) (a b : α) :
   u (l a ⊔ l b) = a ⊔ b :=
 gi.dual.l_inf_u _ _