-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
l : (↑(MaxProducts C ho) : Type u)
h₁ :
  LE.le (α := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)) ⊤
    (Submodule.span ℤ
      (Set.range (ι := { l : Products I // Products.isGood (π C fun (x : I) ↦ ord I x < o) l })
        (eval (π C fun (x : I) ↦ ord I x < o))))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : (↑m.support : Set (Products I)) ⊆ {m : Products I | m < (↑l : Products I).Tail}
hmsum :
  Eq (α := LocallyConstant (↑(C' C ho) : Type u) ℤ)
    (m.sum fun (i : Products I) (a : ℤ) ↦ a • Products.eval (C' C ho) i : LocallyConstant (↑(C' C ho) : Type u) ℤ)
    ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
        (Products.eval C (↑l : Products I)) :
      LocallyConstant (↑(C' C ho) : Type u) ℤ)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l : Products I).Tail
p : Products I
hp : (↑p : List I) ≠ [] ∧ (↑p : List I).head! = term I ho ∧ q = p.Tail
h :
  HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (List.map (e C) (term I ho :: (↑p.Tail : List I))).prod :
        LocallyConstant (↑(C' C ho) : Type u) ℤ) =
    HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (e C (term I ho) * (List.map (e C) (↑p.Tail : List I)).prod) :
        LocallyConstant (↑(C' C ho) : Type u) ℤ)
h₂ :
  HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (e C (term I ho) :: List.map (e C) (↑p.Tail : List I)).prod :
        LocallyConstant (↑(C' C ho) : Type u) ℤ) =
    HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (e C (term I ho) * (List.map (e C) (↑p.Tail : List I)).prod) :
        LocallyConstant (↑(C' C ho) : Type u) ℤ)
h₃ h₄ :
  HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (e C (term I ho) * (List.map (e C) (↑p.Tail : List I)).prod) :
        LocallyConstant (↑(C' C ho) : Type u) ℤ) =
    HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (e C (term I ho) * (List.map (e C) (↑p.Tail : List I)).prod) :
        LocallyConstant (↑(C' C ho) : Type u) ℤ)
⊢ HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (List.map (e C) (↑p : List I)).prod :
        LocallyConstant (↑(C' C ho) : Type u) ℤ) =
    HSMul.hSMul (α := ℤ) (β := LocallyConstant (↑(C' C ho) : Type u) ℤ) ((m : (a : Products I) → ℤ) p.Tail : ℤ)
      ((Linear_CC' C hsC ho : (a : LocallyConstant (↑C : Type u) ℤ) → LocallyConstant (↑(C' C ho) : Type u) ℤ)
          (e C (term I ho) * (List.map (e C) (↑p.Tail : List I)).prod) :
        LocallyConstant (↑(C' C ho) : Type u) ℤ)

Tactic:
rw [Products.max_eq_o_cons_tail ho p hp.1 hp.2.1, List.map_cons, List.prod_cons]

Premises used: List.map_cons, And.right, And.left, List.prod_cons, Profinite.NobelingProof.Products.max_eq_o_cons_tail