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
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
⊢ ∃ (a : I), (↑y : I → Bool) a ≠ (↑x : I → Bool) a
have contrapose! : ∀ (h : ∀ (a : I), (↑y : I → Bool) a = (↑x : I → Bool) a), y = x
Tactic: contrapose! h
Cleared hypotheses: 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
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)
have a : ∀ (a : I) (ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a),
  ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)
Tactic: obtain ⟨a, ha⟩ : ∃ a, y.val a ≠ x.val a := by contrapose! h; ext; apply 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
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)
have a₁ : ∀ (hx : (↑x : I → Bool) a = false),
  ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)
Tactic: cases hx : x.val 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)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
a₁ :
  ∀ (hx : (↑x : I → Bool) a = false),
    ∃ a ∈ factors C s x,
      Eq (α := ℤ)
        ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
        (0 : ℤ)
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)
have a₂ : ∀ (hx : (↑x : I → Bool) a = true),
  ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)
Tactic: cases hx : x.val a
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (hypothesis)
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
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
hx : (↑x : I → Bool) a = false
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)
have ha₁ : (↑y : I → Bool) a = true
Tactic: rw [hx, ne_eq, Bool.not_eq_false] at ha
Cleared hypotheses: ha, 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)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)
have a₁ : Eq (α := ℤ)
  ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
      (1 - e (π C fun (x : I) ↦ x ∈ s) a) :
    ℤ)
  (0 : ℤ)
Tactic: refine ⟨1 - (e (π C (· ∈ s)) a), ⟨one_sub_e_mem_of_false _ _ ha 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)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 - e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₁ : Eq (α := ℤ)
  ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
      (1 -
        { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
          isLocallyConstant := sorry : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ }) :
    ℤ)
  (0 : ℤ)
Tactic: rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]
-- 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
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
a₁ :
  Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 -
          { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ }) :
      ℤ)
    (0 : ℤ)
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 - e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₂ : Eq (α := ℤ)
  ((1 -
          { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = 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)) → ℤ)
      y :
    ℤ)
  (0 : ℤ)
Tactic: rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]
-- 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
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
a₁ :
  Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 -
          { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ }) :
      ℤ)
    (0 : ℤ)
a₂ :
  Eq (α := ℤ)
    ((1 -
            { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        y :
      ℤ)
    (0 : ℤ)
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 - e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₃ : HSub.hSub (α := ℤ) (β := ℤ) ((1 : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
    (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = 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)) → ℤ)
        y :
      ℤ) =
  0
Tactic: rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]
-- 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
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
a₁ :
  Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 -
          { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ }) :
      ℤ)
    (0 : ℤ)
a₂ :
  Eq (α := ℤ)
    ((1 -
            { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        y :
      ℤ)
    (0 : ℤ)
a₃ :
  HSub.hSub (α := ℤ) (β := ℤ) ((1 : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 - e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₄ : HSub.hSub (α := ℤ) (β := ℤ) (1 y : ℤ)
    (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = 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)) → ℤ)
        y :
      ℤ) =
  0
Tactic: rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]
-- 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
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
a₁ :
  Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 -
          { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ }) :
      ℤ)
    (0 : ℤ)
a₂ :
  Eq (α := ℤ)
    ((1 -
            { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        y :
      ℤ)
    (0 : ℤ)
a₃ :
  HSub.hSub (α := ℤ) (β := ℤ) ((1 : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₄ :
  HSub.hSub (α := ℤ) (β := ℤ) (1 y : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 - e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₅ : HSub.hSub (α := ℤ) (β := ℤ) (1 : ℤ)
    (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = 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)) → ℤ)
        y :
      ℤ) =
  0
Tactic: rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]
-- 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
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
a₁ :
  Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 -
          { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ }) :
      ℤ)
    (0 : ℤ)
