-- Lean 4 proof step from Mathlib.Logic.Equiv.Set (goal)
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : DecidablePred fun (x : β) ↦ x ∈ t
e₀ : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)
e :
  { e : α ≃ β //
    ∀ (x : (↑s : Type u)),
      Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β) ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }
x : α
pos :
  ∀ (hx : x ∈ s),
    Eq.{v + 1} (α := β)
      (((↑((fun (e₁ : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)) ↦
                    (Subtype.mk (p := fun (e : α ≃ β) ↦
                        ∀ (x : (↑s : Type u)),
                          Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                            ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β))
                        (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                          (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Set.sumCompl s).symm (e₀.sumCongr e₁))
                          (Set.sumCompl t))
                        ⋯ :
                      { e : α ≃ β //
                        ∀ (x : (↑s : Type u)),
                          Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                            ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }))
                  ((fun
                        (e :
                          { e : α ≃ β //
                            ∀ (x : (↑s : Type u)),
                              Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                                ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }) ↦
                      ((↑e : α ≃ β).subtypeEquiv (p := Membership.mem sᶜ) (q := Membership.mem tᶜ) ⋯ :
                        Equiv.{u + 1, v + 1} { a : α // a ∈ sᶜ } { b : β // b ∈ tᶜ }))
                    e)) :
              α ≃ β) :
            (a : α) → β)
          x :
        β)
      (((↑e : α ≃ β) : (a : α) → β) x : β)
⊢ Eq.{v + 1} (α := β)
    (((↑((fun (e₁ : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)) ↦
                  (Subtype.mk (p := fun (e : α ≃ β) ↦
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β))
                      (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                        (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Set.sumCompl s).symm (e₀.sumCongr e₁))
                        (Set.sumCompl t))
                      ⋯ :
                    { e : α ≃ β //
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }))
                ((fun
                      (e :
                        { e : α ≃ β //
                          ∀ (x : (↑s : Type u)),
                            Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                              ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }) ↦
                    ((↑e : α ≃ β).subtypeEquiv (p := Membership.mem sᶜ) (q := Membership.mem tᶜ) ⋯ :
                      Equiv.{u + 1, v + 1} { a : α // a ∈ sᶜ } { b : β // b ∈ tᶜ }))
                  e)) :
            α ≃ β) :
          (a : α) → β)
        x :
      β)
    (((↑e : α ≃ β) : (a : α) → β) x : β)
have neg : ∀ (hx : ¬x ∈ s),
  Eq.{v + 1} (α := β)
    (((↑((fun (e₁ : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)) ↦
                  (Subtype.mk (p := fun (e : α ≃ β) ↦
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β))
                      (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                        (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Set.sumCompl s).symm (e₀.sumCongr e₁))
                        (Set.sumCompl t))
                      sorry :
                    { e : α ≃ β //
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }))
                ((fun
                      (e :
                        { e : α ≃ β //
                          ∀ (x : (↑s : Type u)),
                            Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                              ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }) ↦
                    ((↑e : α ≃ β).subtypeEquiv (p := Membership.mem sᶜ) (q := Membership.mem tᶜ) sorry :
                      Equiv.{u + 1, v + 1} { a : α // a ∈ sᶜ } { b : β // b ∈ tᶜ }))
                  e)) :
            α ≃ β) :
          (a : α) → β)
        x :
      β)
    (((↑e : α ≃ β) : (a : α) → β) x : β)
Tactic: by_cases hx : x ∈ s