-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem GoodProducts.finsupp_sum_mem_span_eval {a : I} {as : List I}
    (ha : List.Chain' (· > ·) (a :: as)) {c : Products I →₀ ℤ}
    (hc : (c.support : Set (Products I)) ⊆ {m | m.val ≤ as}) :
    (Finsupp.sum c fun a_1 b ↦ e (π C (· ∈ s)) a * b • Products.eval (π C (· ∈ s)) a_1) ∈
      Submodule.span ℤ (Products.eval (π C (· ∈ s)) '' {m | m.val ≤ a :: as})

Proof state:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
⊢ (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.finsupp_sum_mem

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
⊢ ∀ (c_1 : Products I),
    c c_1 ≠ 0 →
      e (π C fun x => x ∈ s) a * c c_1 • Products.eval (π C fun x => x ∈ s) c_1 ∈
        Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Proof state:
case h.h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
⊢ e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
apply Submodule.subset_span

Result:
case h.h.a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
⊢ e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m ∈
    Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as}

Proof state:
case h.h.a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
⊢ e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m ∈
    Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as}

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

Result:
case h.h.a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
hmas : ↑m ≤ as
⊢ e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m ∈
    Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as}

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
⊢ c m • (e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m) ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
apply Submodule.smul_mem

Result:
case h.h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
⊢ e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m ∈
    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
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
⊢ ↑m ≤ as

Tactic:
apply hc

Result:
case a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
⊢ m ∈ ↑c.support

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
⊢ ∀ (c_1 : Products I),
    c c_1 ≠ 0 →
      e (π C fun x => x ∈ s) a * c c_1 • Products.eval (π C fun x => x ∈ s) c_1 ∈
        Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
intro m hm

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
⊢ e (π C fun x => x ∈ s) a * c m • Products.eval (π C fun x => x ∈ s) m ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
⊢ e (π C fun x => x ∈ s) a * c m • Products.eval (π C fun x => x ∈ s) m ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
rw [hsm]

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
⊢ c m • (e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m) ∈
    Submodule.span ℤ (Products.eval (π C fun x => x ∈ s) '' {m | ↑m ≤ a :: as})

Proof state:
case h.h.a
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.Chain' (fun x1 x2 => x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x => x ∈ s) ℤ),
    e (π C fun x => x ∈ s) a * c • x = c • (e (π C fun x => x ∈ s) a * x)
hmas : ↑m ≤ as
⊢ Products.eval (π C fun x => x ∈ s) ⟨a :: ↑m, ⋯⟩ = e (π C fun x => x ∈ s) a * Products.eval (π C fun x => x ∈ s) m

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

Result:
no goals