feat(logic/embedding): subtype_or_{embedding,equiv} (#8489)

Provide explicit embedding from a subtype of a disjuction into a sum type.
If the disjunction is disjoint, upgrade to an equiv.
Additionally, provide `subtype.imp_embedding`, lowering a subtype
along an implication.

src/data/equiv/basic.lean

@@ -827,7 +827,10 @@ section sum_compl
 
 /-- For any predicate `p` on `α`,
 the sum of the two subtypes `{a // p a}` and its complement `{a // ¬ p a}`
-is naturally equivalent to `α`. -/
+is naturally equivalent to `α`.
+
+See `subtype_or_equiv` for sum types over subtypes `{x // p x}` and `{x // q x}`
+that are not necessarily `is_compl p q`.  -/
 def sum_compl {α : Type*} (p : α → Prop) [decidable_pred p] :
   {a // p a} ⊕ {a // ¬ p a} ≃ α :=
 { to_fun := sum.elim coe coe,

src/logic/embedding.lean

@@ -320,3 +320,77 @@ namespace set
 ⟨λ x, ⟨x.1, h x.2⟩, λ ⟨x, hx⟩ ⟨y, hy⟩ h, by { congr, injection h }⟩
 
 end set
+
+section subtype
+
+variable {α : Type*}
+
+/-- A subtype `{x // p x ∨ q x}` over a disjunction of `p q : α → Prop` can be injectively split
+into a sum of subtypes `{x // p x} ⊕ {x // q x}` such that `¬ p x` is sent to the right. -/
+def subtype_or_left_embedding (p q : α → Prop) [decidable_pred p] :
+  {x // p x ∨ q x} ↪ {x // p x} ⊕ {x // q x} :=
+⟨λ x, if h : p x then sum.inl ⟨x, h⟩ else sum.inr ⟨x, x.prop.resolve_left h⟩,
+  begin
+    intros x y,
+    dsimp only,
+    split_ifs;
+    simp [subtype.ext_iff]
+  end⟩
+
+lemma subtype_or_left_embedding_apply_left {p q : α → Prop} [decidable_pred p]
+  (x : {x // p x ∨ q x}) (hx : p x) : subtype_or_left_embedding p q x = sum.inl ⟨x, hx⟩ :=
+dif_pos hx
+
+lemma subtype_or_left_embedding_apply_right {p q : α → Prop} [decidable_pred p]
+  (x : {x // p x ∨ q x}) (hx : ¬ p x) :
+  subtype_or_left_embedding p q x = sum.inr ⟨x, x.prop.resolve_left hx⟩ :=
+dif_neg hx
+
+/-- A subtype `{x // p x}` can be injectively sent to into a subtype `{x // q x}`,
+if `p x → q x` for all `x : α`. -/
+@[simps] def subtype.imp_embedding (p q : α → Prop) (h : p ≤ q) :
+  {x // p x} ↪ {x // q x} :=
+⟨λ x, ⟨x, h x x.prop⟩, λ x y, by simp [subtype.ext_iff]⟩
+
+/-- A subtype `{x // p x ∨ q x}` over a disjunction of `p q : α → Prop` is equivalent to a sum of
+subtypes `{x // p x} ⊕ {x // q x}` such that `¬ p x` is sent to the right, when
+`disjoint p q`.
+
+See also `equiv.sum_compl`, for when `is_compl p q`.  -/
+@[simps apply] def subtype_or_equiv (p q : α → Prop) [decidable_pred p] (h : disjoint p q) :
+  {x // p x ∨ q x} ≃ {x // p x} ⊕ {x // q x} :=
+{ to_fun := subtype_or_left_embedding p q,
+  inv_fun := sum.elim
+    (subtype.imp_embedding _ _ (λ x hx, (or.inl hx : p x ∨ q x)))
+    (subtype.imp_embedding _ _ (λ x hx, (or.inr hx : p x ∨ q x))),
+  left_inv := λ x, begin
+    by_cases hx : p x,
+    { rw subtype_or_left_embedding_apply_left _ hx,
+      simp [subtype.ext_iff] },
+    { rw subtype_or_left_embedding_apply_right _ hx,
+      simp [subtype.ext_iff] },
+  end,
+  right_inv := λ x, begin
+    cases x,
+    { simp only [sum.elim_inl],
+      rw subtype_or_left_embedding_apply_left,
+      { simp },
+      { simpa using x.prop } },
+    { simp only [sum.elim_inr],
+      rw subtype_or_left_embedding_apply_right,
+      { simp },
+      { suffices : ¬ p x,
+        { simpa },
+        intro hp,
+        simpa using h x ⟨hp, x.prop⟩ } }
+  end }
+
+@[simp] lemma subtype_or_equiv_symm_inl (p q : α → Prop) [decidable_pred p] (h : disjoint p q)
+  (x : {x // p x}) : (subtype_or_equiv p q h).symm (sum.inl x) = ⟨x, or.inl x.prop⟩ :=
+rfl
+
+@[simp] lemma subtype_or_equiv_symm_inr (p q : α → Prop) [decidable_pred p] (h : disjoint p q)
+  (x : {x // q x}) : (subtype_or_equiv p q h).symm (sum.inr x) = ⟨x, or.inr x.prop⟩ :=
+rfl
+
+end subtype