-- Lean 4 proof step from Mathlib.Combinatorics.KatonaCircle (goal)
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x_1 : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
pos :
  ∀ (hx : x ∈ s),
    (↑((({
                    toFun := fun (x : X) ↦
                      if hx : x ∈ s then
                        Fin.castLE (n := Fintype.card.{u_1} ↥s) ⋯
                          ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
                      else
                        Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) ⋯
                          (Fin.addNat
                            ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x ⋯))
                            #s),
                    invFun := fun (n : Fin (Fintype.card X)) ↦
                      if hn : (↑n : ℕ) < #s then
                        (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s)
                              (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s))) :
                          X)
                      else
                        (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ)
                              (⟨(↑n : ℕ) - #s, ⋯⟩ : Fin (Fintype.card.{u_1} ↥sᶜ))) :
                          X),
                    left_inv := ⋯, right_inv := ⋯ } :
                  X ≃ Fin (Fintype.card X)) :
                (a : X) → Fin (Fintype.card X))
              x) :
          ℕ) <
        #s →
      x ∈ s
⊢ (↑((({
                  toFun := fun (x : X) ↦
                    if hx : x ∈ s then
                      Fin.castLE (n := Fintype.card.{u_1} ↥s) ⋯
                        ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
                    else
                      Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) ⋯
                        (Fin.addNat
                          ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x ⋯)) #s),
                  invFun := fun (n : Fin (Fintype.card X)) ↦
                    if hn : (↑n : ℕ) < #s then
                      (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s)
                            (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card.{u_1} ↥s))) :
                        X)
                    else
                      (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ)
                            (⟨(↑n : ℕ) - #s, ⋯⟩ : Fin (Fintype.card.{u_1} ↥sᶜ))) :
                        X),
                  left_inv := ⋯, right_inv := ⋯ } :
                X ≃ Fin (Fintype.card X)) :
              (a : X) → Fin (Fintype.card X))
            x) :
        ℕ) <
      #s →
    x ∈ s
have neg : ∀ (hx : x ∉ s),
  (↑((({
                  toFun := fun (x : X) ↦
                    if hx : x ∈ s then
                      Fin.castLE (n := Fintype.card.{u_1} ↥s) sorry
                        ((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx))
                    else
                      Fin.cast (n := Fintype.card.{u_1} ↥sᶜ + #s) sorry
                        (Fin.addNat
                          ((g' : (a : ↥sᶜ) → Fin (Fintype.card ↥sᶜ)) (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x sorry)) #s),
                  invFun := fun (n : Fin (Fintype.card X)) ↦
                    if hn : (↑n : ℕ) < #s then
                      (↑((Equiv.symm g : (a : Fin (Fintype.card ↥s)) → ↥s)
                            (⟨(↑n : ℕ), sorry⟩ : Fin (Fintype.card.{u_1} ↥s))) :
                        X)
                    else
                      (↑((Equiv.symm g' : (a : Fin (Fintype.card ↥sᶜ)) → ↥sᶜ)
                            (⟨(↑n : ℕ) - #s, sorry⟩ : Fin (Fintype.card.{u_1} ↥sᶜ))) :
                        X),
                  left_inv := sorry, right_inv := sorry } :
                X ≃ Fin (Fintype.card X)) :
              (a : X) → Fin (Fintype.card X))
            x) :
        ℕ) <
      #s →
    x ∈ s
Tactic: by_cases hx : x ∈ s