chore(logic/embedding): reuse proofs from data.* (#3341)

Other changes:

* rename `injective.prod` to `injective.prod_map`;
* add `surjective.prod_map`;
* redefine `sigma.map` without pattern matching;
* rename `sigma_map_injective` to `injective.sigma_map`;
* add `surjective.sigma_map`;
* add `injective.sum_map` and `surjective.sum_map`;
* rename `embedding.prod_congr` to `embedding.prod_map`;
* rename `embedding.sum_congr` to `embedding.sum_map`;
* delete `embedding.sigma_congr_right`, add more
  general `embedding.sigma_map`.

src/data/prod.lean

@@ -111,9 +111,10 @@ end prod
 
 open function
 
-lemma function.injective.prod {f : α → γ} {g : β → δ} (hf : injective f) (hg : injective g) :
-  injective (λ p : α × β, (f p.1, g p.2)) :=
-assume ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h,
-  have a₁ = a₂, from hf (by cc),
-  have b₁ = b₂, from hg (by cc),
-  by cc
+lemma function.injective.prod_map {f : α → γ} {g : β → δ} (hf : injective f) (hg : injective g) :
+  injective (prod.map f g) :=
+λ x y h, prod.ext (hf (prod.ext_iff.1 h).1) (hg $ (prod.ext_iff.1 h).2)
+
+lemma function.surjective.prod_map {f : α → γ} {g : β → δ} (hf : surjective f) (hg : surjective g) :
+  surjective (prod.map f g) :=
+λ p, let ⟨x, hx⟩ := hf p.1 in let ⟨y, hy⟩ := hg p.2 in ⟨(x, y), prod.ext hx hy⟩

src/data/sigma/basic.lean

@@ -43,10 +43,10 @@ by simp
 variables {α₁ : Type*} {α₂ : Type*} {β₁ : α₁ → Type*} {β₂ : α₂ → Type*}
 
 /-- Map the left and right components of a sigma -/
-def sigma.map (f₁ : α₁ → α₂) (f₂ : Πa, β₁ a → β₂ (f₁ a)) : sigma β₁ → sigma β₂
-| ⟨a, b⟩ := ⟨f₁ a, f₂ a b⟩
+def sigma.map (f₁ : α₁ → α₂) (f₂ : Πa, β₁ a → β₂ (f₁ a)) (x : sigma β₁) : sigma β₂ :=
+⟨f₁ x.1, f₂ x.1 x.2⟩
 
-lemma sigma_map_injective {f₁ : α₁ → α₂} {f₂ : Πa, β₁ a → β₂ (f₁ a)}
+lemma function.injective.sigma_map {f₁ : α₁ → α₂} {f₂ : Πa, β₁ a → β₂ (f₁ a)}
   (h₁ : function.injective f₁) (h₂ : ∀ a, function.injective (f₂ a)) :
   function.injective (sigma.map f₁ f₂)
 | ⟨i, x⟩ ⟨j, y⟩ h :=
@@ -57,6 +57,20 @@ begin
   subst y
 end
 
+lemma function.surjective.sigma_map {f₁ : α₁ → α₂} {f₂ : Πa, β₁ a → β₂ (f₁ a)}
+  (h₁ : function.surjective f₁) (h₂ : ∀ a, function.surjective (f₂ a)) :
+  function.surjective (sigma.map f₁ f₂) :=
+begin
+  intros y,
+  cases y with j y,
+  cases h₁ j with i hi,
+  subst j,
+  cases h₂ i y with x hx,
+  subst y,
+  exact ⟨⟨i, x⟩, rfl⟩
+end
+
+
 end sigma
 
 section psigma

src/data/sum.lean

@@ -139,3 +139,19 @@ swap_swap
 swap_swap
 
 end sum
+
+namespace function
+
+open sum
+
+lemma injective.sum_map {f : α → β} {g : α' → β'} (hf : injective f) (hg : injective g) :
+  injective (sum.map f g)
+| (inl x) (inl y) h := congr_arg inl $ hf $ inl.inj h
+| (inr x) (inr y) h := congr_arg inr $ hg $ inr.inj h
+
+lemma surjective.sum_map {f : α → β} {g : α' → β'} (hf : surjective f) (hg : surjective g) :
+  surjective (sum.map f g)
+| (inl y) := let ⟨x, hx⟩ := hf y in ⟨inl x, congr_arg inl hx⟩
+| (inr y) := let ⟨x, hx⟩ := hg y in ⟨inr x, congr_arg inr hx⟩
+
+end function

src/logic/embedding.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import data.equiv.basic
+import data.sigma
 
 /-!
 # Injective functions
@@ -127,28 +128,28 @@ def cod_restrict {α β} (p : set β) (f : α ↪ β) (H : ∀ a, f a ∈ p) : 
 @[simp] theorem cod_restrict_apply {α β} (p) (f : α ↪ β) (H a) :
   cod_restrict p f H a = ⟨f a, H a⟩ := rfl
 
-def prod_congr {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α × γ ↪ β × δ :=
-⟨assume ⟨a, b⟩, (e₁ a, e₂ b),
-  assume ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h,
-  have a₁ = a₂ ∧ b₁ = b₂, from
-    (prod.mk.inj h).imp (assume h, e₁.injective h) (assume h, e₂.injective h),
-  this.left ▸ this.right ▸ rfl⟩
+/-- If `e₁` and `e₂` are embeddings, then so is `prod.map e₁ e₂ : (a, b) ↦ (e₁ a, e₂ b)`. -/
+def prod_map {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α × γ ↪ β × δ :=
+⟨prod.map e₁ e₂, e₁.injective.prod_map e₂.injective⟩
+
+@[simp] lemma coe_prod_map {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) :
+  ⇑(e₁.prod_map e₂) = prod.map e₁ e₂ :=
+rfl
 
 section sum
 open sum
 
-def sum_congr {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α ⊕ γ ↪ β ⊕ δ :=
-⟨assume s, match s with inl a := inl (e₁ a) | inr b := inr (e₂ b) end,
+/-- If `e₁` and `e₂` are embeddings, then so is `sum.map e₁ e₂`. -/
+def sum_map {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α ⊕ γ ↪ β ⊕ δ :=
+⟨sum.map e₁ e₂,
     assume s₁ s₂ h, match s₁, s₂, h with
     | inl a₁, inl a₂, h := congr_arg inl $ e₁.injective $ inl.inj h
     | inr b₁, inr b₂, h := congr_arg inr $ e₂.injective $ inr.inj h
     end⟩
 
-@[simp] theorem sum_congr_apply_inl {α β γ δ}
-  (e₁ : α ↪ β) (e₂ : γ ↪ δ) (a) : sum_congr e₁ e₂ (inl a) = inl (e₁ a) := rfl
-
-@[simp] theorem sum_congr_apply_inr {α β γ δ}
-  (e₁ : α ↪ β) (e₂ : γ ↪ δ) (b) : sum_congr e₁ e₂ (inr b) = inr (e₂ b) := rfl
+@[simp] theorem coe_sum_map {α β γ δ} (e₁ : α ↪ β) (e₂ : γ ↪ δ) :
+  ⇑(sum_map e₁ e₂) = sum.map e₁ e₂ :=
+rfl
 
 /-- The embedding of `α` into the sum `α ⊕ β`. -/
 def inl {α β : Type*} : α ↪ α ⊕ β :=
@@ -161,14 +162,18 @@ def inr {α β : Type*} : β ↪ α ⊕ β :=
 end sum
 
 section sigma
-open sigma
-
-def sigma_congr_right {α : Type*} {β γ : α → Type*} (e : ∀ a, β a ↪ γ a) : sigma β ↪ sigma γ :=
-⟨λ ⟨a, b⟩, ⟨a, e a b⟩, λ ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ h, begin
-  injection h with h₁ h₂, subst a₂,
-  congr,
-  exact (e a₁).2 (eq_of_heq h₂)
-end⟩
+
+variables {α α' : Type*} {β : α → Type*} {β' : α' → Type*}
+
+/-- If `f : α ↪ α'` is an embedding and `g : Π a, β α ↪ β' (f α)` is a family
+of embeddings, then `sigma.map f g` is an embedding. -/
+def sigma_map (f : α ↪ α') (g : Π a, β a ↪ β' (f a)) :
+  (Σ a, β a) ↪ Σ a', β' a' :=
+⟨sigma.map f (λ a, g a), f.injective.sigma_map (λ a, (g a).injective)⟩
+
+@[simp] lemma coe_sigma_map (f : α ↪ α') (g : Π a, β a ↪ β' (f a)) :
+  ⇑(f.sigma_map g) = sigma.map f (λ a, g a) :=
+rfl
 
 end sigma
 

src/set_theory/cardinal.lean

@@ -243,7 +243,7 @@ lemma zero_power_le (c : cardinal.{u}) : (0 : cardinal.{u}) ^ c ≤ 1 :=
 by { by_cases h : c = 0, rw [h, power_zero], rw [zero_power h], apply zero_le }
 
 theorem add_le_add : ∀{a b c d : cardinal}, a ≤ b → c ≤ d → a + c ≤ b + d :=
-by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨embedding.sum_congr e₁ e₂⟩
+by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨e₁.sum_map e₂⟩
 
 theorem add_le_add_left (a) {b c : cardinal} : b ≤ c → a + b ≤ a + c :=
 add_le_add (le_refl _)
@@ -258,7 +258,7 @@ theorem le_add_left (a b : cardinal) : a ≤ b + a :=
 by simpa using add_le_add_right a (zero_le b)
 
 theorem mul_le_mul : ∀{a b c d : cardinal}, a ≤ b → c ≤ d → a * c ≤ b * d :=
-by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨embedding.prod_congr e₁ e₂⟩
+by rintros ⟨α⟩ ⟨β⟩ ⟨γ⟩ ⟨δ⟩ ⟨e₁⟩ ⟨e₂⟩; exact ⟨e₁.prod_map e₂⟩
 
 theorem mul_le_mul_left (a) {b c : cardinal} : b ≤ c → a * b ≤ a * c :=
 mul_le_mul (le_refl _)
@@ -394,7 +394,7 @@ quotient.induction_on a $ λ α, by simp; exact
   quotient.sound ⟨equiv.sigma_equiv_prod _ _⟩
 
 theorem sum_le_sum {ι} (f g : ι → cardinal) (H : ∀ i, f i ≤ g i) : sum f ≤ sum g :=
-⟨embedding.sigma_congr_right $ λ i, classical.choice $
+⟨(embedding.refl _).sigma_map $ λ i, classical.choice $
   by have := H i; rwa [← quot.out_eq (f i), ← quot.out_eq (g i)] at this⟩
 
 /-- The indexed supremum of cardinals is the smallest cardinal above

src/set_theory/game/domineering.lean

@@ -27,14 +27,10 @@ open function
 
 /-- The embedding `(x, y) ↦ (x, y+1)`. -/
 def shift_up : ℤ × ℤ ↪ ℤ × ℤ :=
-⟨λ p : ℤ × ℤ, (p.1, p.2 + 1),
- have injective (λ (n : ℤ), n + 1) := λ _ _, (add_left_inj 1).mp,
- injective_id.prod this⟩
+(embedding.refl ℤ).prod_map ⟨λ n, n + 1, add_left_injective 1⟩
 /-- The embedding `(x, y) ↦ (x+1, y)`. -/
 def shift_right : ℤ × ℤ ↪ ℤ × ℤ :=
-⟨λ p : ℤ × ℤ, (p.1 + 1, p.2),
- have injective (λ (n : ℤ), n + 1) := λ _ _, (add_left_inj 1).mp,
- this.prod injective_id⟩
+embedding.prod_map ⟨λ n, n + 1, add_left_injective 1⟩ (embedding.refl ℤ)
 
 /-- A Domineering board is an arbitrary finite subset of `ℤ × ℤ`. -/
 @[derive inhabited]

src/set_theory/ordinal.lean

@@ -723,7 +723,7 @@ by rw [one_le_iff_pos, pos_iff_ne_zero]
 theorem add_le_add_left {a b : ordinal} : a ≤ b → ∀ c, c + a ≤ c + b :=
 induction_on a $ λ α₁ r₁ _, induction_on b $ λ α₂ r₂ _ ⟨⟨⟨f, fo⟩, fi⟩⟩ c,
 induction_on c $ λ β s _,
-⟨⟨⟨(embedding.refl _).sum_congr f,
+⟨⟨⟨(embedding.refl _).sum_map f,
   λ a b, match a, b with
     | sum.inl a, sum.inl b := sum.lex_inl_inl.trans sum.lex_inl_inl.symm
     | sum.inl a, sum.inr b := by apply iff_of_true; apply sum.lex.sep
@@ -904,7 +904,7 @@ induction_on a $ λ α₁ r₁ hr₁, induction_on b $ λ α₂ r₂ hr₂ ⟨
 induction_on c $ λ β s hs, (@type_le' _ _ _ _
   (@sum.lex.is_well_order _ _ _ _ hr₁ hs)
   (@sum.lex.is_well_order _ _ _ _ hr₂ hs)).2
-⟨⟨embedding.sum_congr f (embedding.refl _), λ a b, begin
+⟨⟨f.sum_map (embedding.refl _), λ a b, begin
   split; intro H,
   { cases H; constructor; [rwa ← fo, assumption] },
   { cases a with a a; cases b with b b; cases H; constructor; [rwa fo, assumption] }

src/topology/constructions.lean

@@ -744,7 +744,7 @@ end
 lemma embedding_sigma_map {τ : ι → Type*} [Π i, topological_space (τ i)]
   {f : Π i, σ i → τ i} (hf : ∀ i, embedding (f i)) : embedding (sigma.map id f) :=
 begin
-  refine ⟨⟨_⟩, sigma_map_injective function.injective_id (λ i, (hf i).inj)⟩,
+  refine ⟨⟨_⟩, function.injective_id.sigma_map (λ i, (hf i).inj)⟩,
   refine le_antisymm
     (continuous_iff_le_induced.mp (continuous_sigma_map (λ i, (hf i).continuous))) _,
   intros s hs,

src/topology/uniform_space/uniform_embedding.lean

@@ -157,7 +157,7 @@ lemma uniform_embedding_subtype_emb (p : α → Prop) {e : α → β} (ue : unif
 lemma uniform_embedding.prod {α' : Type*} {β' : Type*} [uniform_space α'] [uniform_space β']
   {e₁ : α → α'} {e₂ : β → β'} (h₁ : uniform_embedding e₁) (h₂ : uniform_embedding e₂) :
   uniform_embedding (λp:α×β, (e₁ p.1, e₂ p.2)) :=
-{ inj := h₁.inj.prod h₂.inj,
+{ inj := h₁.inj.prod_map h₂.inj,
   ..h₁.to_uniform_inducing.prod h₂.to_uniform_inducing }
 
 lemma is_complete_of_complete_image {m : α → β} {s : set α} (hm : uniform_inducing m)