awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
f : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ
_ :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f →
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
      (Submodule.span ℤ (Set.range (spanFinBasis C s))) f
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f →
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
      (Submodule.span ℤ (Set.range (spanFinBasis C s))) f

Tactic:
_
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
rw :
  ∃ (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
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ (Set.range (spanFinBasis C s))) f

Tactic:
rw [Finsupp.mem_span_range_iff_exists_finsupp]

Premises used: Finsupp.mem_span_range_iff_exists_finsupp
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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_1 : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
h :
  (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
⊢ ∃ (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

Tactic:
use Finsupp.onFinset (Finset.univ) f.toFun (fun _ _ ↦ Finset.mem_univ _)

Premises used: Finset.mem_univ, Finset.univ, Finsupp.onFinset, LocallyConstant.toFun
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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_1 : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
h :
  ∀ (x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)),
    Eq (α := ℤ)
      ((Finsupp.sum (Finsupp.onFinset Finset.univ f.toFun ⋯) 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 : ℤ)
⊢ (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

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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_1 : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h :
  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 : ℤ)
⊢ 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 : ℤ)

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]

Premises used: Finsupp.mem_support_iff, zsmul_eq_mul, Profinite.NobelingProof.spanFinBasis, Pi.mul_apply, Finsupp.sum_ite_eq, mul_ite, LocallyConstant.evalₗ_apply, LocallyConstant.coe_mul, ne_eq, MulZeroClass.mul_zero, LocallyConstant.coe_mk, map_finsuppSum, ite_not, mul_one
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 : ℤ)
neg :
  ∀
    (h :
      ¬Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
          (0 : ℤ)),
    Eq (α := ℤ)
      (((↑((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 : ℤ)
⊢ 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 : ℤ)

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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_1 : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
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 : ℤ)

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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_1 : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
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 : ℤ)

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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_1 : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤ f
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
h :
  ¬Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
      (0 : ℤ)
⊢ Eq (α := ℤ)
    (((↑((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 : ℤ)

Tactic:
rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 : ℤ)
neg :
  ∀
    (h :
      ¬Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
          (0 : ℤ)),
    Eq (α := ℤ)
      (((↑((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 : ℤ)
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 : ℤ)
neg₁ :
  ∀
    (h :
      ¬Eq (α := ℤ) ((Finsupp.onFinset Finset.univ f.toFun ⋯ : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ)
          (0 : ℤ)),
    Eq (α := ℤ)
      (((↑((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 : ℤ)
⊢ 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 : ℤ)

Tactic:
split_ifs with h <;> [exact h.symm; rfl]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 : ℤ)
rw₁ rw₂ : Eq (α := ℤ) ((l.prod : (a : (↑C : Type u_1)) → ℤ) x : ℤ) ((l.prod : (a : (↑C : Type u_1)) → ℤ) x : ℤ)
⊢ Eq (α := ℤ) ((l.prod : (a : (↑C : Type u_1)) → ℤ) x : ℤ)
    (List.prod (List.map (⇑(LocallyConstant.evalMonoidHom x) : (a : LocallyConstant (↑C : Type u_1) ℤ) → ℤ) l) : ℤ)

Tactic:
rw [← map_list_prod (LocallyConstant.evalMonoidHom x) l, LocallyConstant.evalMonoidHom_apply]

Premises used: LocallyConstant.evalMonoidHom_apply, map_list_prod, LocallyConstant.evalMonoidHom
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
rw :
  Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (factors C s x)))
    1
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (1 : ℤ)

Tactic:
rw [list_prod_apply (π C (· ∈ s)) y _]

Premises used: Profinite.NobelingProof.π, Membership.mem, Profinite.NobelingProof.list_prod_apply
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
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
⊢ Eq (α := ℤ)
    (List.prod
      (List.map (⇑(LocallyConstant.evalMonoidHom y) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) → ℤ)
        (factors C s x)))
    1

Tactic:
apply List.prod_eq_one

Premises used: List.prod_eq_one
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
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
⊢ ∀ (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:
simp only [h, List.mem_map, LocallyConstant.evalMonoidHom, factors]

Premises used: List.mem_map, LocallyConstant.evalMonoidHom, Profinite.NobelingProof.factors
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
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 : ℤ)
⊢ 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 : ℤ)

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 : ℤ)
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 : ℤ)
⊢ 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:
split_ifs with hh
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
pos₂ pos₃ : Eq (α := ℤ) 1 1
⊢ Eq (α := ℤ) ((e (π C fun (x : I) ↦ x ∈ s) b : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ) (1 : ℤ)

Tactic:
rw [e, LocallyConstant.coe_mk, if_pos hh]

Premises used: if_pos, LocallyConstant.coe_mk, Profinite.NobelingProof.e
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
neg : HSub.hSub (α := ℤ) (LocallyConstant.toFun 1 x) 0 = 1
⊢ Eq (α := ℤ) ((1 - e (π C fun (x : I) ↦ x ∈ s) b : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) x : ℤ) (1 : ℤ)

Tactic:
rw [LocallyConstant.sub_apply, e, LocallyConstant.coe_mk, LocallyConstant.coe_mk, if_neg hh]

Premises used: LocallyConstant.coe_mk, LocallyConstant.sub_apply, Profinite.NobelingProof.e, if_neg
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
⊢ HSub.hSub (α := ℤ) (LocallyConstant.toFun 1 x) 0 = 1

Tactic:
simp only [LocallyConstant.toFun_eq_coe, LocallyConstant.coe_one, Pi.one_apply, sub_zero]

Premises used: sub_zero, Pi.one_apply, LocallyConstant.coe_one, LocallyConstant.toFun_eq_coe
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
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) ⋯) :
            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)
⊢ e (π C fun (x : I) ↦ x ∈ s) a ∈ factors C s x

Tactic:
rcases x with ⟨_, z, hz, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
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
⊢ 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)

Tactic:
simp only [factors, List.mem_map, Finset.mem_sort]

Premises used: Finset.mem_sort, List.mem_map, Profinite.NobelingProof.factors
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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

Tactic:
⟨a, ?_, if_pos hx⟩

Premises used: if_pos, And.intro, Exists.intro
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
refine : a ∈ s
⊢ ∃ 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:
refine ⟨a, ?_, if_pos hx⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 ∈ s

Tactic:
aesop (add simp Proj)

Premises used: Profinite.NobelingProof.Proj
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
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
⊢ 1 - e (π C fun (x : I) ↦ x ∈ s) a ∈ factors C s x

Tactic:
simp only [factors, List.mem_map, Finset.mem_sort]

Premises used: Finset.mem_sort, List.mem_map, Profinite.NobelingProof.factors
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
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
⊢ ∃ 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:
use a
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
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
⊢ 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:
simp only [hx]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
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) ⋯) :
            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
⊢ 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⟩

Premises used: rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 = false
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) ⋯) : 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:
aesop (add simp Proj)

Premises used: Profinite.NobelingProof.Proj