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

Proof state:
case neg.h₁
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})

Tactic:
apply Submodule.neg_mem

Result:
case neg.h₁.hx
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})

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
⊢ Products.eval (π C fun x => x ∈ s) m ∈ Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as}

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

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 ∈ {m | ↑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}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    (LinearMap.mulLeft ℤ (e (π C fun x => x ∈ s) a)) (c.sum g) =
      c.sum fun a_1 b => (LinearMap.mulLeft ℤ (e (π C fun x => x ∈ s) a)) (g a_1 b)
⊢ ((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:
dsimp at hmap ⊢

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}
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
⊢ ((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
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})

Tactic:
apply Submodule.add_mem

Result:
case neg.h₁
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})

case neg.h₂
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 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
hmas : ↑m ≤ as
⊢ ↑m ≤ a :: as

Tactic:
refine le_trans hmas ?_

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