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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
have neg : ∀ (c_1 : Products I),
  Ne (α := ℤ) ((c : (a : Products I) → ℤ) c_1 : ℤ) (0 : ℤ) →
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
      (Submodule.span ℤ
        (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
          {m : Products I | (↑m : List I) ≤ a :: as}))
      (HSMul.hSMul (α := ℤ) ((c : (a : Products I) → ℤ) c_1 : ℤ) (Products.eval (π C fun (x : I) ↦ x ∈ s) c_1))
Tactic: apply Submodule.finsuppSum_mem
-- 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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (HSMul.hSMul (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (Products.eval (π C fun (x : I) ↦ x ∈ s) m))
have neg : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
  (Submodule.span ℤ
    (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)) {m : Products I | (↑m : List I) ≤ a :: as}))
  (Products.eval (π C fun (x : I) ↦ x ∈ s) m)
Tactic: apply Submodule.smul_mem
-- 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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (Products.eval (π C fun (x : I) ↦ x ∈ s) m)
have neg : Products.eval (π C fun (x : I) ↦ x ∈ s) m ∈
  Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)) {m : Products I | (↑m : List I) ≤ a :: as}
Tactic: apply Submodule.subset_span
-- 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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
⊢ Products.eval (π C fun (x : I) ↦ x ∈ s) m ∈
    Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)) {m : Products I | (↑m : List I) ≤ a :: as}
have neg : Membership.mem (γ := Set (Products I)) {m : Products I | (↑m : List I) ≤ a :: as} m
Tactic: refine ⟨m, ⟨?_, rfl⟩⟩
-- 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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
⊢ (↑m : List I) ≤ a :: as
have hmas : (↑m : List I) ≤ as
Tactic: have hmas : m.val ≤ as :=
          hc (by simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm)
-- 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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hmas : (↑m : List I) ≤ as
⊢ (↑m : List I) ≤ a :: as
have neg : as ≤ a :: as
Tactic: refine le_trans hmas ?_
-- 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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
b : I
bs : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: b :: bs)
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ b :: bs}
hmas : (↑m : List I) ≤ b :: bs
⊢ b :: bs ≤ a :: b :: bs
have neg : b :: bs < a :: b :: bs
Tactic: apply le_of_lt
-- 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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
b : I
bs : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: b :: bs)
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ b :: bs}
hmas : (↑m : List I) ≤ b :: bs
⊢ b :: bs < a :: b :: bs
have ha₁ : a > b ∧ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (b :: bs)
Tactic: rw [List.isChain_cons_cons] at ha
Cleared hypotheses: ha, hc, hmas
-- 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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hmas : (↑m : List I) ≤ as
⊢ as ≤ a :: as
have neg : ∀ (ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) [a])
  (hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ []}) (hmas : (↑m : List I) ≤ []), [] ≤ [a]
Tactic: cases as with
        | nil => exact (List.nil_lt_cons a []).le
        | cons b bs =>
          apply le_of_lt
          rw [List.isChain_cons_cons] at ha
          exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel ha.1)
Cleared hypotheses: as, ha, hc, hmas
-- 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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hmas : (↑m : List I) ≤ as
neg :
  ∀ (ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) [a])
    (hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ []}) (hmas : (↑m : List I) ≤ []), [] ≤ [a]
⊢ as ≤ a :: as
have neg₁ : ∀ (b : I) (bs : List I) (ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: b :: bs))
  (hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ b :: bs}) (hmas : (↑m : List I) ≤ b :: bs),
  b :: bs ≤ a :: b :: bs
Tactic: cases as with
        | nil => exact (List.nil_lt_cons a []).le
        | cons b bs =>
          apply le_of_lt
          rw [List.isChain_cons_cons] at ha
          exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel ha.1)
Cleared hypotheses: as, ha, hc, hmas
-- 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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
a : I
as : List I
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c.sum g =
      c.sum fun (a_1 : Products I) (b : ℤ) ↦ e (π C fun (x : I) ↦ x ∈ s) a * g a_1 b
h : ¬(↑x : I → Bool) a = true
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))
        {m : Products I | (↑m : List I) ≤ a :: as}))
    (HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) (-1)
      (c.sum fun (a_1 : Products I) (b : ℤ) ↦
        e (π C fun (x : I) ↦ x ∈ s) a * b • Products.eval (π C fun (x : I) ↦ x ∈ s) a_1))
