awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ↥sᶜ
this : #s ≤ (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ)
⊢ (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #s < Fintype.card X - #s

Tactic:
omega
-- 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)
n : Fin (Fintype.card.{u_1} ↥sᶜ)
⊢ (↑n : ℕ) < Fintype.card X - #s

Tactic:
simpa using n.2

Premises used: Fin.isLt
-- 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)
n : Fin (Fintype.card.{u_1} ↥sᶜ)
rw :
  ¬(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X))
            ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X)
              (⟨(↑n : ℕ) + #s, ⋯⟩ : Fin (Fintype.card X)))) :
        ℕ) <
      #s
⊢ Membership.mem (α := X) sᶜ
    ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X) (⟨(↑n : ℕ) + #s, ⋯⟩ : Fin (Fintype.card X)) : X)

Tactic:
rw [s.mem_compl, mem_prefixed.1 f.2]

Premises used: Finset.mem_compl, Iff.mp, Numbering.mem_prefixed, Subtype.property
-- 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)
n : Fin (Fintype.card.{u_1} ↥sᶜ)
⊢ ¬(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X))
            ((Equiv.symm (↑f : Numbering X) : (a : Fin (Fintype.card X)) → X)
              (⟨(↑n : ℕ) + #s, ⋯⟩ : Fin (Fintype.card X)))) :
        ℕ) <
      #s

Tactic:
simp
-- 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
hx : x ∈ sᶜ
⊢ #s ≤ (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) x) : ℕ)

Tactic:
rw [s.mem_compl, mem_prefixed.1 f.2, not_lt] at hx

Premises used: Finset.mem_compl, not_lt, Iff.mp, Numbering.mem_prefixed, Subtype.property
-- 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
hx_1 : x ∈ sᶜ
hx : #s ≤ (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) x) : ℕ)
⊢ (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)))
            ⋯ :
          ↥sᶜ))
      ((fun (x : ↥sᶜ) ↦
          (⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #s, ⋯⟩ :
            Fin (Fintype.card.{u_1} ↥sᶜ)))
        (Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x hx_1)) =
    Subtype.mk (p := fun (x : X) ↦ x ∈ sᶜ) x hx_1

Tactic:
simp [Nat.sub_add_cancel hx]

Premises used: Nat.sub_add_cancel
-- 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)
n : ℕ
hn : n < Fintype.card.{u_1} ↥sᶜ
⊢ (fun (x : ↥sᶜ) ↦
        (⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #s, ⋯⟩ :
          Fin (Fintype.card.{u_1} ↥sᶜ)))
      ((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)))
              ⋯ :
            ↥sᶜ))
        ⟨n, hn⟩) =
    (⟨n, hn⟩ : Fin (Fintype.card.{u_1} ↥sᶜ))

Tactic:
simp
-- Module: Mathlib.Combinatorics.KatonaCircle
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
hx : x ∉ s
⊢ x ∈ sᶜ

Tactic:
simpa
-- Module: Mathlib.Combinatorics.KatonaCircle
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
hx : x ∉ s
⊢ Fintype.card.{u_1} ↥sᶜ + #s = Fintype.card X

Tactic:
simp [card_le_univ]

Premises used: Finset.card_le_univ
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hn : (↑n : ℕ) < #s
⊢ (↑n : ℕ) < Fintype.card.{u_1} ↥s

Tactic:
simpa using hn
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hn : ¬(↑n : ℕ) < #s
simp : (↑n : ℕ) - #s < Fintype.card X - #s
⊢ (↑n : ℕ) - #s < Fintype.card.{u_1} ↥sᶜ

Tactic:
simp
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hn : ¬(↑n : ℕ) < #s
⊢ (↑n : ℕ) - #s < Fintype.card X - #s

Tactic:
omega
-- Module: Mathlib.Combinatorics.KatonaCircle
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),
    (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, ⋯⟩) : X) :
            X))
        ((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) :
              Fin (Fintype.card X)))
          x) =
      x
neg :
  ∀ (hx : x ∉ s),
    (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, ⋯⟩) : X) :
            X))
        ((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) :
              Fin (Fintype.card X)))
          x) =
      x
⊢ (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, ⋯⟩) : X) :
          X))
      ((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) :
            Fin (Fintype.card X)))
        x) =
    x

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Combinatorics.KatonaCircle
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
hx : x ∈ s
⊢ (↑((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx)) : ℕ) < #s

Tactic:
simpa using (g ⟨x, hx⟩).2

Premises used: Fin.isLt, Subtype.mk, DFunLike.coe
-- Module: Mathlib.Combinatorics.KatonaCircle
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
hx : x ∈ s
⊢ (↑((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx)) : ℕ) < #s

