awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ 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))
have ih₁ : 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))
Tactic: specialize ih (by rw [List.isChain_cons] at ha; exact ha.2)
Cleared hypotheses: ih
-- 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)
ih :
  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))
⊢ 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))
have ih₁ : ∃ (l : Products I →₀ ℤ),
  Membership.mem (γ := Submodule ℤ (Products I →₀ ℤ)) (Finsupp.supported ℤ ℤ {m : Products I | (↑m : List I) ≤ as}) l ∧
    Eq (α := LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
      ((Finsupp.linearCombination ℤ (Products.eval (π C fun (x : I) ↦ x ∈ s)) :
            (a : Products I →₀ ℤ) → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
          l :
        LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
      (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) :
        LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
Tactic: rw [Finsupp.mem_span_image_iff_linearCombination] at ih
Cleared hypotheses: ih
-- 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)
ih :
  ∃ (l : Products I →₀ ℤ),
    Membership.mem (γ := Submodule ℤ (Products I →₀ ℤ)) (Finsupp.supported ℤ ℤ {m : Products I | (↑m : List I) ≤ as})
        l ∧
      Eq (α := LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
        ((Finsupp.linearCombination ℤ (Products.eval (π C fun (x : I) ↦ x ∈ s)) :
              (a : Products I →₀ ℤ) → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
            l :
          LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
        (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) :
          LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
⊢ 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))
have ih₁ : ∃ (l : Products I →₀ ℤ),
  (↑l.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as} ∧
    Eq (α := LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
      (l.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) 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)
          as))
Tactic: simp only [Finsupp.mem_supported, Finsupp.linearCombination_apply] at ih
Cleared hypotheses: ih
-- 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)
ih :
  ∃ (l : Products I →₀ ℤ),
    (↑l.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as} ∧
      Eq (α := LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
        (l.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) 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)
            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))
have cons : ∀ (c : Products I →₀ ℤ) (hc : (↑c.support : Set (Products I)) ⊆ {m : Products I | (↑m : List I) ≤ as})
  (hc' :
    Eq (α := LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
      (c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) 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)
          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: obtain ⟨c, hc, hc'⟩ := ih
Cleared hypotheses: ih
-- 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}
hc' :
  Eq (α := LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
    (c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) 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)
        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))
have cons : 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) *
    c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
Tactic: rw [← 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
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}
⊢ 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) *
      c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
have hmap : ∀ (g : Products I → ℤ → LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ),
  Eq (α := 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.sum g) :
      LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
    (c.sum fun (a_1 : Products I) (b : ℤ) ↦
        (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) ℤ)
          (g a_1 b) :
      LocallyConstant (↑(π C fun (x : I) ↦ x ∈ s) : Type u) ℤ)
Tactic: have hmap := fun g ↦ map_finsuppSum (LinearMap.mulLeft ℤ (e (π C (· ∈ s)) a)) c g
-- 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
⊢ 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) *
      c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
have pos : (↑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}))
    (e (π C fun (x : I) ↦ x ∈ s) a * c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
Tactic: split_ifs
-- 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
pos :
  (↑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}))
      (e (π C fun (x : I) ↦ x ∈ s) a *
        c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
⊢ 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) *
      c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
have neg : ¬(↑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}))
    ((1 - e (π C fun (x : I) ↦ x ∈ s) a) *
      c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
Tactic: split_ifs
-- 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}))
    (e (π C fun (x : I) ↦ x ∈ s) a * c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
have pos : 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: rw [hmap]
-- 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}))
    ((1 - e (π C fun (x : I) ↦ x ∈ s) a) *
      c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
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 (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i) +
    HSMul.hSMul (α := ℤ) (-1)
      (e (π C fun (x : I) ↦ x ∈ s) a *
        c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i))
Tactic: noncomm_ring
-- 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) +
      HSMul.hSMul (α := ℤ) (-1)
        (e (π C fun (x : I) ↦ x ∈ s) a *
          c.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i))
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 (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i) +
    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))
Tactic: rw [hmap]
-- 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) +
      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 (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
Tactic: apply Submodule.add_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
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 (i : Products I) (a : ℤ) ↦ a • Products.eval (π C fun (x : I) ↦ x ∈ s) i)
⊢ 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) +
      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}))
  (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))
Tactic: apply Submodule.add_mem