-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.spanFin [WellFoundedLT I] :
    ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C (· ∈ s))))

Proof state:
case intro.cons.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hc' :
  (c.sum fun i a => a • Products.eval (π C fun x => x ∈ s) i) =
    (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod
⊢ (if ↑x a = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) *
      (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
rw [← hc']

Result:
case intro.cons.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hc' :
  (c.sum fun i a => a • Products.eval (π C fun x => x ∈ s) i) =
    (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod
⊢ ((if ↑x a = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) *
      c.sum fun i a => a • Products.eval (π C fun x => x ∈ s) i) ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Proof state:
case neg.h₂.h.h.a
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c.sum g = c.sum fun a_1 b => e (π C fun x => x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
⊢ m ∈ {m | ↑m ≤ a :: as}

Tactic:
simp only [Set.mem_setOf_eq]

Result:
case neg.h₂.h.h.a
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c.sum g = c.sum fun a_1 b => e (π C fun x => x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
⊢ ↑m ≤ a :: as

Proof state:
case intro.cons
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
ih :
  (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ as})
⊢ (if ↑x a = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) *
      (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
rw [Finsupp.mem_span_image_iff_linearCombination] at ih

Result:
case intro.cons
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
ih :
  ∃ l ∈ Finsupp.supported ℤ ℤ {m | ↑m ≤ as},
    (Finsupp.linearCombination ℤ (Products.eval (π C fun x => x ∈ s))) l =
      (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod
⊢ (if ↑x a = true then e (π C fun x => x ∈ s) a else 1 - e (π C fun x => x ∈ s) a) *
      (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Proof state:
case intro.nil
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a✝ : List.Chain' (fun x1 x2 => x1 > x2) []
⊢ (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) []).prod ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ []})

Tactic:
apply Submodule.subset_span

Result:
case intro.nil.a
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a✝ : List.Chain' (fun x1 x2 => x1 > x2) []
⊢ (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) []).prod ∈
    Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ []}

Proof state:
case neg.h₂.h.h.a.cons.hab
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c.sum g = c.sum fun a_1 b => e (π C fun x => x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
b : I
bs : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: b :: bs)
hc : ↑c.support ⊆ {m | ↑m ≤ b :: bs}
hmas : ↑m ≤ b :: bs
⊢ b :: bs < a :: b :: bs

Tactic:
rw [List.chain'_cons] at ha

Result:
case neg.h₂.h.h.a.cons.hab
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c.sum g = c.sum fun a_1 b => e (π C fun x => x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
b : I
bs : List I
ha : a > b ∧ List.Chain' (fun x1 x2 => x1 > x2) (b :: bs)
hc : ↑c.support ⊆ {m | ↑m ≤ b :: bs}
hmas : ↑m ≤ b :: bs
⊢ b :: bs < a :: b :: bs

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ih :
  List.Chain' (fun x1 x2 => x1 > x2) as →
    (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod ∈
      Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ as})
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
⊢ List.Chain' (fun x1 x2 => x1 > x2) as

Tactic:
rw [List.chain'_cons'] at ha

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x => x ∈ s)
l : List I := Finset.sort (fun x1 x2 => x1 ≥ x2) s
a : I
as : List I
ih :
  List.Chain' (fun x1 x2 => x1 > x2) as →
    (List.map (fun i => if ↑x i = true then e (π C fun x => x ∈ s) i else 1 - e (π C fun x => x ∈ s) i) as).prod ∈
      Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ as})
ha : (∀ y ∈ as.head?, a > y) ∧ List.Chain' (fun x1 x2 => x1 > x2) as
⊢ List.Chain' (fun x1 x2 => x1 > x2) as