awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s t : Finset I
f : unop (op t) ≤ unop (op s)
x :
  (↑(((spanFunctor (C := C) hC).obj (op s)).toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
h :
  ∀ (x : (↑(π C (Membership.mem (unop (op s)))) : Type u)) (i : ↥t),
    Eq (α := Bool)
      ((↑(Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ t) : Type u))
              (⇑(iso_map C fun (x : I) ↦ x ∈ t) :
                (a : (↑(π C fun (x : I) ↦ x ∈ t) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ t) : Type u))
              (ProjRestricts C (J := fun (x : I) ↦ x ∈ t) (K := Membership.mem (unop (op s))) f) x) :
          (i : ↥t) → Bool)
        i)
      ((↑(Function.comp (β := (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C (Membership.mem (unop (op s)))) : Type u))
              (⇑(IndexFunctor.map (X := fun (i : I) ↦ Bool) C (J := Membership.mem (unop (op t))) (K :=
                    Membership.mem (unop (op s))) f) :
                (a : (↑(IndexFunctor.obj C (Membership.mem (unop (op s)))) : Type u)) →
                  (↑(IndexFunctor.obj C (Membership.mem (unop (op t)))) : Type u))
              (⇑(iso_map C fun (x : I) ↦ x ∈ s) :
                (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
              x) :
          (i : ↥t) → Bool)
        i)
⊢ Eq (α :=
    (↑(π C (Membership.mem (unop (op s)))) : Type u) →
      (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ t) : Type u))
    (Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ t) : Type u))
      (⇑(iso_map C fun (x : I) ↦ x ∈ t) :
        (a : (↑(π C fun (x : I) ↦ x ∈ t) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ t) : Type u))
      (ProjRestricts C (J := fun (x : I) ↦ x ∈ t) (K := Membership.mem (unop (op s))) f))
    (Function.comp (β := (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C (Membership.mem (unop (op s)))) : Type u))
      (⇑(IndexFunctor.map (X := fun (i : I) ↦ Bool) C (J := Membership.mem (unop (op t))) (K :=
            Membership.mem (unop (op s))) f) :
        (a : (↑(IndexFunctor.obj C (Membership.mem (unop (op s)))) : Type u)) →
          (↑(IndexFunctor.obj C (Membership.mem (unop (op t)))) : Type u))
      (⇑(iso_map C fun (x : I) ↦ x ∈ s) :
        (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u)))

