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

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) →
    (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:
intro ha

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})
ha : 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:
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})

Tactic:
simp only [Finsupp.mem_supported, Finsupp.linearCombination_apply] 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,
    ↑l.support ⊆ {m | ↑m ≤ as} ∧
      (l.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})

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) ℤ),
    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})

Tactic:
split_ifs

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

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

Tactic:
exact finsupp_sum_mem_span_eval _ _ ha hc

Result:
no goals

Proof state:
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 ≤ []}

Tactic:
exact ⟨⟨[], List.chain'_nil⟩,⟨Or.inl rfl, rfl⟩⟩

Result:
no goals