even shorter

Author: staroperator

Mathlib/Data/Set/Finite/Lattice.lean

@@ -424,8 +424,7 @@ theorem Finite.biSup_iInf_eq {ι} {κ : ι → Sort*} [Nonempty (∀ a, κ a)] [
 theorem _root_.iInf_iSup_eq_of_finite {α ι} {κ : ι → Sort*} [Order.Frame α] [Finite ι]
     {f : ∀ a, κ a → α} : ⨅ a, ⨆ b, f a b = ⨆ g : ∀ a, κ a, ⨅ a, f a (g a) := by
   by_cases h : ∀ a, Nonempty (κ a)
-  · simpa [← Equiv.plift.symm.iInf_comp,
-      ← (Equiv.plift.piCongrLeft' (κ <| PLift.down ·)).symm.iSup_comp]
+  · simpa [← Equiv.plift.symm.iInf_comp, ← (Equiv.plift.piCongrLeft' _).symm.iSup_comp]
       using Finite.biInf_iSup_eq (f := (f <| PLift.down ·)) finite_univ
   · simp only [not_forall, not_nonempty_iff] at h
     haveI : IsEmpty (∀ a, κ a) := by simpa
@@ -435,8 +434,7 @@ theorem _root_.iInf_iSup_eq_of_finite {α ι} {κ : ι → Sort*} [Order.Frame 
 theorem _root_.iSup_iInf_eq_of_finite {α ι} {κ : ι → Sort*} [Order.Coframe α] [Finite ι]
     {f : ∀ a, κ a → α} : ⨆ a, ⨅ b, f a b = ⨅ g : ∀ a, κ a, ⨆ a, f a (g a) := by
   by_cases h : ∀ a, Nonempty (κ a)
-  · simpa [← Equiv.plift.symm.iSup_comp,
-      ← (Equiv.plift.piCongrLeft' (κ <| PLift.down ·)).symm.iInf_comp]
+  · simpa [← Equiv.plift.symm.iSup_comp, ← (Equiv.plift.piCongrLeft' _).symm.iInf_comp]
       using Finite.biSup_iInf_eq (f := (f <| PLift.down ·)) finite_univ
   · simp only [not_forall, not_nonempty_iff] at h
     haveI : IsEmpty (∀ a, κ a) := by simpa