have neg : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
  (Submodule.span ℤ
    (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)) {m : Products I | (↑m : List I) ≤ a :: as}))
  (c.sum fun (a_1 : Products I) (b : ℤ) ↦
    e (π C fun (x : I) ↦ x ∈ s) a * b • Products.eval (π C fun (x : I) ↦ x ∈ s) a_1)
Tactic: apply Submodule.smul_mem
-- 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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l →
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
      (Submodule.span ℤ
        (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)) {m : Products I | (↑m : List I) ≤ l}))
      (List.prod
        (List.map
          (fun (i : I) ↦
            if (↑x : I → Bool) i = true then e (π C fun (x : I) ↦ x ∈ s) i else 1 - e (π C fun (x : I) ↦ x ∈ s) i)
          l))
have induction : ∀ (x_1 : List I),
  List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) x_1 →
    Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
      (Submodule.span ℤ
        (Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)) {m : Products I | (↑m : List I) ≤ x_1}))
      (List.prod
        (List.map
          (fun (i : I) ↦
            if (↑x : I → Bool) i = true then e (π C fun (x : I) ↦ x ∈ s) i else 1 - e (π C fun (x : I) ↦ x ∈ s) i)
          x_1))
Tactic: induction l with
  | nil =>
    intro _
    apply Submodule.subset_span
    exact ⟨⟨[], List.isChain_nil⟩,⟨Or.inl rfl, rfl⟩⟩
  | cons a as ih =>
    rw [List.map_cons, List.prod_cons]
    intro ha
    specialize ih (by rw [List.isChain_cons] at ha; exact ha.2)
    rw [Finsupp.mem_span_image_iff_linearCombination] at ih
    simp only [Finsupp.mem_supported, Finsupp.linearCombination_apply] at ih
    obtain ⟨c, hc, hc'⟩ := ih
    rw [← hc']; clear hc'
    have hmap := fun g ↦ map_finsuppSum (LinearMap.mulLeft ℤ (e (π C (· ∈ s)) a)) c g
    dsimp at hmap ⊢
    split_ifs
    · rw [hmap]
      exact finsuppSum_mem_span_eval _ _ ha hc
    · noncomm_ring
      -- we use `noncomm_ring` even though this is a commutative ring, because we want a weaker
      -- normalization which preserves multiplication order (i.e. doesn't use commutativity rules)
      rw [hmap]
      apply Submodule.add_mem
      · apply Submodule.finsuppSum_mem
        intro m hm
        apply Submodule.smul_mem
        apply Submodule.subset_span
        refine ⟨m, ⟨?_, rfl⟩⟩
        simp only [Set.mem_setOf_eq]
        have hmas : m.val ≤ as :=
          hc (by simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm)
        refine le_trans hmas ?_
        cases as with
        | nil => exact (List.nil_lt_cons a []).le
        | cons b bs =>
          apply le_of_lt
          rw [List.isChain_cons_cons] at ha
          exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel ha.1)
      · apply Submodule.smul_mem
        exact finsuppSum_mem_span_eval _ _ ha hc
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
hC : IsClosed C
f : LocallyConstant (↑C : Type u) ℤ
⊢ ∃ (s : Finset I) (g : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    f = LocallyConstant.comap { toFun := ProjRestrict C fun (x : I) ↦ x ∈ s, continuous_toFun := ⋯ } g
have obtain : ∀ (J : (Finset I)ᵒᵖ)
  (g :
    LocallyConstant
      (↑(((spanFunctor (C := C) sorry).obj J).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      ℤ)
  (h :
    f =
      LocallyConstant.comap
        (TopCat.Hom.hom
          (CategoryTheory.InducedCategory.Hom.hom
            (CategoryTheory.NatTrans.app (CategoryTheory.Limits.Cone.π (spanCone (C := C) sorry)) J)))
        g),
  ∃ (s : Finset I) (g : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    f = LocallyConstant.comap { toFun := ProjRestrict C fun (x : I) ↦ x ∈ s, continuous_toFun := sorry } g
Tactic: obtain ⟨J, g, h⟩ := @Profinite.exists_locallyConstant (Finset I)ᵒᵖ _ _ _
    (spanCone hC.isCompact) ℤ
    (spanCone_isLimit hC.isCompact) f
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
hC : IsClosed C
⊢ LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤
    (Submodule.span ℤ (Set.range (ι := { l : Products I // Products.isGood C l }) (eval C)))
have rw : LE.le (α := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤
  (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval C)))
Tactic: rw [span_iff_products]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
hC : IsClosed C
f : LocallyConstant (↑C : Type u) ℤ
h : Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤ f
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval C))) f
have obtain : ∀ (K : Finset I) (f' : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ),
  Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤
      ((πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) f' :
        LocallyConstant (↑C : Type u) ℤ) →
    Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
      (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval C)))
      ((πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) f' :
        LocallyConstant (↑C : Type u) ℤ)
Tactic: obtain ⟨K, f', rfl⟩ : ∃ K f', f = πJ C K f' := fin_comap_jointlySurjective C hC f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Span (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
hC : IsClosed C
K : Finset I
f' : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ
h :
  Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ)) ⊤
    ((πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) f' :
      LocallyConstant (↑C : Type u) ℤ)
⊢ Membership.mem (α := LocallyConstant (↑C : Type u) ℤ) (γ := Submodule ℤ (LocallyConstant (↑C : Type u) ℤ))
    (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval C)))
    ((πJ C K : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) f' :
      LocallyConstant (↑C : Type u) ℤ)
