-- 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 intro.intro.intro.intro.h₂.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
⊢ ∀ (c : Products I),
    m c ≠ 0 → m c • (List.map (e C) (term I ho :: ↑c)).prod ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
intro q hq

Result:
case intro.intro.intro.intro.h₂.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
q : Products I
hq : m q ≠ 0
⊢ m q • (List.map (e C) (term I ho :: ↑q)).prod ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Proof state:
case intro.intro.intro.intro.h₂.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
q : Products I
hq : m q ≠ 0
⊢ m q • (List.map (e C) (term I ho :: ↑q)).prod ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
apply Submodule.smul_mem

Result:
case intro.intro.intro.intro.h₂.h.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
q : Products I
hq : m q ≠ 0
⊢ (List.map (e C) (term I ho :: ↑q)).prod ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

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
⊢ Products.eval C ↑l ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
rw [← hn]

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