awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
J_1 K L : I → Prop
inst : (i : I) → Decidable (J_1 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
J : (Finset I)ᵒᵖ
⊢ CompHausLike.ofHom (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
      { toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop J) (K := fun (x : I) ↦ x ∈ unop J) ⋯,
        continuous_toFun := ⋯ } =
    𝟙 (of (↑(π C fun (x : I) ↦ x ∈ unop J) : Type u))
have simp : CompHausLike.ofHom (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
    { toFun := id, continuous_toFun := sorry } =
  𝟙 (of (↑(π C fun (x : I) ↦ x ∈ unop J) : Type u))
Tactic: simp only [projRestricts_eq_id C (· ∈ (unop J))]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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 Y Z : (Finset I)ᵒᵖ
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α := of (↑(π C fun (x : I) ↦ x ∈ unop X) : Type u) ⟶ of (↑(π C fun (x : I) ↦ x ∈ unop Z) : Type u))
    (CompHausLike.ofHom (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
      { toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop X) ⋯,
        continuous_toFun := ⋯ })
    (CompHausLike.ofHom (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
      (comp (β := (↑(π C fun (x : I) ↦ x ∈ unop Y) : Type u))
        { toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop Y) ⋯,
          continuous_toFun := ⋯ }
        { toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Y) (K := fun (x : I) ↦ x ∈ unop X) ⋯,
          continuous_toFun := ⋯ }))
have e_f : Eq (α := (↑(π C fun (x : I) ↦ x ∈ unop X) : Type u) → (↑(π C fun (x : I) ↦ x ∈ unop Z) : Type u))
  (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop X) sorry)
  (Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ unop Y) : Type u))
    (⇑{ toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop Y) sorry,
          continuous_toFun := sorry } :
      (a : (↑(π C fun (x : I) ↦ x ∈ unop Y) : Type u)) → (↑(π C fun (x : I) ↦ x ∈ unop Z) : Type u))
    (⇑{ toFun := ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Y) (K := fun (x : I) ↦ x ∈ unop X) sorry,
          continuous_toFun := sorry } :
      (a : (↑(π C fun (x : I) ↦ x ∈ unop X) : Type u)) → (↑(π C fun (x : I) ↦ x ∈ unop Y) : Type u)))
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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 Y Z : (Finset I)ᵒᵖ
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α := (↑(π C fun (x : I) ↦ x ∈ unop X) : Type u) → (↑(π C fun (x : I) ↦ x ∈ unop Z) : Type u))
    (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop X) ⋯)
    (Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ unop Y) : Type u))
      (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop Y) ⋯)
      (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Y) (K := fun (x : I) ↦ x ∈ unop X) ⋯))
have e_f : Eq (α := (↑(π C fun (x : I) ↦ x ∈ unop X) : Type u) → (↑(π C fun (x : I) ↦ x ∈ unop Z) : Type u))
  (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop X) sorry)
  (ProjRestricts C (J := fun (x : I) ↦ x ∈ unop Z) (K := fun (x : I) ↦ x ∈ unop X) sorry)
Tactic: rw [projRestricts_eq_comp]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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)))
have 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)
Tactic: ext _ i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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))
have 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)
Tactic: ext _ i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
i : I
⊢ IsLocallyConstant (Y := ℤ) fun (f : (↑C : Type u)) ↦ if (↑f : I → Bool) i = true then 1 else 0
have rw : Continuous (Y := ℤ) fun (f : (↑C : Type u)) ↦ if (↑f : I → Bool) i = true then 1 else 0
Tactic: rw [IsLocallyConstant.iff_continuous]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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)
have h : ∀ (x x_1 : Products I), x < x_1 ↔ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑x : List I) (↑x_1 : List I)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
⊢ WellFoundedLT.{u} (Products I)
have 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)
Tactic: have : (· < · : Products I → _ → _) = (fun l m ↦ List.Lex (· < ·) l.val m.val) := by
    ext; exact lt_iff_lex_lt _ _
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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)
⊢ WellFoundedLT.{u} (Products I)
have rw : IsWellFounded.{u} (Products I) fun (l m : Products I) ↦ List.Lex (fun (x1 x2 : I) ↦ x1 < x2) (↑l : List I) (↑m : List I)
Tactic: rw [WellFoundedLT, this]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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 (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)
have 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)
Tactic: rw [(by rfl : (· > · : I → _) = flip (· < ·))]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
a : Products I
ha : Products.isGood C a
⊢ ∀ ⦃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₂
have 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
Tactic: ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ 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
have 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
Tactic: by_contra! hne
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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
⊢ False
have 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)
Tactic: apply hb
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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 b)
have 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)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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) b hb <
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha
⊢ False
have inr : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
  (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < a})) (Products.eval C a)
