@[simp]

theorem Sum.pure_eq {α β : Type} {x : β} : pure x = inr x

@[simp]

theorem Sum.bind_eq_inl_iff {α β γ : Type} {m : α ⊕ β} {f : β → α ⊕ γ} {x : α} : m >>= f = inl x ↔ m = inl x ∨ ∃ (y : β), m = inr y ∧ f y = inl x

@[simp]

theorem Sum.bind_eq_inr_iff {α β γ : Type} {m : α ⊕ β} {f : β → α ⊕ γ} {x : γ} : m >>= f = inr x ↔ ∃ (y : β), m = inr y ∧ f y = inr x

@[simp]

theorem Sum.fmap_eq_inl_iff {α β γ : Type} {m : α ⊕ β} {f : β → γ} {x : α} : f <$> m = inl x ↔ m = inl x

@[simp]

theorem Sum.fmap_eq_inr_iff {α β γ : Type} {m : α ⊕ β} {f : β → γ} {x : γ} : f <$> m = inr x ↔ ∃ (y : β), m = inr y ∧ f y = x