-- 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
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 : (Finsupp.linearCombination ℤ (Products.eval (C' C ho))) m = (Linear_CC' C hsC ho) (Products.eval C ↑l)
⊢ False

Tactic:
rw [Finsupp.linearCombination_apply] at hmsum

Result:
case 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)
⊢ False

Proof state:
case 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)
this :
  (Linear_CC' C hsC ho) (Products.eval C ↑l) =
    (Linear_CC' C hsC ho) (m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod)
hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)
⊢ False

Tactic:
rw [← LinearMap.sub_mem_ker_iff, ← hse] at this

Result:
case 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)
this : (Products.eval C ↑l - m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod) ∈ LinearMap.range (πs C o)
hse : LinearMap.range (πs C o) = LinearMap.ker (Linear_CC' C hsC ho)
⊢ False

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

Tactic:
intro q _

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

Proof state:
case 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)
this :
  (Linear_CC' C hsC ho) (Products.eval C ↑l) =
    (Linear_CC' C hsC ho) (m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod)
hse : (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).Exact
⊢ False

Tactic:
rw [ShortComplex.moduleCat_exact_iff_range_eq_ker] at hse

Result:
case 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)
this :
  (Linear_CC' C hsC ho) (Products.eval C ↑l) =
    (Linear_CC' C hsC ho) (m.sum fun i a => a • (List.map (e C) (term I ho :: ↑i)).prod)
hse :
  LinearMap.range
      (ModuleCat.Hom.hom (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).f) =
    LinearMap.ker
      (ModuleCat.Hom.hom (ShortComplex.mk (ModuleCat.ofHom (πs C o)) (ModuleCat.ofHom (Linear_CC' C hsC ho)) ⋯).g)
⊢ False