-- 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.h.a
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)
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 : q ∈ m.support
⊢ List.Lex (fun x1 x2 => x1 < x2) (term I ho :: ↑q) (term I ho :: ↑(↑l).Tail)

Tactic:
exact List.Lex.cons ((Products.lt_iff_lex_lt q l.val.Tail).mp (hmmem hq))

Result:
no goals

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 ∈ 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)
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:
rw [Finsupp.mem_supported] at hmmem

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
⊢ 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.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 : { l // Products.isGood (π C fun x => ord I x < o) l }
a✝ : w q ≠ 0
⊢ (πs C o) (w q • eval (π C fun x => ord I x < o) q) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
rw [LinearMap.map_smul]

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 : { l // Products.isGood (π C fun x => ord I x < o) l }
a✝ : w q ≠ 0
⊢ w q • (πs C o) (eval (π C fun x => ord I x < o) q) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Proof state:
case intro.intro.intro.intro.h₁.h.h.a
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 : { l // Products.isGood (π C fun x => ord I x < o) l }
a✝ : w q ≠ 0
⊢ List.Lex (fun x1 x2 => x1 < x2) ↑↑q ↑↑l

Tactic:
exact good_lt_maxProducts C hsC ho q l

Result:
no goals

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

Tactic:
rw [Products.max_eq_o_cons_tail ho p hp.1 hp.2.1]

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) (term I ho :: ↑p.Tail)).prod =
    m p.Tail • (Linear_CC' C hsC ho) (e C (term I ho) * (List.map (e C) ↑p.Tail).prod)