a₂ :
  Eq (α := ℤ)
    ((1 -
            { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        y :
      ℤ)
    (0 : ℤ)
a₃ :
  HSub.hSub (α := ℤ) (β := ℤ) ((1 : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₄ :
  HSub.hSub (α := ℤ) (β := ℤ) (1 y : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₅ :
  HSub.hSub (α := ℤ) (β := ℤ) (1 : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 - e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₆ : HSub.hSub (α := ℤ) 1 (if (↑y : I → Bool) a = true then 1 else 0) = 0
Tactic: rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]
-- 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
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
a₁ :
  Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 -
          { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ }) :
      ℤ)
    (0 : ℤ)
a₂ :
  Eq (α := ℤ)
    ((1 -
            { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        y :
      ℤ)
    (0 : ℤ)
a₃ :
  HSub.hSub (α := ℤ) (β := ℤ) ((1 : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₄ :
  HSub.hSub (α := ℤ) (β := ℤ) (1 y : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₅ :
  HSub.hSub (α := ℤ) (β := ℤ) (1 : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₆ : HSub.hSub (α := ℤ) 1 (if (↑y : I → Bool) a = true then 1 else 0) = 0
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 - e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₇ : HSub.hSub (α := ℤ) 1 1 = 0
Tactic: rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]
-- 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
a : I
ha : (↑y : I → Bool) a = true
hx : (↑x : I → Bool) a = false
a₁ :
  Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 -
          { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ }) :
      ℤ)
    (0 : ℤ)
a₂ :
  Eq (α := ℤ)
    ((1 -
            { toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        y :
      ℤ)
    (0 : ℤ)
a₃ :
  HSub.hSub (α := ℤ) (β := ℤ) ((1 : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₄ :
  HSub.hSub (α := ℤ) (β := ℤ) (1 y : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₅ :
  HSub.hSub (α := ℤ) (β := ℤ) (1 : ℤ)
      (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
              isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
            (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
          y :
        ℤ) =
    0
a₆ : HSub.hSub (α := ℤ) 1 (if (↑y : I → Bool) a = true then 1 else 0) = 0
a₇ : HSub.hSub (α := ℤ) 1 1 = 0
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (1 - e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₈ : Eq (α := ℤ) 0 0
Tactic: rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]
-- 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
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
hx : (↑x : I → Bool) a = true
⊢ ∃ a ∈ factors C s x,
    Eq (α := ℤ)
      ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ) a : ℤ)
      (0 : ℤ)
have a₁ : Eq (α := ℤ)
  ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
      (e (π C fun (x : I) ↦ x ∈ s) a) :
    ℤ)
  (0 : ℤ)
Tactic: refine ⟨e (π C (· ∈ s)) a, ⟨e_mem_of_eq_true _ _ hx, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (hypothesis)
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
a : I
ha : (↑y : I → Bool) a ≠ (↑x : I → Bool) a
hx : (↑x : I → Bool) a = true
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have ha₁ : (↑y : I → Bool) a ≠ true
Tactic: rw [hx] at ha
Cleared hypotheses: ha, 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)
h : y ≠ x
a : I
ha : (↑y : I → Bool) a ≠ true
hx : (↑x : I → Bool) a = true
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₁ : Eq (α := ℤ) ((e (π C fun (x : I) ↦ x ∈ s) a : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)
Tactic: rw [LocallyConstant.evalMonoidHom_apply, e, LocallyConstant.coe_mk, if_neg 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
a : I
ha : (↑y : I → Bool) a ≠ true
hx : (↑x : I → Bool) a = true
a₁ : Eq (α := ℤ) ((e (π C fun (x : I) ↦ x ∈ s) a : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₂ : Eq (α := ℤ)
  (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = 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)) → ℤ)
      y :
    ℤ)
  (0 : ℤ)
Tactic: rw [LocallyConstant.evalMonoidHom_apply, e, LocallyConstant.coe_mk, if_neg 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
a : I
ha : (↑y : I → Bool) a ≠ true
hx : (↑x : I → Bool) a = true
a₁ : Eq (α := ℤ) ((e (π C fun (x : I) ↦ x ∈ s) a : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)
a₂ :
  Eq (α := ℤ)
    (({ toFun := fun (f : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) ↦ if (↑f : I → Bool) a = true then 1 else 0,
            isLocallyConstant := ⋯ : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ } :
          (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ)
        y :
      ℤ)
    (0 : ℤ)
⊢ Eq (α := ℤ)
    ((LocallyConstant.evalMonoidHom y : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₃ : Eq (α := ℤ) (if (↑y : I → Bool) a = true then 1 else 0) 0
Tactic: rw [LocallyConstant.evalMonoidHom_apply, e, LocallyConstant.coe_mk, if_neg ha]