feat: missing API lemmas about the prod instance in Order/CompleteLat…

…tice (#1369)

This adds lemmas about how `fst`, `snd`, and `swap` interact with `supₛ` and `infₛ`.

Manual port of a [mathlib PR](leanprover-community/mathlib#18029) by @eric-wieser 

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Order/CompleteLattice.lean

@@ -1844,6 +1844,70 @@ instance supSet [SupSet α] [SupSet β] : SupSet (α × β) :=
 instance infSet [InfSet α] [InfSet β] : InfSet (α × β) :=
   ⟨fun s => (infₛ (Prod.fst '' s), infₛ (Prod.snd '' s))⟩
 
+variable {α β}
+
+theorem fst_infₛ [InfSet α] [InfSet β] (s : Set (α × β)) : (infₛ s).fst = infₛ (Prod.fst '' s) :=
+  rfl
+#align prod.fst_Inf Prod.fst_infₛ
+
+theorem snd_infₛ [InfSet α] [InfSet β] (s : Set (α × β)) : (infₛ s).snd = infₛ (Prod.snd '' s) :=
+  rfl
+#align prod.snd_Inf Prod.snd_infₛ
+
+theorem swap_infₛ [InfSet α] [InfSet β] (s : Set (α × β)) : (infₛ s).swap = infₛ (Prod.swap '' s) :=
+  ext (congr_arg infₛ <| image_comp Prod.fst swap s : _)
+    (congr_arg infₛ <| image_comp Prod.snd swap s : _)
+#align prod.swap_Inf Prod.swap_infₛ
+
+theorem fst_supₛ [SupSet α] [SupSet β] (s : Set (α × β)) : (supₛ s).fst = supₛ (Prod.fst '' s) :=
+  rfl
+#align prod.fst_Sup Prod.fst_supₛ
+
+theorem snd_supₛ [SupSet α] [SupSet β] (s : Set (α × β)) : (supₛ s).snd = supₛ (Prod.snd '' s) :=
+  rfl
+#align prod.snd_Sup Prod.snd_supₛ
+
+theorem swap_supₛ [SupSet α] [SupSet β] (s : Set (α × β)) : (supₛ s).swap = supₛ (Prod.swap '' s) :=
+  ext (congr_arg supₛ <| image_comp Prod.fst swap s : _)
+    (congr_arg supₛ <| image_comp Prod.snd swap s : _)
+#align prod.swap_Sup Prod.swap_supₛ
+
+theorem fst_infᵢ [InfSet α] [InfSet β] (f : ι → α × β) : (infᵢ f).fst = ⨅ i, (f i).fst :=
+  congr_arg infₛ (range_comp _ _).symm
+#align prod.fst_infi Prod.fst_infᵢ
+
+theorem snd_infᵢ [InfSet α] [InfSet β] (f : ι → α × β) : (infᵢ f).snd = ⨅ i, (f i).snd :=
+  congr_arg infₛ (range_comp _ _).symm
+#align prod.snd_infi Prod.snd_infᵢ
+
+theorem swap_infᵢ [InfSet α] [InfSet β] (f : ι → α × β) : (infᵢ f).swap = ⨅ i, (f i).swap := by
+  simp_rw [infᵢ, swap_infₛ, ←range_comp, Function.comp]  -- Porting note: need to unfold `∘`
+#align prod.swap_infi Prod.swap_infᵢ
+
+theorem infᵢ_mk [InfSet α] [InfSet β] (f : ι → α) (g : ι → β) :
+    (⨅ i, (f i, g i)) = (⨅ i, f i, ⨅ i, g i) :=
+  congr_arg₂ Prod.mk (fst_infᵢ _) (snd_infᵢ _)
+#align prod.infi_mk Prod.infᵢ_mk
+
+theorem fst_supᵢ [SupSet α] [SupSet β] (f : ι → α × β) : (supᵢ f).fst = ⨆ i, (f i).fst :=
+  congr_arg supₛ (range_comp _ _).symm
+#align prod.fst_supr Prod.fst_supᵢ
+
+theorem snd_supᵢ [SupSet α] [SupSet β] (f : ι → α × β) : (supᵢ f).snd = ⨆ i, (f i).snd :=
+  congr_arg supₛ (range_comp _ _).symm
+#align prod.snd_supr Prod.snd_supᵢ
+
+theorem swap_supᵢ [SupSet α] [SupSet β] (f : ι → α × β) : (supᵢ f).swap = ⨆ i, (f i).swap := by
+  simp_rw [supᵢ, swap_supₛ, ←range_comp, Function.comp]  -- Porting note: need to unfold `∘`
+#align prod.swap_supr Prod.swap_supᵢ
+
+theorem supᵢ_mk [SupSet α] [SupSet β] (f : ι → α) (g : ι → β) :
+    (⨆ i, (f i, g i)) = (⨆ i, f i, ⨆ i, g i) :=
+  congr_arg₂ Prod.mk (fst_supᵢ _) (snd_supᵢ _)
+#align prod.supr_mk Prod.supᵢ_mk
+
+variable (α β)
+
 instance completeLattice [CompleteLattice α] [CompleteLattice β] : CompleteLattice (α × β) :=
   { Prod.lattice α β, Prod.boundedOrder α β, Prod.supSet α β, Prod.infSet α β with
     le_supₛ := fun _ _ hab => ⟨le_supₛ <| mem_image_of_mem _ hab, le_supₛ <| mem_image_of_mem _ hab⟩
@@ -1857,6 +1921,14 @@ instance completeLattice [CompleteLattice α] [CompleteLattice β] : CompleteLat
 
 end Prod
 
+lemma infₛ_Prod [InfSet α] [InfSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) :
+  infₛ (s ×ˢ t) = (infₛ s, infₛ t) :=
+congr_arg₂ Prod.mk (congr_arg infₛ $ fst_image_prod _ ht) (congr_arg infₛ $ snd_image_prod hs _)
+
+lemma Sup_prod [SupSet α] [SupSet β] {s : Set α} {t : Set β} (hs : s.Nonempty) (ht : t.Nonempty) :
+  supₛ (s ×ˢ t) = (supₛ s, supₛ t) :=
+congr_arg₂ Prod.mk (congr_arg supₛ $ fst_image_prod _ ht) (congr_arg supₛ $ snd_image_prod hs _)
+
 section CompleteLattice
 
 variable [CompleteLattice α] {a : α} {s : Set α}