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
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 : ℤ)
a₃ : Eq (α := ℤ) (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) ℤ) → ℤ)
        (e (π C fun (x : I) ↦ x ∈ s) a) :
      ℤ)
    (0 : ℤ)
have a₄ : Eq (α := ℤ) 0 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 : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
⊢ (factors C s x).prod = spanFinBasis C s x
have h : ∀ (y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)),
  Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
    ((spanFinBasis C s x : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
Tactic: ext 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)
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
    ((spanFinBasis C s x : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
have h : Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
  (if y = x then 1 else 0 : ℤ)
Tactic: dsimp [spanFinBasis]
-- 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)
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
    (if y = x then 1 else 0 : ℤ)
have pos : ∀ (h : y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (1 : ℤ)
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
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
pos :
  ∀ (h : y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (1 : ℤ)
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
    (if y = x then 1 else 0 : ℤ)
have neg : ∀ (h : ¬y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)
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
x y : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
    (if y = x then 1 else 0 : ℤ)
have pos : ∀ (h : y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (1 : ℤ)
Tactic: split_ifs with h <;> [exact factors_prod_eq_basis_of_eq _ _ h;
    exact factors_prod_eq_basis_of_ne _ _ 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)
pos :
  ∀ (h : y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (1 : ℤ)
⊢ Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ)
    (if y = x then 1 else 0 : ℤ)
have neg : ∀ (h : ¬y = x), Eq (α := ℤ) (((factors C s x).prod : (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → ℤ) y : ℤ) (0 : ℤ)
Tactic: split_ifs with h <;> [exact factors_prod_eq_basis_of_eq _ _ h;
    exact factors_prod_eq_basis_of_ne _ _ 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
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}
⊢ 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)
have h : ∀ (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}))
      (e (π C fun (x : I) ↦ x ∈ s) a *
        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 (hypothesis)
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
s : Finset I
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}
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}))
    (e (π C fun (x : I) ↦ x ∈ s) a *
      HSMul.hSMul (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (Products.eval (π C fun (x : I) ↦ x ∈ s) m))
have hsm : ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
  (LinearMap.mulLeft ℤ (e (π C fun (x : I) ↦ x ∈ s) a) :
        (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) →
          LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
      (c • x) =
    HSMul.hSMul (β := LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) c
      ((LinearMap.mulLeft ℤ (e (π C fun (x : I) ↦ x ∈ s) a) :
            (a : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ) →
              LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
          x :
        LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
Tactic: have hsm := (LinearMap.mulLeft ℤ (e (π C (· ∈ s)) a)).map_smul
-- 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
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}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hsm :
  ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c • x = c • (e (π C fun (x : I) ↦ x ∈ s) a * x)
⊢ 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}))
    (e (π C fun (x : I) ↦ x ∈ s) a *
      HSMul.hSMul (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (Products.eval (π C fun (x : I) ↦ x ∈ s) m))
have h : 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 : ℤ)
    (e (π C fun (x : I) ↦ x ∈ s) a * Products.eval (π C fun (x : I) ↦ x ∈ s) m))
Tactic: rw [hsm]
-- 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
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}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hsm :
  ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c • x = c • (e (π C fun (x : I) ↦ x ∈ s) a * x)
⊢ 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 : ℤ)
      (e (π C fun (x : I) ↦ x ∈ s) a * Products.eval (π C fun (x : I) ↦ x ∈ s) m))
have h : 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}))
  (e (π C fun (x : I) ↦ x ∈ s) a * 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
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}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hsm :
  ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c • x = c • (e (π C fun (x : I) ↦ x ∈ s) a * x)
⊢ 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}))
    (e (π C fun (x : I) ↦ x ∈ s) a * Products.eval (π C fun (x : I) ↦ x ∈ s) m)
have h : e (π C fun (x : I) ↦ x ∈ s) a * 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
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}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hsm :
  ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c • x = c • (e (π C fun (x : I) ↦ x ∈ s) a * x)
⊢ (↑m : List I) ≤ as
have a₁ : m ∈ (↑c.support : Set (Products I))
Tactic: apply hc
-- 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
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}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hsm :
  ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c • x = c • (e (π C fun (x : I) ↦ x ∈ s) a * x)
