Removing a left summand from a sum type

For a : α, the elements of α ⊕ β other than Sum.inl a are the disjoint union of the elements of α other than a and of β. This file records this equivalence, Equiv.sumSubtypeNe, which identifies the columns left after deleting the column Sum.inl a of a matrix whose columns are indexed by α ⊕ β.

def Equiv.sumSubtypeNe {α : Type u_1} {β : Type u_2} (a : α) : { x : α // x ≠ a } ⊕ β ≃ { j : α ⊕ β // j ≠ Sum.inl a }

The disjoint union of the elements other than a and of β, as the subtype of α ⊕ β of the elements other than Sum.inl a.

@[simp]

theorem Equiv.coe_sumSubtypeNe_apply {α : Type u_1} {β : Type u_2} (a : α) (x : { x : α // x ≠ a } ⊕ β) : ↑((sumSubtypeNe a) x) = Sum.map Subtype.val id x

Equiv.sumSubtypeNe a sends Sum.inl x to Sum.inl x and Sum.inr y to Sum.inr y.