Tactic: apply ha
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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) b hb <
    Subtype.mk (p := fun (l : Products I) ↦ Products.isGood C l) a ha
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < a})) (Products.eval C a)
have inr : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
  (span ℤ (Set.image (α := Products I) (Products.eval C) {m : Products I | m < a})) (Products.eval C b)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (hypothesis)
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
⊢ False
have x : 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 ∨
  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
Tactic: cases hne.lt_or_gt with
  | inl h' => apply hb; rw [← h]; exact Submodule.subset_span ⟨a, h', rfl⟩
  | inr h' => apply ha; rw [h]; exact Submodule.subset_span ⟨b, h', rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
⊢ Eq (α := ℤ) ((eval C l : (a : (↑C : Type u)) → ℤ) x : ℤ)
    (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0 : ℤ)
have change : Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (eval C l) : ℤ)
  (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0 : ℤ)
Tactic: change LocallyConstant.evalMonoidHom x (l.eval C) = _
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
⊢ Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (eval C l) : ℤ)
    (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0 : ℤ)
have rw : Eq (α := ℤ)
  (List.prod
    (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
      (List.map (e C) (↑l : List I))))
  (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0)
Tactic: rw [eval, map_list_prod]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
⊢ Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
        (List.map (e C) (↑l : List I))))
    (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0)
have pos : ∀ (h : ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true),
  Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
        (List.map (e C) (↑l : List I))))
    1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
pos :
  ∀ (h : ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true),
    Eq (α := ℤ)
      (List.prod
        (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
          (List.map (e C) (↑l : List I))))
      1
⊢ Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
        (List.map (e C) (↑l : List I))))
    (if ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true then 1 else 0)
have neg : ∀ (h : ¬∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true),
  Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
        (List.map (e C) (↑l : List I))))
    0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
⊢ Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
        (List.map (e C) (↑l : List I))))
    1
have pos : Eq (α := ℤ)
  (List.prod
    (List.map ((⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) ∘ e C) (↑l : List I)))
  1
Tactic: simp only [List.map_map]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
⊢ Eq (α := ℤ)
    (List.prod
      (List.map ((⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) ∘ e C) (↑l : List I)))
    1
have pos : ∀ (x_1 : ℤ),
  Membership.mem (γ := List ℤ)
      (List.map ((⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) ∘ e C) (↑l : List I))
      x_1 →
    x_1 = 1
Tactic: apply List.prod_eq_one
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
⊢ ∀ (x_1 : ℤ),
    Membership.mem (γ := List ℤ)
        (List.map ((⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) ∘ e C)
          (↑l : List I))
        x_1 →
      x_1 = 1
have pos : ∀ (x_1 : ℤ),
  (∃ a ∈ (↑l : List I), (LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C a) = x_1) →
    x_1 = 1
Tactic: simp only [List.mem_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ¬∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
⊢ Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ)
        (List.map (e C) (↑l : List I))))
    0
have neg : ∃ a ∈ (↑l : List I),
  Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C a) : ℤ) (0 : ℤ)
Tactic: simp only [List.map_map, List.prod_eq_zero_iff, List.mem_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ¬∀ i ∈ (↑l : List I), (↑x : I → Bool) i = true
⊢ ∃ a ∈ (↑l : List I),
    Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C a) : ℤ) (0 : ℤ)
have h₁ : ∃ i ∈ (↑l : List I), (↑x : I → Bool) i ≠ true
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∃ i ∈ (↑l : List I), (↑x : I → Bool) i ≠ true
⊢ ∃ a ∈ (↑l : List I),
    Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C a) : ℤ) (0 : ℤ)
have h₁ : ∀ (i : I),
  Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C i) : ℤ) (0 : ℤ) ↔
    (↑x : I → Bool) i ≠ true
Tactic: convert! h with i
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
x : (↑C : Type u)
h : ∃ i ∈ (↑l : List I), (↑x : I → Bool) i ≠ true
i : I
⊢ Eq (α := ℤ) ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u) ℤ) → ℤ) (e C i) : ℤ) (0 : ℤ) ↔
    (↑x : I → Bool) i ≠ true
have h₁ : Eq (α := ℤ) (if (↑x : I → Bool) i = true then 1 else 0) 0 ↔ ¬(↑x : I → Bool) i = true
Tactic: dsimp [LocallyConstant.evalMonoidHom, e]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ (↑l : List I), J a
inst_1 : (j : I) → Decidable (J j)
⊢ Eq (α := (↑C : Type u) → ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ) (ProjRestrict C J))
    (⇑(eval C l) : (a : (↑C : Type u)) → ℤ)
have h₁ : ∀ (x : (↑C : Type u)),
  Eq (α := ℤ)
    (Function.comp (β := (↑(π C J) : Type u)) (⇑(eval (π C J) l) : (a : (↑(π C J) : Type u)) → ℤ) (ProjRestrict C J) x :
      ℤ)
    ((eval C l : (a : (↑C : Type u)) → ℤ) x : ℤ)
Tactic: ext x