⊢ e (π C fun (x : I) ↦ x ∈ s) a * 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 hmas : (↑m : List I) ≤ as
Tactic: have hmas : m.val ≤ as := by
    apply hc
    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
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}
m : Products I
hm : Ne (α := ℤ) ((c : (a : Products I) → ℤ) m : ℤ) (0 : ℤ)
hsm :
  ∀ (c : ℤ) (x : LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
    e (π C fun (x : I) ↦ x ∈ s) a * c • x = c • (e (π C fun (x : I) ↦ x ∈ s) a * x)
hmas : (↑m : List I) ≤ as
⊢ e (π C fun (x : I) ↦ x ∈ s) a * 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 h : Products.eval (π C fun (x : I) ↦ x ∈ s)
    (Subtype.mk (p := fun (l : List I) ↦ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) l) (a :: (↑m : List I)) sorry) =
  e (π C fun (x : I) ↦ x ∈ s) a * Products.eval (π C fun (x : I) ↦ x ∈ s) m
Tactic: refine ⟨⟨a :: m.val, ha.cons_of_le m.prop hmas⟩, ⟨List.cons_le_cons a 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
⊢ LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ x ∈ s) l })
        (eval (π C fun (x : I) ↦ x ∈ s))))
have rw : LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤
  (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))))
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
s : Finset I
inst_1 : WellFoundedLT I
⊢ LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)) ⊤
    (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))))
have refine : LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
  (Submodule.span ℤ (Set.range (spanFinBasis C s)))
  (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))))
Tactic: refine le_trans (spanFinBasis.span C s) ?_
-- 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
⊢ LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
    (Submodule.span ℤ (Set.range (spanFinBasis C s)))
    (Submodule.span ℤ (Set.range (ι := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s))))
have rw : Set.range (spanFinBasis C s) ⊆
  (↑(Submodule.span ℤ (Set.range (ι := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)))) :
    Set (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
Tactic: rw [Submodule.span_le]
-- 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)
⊢ spanFinBasis C s x ∈
    (↑(Submodule.span ℤ (Set.range (ι := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)))) :
      Set (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
have rw : (factors C s x).prod ∈
  (↑(Submodule.span ℤ (Set.range (ι := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)))) :
    Set (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
Tactic: rw [← factors_prod_eq_basis]
-- 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.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)
        (s.sort fun (x1 x2 : I) ↦ x1 ≥ x2)) ∈
    (↑(Submodule.span ℤ (Set.range (ι := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)))) :
      Set (LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ))
have suffices : l.SortedGT →
  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))
Tactic: suffices l.SortedGT → (l.map (fun i ↦ if x.val i = true then e (π C (· ∈ s)) i
      else (1 - (e (π C (· ∈ s)) i)))).prod ∈
      Submodule.span ℤ ((Products.eval (π C (· ∈ s))) '' {m | m.val ≤ l}) from
    Submodule.span_mono (Set.image_subset_range _ _)
      (this (Finset.sortedGT_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
inst_1 : WellFoundedLT I
x : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)
l : List I := s.sort fun (x1 x2 : I) ↦ x1 ≥ x2
⊢ l.SortedGT →
    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 rw : 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))
Tactic: rw [List.sortedGT_iff_isChain]
-- 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
h : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) []
⊢ 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) ≤ []}))
    (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)
        []))
have nil : 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)
      []) ∈
  Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)) {m : Products I | (↑m : List I) ≤ []}
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
ih :
  List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) as →
    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) ≤ as}))
      (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)
          as))
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as) →
    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}))
      (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)
          (a :: as)))
have cons : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as) →
  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}))
    ((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) *
      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)
          as))
Tactic: rw [List.map_cons, List.prod_cons]
-- 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
ih :
  List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) as →
    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) ≤ as}))
      (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)
          as))
ha : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) (a :: as)
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) as
have ha₁ : (∀ y ∈ as.head?, a > y) ∧ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) as
Tactic: rw [List.isChain_cons] at ha
Cleared hypotheses: ha