awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
h :
  ∀ (x : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    Membership.mem (γ :=
        Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        (Set.preimage (β := Bool)
            (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
              decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
            {false})ᶜ
        x ↔
      x ∈ (↑C : Set (↑S.toTop : Type u))
⊢ (Set.preimage (β := Bool)
        (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
          decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
        {false})ᶜ =
    (↑C : Set (↑S.toTop : Type u))

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
x : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ Membership.mem (γ :=
      Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      (Set.preimage (β := Bool)
          (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
            decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
          {false})ᶜ
      x ↔
    x ∈ (↑C : Set (↑S.toTop : Type u))

Tactic:
simp
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
⊢ IsOpen.{u} (X := (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {true})

Tactic:
IsClopen.isOpen ?_

Premises used: IsClopen.isOpen
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
h :
  IsClopen.{u} (X := (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {true})
⊢ IsOpen.{u} (X := (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {true})

Tactic:
refine IsClopen.isOpen ?_

Premises used: IsClopen.isOpen
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
h :
  Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {true} =
    (↑C : Set (↑S.toTop : Type u))
⊢ IsClopen.{u} (X := (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {true})

Tactic:
convert! C.2

Premises used: Subtype.property
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
h :
  ∀ (x : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    Membership.mem (γ :=
        Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        (Set.preimage (β := Bool)
          (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
            decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
          {true})
        x ↔
      x ∈ (↑C : Set (↑S.toTop : Type u))
⊢ Set.preimage (β := Bool)
      (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
        decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
      {true} =
    (↑C : Set (↑S.toTop : Type u))

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
C :
  { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
    IsClopen C }
x : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ Membership.mem (γ :=
      Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      (Set.preimage (β := Bool)
        (fun (a : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
          decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
        {true})
      x ↔
    x ∈ (↑C : Set (↑S.toTop : Type u))

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff, decide_eq_true_eq]

Premises used: Set.mem_singleton_iff, decide_eq_true_eq, Set.mem_preimage
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
a b : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : ι S a = ι S b
hf : ∀ (hn : ¬a = b), False
⊢ a = b

Tactic:
by_contra hn
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
a b : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : ι S a = ι S b
hn : ¬a = b
hf :
  ∀ (C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    (hC : IsClopen C) (hh : a ∈ C ∧ b ∈ Cᶜ), False
⊢ False

Tactic:
obtain ⟨C, hC, hh⟩ := exists_isClopen_of_totally_separated hn

Premises used: exists_isClopen_of_totally_separated
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
a b : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h : ι S a = ι S b
hn : ¬a = b
C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
hf : decide (b ∈ C) = true
⊢ False

Tactic:
apply hh.2 ∘ of_decide_eq_true

Premises used: of_decide_eq_true, And.right
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
a b : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h :
  Eq.{u + 1} (α :=
    { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
        IsClopen C } →
      Bool)
    (fun
        (C :
          { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
            IsClopen C }) ↦
      decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
    fun
      (C :
        { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
          IsClopen C }) ↦
    decide (b ∈ (↑C : Set (↑S.toTop : Type u)))
hn : ¬a = b
C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
hf :
  decide
      (a ∈
        (↑(Subtype.mk (p :=
              fun
                (C :
                  Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
              IsClopen C) C hC) :
          Set (↑S.toTop : Type u))) =
    true
⊢ decide (b ∈ C) = true

Tactic:
rw [← congr_fun h ⟨C, hC⟩]

Premises used: Subtype.mk, congr_fun
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
a b : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h :
  Eq.{u + 1} (α :=
    { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
        IsClopen C } →
      Bool)
    (fun
        (C :
          { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
            IsClopen C }) ↦
      decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
    fun
      (C :
        { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
          IsClopen C }) ↦
    decide (b ∈ (↑C : Set (↑S.toTop : Type u)))
hn : ¬a = b
C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide
      (a ∈
        (↑(Subtype.mk (p :=
              fun
                (C :
                  Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
              IsClopen C) C hC) :
          Set (↑S.toTop : Type u))) =
    true

Tactic:
decide_eq_true hh.1

Premises used: decide_eq_true, And.left
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
a b : (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
h :
  Eq.{u + 1} (α :=
    { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
        IsClopen C } →
      Bool)
    (fun
        (C :
          { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
            IsClopen C }) ↦
      decide (a ∈ (↑C : Set (↑S.toTop : Type u))))
    fun
      (C :
        { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
          IsClopen C }) ↦
    decide (b ∈ (↑C : Set (↑S.toTop : Type u)))
hn : ¬a = b
C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide
      (a ∈
        (↑(Subtype.mk (p :=
              fun
                (C :
                  Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) ↦
              IsClopen C) C hC) :
          Set (↑S.toTop : Type u))) =
    true

Tactic:
exact decide_eq_true hh.1

Premises used: decide_eq_true, And.left
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
obtain :
  ∀
    (w :
      LinearOrder
        { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
          IsClopen C }),
    WellFoundedLT.{u}
        { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
          IsClopen C } →
      Free.{0, u} ℤ
        (LocallyConstant (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
          ℤ)
⊢ Free.{0, u} ℤ
    (LocallyConstant (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ℤ)

Tactic:
obtain ⟨_, _⟩ := exists_wellFoundedLT {C : Set S // IsClopen C}

Premises used: Subtype, exists_wellFoundedLT, IsClopen
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
w :
  LinearOrder
    { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
      IsClopen C }
h :
  WellFoundedLT.{u}
    { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
      IsClopen C }
⊢ Free.{0, u} ℤ
    (LocallyConstant (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ℤ)

Tactic:
@Nobeling_aux {C : Set S // IsClopen C} _ _ S (Nobeling.ι S) (Nobeling.isClosedEmbedding S)

Premises used: Profinite.NobelingProof.Nobeling_aux, Profinite.Nobeling.isClosedEmbedding
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction
Goal:
S : Profinite
w :
  LinearOrder
    { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
      IsClopen C }
h :
  WellFoundedLT.{u}
    { C : Set (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) //
      IsClopen C }
⊢ Free.{0, u} ℤ
    (LocallyConstant (↑(S.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) ℤ)

Tactic:
exact @Nobeling_aux {C : Set S // IsClopen C} _ _ S (Nobeling.ι S) (Nobeling.isClosedEmbedding S)

Premises used: Profinite.NobelingProof.Nobeling_aux, Profinite.Nobeling.isClosedEmbedding
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
l : Products I
hl : Products.isGood (π C fun (x : I) ↦ x ∈ s) l
h :
  ∀ (f : (↑C : Type u)),
    Eq (α := ℤ) ((Products.eval C l : (a : (↑C : Type u)) → ℤ) f : ℤ)
      ((((πJ C s : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
                (Products.eval (π C fun (x : I) ↦ x ∈ s) l) :
              LocallyConstant (↑C : Type u) ℤ) :
            (a : (↑C : Type u)) → ℤ)
          f :
        ℤ)
⊢ Products.eval C l =
    (πJ C s : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
      (Products.eval (π C fun (x : I) ↦ x ∈ s) l)

Tactic:
ext f
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
l : Products I
hl : Products.isGood (π C fun (x : I) ↦ x ∈ s) l
f : (↑C : Type u)
h :
  Eq (α := ℤ) ((Products.eval C l : (a : (↑C : Type u)) → ℤ) f : ℤ)
    ((Products.eval (π C fun (x : I) ↦ x ∈ s) l : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        (({ toFun := ProjRestrict C fun (x : I) ↦ x ∈ s, continuous_toFun := ⋯ } :
              (a : (↑C : Type u)) → (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
            f :
          (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) :
      ℤ)
⊢ Eq (α := ℤ) ((Products.eval C l : (a : (↑C : Type u)) → ℤ) f : ℤ)
    ((((πJ C s : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ)
              (Products.eval (π C fun (x : I) ↦ x ∈ s) l) :
            LocallyConstant (↑C : Type u) ℤ) :
          (a : (↑C : Type u)) → ℤ)
        f :
      ℤ)

Tactic:
simp only [πJ, LocallyConstant.comapₗ, LinearMap.coe_mk, AddHom.coe_mk,
    LocallyConstant.coe_comap, Function.comp_apply]

Premises used: LinearMap.coe_mk, Profinite.NobelingProof.πJ, LocallyConstant.coe_comap, LocallyConstant.comapₗ, Function.comp_apply, AddHom.coe_mk
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
l : Products I
hl : Products.isGood (π C fun (x : I) ↦ x ∈ s) l
f : (↑C : Type u)
⊢ Eq (α := ℤ) ((Products.eval C l : (a : (↑C : Type u)) → ℤ) f : ℤ)
    ((Products.eval (π C fun (x : I) ↦ x ∈ s) l : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        (({ toFun := ProjRestrict C fun (x : I) ↦ x ∈ s, continuous_toFun := ⋯ } :
              (a : (↑C : Type u)) → (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
            f :
          (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) :
      ℤ)

Tactic:
(congr_fun (Products.evalFacProp C (· ∈ s) (Products.prop_of_isGood C (· ∈ s) hl)) _).symm

Premises used: Subtype.map, Membership.mem, Profinite.NobelingProof.ProjRestrict, Profinite.NobelingProof.Products.prop_of_isGood, Profinite.NobelingProof.Products.evalFacProp, congr_fun, Eq.symm, Set.MapsTo.restrict
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
l : Products I
hl : Products.isGood (π C fun (x : I) ↦ x ∈ s) l
f : (↑C : Type u)
⊢ Eq (α := ℤ) ((Products.eval C l : (a : (↑C : Type u)) → ℤ) f : ℤ)
    ((Products.eval (π C fun (x : I) ↦ x ∈ s) l : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        (({ toFun := ProjRestrict C fun (x : I) ↦ x ∈ s, continuous_toFun := ⋯ } :
              (a : (↑C : Type u)) → (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
            f :
          (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) :
      ℤ)

Tactic:
exact (congr_fun (Products.evalFacProp C (· ∈ s) (Products.prop_of_isGood C (· ∈ s) hl)) _).symm

Premises used: Membership.mem, Profinite.NobelingProof.Products.prop_of_isGood, Profinite.NobelingProof.Products.evalFacProp, congr_fun, Eq.symm
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
refine : Function.Injective f
⊢ Fintype (↑(π C fun (x : I) ↦ x ∈ s) : Type u)

Tactic:
refine Fintype.ofInjective f ?_

Premises used: Fintype.ofInjective
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
x : I → Bool
hx : x ∈ C
this :
  ∀ (y : I → Bool) (hy : y ∈ C),
    f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) =
        f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯) →
      Eq (α := (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
        (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯)
        (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯)
⊢ ∀ ⦃a₂ : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)⦄,
    f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) = f a₂ →
      Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯ = a₂

Tactic:
⟨_, y, hy, rfl⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
x : I → Bool
hx : x ∈ C
y : I → Bool
hy : y ∈ C
h :
  f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) =
    f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯)
a :
  ∀ (i : I),
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) : I → Bool)
        i =
      (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯) :
          I → Bool)
        i
⊢ Eq (α := (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
    (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯)
    (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯)

Tactic:
ext i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
x : I → Bool
hx : x ∈ C
y : I → Bool
hy : y ∈ C
h :
  f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) =
    f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯)
i : I
pos :
  ∀ (hi : i ∈ s),
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) : I → Bool)
        i =
      (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯) :
          I → Bool)
        i
neg :
  ∀ (hi : i ∉ s),
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) : I → Bool)
        i =
      (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯) :
          I → Bool)
        i
⊢ (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) : I → Bool)
      i =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯) : I → Bool)
      i

Tactic:
by_cases hi : i ∈ s
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
x : I → Bool
hx : x ∈ C
y : I → Bool
hy : y ∈ C
h :
  f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) =
    f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯)
i : I
hi : i ∈ s
⊢ (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) : I → Bool)
      i =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯) : I → Bool)
      i

Tactic:
congrFun h ⟨i, hi⟩

Premises used: Subtype.mk, congrFun
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
x : I → Bool
hx : x ∈ C
y : I → Bool
hy : y ∈ C
h :
  f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) =
    f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯)
i : I
hi : i ∈ s
⊢ (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) : I → Bool)
      i =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯) : I → Bool)
      i

Tactic:
exact congrFun h ⟨i, hi⟩

Premises used: Subtype.mk, congrFun
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) → ↥s → Bool :=
  fun (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (j : ↥s) ↦ (↑x : I → Bool) (↑j : I)
x : I → Bool
hx : x ∈ C
y : I → Bool
hy : y ∈ C
h :
  f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) =
    f (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯)
i : I
hi : i ∉ s
⊢ (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) x) ⋯) : I → Bool)
      i =
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) y) ⋯) : I → Bool)
      i

Tactic:
simp only [Proj, if_neg hi]

Premises used: Profinite.NobelingProof.Proj, if_neg