have refine : (⇑(πJ C K) : (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ K) : Type u) ℤ) → LocallyConstant (↑C : Type u) ℤ) ''
    Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ x ∈ K) l })
      (eval (π C fun (x : I) ↦ x ∈ K)) ⊆
  Set.range (ι := Products I) (Products.eval C)
Tactic: refine Submodule.span_mono ?_ <| Submodule.apply_mem_span_image_of_mem_span (πJ C K) <|
    spanFin C K (Submodule.mem_top : f' ∈ ⊤)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ IsClosed (C0 C ho)
have refine : IsClosed.{u} (X := I → Bool) {f : I → Bool | f (term I ho) = false}
Tactic: refine hC.inter ?_
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ IsClosed.{u} (X := I → Bool) {f : I → Bool | f (term I ho) = false}
have h : Continuous (Y := Bool) fun (f : I → Bool) ↦ f (term I ho)
Tactic: have h : Continuous (fun (f : I → Bool) ↦ f (term I ho)) := continuous_apply (term I ho)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ IsClosed (C1 C ho)
have refine : IsClosed.{u} (X := I → Bool) {f : I → Bool | f (term I ho) = true}
Tactic: refine hC.inter ?_
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ IsClosed.{u} (X := I → Bool) {f : I → Bool | f (term I ho) = true}
have h : Continuous (Y := Bool) fun (f : I → Bool) ↦ f (term I ho)
Tactic: have h : Continuous (fun (f : I → Bool) ↦ f (term I ho)) := continuous_apply (term I ho)
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
⊢ C0 C ho ∪ C1 C ho = C
have h : ∀ (x : I → Bool), x ∈ C0 C ho ∪ C1 C ho ↔ x ∈ C
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
⊢ Continuous (Y := I → Bool) fun (f : I → Bool) (i : I) ↦ if ord I i = o then true else f i
have h : ∀ (i : I), Continuous (Y := Bool) fun (a : I → Bool) ↦ if ord I i = o then true else a i
Tactic: apply continuous_pi
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous (Y := Bool) fun (a : I → Bool) ↦ if ord I i = o then true else a i
have h : Continuous (ite (ord I i = o) true)
Tactic: apply Continuous.comp'
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
i : I
h : Continuous (ite (ord I i = o) true)
⊢ Continuous (Y := Bool) fun (a : I → Bool) ↦ if ord I i = o then true else a i
have h₁ : Continuous (Y := Bool) fun (x : I → Bool) ↦ x i
Tactic: apply Continuous.comp'
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Successor (goal)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
f : (↑(π (C1 C ho) fun (x : I) ↦ ord I x < o) : Type u)
⊢ SwapTrue o (↑f : I → Bool) ∈ C1 C ho
have obtain : ∀ (g : I → Bool) (hg : g ∈ C1 C ho),
  SwapTrue o
      (↑(Subtype.mk (p := fun (x : I → Bool) ↦ x ∈ π (C1 C ho) fun (x : I) ↦ ord I x < o)
            (Proj (fun (x : I) ↦ ord I x < o) g) sorry) :
        I → Bool) ∈
    C1 C ho
Tactic: obtain ⟨f, g, hg, rfl⟩ := f
Cleared hypotheses: f