Tactic:
have : g ⟨x, hx⟩ < #s := by simpa using (g ⟨x, hx⟩).2
-- Module: Mathlib.Combinatorics.KatonaCircle
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
hx : x ∈ s
this : (↑((g : (a : ↥s) → Fin (Fintype.card ↥s)) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x hx)) : ℕ) < #s
⊢ (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, ⋯⟩) : X) :
          X))
      ((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) :
            Fin (Fintype.card X)))
        x) =
    x

Tactic:
simp [hx, this]
-- Module: Mathlib.Combinatorics.KatonaCircle
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
hx : x ∉ s
⊢ (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, ⋯⟩) : X) :
          X))
      ((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) :
            Fin (Fintype.card X)))
        x) =
    x

Tactic:
simp [hx]
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
inl :
  ∀ (hns : (↑n : ℕ) < #s),
    (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) :
            Fin (Fintype.card X)))
        ((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, ⋯⟩) : X) :
              X))
          n) =
      n
inr :
  ∀ (hsn : #s ≤ (↑n : ℕ)),
    (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) :
            Fin (Fintype.card X)))
        ((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, ⋯⟩) : X) :
              X))
          n) =
      n
⊢ (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) :
          Fin (Fintype.card X)))
      ((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, ⋯⟩) : X) :
            X))
        n) =
    n

Tactic:
obtain hns | hsn := lt_or_ge n.1 #s

Premises used: Fin.val, Finset.card, lt_or_ge
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hns : (↑n : ℕ) < #s
⊢ (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) :
          Fin (Fintype.card X)))
      ((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, ⋯⟩) : X) :
            X))
        n) =
    n

Tactic:
simp [hns]
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
x : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
n : Fin (Fintype.card X)
hsn : #s ≤ (↑n : ℕ)
⊢ (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) :
          Fin (Fintype.card X)))
      ((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, ⋯⟩) : X) :
            X))
        n) =
    n

Tactic:
simp [hsn.not_gt, hsn, mem_compl.1 <| Subtype.prop _]

Premises used: Finset.mem_compl, LE.le.not_gt, Subtype.prop, Iff.mp
-- Module: Mathlib.Combinatorics.KatonaCircle
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
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

Tactic:
simpa [hx, -Fin.is_lt] using (g _).is_lt

Premises used: Fin.is_lt, DFunLike.coe
-- Module: Mathlib.Combinatorics.KatonaCircle
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
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

Tactic:
simp [hx]
-- Module: Mathlib.Combinatorics.KatonaCircle
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
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

Tactic:
simp [hx]
-- 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
hx : x ∉ s
⊢ #s ≤ (↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) x) : ℕ)

Tactic:
rw [mem_prefixed.1 f.2, not_lt] at hx

Premises used: not_lt, Iff.mp, Numbering.mem_prefixed, Subtype.property
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
f : Numbering X
s_1 t : Finset X
inst_1 : DecidableEq X
s : Finset X
g : Numbering ↥s × Numbering ↥sᶜ
⊢ (fun (f : ↥(prefixed s)) ↦
        (({ toFun := fun (x : ↥s) ↦ ⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ), ⋯⟩,
              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 : ℕ), ⋯⟩) ⋯,
              left_inv := ⋯, right_inv := ⋯ },
            {
              toFun := fun (x : ↥sᶜ) ↦
                ⟨(↑(((↑f : Numbering X) : (a : X) → Fin (Fintype.card X)) (↑x : X)) : ℕ) - #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 := ⋯ }) :
          Numbering ↥s × Numbering ↥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, ⋯⟩) : X),
                  left_inv := ⋯, right_inv := ⋯ }
                ⋯ :
            ↥(prefixed s)))
        g) =
    g

Tactic:
simp +contextual [Prod.ext_iff, DFunLike.ext_iff]

Premises used: Prod.ext_iff, DFunLike.ext_iff
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
inst_1 : DecidableEq X
s : Finset X
⊢ Finset.card (α := Numbering X) (prefixed s) = (#s)! * (Fintype.card X - #s)!

Tactic:
simpa [-mem_prefixed] using Fintype.card_congr (prefixedEquiv s)

Premises used: Numbering.prefixedEquiv, Fintype.card_congr, Numbering.mem_prefixed
-- Module: Mathlib.Combinatorics.KatonaCircle
Goal:
X : Type u_1
inst : Fintype X
inst_1 : DecidableEq X
s : Finset X
⊢ dens (α := Numbering X) (prefixed s) = (↑((Fintype.card X).choose #s) : ℚ≥0)⁻¹

Tactic:
simp [dens, card_prefixed, Nat.cast_choose _ s.card_le_univ]

Premises used: Finset.dens, Finset.card_le_univ, Numbering.card_prefixed, Nat.cast_choose