-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun (x : I) ↦ ord I x < o) l
hslt : ((↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) < o
he :
  Membership.mem (γ :=
    Submodule ℤ
      (LocallyConstant
        (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)
hlt : ∀ i ∈ (↑l : List I), ord I i < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)
h₁ :
  Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ
      ((⇑(πs' C ⋯) :
          (a :
              LocallyConstant
                (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u)
                ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) ''
        Set.image (α := Products I)
          (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
          {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o) l)
h₂ :
  Membership.mem (α := LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) (γ :=
    Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ
      ((⇑(πs' C ⋯) :
          (a :
              LocallyConstant
                (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u)
                ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ) ''
        Set.image (α := Products I)
          (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
          {m : Products I | m < l}))
    ((πs' C ⋯ :
          (a :
              LocallyConstant
                (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u)
                ℤ) →
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l) :
      LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ)
h₃ h₄ h₅ h₆ :
  Membership.mem (γ :=
    Submodule ℤ
      (LocallyConstant
        (↑(π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) : Type u) ℤ))
    (Submodule.span ℤ
      (Set.image (α := Products I)
        (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)))
        {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < (↑l : List I).toFinset.sup fun (a : I) ↦ Order.succ (ord I a)) l)
⊢ Membership.mem (γ := Submodule ℤ (LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o) : Type u) ℤ))
    (Submodule.span ℤ (Set.image (α := Products I) (eval (π C fun (x : I) ↦ ord I x < o)) {m : Products I | m < l}))
    (eval (π C fun (x : I) ↦ ord I x < o) l)

Tactic:
rwa [eval_πs_image' C (le_of_lt hslt) hlt, ← eval_πs' C (le_of_lt hslt) hlt,
    Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C _)]

Premises used: Profinite.NobelingProof.injective_πs', Profinite.NobelingProof.Products.eval_πs', Submodule.apply_mem_span_image_iff_mem_span, le_of_lt, Profinite.NobelingProof.Products.eval_πs_image'