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
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

Tactic:
have hmas : m.val ≤ as := by
    apply hc
    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
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}

Tactic:
⟨⟨a :: m.val, ha.cons_of_le m.prop hmas⟩, ⟨List.cons_le_cons a hmas, ?_⟩⟩

Premises used: Set.Mem, setOf, List.cons_le_cons, List.cons, Subtype.mk, Subtype.prop, And.intro, Exists.intro, Set.image, Subtype.val, List.IsChain.cons_of_le
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
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)) ⋯) =
    e (π C fun (x : I) ↦ x ∈ s) a * Products.eval (π C fun (x : I) ↦ x ∈ s) m
⊢ 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:
refine ⟨⟨a :: m.val, ha.cons_of_le m.prop hmas⟩, ⟨List.cons_le_cons a hmas, ?_⟩⟩
-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Span
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
⊢ 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)) ⋯) =
    e (π C fun (x : I) ↦ x ∈ s) a * Products.eval (π C fun (x : I) ↦ x ∈ s) m

Tactic:
simp only [Products.eval, List.map, List.prod_cons]

Premises used: Profinite.NobelingProof.Products.eval, List.map, List.prod_cons
-- 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
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))))
⊢ 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))))

Tactic:
rw [span_iff_products]

Premises used: Profinite.NobelingProof.GoodProducts.span_iff_products
-- 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
⊢ 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:
le_trans (spanFinBasis.span C s) ?_

Premises used: Profinite.NobelingProof.spanFinBasis.span, 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
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))))
⊢ 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:
refine le_trans (spanFinBasis.span C s) ?_

Premises used: Profinite.NobelingProof.spanFinBasis.span, 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
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) ℤ))
⊢ 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:
rw [Submodule.span_le]

Premises used: Submodule.span_le
-- 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)
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) ℤ))
⊢ 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) ℤ))

Tactic:
rw [← factors_prod_eq_basis]

Premises used: Profinite.NobelingProof.factors_prod_eq_basis
-- 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
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))
⊢ 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) ℤ))

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 _))
-- 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
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))
⊢ 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:
rw [List.sortedGT_iff_isChain]

Premises used: List.sortedGT_iff_isChain
-- 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
h : List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) []
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) ≤ []}
⊢ 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)
        []))

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
h : List.IsChain (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)
        []) ∈
    Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)) {m : Products I | (↑m : List I) ≤ []}

Tactic:
⟨⟨[], List.isChain_nil⟩,⟨Or.inl rfl, rfl⟩⟩

Premises used: List.isChain_nil, Set.Mem, setOf, Subtype.mk, And.intro, Exists.intro, Set.image, Or.inl, rfl, List.nil
-- 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
h : List.IsChain (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)
        []) ∈
    Set.image (α := Products I) (Products.eval (π C fun (x : I) ↦ x ∈ s)) {m : Products I | (↑m : List I) ≤ []}

Tactic:
exact ⟨⟨[], List.isChain_nil⟩,⟨Or.inl rfl, 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
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))
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))
⊢ 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)))

Tactic:
rw [List.map_cons, List.prod_cons]

Premises used: List.map_cons, List.prod_cons
-- 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
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)
⊢ (∀ y ∈ as.head?, a > y) ∧ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) as

Tactic:
rw [List.isChain_cons] at ha

Premises used: List.isChain_cons
-- 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
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 : (∀ y ∈ as.head?, a > y) ∧ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) as
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) as

Tactic:
ha.2

Premises used: And.right
-- 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
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 : (∀ y ∈ as.head?, a > y) ∧ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) as
⊢ List.IsChain (fun (x1 x2 : I) ↦ x1 > x2) as

Tactic:
exact ha.2

Premises used: And.right
-- 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
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) ≤ 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)
-- 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)
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))
⊢ ∃ (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

Premises used: Finsupp.mem_span_image_iff_linearCombination
-- 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)
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) ℤ)
⊢ ∃ (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

Premises used: Finsupp.mem_supported, Finsupp.linearCombination_apply
-- 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)
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))
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))
⊢ 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