Tactic:
ext _ i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s t : Finset I
f : unop (op t) ≤ unop (op s)
x :
  (↑(((spanFunctor (C := C) hC).obj (op s)).toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
x_1 : (↑(π C (Membership.mem (unop (op s)))) : Type u)
i : ↥t
⊢ Eq (α := Bool)
    ((↑(Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ t) : Type u))
            (⇑(iso_map C fun (x : I) ↦ x ∈ t) :
              (a : (↑(π C fun (x : I) ↦ x ∈ t) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ t) : Type u))
            (ProjRestricts C (J := fun (x : I) ↦ x ∈ t) (K := Membership.mem (unop (op s))) f) x_1) :
        (i : ↥t) → Bool)
      i)
    ((↑(Function.comp (β := (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C (Membership.mem (unop (op s)))) : Type u))
            (⇑(IndexFunctor.map (X := fun (i : I) ↦ Bool) C (J := Membership.mem (unop (op t))) (K :=
                  Membership.mem (unop (op s))) f) :
              (a : (↑(IndexFunctor.obj C (Membership.mem (unop (op s)))) : Type u)) →
                (↑(IndexFunctor.obj C (Membership.mem (unop (op t)))) : Type u))
            (⇑(iso_map C fun (x : I) ↦ x ∈ s) :
              (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
            x_1) :
        (i : ↥t) → Bool)
      i)

Tactic:
dif_pos i.prop

Premises used: Set.Mem, setOf, dif_pos, Profinite.NobelingProof.Proj, dite, Subtype.prop, ite
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s t : Finset I
f : unop (op t) ≤ unop (op s)
x :
  (↑(((spanFunctor (C := C) hC).obj (op s)).toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
x_1 : (↑(π C (Membership.mem (unop (op s)))) : Type u)
i : ↥t
⊢ Eq (α := Bool)
    ((↑(Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ t) : Type u))
            (⇑(iso_map C fun (x : I) ↦ x ∈ t) :
              (a : (↑(π C fun (x : I) ↦ x ∈ t) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ t) : Type u))
            (ProjRestricts C (J := fun (x : I) ↦ x ∈ t) (K := Membership.mem (unop (op s))) f) x_1) :
        (i : ↥t) → Bool)
      i)
    ((↑(Function.comp (β := (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C (Membership.mem (unop (op s)))) : Type u))
            (⇑(IndexFunctor.map (X := fun (i : I) ↦ Bool) C (J := Membership.mem (unop (op t))) (K :=
                  Membership.mem (unop (op s))) f) :
              (a : (↑(IndexFunctor.obj C (Membership.mem (unop (op s)))) : Type u)) →
                (↑(IndexFunctor.obj C (Membership.mem (unop (op t)))) : Type u))
            (⇑(iso_map C fun (x : I) ↦ x ∈ s) :
              (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
            x_1) :
        (i : ↥t) → Bool)
      i)

Tactic:
exact dif_pos i.prop

Premises used: dif_pos, Subtype.prop
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s t : Finset I
f : unop (op t) ≤ unop (op s)
x :
  (↑(((spanFunctor (C := C) hC).obj (op s)).toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
⊢ Eq (α :=
    (↑(π C (Membership.mem (unop (op s)))) : Type u) →
      (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ t) : Type u))
    (Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ t) : Type u))
      (⇑(iso_map C fun (x : I) ↦ x ∈ t) :
        (a : (↑(π C fun (x : I) ↦ x ∈ t) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ t) : Type u))
      (ProjRestricts C (J := fun (x : I) ↦ x ∈ t) (K := Membership.mem (unop (op s))) f))
    (Function.comp (β := (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C (Membership.mem (unop (op s)))) : Type u))
      (⇑(IndexFunctor.map (X := fun (i : I) ↦ Bool) C (J := Membership.mem (unop (op t))) (K :=
            Membership.mem (unop (op s))) f) :
        (a : (↑(IndexFunctor.obj C (Membership.mem (unop (op s)))) : Type u)) →
          (↑(IndexFunctor.obj C (Membership.mem (unop (op t)))) : Type u))
      (⇑(iso_map C fun (x : I) ↦ x ∈ s) :
        (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u)))

