feat: forward-port leanprover-community/mathlib#18446 (#2346)

Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Mathlib/Data/Prod/Basic.lean

@@ -4,14 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 
 ! This file was ported from Lean 3 source module data.prod.basic
-! leanprover-community/mathlib commit 2ed7e4aec72395b6a7c3ac4ac7873a7a43ead17c
+! leanprover-community/mathlib commit bd9851ca476957ea4549eb19b40e7b5ade9428cc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathlib.Init.Core
 import Mathlib.Init.Data.Prod
 import Mathlib.Init.Function
 import Mathlib.Logic.Function.Basic
+import Mathlib.Tactic.Inhabit
 
 /-!
 # Extra facts about `prod`
@@ -341,3 +342,71 @@ theorem Involutive.Prod_map {f : α → α} {g : β → β} :
 #align function.involutive.prod_map Function.Involutive.Prod_map
 
 end Function
+
+namespace Prod
+
+open Function
+
+@[simp]
+theorem map_injective [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} :
+    Injective (map f g) ↔ Injective f ∧ Injective g :=
+  ⟨fun h =>
+    ⟨fun a₁ a₂ ha => by
+      inhabit β
+      injection
+        @h (a₁, default) (a₂, default) (congr_arg (fun c : γ => Prod.mk c (g default)) ha : _),
+      fun b₁ b₂ hb => by
+      inhabit α
+      injection @h (default, b₁) (default, b₂) (congr_arg (Prod.mk (f default)) hb : _)⟩,
+    fun h => h.1.Prod_map h.2⟩
+#align prod.map_injective Prod.map_injective
+
+@[simp]
+theorem map_surjective [Nonempty γ] [Nonempty δ] {f : α → γ} {g : β → δ} :
+    Surjective (map f g) ↔ Surjective f ∧ Surjective g :=
+  ⟨fun h =>
+    ⟨fun c => by
+      inhabit δ
+      obtain ⟨⟨a, b⟩, h⟩ := h (c, default)
+      exact ⟨a, congr_arg Prod.fst h⟩,
+      fun d => by
+      inhabit γ
+      obtain ⟨⟨a, b⟩, h⟩ := h (default, d)
+      exact ⟨b, congr_arg Prod.snd h⟩⟩,
+    fun h => h.1.Prod_map h.2⟩
+#align prod.map_surjective Prod.map_surjective
+
+@[simp]
+theorem map_bijective [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ} :
+    Bijective (map f g) ↔ Bijective f ∧ Bijective g := by
+  haveI := Nonempty.map f ‹_›
+  haveI := Nonempty.map g ‹_›
+  exact (map_injective.and map_surjective).trans (and_and_and_comm)
+#align prod.map_bijective Prod.map_bijective
+
+@[simp]
+theorem map_leftInverse [Nonempty β] [Nonempty δ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α}
+    {g₂ : δ → γ} : LeftInverse (map f₁ g₁) (map f₂ g₂) ↔ LeftInverse f₁ f₂ ∧ LeftInverse g₁ g₂ :=
+  ⟨fun h =>
+    ⟨fun b => by
+      inhabit δ
+      exact congr_arg Prod.fst (h (b, default)),
+      fun d => by
+      inhabit β
+      exact congr_arg Prod.snd (h (default, d))⟩,
+    fun h => h.1.Prod_map h.2 ⟩
+#align prod.map_left_inverse Prod.map_leftInverse
+
+@[simp]
+theorem map_rightInverse [Nonempty α] [Nonempty γ] {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α}
+    {g₂ : δ → γ} : RightInverse (map f₁ g₁) (map f₂ g₂) ↔ RightInverse f₁ f₂ ∧ RightInverse g₁ g₂ :=
+  map_leftInverse
+#align prod.map_right_inverse Prod.map_rightInverse
+
+@[simp]
+theorem map_involutive [Nonempty α] [Nonempty β] {f : α → α} {g : β → β} :
+    Involutive (map f g) ↔ Involutive f ∧ Involutive g :=
+  map_leftInverse
+#align prod.map_involutive Prod.map_involutive
+
+end Prod

Mathlib/Data/Sum/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Yury G. Kudryashov
 
 ! This file was ported from Lean 3 source module data.sum.basic
-! leanprover-community/mathlib commit f4ecb599422baaf39055d8278c7d9ef3b5b72b88
+! leanprover-community/mathlib commit bd9851ca476957ea4549eb19b40e7b5ade9428cc
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -588,12 +588,47 @@ theorem Surjective.sum_map {f : α → β} {g : α' → β'} (hf : Surjective f)
     ⟨inr x, congr_arg inr hx⟩
 #align function.surjective.sum_map Function.Surjective.sum_map
 
+theorem Bijective.sum_map {f : α → β} {g : α' → β'} (hf : Bijective f) (hg : Bijective g) :
+    Bijective (Sum.map f g) :=
+  ⟨hf.injective.sum_map hg.injective, hf.surjective.sum_map hg.surjective⟩
+#align function.bijective.sum_map Function.Bijective.sum_map
+
 end Function
 
 namespace Sum
 
 open Function
 
+@[simp]
+theorem map_injective {f : α → γ} {g : β → δ} :
+    Injective (Sum.map f g) ↔ Injective f ∧ Injective g :=
+  ⟨fun h =>
+    ⟨fun a₁ a₂ ha => inl_injective <| @h (inl a₁) (inl a₂) (congr_arg inl ha : _), fun b₁ b₂ hb =>
+      inr_injective <| @h (inr b₁) (inr b₂) (congr_arg inr hb : _)⟩,
+    fun h => h.1.sum_map h.2⟩
+#align sum.map_injective Sum.map_injective
+
+@[simp]
+theorem map_surjective {f : α → γ} {g : β → δ} :
+    Surjective (Sum.map f g) ↔ Surjective f ∧ Surjective g :=
+  ⟨ fun h => ⟨
+      (fun c => by
+        obtain ⟨a | b, h⟩ := h (inl c)
+        · exact ⟨a, inl_injective h⟩
+        · cases h),
+      (fun d => by
+        obtain ⟨a | b, h⟩ := h (inr d)
+        · cases h
+        · exact ⟨b, inr_injective h⟩)⟩,
+    fun h => h.1.sum_map h.2⟩
+#align sum.map_surjective Sum.map_surjective
+
+@[simp]
+theorem map_bijective {f : α → γ} {g : β → δ} :
+    Bijective (Sum.map f g) ↔ Bijective f ∧ Bijective g :=
+  (map_injective.and map_surjective).trans <| and_and_and_comm
+#align sum.map_bijective Sum.map_bijective
+
 theorem elim_const_const (c : γ) :
     Sum.elim (const _ c : α → γ) (const _ c : β → γ) = const _ c := by
   ext x