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
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))
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)
⊢ 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 [← hc']
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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}
⊢ ∀ (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
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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)
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)
⊢ 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:
split_ifs
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
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)
⊢ 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:
rw [hmap]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 (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:
finsuppSum_mem_span_eval _ _ ha hc

Premises used: Set.Mem, Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 (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:
exact finsuppSum_mem_span_eval _ _ ha hc

Premises used: Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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) +
      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))
⊢ 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:
noncomm_ring
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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) +
      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))
⊢ 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:
rw [hmap]
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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)
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))
⊢ 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:
apply Submodule.add_mem

Premises used: Submodule.add_mem
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 :
  ∀ (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))
⊢ 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.finsuppSum_mem

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

Tactic:
apply Submodule.smul_mem

Premises used: Submodule.smul_mem
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 : ℤ)
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}
⊢ 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.subset_span

Premises used: Submodule.subset_span
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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}

Tactic:
⟨m, ⟨?_, rfl⟩⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 : ℤ)
neg : Membership.mem (γ := Set (Products I)) {m : Products I | (↑m : List I) ≤ a :: as} m
⊢ 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:
refine ⟨m, ⟨?_, rfl⟩⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 ∈ (↑c.support : Set (Products I))

Tactic:
simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm

Premises used: Finsupp.mem_support_iff, Finset.mem_coe
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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) ≤ as

Tactic:
have hmas : m.val ≤ as :=
          hc (by simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm)
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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

Tactic:
le_trans hmas ?_

Premises used: le_trans
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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 : as ≤ a :: as
⊢ (↑m : List I) ≤ a :: as

Tactic:
refine le_trans hmas ?_

Premises used: le_trans