Tactic:
have : iso_map C (· ∈ t) ∘ ProjRestricts C f =
            IndexFunctor.map C f ∘ iso_map C (· ∈ s) := by
          ext _ i; exact dif_pos i.prop
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
x : (Finset I)ᵒᵖ
s : Finset I
a :
  (↑((Functor.obj
            (Functor.obj (Functor.const (Finset I)ᵒᵖ)
              (Cone.pt (F := indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC)
                (indexCone (X := fun (i : I) ↦ Bool) (C := C) hC)))
            (op s)).toTop
        (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
h :
  ∀ (x : (↑C : Type u)) (i : ↥s),
    Eq (α := Bool)
      ((↑(Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
              (⇑(iso_map C fun (x : I) ↦ x ∈ s) :
                (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
              (ProjRestrict C fun (x : I) ↦ x ∈ s) x) :
          (i : ↥s) → Bool)
        i)
      ((↑((IndexFunctor.π_app (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ s :
                (a : (↑C : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
              x) :
          (i : ↥s) → Bool)
        i)
⊢ Eq (α := (↑C : Type u) → (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ s) : Type u))
    (Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
      (⇑(iso_map C fun (x : I) ↦ x ∈ s) :
        (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
      (ProjRestrict C fun (x : I) ↦ x ∈ s))
    (⇑(IndexFunctor.π_app (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ s) :
      (a : (↑C : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))

Tactic:
ext _ i
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
x : (Finset I)ᵒᵖ
s : Finset I
a :
  (↑((Functor.obj
            (Functor.obj (Functor.const (Finset I)ᵒᵖ)
              (Cone.pt (F := indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC)
                (indexCone (X := fun (i : I) ↦ Bool) (C := C) hC)))
            (op s)).toTop
        (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
x_1 : (↑C : Type u)
i : ↥s
⊢ Eq (α := Bool)
    ((↑(Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
            (⇑(iso_map C fun (x : I) ↦ x ∈ s) :
              (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
            (ProjRestrict C fun (x : I) ↦ x ∈ s) x_1) :
        (i : ↥s) → Bool)
      i)
    ((↑((IndexFunctor.π_app (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ s :
              (a : (↑C : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
            x_1) :
        (i : ↥s) → Bool)
      i)

Tactic:
dif_pos i.prop

Premises used: Set.Mem, setOf, dif_pos, Profinite.NobelingProof.Proj, dite, Subtype.prop, ite
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
x : (Finset I)ᵒᵖ
s : Finset I
a :
  (↑((Functor.obj
            (Functor.obj (Functor.const (Finset I)ᵒᵖ)
              (Cone.pt (F := indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC)
                (indexCone (X := fun (i : I) ↦ Bool) (C := C) hC)))
            (op s)).toTop
        (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
x_1 : (↑C : Type u)
i : ↥s
⊢ Eq (α := Bool)
    ((↑(Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
            (⇑(iso_map C fun (x : I) ↦ x ∈ s) :
              (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
            (ProjRestrict C fun (x : I) ↦ x ∈ s) x_1) :
        (i : ↥s) → Bool)
      i)
    ((↑((IndexFunctor.π_app (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ s :
              (a : (↑C : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
            x_1) :
        (i : ↥s) → Bool)
      i)

Tactic:
exact dif_pos i.prop

Premises used: dif_pos, Subtype.prop
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
x : (Finset I)ᵒᵖ
s : Finset I
a :
  (↑((Functor.obj
            (Functor.obj (Functor.const (Finset I)ᵒᵖ)
              (Cone.pt (F := indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC)
                (indexCone (X := fun (i : I) ↦ Bool) (C := C) hC)))
            (op s)).toTop
        (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
⊢ Eq (α := (↑C : Type u) → (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ s) : Type u))
    (Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ s) : Type u))
      (⇑(iso_map C fun (x : I) ↦ x ∈ s) :
        (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
      (ProjRestrict C fun (x : I) ↦ x ∈ s))
    (⇑(IndexFunctor.π_app (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ s) :
      (a : (↑C : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))

Tactic:
have : iso_map C (· ∈ s) ∘ ProjRestrict C (· ∈ s) = IndexFunctor.π_app C (· ∈ s) := by
        ext _ i; exact dif_pos i.prop
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
i : I
rw : Continuous (Y := ℤ) fun (f : (↑C : Type u)) ↦ if (↑f : I → Bool) i = true then 1 else 0
⊢ IsLocallyConstant (Y := ℤ) fun (f : (↑C : Type u)) ↦ if (↑f : I → Bool) i = true then 1 else 0

Tactic:
rw [IsLocallyConstant.iff_continuous]

Premises used: IsLocallyConstant.iff_continuous
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
i : I
⊢ Continuous (Y := ℤ) fun (f : (↑C : Type u)) ↦ if (↑f : I → Bool) i = true then 1 else 0

Tactic:
(continuous_of_discreteTopology (f := fun (a : Bool) ↦ (if a then (1 : ℤ) else 0))).comp
      ((continuous_apply i).comp continuous_subtype_val)

Premises used: continuous_subtype_val, Continuous.comp, continuous_apply, continuous_of_discreteTopology, ite
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
i : I
⊢ Continuous (Y := ℤ) fun (f : (↑C : Type u)) ↦ if (↑f : I → Bool) i = true then 1 else 0

Tactic:
exact (continuous_of_discreteTopology (f := fun (a : Bool) ↦ (if a then (1 : ℤ) else 0))).comp
      ((continuous_apply i).comp continuous_subtype_val)

Premises used: Continuous.comp, continuous_of_discreteTopology
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
inst : LinearOrder I
l m : Products I
⊢ l < m ↔ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)

Tactic:
simp
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
h : ∀ (x x_1 : Products I), x < x_1 ↔ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑x : List I) (↑x_1 : List I)
⊢ Eq.{u + 1} (α := Products I → Products I → Prop) (fun (x1 x2 : Products I) ↦ x1 < x2) fun (l m : Products I) ↦
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)

Tactic:
ext
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
x x_1 : Products I
⊢ x < x_1 ↔ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑x : List I) (↑x_1 : List I)

Tactic:
lt_iff_lex_lt _ _

Premises used: Profinite.NobelingProof.Products.lt_iff_lex_lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
x x_1 : Products I
⊢ x < x_1 ↔ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑x : List I) (↑x_1 : List I)

Tactic:
exact lt_iff_lex_lt _ _

Premises used: Profinite.NobelingProof.Products.lt_iff_lex_lt
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
⊢ Eq.{u + 1} (α := Products I → Products I → Prop) (fun (x1 x2 : Products I) ↦ x1 < x2) fun (l m : Products I) ↦
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)

Tactic:
have : (· < · : Products I → _ → _) = (fun l m ↦ List.Lex (· < ·) l.val m.val) := by
    ext; exact lt_iff_lex_lt _ _
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
this :
  Eq.{u + 1} (α := Products I → Products I → Prop) (fun (x1 x2 : Products I) ↦ x1 < x2) fun (l m : Products I) ↦
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)
rw :
  IsWellFounded.{u} (Products I) fun (l m : Products I) ↦
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)
⊢ WellFoundedLT.{u} (Products I)

Tactic:
rw [WellFoundedLT, this]

Premises used: WellFoundedLT
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
this :
  Eq.{u + 1} (α := Products I → Products I → Prop) (fun (x1 x2 : Products I) ↦ x1 < x2) fun (l m : Products I) ↦
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)
⊢ Eq.{u + 1} (α := I → I → Prop) (fun (x1 x2 : I) ↦ x1 > x2) (flip fun (x1 x2 : I) ↦ x1 < x2)

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
this :
  Eq.{u + 1} (α := Products I → Products I → Prop) (fun (x1 x2 : Products I) ↦ x1 < x2) fun (l m : Products I) ↦
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)
rw :
  IsWellFounded.{u} { l : List I // List.IsChain (flip fun (x1 x2 : I) ↦ x1 < x2) l }
    fun (l m : { l : List I // List.IsChain (flip fun (x1 x2 : I) ↦ x1 < x2) l }) ↦
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)
⊢ IsWellFounded.{u} { l : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l }
    fun (l m : { l : List I // List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l }) ↦
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)

Tactic:
rw [(by rfl : (· > · : I → _) = flip (· < ·))]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
this :
  Eq.{u + 1} (α := Products I → Products I → Prop) (fun (x1 x2 : Products I) ↦ x1 < x2) fun (l m : Products I) ↦
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)
⊢ IsWellFounded.{u} { l : List I // List.IsChain (flip fun (x1 x2 : I) ↦ x1 < x2) l }
    fun (l m : { l : List I // List.IsChain (flip fun (x1 x2 : I) ↦ x1 < x2) l }) ↦
    List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
inst : LinearOrder I
inst_1 : Inhabited I
i : I
l : Products I
hi : i ∈ (↑l : List I)
⊢ i ≤ (↑l : List I).head!

Tactic:
List.Pairwise.head!_le l.2.sortedGT.sortedGE.pairwise hi

Premises used: List.Pairwise.head!_le, List.SortedGE.pairwise, List.SortedGT.sortedGE, List.IsChain.sortedGT, Subtype.property
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
inst : LinearOrder I
inst_1 : Inhabited I
q l : Products I
h : q < l
hq : (↑q : List I) ≠ []
⊢ (↑q : List I).head! ≤ (↑l : List I).head!

Tactic:
List.head!_le_of_lt l.val q.val h hq

Premises used: List.head!_le_of_lt, Subtype.val
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
a : Products I
ha : Products.isGood C a
this :
  ∀ (b : Products I) (hb : Products.isGood C b),
    eval C (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha) =
        eval C (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb) →
      Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha =
        Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
⊢ ∀ ⦃a₂ : { l : Products I // Products.isGood C l }⦄,
    eval C (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha) = eval C a₂ →
      Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha = a₂

Tactic:
⟨b, hb⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
by_contra! :
  ∀
    (hne :
      Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha ≠
        Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb),
    False
⊢ Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha =
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb

Tactic:
by_contra! hne
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha ≠
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
h' :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha <
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
inl :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < b})) (Products.eval C b)
⊢ False

Tactic:
apply hb
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha ≠
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
h' :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha <
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
inl :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < b})) (Products.eval C a)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < b})) (Products.eval C b)

Tactic:
rw [← h]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha ≠
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
h' :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha <
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < b})) (Products.eval C a)

Tactic:
Submodule.subset_span ⟨a, h', rfl⟩

Premises used: And.intro, Exists.intro, Submodule.subset_span, rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha ≠
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
h' :
  Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha <
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) b hb
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < b})) (Products.eval C a)

Tactic:
exact Submodule.subset_span ⟨a, h', rfl⟩