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

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 ≤ a :: as

Tactic:
have hmas : m.val ≤ as :=
  hc (by simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm)

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
hmas : ↑m ≤ as
⊢ ↑m ≤ a :: as

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) *
      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})

Tactic:
clear 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}
⊢ ((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 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
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})
⊢ List.Chain' (fun x1 x2 => x1 > x2) (a :: 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)
          (a :: as)).prod ∈
      Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

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

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
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})
⊢ List.Chain' (fun x1 x2 => x1 > x2) (a :: 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})

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ Submodule.span ℤ (Set.range (spanFinBasis C s)) ≤ Submodule.span ℤ (Set.range (Products.eval (π C fun x => x ∈ s)))

Tactic:
rw [Submodule.span_le]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ Set.range (spanFinBasis C s) ⊆ ↑(Submodule.span ℤ (Set.range (Products.eval (π C fun x => x ∈ s))))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => x ∈ s)))

Tactic:
rw [span_iff_products]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval (π C fun x => x ∈ s)))

Proof state:
case neg
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
⊢ (-(e (π C fun x => x ∈ s) a * c.sum fun i a => a • Products.eval (π C fun x => x ∈ s) i) +
      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})

Tactic:
rw [hmap]

Result:
case neg
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
⊢ ((-c.sum fun a_1 b => e (π C fun x => x ∈ s) a * b • Products.eval (π C fun x => x ∈ s) a_1) +
      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 pos
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
⊢ (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})

Tactic:
rw [hmap]

Result:
case pos
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
⊢ (c.sum fun a_1 b => e (π C fun x => x ∈ s) a * b • Products.eval (π C fun x => x ∈ s) a_1) ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})