awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
⊢ ∃ (c : (↑(π C fun (x : I) ↦ x ∈ s) : Type u) →₀ ℤ),
    (c.sum fun (i : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (a : ℤ) ↦ a • spanFinBasis C s i) = f
have h : (Finsupp.sum (Finsupp.onFinset Finset.univ f.toFun sorry) fun (i : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (a : ℤ) ↦
    a • spanFinBasis C s i) =
  f
Tactic: use Finsupp.onFinset (Finset.univ) f.toFun (fun _ _ ↦ Finset.mem_univ _)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
⊢ (Finsupp.sum (Finsupp.onFinset Finset.univ f.toFun ⋯) fun (i : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (a : ℤ) ↦
      a • spanFinBasis C s i) =
    f
have h : ∀ (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)),
  Eq (α := ℤ)
    ((Finsupp.sum (Finsupp.onFinset Finset.univ f.toFun sorry) fun (i : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (a : ℤ) ↦
            a • spanFinBasis C s i :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        x :
      ℤ)
    ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalₗ ℤ x : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (Finsupp.sum (Finsupp.onFinset Finset.univ f.toFun ⋯) fun (i : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) (a : ℤ) ↦
          a • spanFinBasis C s i) :
      ℤ)
    ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
have h : Eq (α := ℤ)
  (if
        Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun sorry : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
          (0 : ℤ) then
      0
    else
      ((↑((Finsupp.onFinset Finset.univ f.toFun sorry : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x) :
            LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        x :
    ℤ)
  ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
Tactic: simp only [zsmul_eq_mul, map_finsuppSum, LocallyConstant.evalₗ_apply,
    LocallyConstant.coe_mul, Pi.mul_apply, spanFinBasis, LocallyConstant.coe_mk, mul_ite, mul_one,
    mul_zero, Finsupp.sum_ite_eq, Finsupp.mem_support_iff, ne_eq, ite_not]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
⊢ Eq (α := ℤ)
    (if
          Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
            (0 : ℤ) then
        0
      else
        ((↑((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x) :
              LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          x :
      ℤ)
    ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
have pos : ∀
  (h :
    Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun sorry : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
      (0 : ℤ)),
  Eq (α := ℤ) (0 : ℤ) ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
pos :
  ∀
    (h :
      Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
        (0 : ℤ)),
    Eq (α := ℤ) (0 : ℤ) ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
⊢ Eq (α := ℤ)
    (if
          Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
            (0 : ℤ) then
        0
      else
        ((↑((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x) :
              LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          x :
      ℤ)
    ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
have neg : ∀
  (h :
    ¬Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun sorry : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
        (0 : ℤ)),
  Eq (α := ℤ)
    (((↑((Finsupp.onFinset Finset.univ f.toFun sorry : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x) :
            LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        x :
      ℤ)
    ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
⊢ Eq (α := ℤ)
    (if
          Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
            (0 : ℤ) then
        0
      else
        ((↑((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x) :
              LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          x :
      ℤ)
    ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
have pos : ∀
  (h :
    Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun sorry : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
      (0 : ℤ)),
  Eq (α := ℤ) (0 : ℤ) ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
Tactic: split_ifs with h <;> [exact h.symm; rfl]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
pos :
  ∀
    (h :
      Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
        (0 : ℤ)),
    Eq (α := ℤ) (0 : ℤ) ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
⊢ Eq (α := ℤ)
    (if
          Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
            (0 : ℤ) then
        0
      else
        ((↑((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x) :
              LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          x :
      ℤ)
    ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
have neg : ∀
  (h :
    ¬Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun sorry : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
        (0 : ℤ)),
  Eq (α := ℤ)
    (((↑((Finsupp.onFinset Finset.univ f.toFun sorry : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x) :
            LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        x :
      ℤ)
    ((f : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
Tactic: split_ifs with h <;> [exact h.symm; rfl]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u_1
C : Set (I → Bool)
x : (↑C : Type u_1)
l : List (LocallyConstant (↑C : Type u_1) ℤ)
⊢ Eq (α := ℤ) ((l.prod : (a : (↑C : Type u_1)) → ℤ) x : ℤ)
    (List.prod (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u_1) ℤ) → ℤ) l) : ℤ)
have rw : Eq (α := ℤ) ((l.prod : (a : (↑C : Type u_1)) → ℤ) x : ℤ)
  ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u_1) ℤ) → ℤ) l.prod : ℤ)
Tactic: rw [← map_list_prod (LocallyConstant.evalMonoidHom x) l, LocallyConstant.evalMonoidHom_apply]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u_1
C : Set (I → Bool)
x : (↑C : Type u_1)
l : List (LocallyConstant (↑C : Type u_1) ℤ)
rw :
  Eq (α := ℤ) ((l.prod : (a : (↑C : Type u_1)) → ℤ) x : ℤ)
    ((LocallyConstant.evalMonoidHom x : (a : LocallyConstant (↑C : Type u_1) ℤ) → ℤ) l.prod : ℤ)
⊢ Eq (α := ℤ) ((l.prod : (a : (↑C : Type u_1)) → ℤ) x : ℤ)
    (List.prod (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u_1) ℤ) → ℤ) l) : ℤ)
have rw₁ : Eq (α := ℤ) ((l.prod : (a : (↑C : Type u_1)) → ℤ) x : ℤ) ((l.prod : (a : (↑C : Type u_1)) → ℤ) x : ℤ)
Tactic: rw [← map_list_prod (LocallyConstant.evalMonoidHom x) l, LocallyConstant.evalMonoidHom_apply]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (1 : ℤ)
have rw : Eq (α := ℤ)
  (List.prod
    (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
      (factors C s x)))
  1
Tactic: rw [list_prod_apply (π C (· ∈ s)) y _]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
⊢ Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (factors C s x)))
    1
have hl : ∀ (x_1 : ℤ),
  Membership.mem (γ := List ℤ)
      (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (factors C s x))
      x_1 →
    x_1 = 1
Tactic: apply List.prod_eq_one
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
⊢ ∀ (x_1 : ℤ),
    Membership.mem (γ := List ℤ)
        (List.map
          (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
          (factors C s x))
        x_1 →
      x_1 = 1
have hl : ∀ (x_1 : ℤ),
  (∃ (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
      (∃ a_1 ∈ s.sort fun (x1 x2 : I) ↦ x1 ≥ x2,
          (if (↑x : I → Bool) a_1 = true then e (π C fun (x : I) ↦ x ∈ s) a_1
            else 1 - e (π C fun (x : I) ↦ x ∈ s) a_1) =
            a) ∧
        (MonoidHom.comp (Pi.evalMonoidHom (fun (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ ℤ) x)
                LocallyConstant.coeFnMonoidHom :
              (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
            a =
          x_1) →
    x_1 = 1
Tactic: simp only [h, List.mem_map, LocallyConstant.evalMonoidHom, factors]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
b : I
left : b ∈ s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
⊢ Eq (α := ℤ)
    ((MonoidHom.comp (Pi.evalMonoidHom (fun (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ ℤ) x)
            LocallyConstant.coeFnMonoidHom :
          (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (if (↑x : I → Bool) b = true then e (π C fun (x : I) ↦ x ∈ s) b else 1 - e (π C fun (x : I) ↦ x ∈ s) b) :
      ℤ)
    (1 : ℤ)
have hl : Eq (α := ℤ)
  ((if (↑x : I → Bool) b = true then e (π C fun (x : I) ↦ x ∈ s) b else 1 - e (π C fun (x : I) ↦ x ∈ s) b :
        (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
      x :
    ℤ)
  (1 : ℤ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
b : I
left : b ∈ s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
⊢ Eq (α := ℤ)
    ((if (↑x : I → Bool) b = true then e (π C fun (x : I) ↦ x ∈ s) b else 1 - e (π C fun (x : I) ↦ x ∈ s) b :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        x :
      ℤ)
    (1 : ℤ)
have pos : ∀ (hh : (↑x : I → Bool) b = true),
  Eq (α := ℤ) ((e (π C fun (x : I) ↦ x ∈ s) b : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ) (1 : ℤ)
Tactic: split_ifs with hh
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
b : I
left : b ∈ s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
pos :
  ∀ (hh : (↑x : I → Bool) b = true),
    Eq (α := ℤ) ((e (π C fun (x : I) ↦ x ∈ s) b : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ) (1 : ℤ)
⊢ Eq (α := ℤ)
    ((if (↑x : I → Bool) b = true then e (π C fun (x : I) ↦ x ∈ s) b else 1 - e (π C fun (x : I) ↦ x ∈ s) b :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        x :
      ℤ)
    (1 : ℤ)
have neg : ∀ (hh : ¬(↑x : I → Bool) b = true),
  Eq (α := ℤ) ((1 - e (π C fun (x : I) ↦ x ∈ s) b : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ) (1 : ℤ)
Tactic: split_ifs with hh
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
b : I
left : b ∈ s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
hh : (↑x : I → Bool) b = true
⊢ Eq (α := ℤ) ((e (π C fun (x : I) ↦ x ∈ s) b : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ) (1 : ℤ)
have pos : Eq (α := ℤ)
  (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) b = true then 1 else 0,
          isLocallyConstant := sorry : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
        (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
      x :
    ℤ)
  (1 : ℤ)
Tactic: rw [e, LocallyConstant.coe_mk, if_pos hh]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
b : I
left : b ∈ s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
hh : (↑x : I → Bool) b = true
pos :
  Eq (α := ℤ)
    (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) b = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        x :
      ℤ)
    (1 : ℤ)
⊢ Eq (α := ℤ) ((e (π C fun (x : I) ↦ x ∈ s) b : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ) (1 : ℤ)
have pos₁ : Eq (α := ℤ) (if (↑x : I → Bool) b = true then 1 else 0) 1
Tactic: rw [e, LocallyConstant.coe_mk, if_pos hh]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
b : I
left : b ∈ s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
hh : (↑x : I → Bool) b = true
pos :
  Eq (α := ℤ)
    (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) b = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        x :
      ℤ)
    (1 : ℤ)
pos₁ : Eq (α := ℤ) (if (↑x : I → Bool) b = true then 1 else 0) 1
⊢ Eq (α := ℤ) ((e (π C fun (x : I) ↦ x ∈ s) b : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ) (1 : ℤ)
have pos₂ : Eq (α := ℤ) 1 1
Tactic: rw [e, LocallyConstant.coe_mk, if_pos hh]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y = x
b : I
left : b ∈ s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
hh : ¬(↑x : I → Bool) b = true
⊢ Eq (α := ℤ) ((1 - e (π C fun (x : I) ↦ x ∈ s) b : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ) (1 : ℤ)
have neg : HSub.hSub (α := ℤ) (LocallyConstant.toFun 1 x) 0 = 1
Tactic: rw [LocallyConstant.sub_apply, e, LocallyConstant.coe_mk, LocallyConstant.coe_mk, if_neg hh]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
a : I
hx : (↑x : I → Bool) a = true
⊢ e (π C fun (x : I) ↦ x ∈ s) a ∈ factors C s x
have rcases : ∀ (z : I → Bool) (hz : z ∈ C)
  (hx :
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) z) sorry) : I → Bool)
        a =
      true),
  Membership.mem (γ := List (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (factors C s (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) z) sorry))
    (e (π C fun (x : I) ↦ x ∈ s) a)
Tactic: rcases x with ⟨_, z, hz, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx :
  (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) z) ⋯) : I → Bool)
      a =
    true
⊢ Membership.mem (γ := List (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (factors C s (Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) z) ⋯))
    (e (π C fun (x : I) ↦ x ∈ s) a)
have simp : ∃ a_1 ∈ s,
  (if Proj (fun (x : I) ↦ x ∈ s) z a_1 = true then e (π C fun (x : I) ↦ x ∈ s) a_1
    else 1 - e (π C fun (x : I) ↦ x ∈ s) a_1) =
    e (π C fun (x : I) ↦ x ∈ s) a
Tactic: simp only [factors, List.mem_map, Finset.mem_sort]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx :
  (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) z) ⋯) : I → Bool)
      a =
    true
⊢ ∃ a_1 ∈ s,
    (if Proj (fun (x : I) ↦ x ∈ s) z a_1 = true then e (π C fun (x : I) ↦ x ∈ s) a_1
      else 1 - e (π C fun (x : I) ↦ x ∈ s) a_1) =
      e (π C fun (x : I) ↦ x ∈ s) a
have refine : a ∈ s
Tactic: refine ⟨a, ?_, if_pos hx⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
⊢ 1 - e (π C fun (x : I) ↦ x ∈ s) a ∈ factors C s x
have simp : ∃ a_1 ∈ s,
  (if (↑x : I → Bool) a_1 = true then e (π C fun (x : I) ↦ x ∈ s) a_1 else 1 - e (π C fun (x : I) ↦ x ∈ s) a_1) =
    1 - e (π C fun (x : I) ↦ x ∈ s) a
Tactic: simp only [factors, List.mem_map, Finset.mem_sort]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
⊢ ∃ a_1 ∈ s,
    (if (↑x : I → Bool) a_1 = true then e (π C fun (x : I) ↦ x ∈ s) a_1 else 1 - e (π C fun (x : I) ↦ x ∈ s) a_1) =
      1 - e (π C fun (x : I) ↦ x ∈ s) a
have h : a ∈ s ∧
  (if (↑x : I → Bool) a = true then e (π C fun (x : I) ↦ x ∈ s) a else 1 - e (π C fun (x : I) ↦ x ∈ s) a) =
    1 - e (π C fun (x : I) ↦ x ∈ s) a
Tactic: use a
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
⊢ a ∈ s ∧
    (if (↑x : I → Bool) a = true then e (π C fun (x : I) ↦ x ∈ s) a else 1 - e (π C fun (x : I) ↦ x ∈ s) a) =
      1 - e (π C fun (x : I) ↦ x ∈ s) a
have h : a ∈ s ∧
  (if false = true then e (π C fun (x : I) ↦ x ∈ s) a else 1 - e (π C fun (x : I) ↦ x ∈ s) a) =
    1 - e (π C fun (x : I) ↦ x ∈ s) a
Tactic: simp only [hx]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
⊢ a ∈ s ∧
    (if false = true then e (π C fun (x : I) ↦ x ∈ s) a else 1 - e (π C fun (x : I) ↦ x ∈ s) a) =
      1 - e (π C fun (x : I) ↦ x ∈ s) a
have h : ∀ (z : I → Bool) (hz : z ∈ C)
  (ha :
    (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π C fun (x : I) ↦ x ∈ s) (Proj (fun (x : I) ↦ x ∈ s) z) sorry) : I → Bool)
        a =
      true),
  a ∈ s ∧
    (if false = true then e (π C fun (x : I) ↦ x ∈ s) a else 1 - e (π C fun (x : I) ↦ x ∈ s) a) =
      1 - e (π C fun (x : I) ↦ x ∈ s) a
Tactic: rcases y with ⟨_, z, hz, rfl⟩
Cleared hypotheses: y, ha
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)
have rw : Eq (α := ℤ)
  (List.prod
    (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
      (factors C s x)))
  0
Tactic: rw [list_prod_apply (π C (· ∈ s)) y _]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
⊢ Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (factors C s x)))
    0
have a : Membership.mem (γ := List ℤ)
  (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
    (factors C s x))
  0
Tactic: apply List.prod_eq_zero
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
⊢ Membership.mem (γ := List ℤ)
    (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
      (factors C s x))
    0
have a : ∃ a ∈ factors C s x,
  Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
    (0 : ℤ)
Tactic: simp only [List.mem_map]