-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem maxTail_isGood (l : MaxProducts C ho)
    (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C (ord I · < o))))) :
    l.val.Tail.isGood (C' C ho)

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : ↑m.support ⊆ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
q : Products I
hq : q ∈ m.support
⊢ m q • Products.eval (C' C ho) q = m q • (Linear_CC' C hsC ho) (List.map (e C) (term I ho :: ↑q)).prod

Tactic:
have hx'' : q < l.val.Tail := hmmem hq

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : ↑m.support ⊆ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l).Tail
⊢ m q • Products.eval (C' C ho) q = m q • (Linear_CC' C hsC ho) (List.map (e C) (term I ho :: ↑q)).prod

Proof state:
case intro.intro.intro.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)
n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
w : { l // Products.isGood (π C fun x => ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) +
      m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a => a • eval (π C fun x => ord I x < o) i) = n
⊢ ((w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) +
      m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) ∈
    Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
apply Submodule.add_mem

Result:
case intro.intro.intro.intro.h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)
n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
w : { l // Products.isGood (π C fun x => ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) +
      m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a => a • eval (π C fun x => ord I x < o) i) = n
⊢ (w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) ∈
    Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

case intro.intro.intro.intro.h₂
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)
n : LocallyConstant ↑(π C fun x => ord I x < o) ℤ
w : { l // Products.isGood (π C fun x => ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b => (πs C o) (b • eval (π C fun x => ord I x < o) a)) +
      m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a => a • eval (π C fun x => ord I x < o) i) = n
⊢ (m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
⊢ (m.sum fun i a => a • Products.eval (C' C ho) i) =
    m.sum fun a b => (Linear_CC' C hsC ho) (b • (List.map (e C) (term I ho :: ↑a)).prod)

Tactic:
apply Finsupp.sum_congr

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
⊢ ∀ x ∈ m.support,
    m x • Products.eval (C' C ho) x = (Linear_CC' C hsC ho) (m x • (List.map (e C) (term I ho :: ↑x)).prod)

Proof state:
case h.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : ↑m.support ⊆ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l).Tail
p : Products I
hp : ↑p ≠ [] ∧ (↑p).head! = term I ho ∧ q = p.Tail
⊢ m p.Tail • (Linear_CC' C hsC ho) (Products.eval C p) =
    m p.Tail • (Linear_CC' C hsC ho) (List.map (e C) (term I ho :: ↑p.Tail)).prod

Tactic:
dsimp [Products.eval]

Result:
case h.intro
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x => ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : ↑m.support ⊆ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a => a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l).Tail
p : Products I
hp : ↑p ≠ [] ∧ (↑p).head! = term I ho ∧ q = p.Tail
⊢ m p.Tail • (Linear_CC' C hsC ho) (List.map (e C) ↑p).prod =
    m p.Tail • (Linear_CC' C hsC ho) (e C (term I ho) * (List.map (e C) ↑p.Tail).prod)