∀ {α : Type u_2} {β : Type u_1} {s : Set α} {t : Set β} [inst : DecidablePred fun x => x ∈ s]
  [inst_1 : DecidablePred fun x => x ∈ t] (e₀ : ↑s ≃ ↑t) (e₁ : ↑sᶜ ≃ ↑tᶜ) (x : ↑s),
  (Trans.trans (Trans.trans (Equiv.Set.sumCompl s).symm (e₀.sumCongr e₁)) (Equiv.Set.sumCompl t)) ↑x = ↑(e₀ x)