-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
f_1 : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
f : ↥(prefixed s)
x : X
pos :
  ∀ (hx : x ∈ s),
    (↑((((↑((fun (x : Numbering ↥s × Numbering ↥sᶜ) ↦
                        (match (motive := Numbering ↥s × Numbering ↥sᶜ → ↥(prefixed s)) x with
                          | (g, g') =>
                            Subtype.mk (p := fun (x : Numbering X) ↦
                              Membership.mem (γ := Finset (Numbering X)) (prefixed s) x)
                              {
                                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) }
                              ⋯ :
                          ↥(prefixed s)))
                      ((fun (f : ↥(prefixed s)) ↦
                          (({
                                toFun := fun (x : ↥s) ↦
                                  (⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ), ⋯⟩ :
                                    Fin (Fintype.card.{u_1} ↥s)),
                                invFun := fun (n : Fin (Fintype.card.{u_1} ↥s)) ↦
                                  Subtype.mk (p := fun (x : X) ↦ x ∈ s)
                                    ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X)
                                      (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card X)))
                                    ⋯,
                                left_inv := ⋯, right_inv := ⋯ : ↥s ≃ Fin (Fintype.card.{u_1} ↥s) },
                              {
                                toFun := fun (x : ↥sᶜ) ↦
                                  (⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #s, ⋯⟩ :
                                    Fin (Fintype.card.{u_1} ↥sᶜ)),
                                invFun := fun (n : Fin (Fintype.card.{u_1} ↥sᶜ)) ↦
                                  Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ)
                                    ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X)
                                      (⟨(↑n : ℕ) + #s, ⋯⟩ : Fin (Fintype.card X)))
                                    ⋯,
                                left_inv := ⋯, right_inv := ⋯ : ↥sᶜ ≃ Fin (Fintype.card.{u_1} ↥sᶜ) }) :
                            Numbering ↥s × Numbering ↥sᶜ))
                        f)) :
                  Numbering X) :
                Numbering X) :
              (a : X) → Fin (Fintype.card X))
            x) :
        ℕ) =
      (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) x) : ℕ)
neg :
  ∀ (hx : x ∉ s),
    (↑((((↑((fun (x : Numbering ↥s × Numbering ↥sᶜ) ↦
                        (match (motive := Numbering ↥s × Numbering ↥sᶜ → ↥(prefixed s)) x with
                          | (g, g') =>
                            Subtype.mk (p := fun (x : Numbering X) ↦
                              Membership.mem (γ := Finset (Numbering X)) (prefixed s) x)
                              {
                                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) }
                              ⋯ :
                          ↥(prefixed s)))
                      ((fun (f : ↥(prefixed s)) ↦
                          (({
                                toFun := fun (x : ↥s) ↦
                                  (⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ), ⋯⟩ :
                                    Fin (Fintype.card.{u_1} ↥s)),
                                invFun := fun (n : Fin (Fintype.card.{u_1} ↥s)) ↦
                                  Subtype.mk (p := fun (x : X) ↦ x ∈ s)
                                    ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X)
                                      (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card X)))
                                    ⋯,
                                left_inv := ⋯, right_inv := ⋯ : ↥s ≃ Fin (Fintype.card.{u_1} ↥s) },
                              {
                                toFun := fun (x : ↥sᶜ) ↦
                                  (⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #s, ⋯⟩ :
                                    Fin (Fintype.card.{u_1} ↥sᶜ)),
                                invFun := fun (n : Fin (Fintype.card.{u_1} ↥sᶜ)) ↦
                                  Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ)
                                    ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X)
                                      (⟨(↑n : ℕ) + #s, ⋯⟩ : Fin (Fintype.card X)))
                                    ⋯,
                                left_inv := ⋯, right_inv := ⋯ : ↥sᶜ ≃ Fin (Fintype.card.{u_1} ↥sᶜ) }) :
                            Numbering ↥s × Numbering ↥sᶜ))
                        f)) :
                  Numbering X) :
                Numbering X) :
              (a : X) → Fin (Fintype.card X))
            x) :
        ℕ) =
      (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) x) : ℕ)
⊢ (↑((((↑((fun (x : Numbering ↥s × Numbering ↥sᶜ) ↦
                      (match (motive := Numbering ↥s × Numbering ↥sᶜ → ↥(prefixed s)) x with
                        | (g, g') =>
                          Subtype.mk (p := fun (x : Numbering X) ↦
                            Membership.mem (γ := Finset (Numbering X)) (prefixed s) x)
                            {
                              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) }
                            ⋯ :
                        ↥(prefixed s)))
                    ((fun (f : ↥(prefixed s)) ↦
                        (({
                              toFun := fun (x : ↥s) ↦
                                (⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ), ⋯⟩ :
                                  Fin (Fintype.card.{u_1} ↥s)),
                              invFun := fun (n : Fin (Fintype.card.{u_1} ↥s)) ↦
                                Subtype.mk (p := fun (x : X) ↦ x ∈ s)
                                  ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X)
                                    (⟨(↑n : ℕ), ⋯⟩ : Fin (Fintype.card X)))
                                  ⋯,
                              left_inv := ⋯, right_inv := ⋯ : ↥s ≃ Fin (Fintype.card.{u_1} ↥s) },
                            {
                              toFun := fun (x : ↥sᶜ) ↦
                                (⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #s, ⋯⟩ :
                                  Fin (Fintype.card.{u_1} ↥sᶜ)),
                              invFun := fun (n : Fin (Fintype.card.{u_1} ↥sᶜ)) ↦
                                Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ)
                                  ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X)
                                    (⟨(↑n : ℕ) + #s, ⋯⟩ : Fin (Fintype.card X)))
                                  ⋯,
                              left_inv := ⋯, right_inv := ⋯ : ↥sᶜ ≃ Fin (Fintype.card.{u_1} ↥sᶜ) }) :
                          Numbering ↥s × Numbering ↥sᶜ))
                      f)) :
                Numbering X) :
              Numbering X) :
            (a : X) → Fin (Fintype.card X))
          x) :
      ℕ) =
    (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) x) : ℕ)

Tactic:
by_cases hx : x ∈ s