-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
s t : Set α
p : α → Prop
inst : DecidablePred p
hs : ∀ (x : α), x ∈ s → p x
ht : ∀ (x : α), x ∈ t → ¬p x
o : (↑s : Type u_3) ⊕ (↑t : Type u_3)
inl :
  ∀ (x : α) (h : x ∈ s),
    Eq (α := (↑s : Type u_3) ⊕ (↑t : Type u_3))
      ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
          (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
            else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
            (↑s : Type u_3) ⊕ (↑t : Type u_3)))
        ((fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
            (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
              | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
              | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
              (↑(s ∪ t) : Type u_3)))
          (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h))))
      (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h))
inr :
  ∀ (x : α) (h : x ∈ t),
    Eq (α := (↑s : Type u_3) ⊕ (↑t : Type u_3))
      ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
          (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
            else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
            (↑s : Type u_3) ⊕ (↑t : Type u_3)))
        ((fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
            (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
              | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
              | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
              (↑(s ∪ t) : Type u_3)))
          (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x h))))
      (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x h))
inl₁ :
  ∀ (x : α) (h : x ∈ s),
    Eq (α := (↑s : Type u_3) ⊕ (↑t : Type u_3))
      ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
          (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
            else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
            (↑s : Type u_3) ⊕ (↑t : Type u_3)))
        ((fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
            (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
              | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
              | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
              (↑(s ∪ t) : Type u_3)))
          (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h))))
      (Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h))
inr₁ :
  ∀ (x : α) (h : x ∈ t),
    Eq (α := (↑s : Type u_3) ⊕ (↑t : Type u_3))
      ((fun (x : (↑(s ∪ t) : Type u_3)) ↦
          (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
            else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
            (↑s : Type u_3) ⊕ (↑t : Type u_3)))
        ((fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
            (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
              | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
              | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
              (↑(s ∪ t) : Type u_3)))
          (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x h))))
      (Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x h))
⊢ (fun (x : (↑(s ∪ t) : Type u_3)) ↦
        (if hp : p (↑x : α) then Sum.inl (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)
          else Sum.inr (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯) :
          (↑s : Type u_3) ⊕ (↑t : Type u_3)))
      ((fun (o : (↑s : Type u_3) ⊕ (↑t : Type u_3)) ↦
          (match (motive := (↑s : Type u_3) ⊕ (↑t : Type u_3) → (↑(s ∪ t) : Type u_3)) o with
            | Sum.inl x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯
            | Sum.inr x => Subtype.mk (p := fun (x : α) ↦ x ∈ s ∪ t) (↑x : α) ⋯ :
            (↑(s ∪ t) : Type u_3)))
        o) =
    o

Tactic:
rcases o with (⟨x, h⟩ | ⟨x, h⟩) <;> [simp [hs _ h]; simp [ht _ h]]