-- Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Goal:
I : Type u
C : Set (I → Bool)
inst : LinearOrder I
inst_1 : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l
x : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)
h₁ :
  Eq (α := ℤ)
    ((Products.eval (π C fun (x : I) ↦ ord I x < o₂)
            (↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l ⋯) :
              Products I) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
    ((((πs' C h :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                  LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
              (eval (π C fun (x : I) ↦ ord I x < o₁)
                (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
h₂ :
  Eq (α := ℤ)
    ((((πs' C h :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                  LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
              (Products.eval (π C fun (x : I) ↦ ord I x < o₁) l) :
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
    ((((πs' C h :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                  LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
              (eval (π C fun (x : I) ↦ ord I x < o₁)
                (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
h₃ h₄ :
  Eq (α := ℤ)
    ((((πs' C h :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                  LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
              (Products.eval (π C fun (x : I) ↦ ord I x < o₁) l) :
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
    ((((πs' C h :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                  LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
              (Products.eval (π C fun (x : I) ↦ ord I x < o₁)
                (↑(Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl) :
                  Products I)) :
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
⊢ Eq (α := ℤ)
    ((eval (π C fun (x : I) ↦ ord I x < o₂)
            (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₂) l) l ⋯) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)
    ((((πs' C h :
                (a : LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₁) : Type u) ℤ) →
                  LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ)
              (eval (π C fun (x : I) ↦ ord I x < o₁)
                (Subtype.mk (p := fun (l : Products I) ↦ Products.isGood (π C fun (x : I) ↦ ord I x < o₁) l) l gl)) :
            LocallyConstant (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u) ℤ) :
          (a : (↑(π C fun (x : I) ↦ ord I x < o₂) : Type u)) → ℤ)
        x :
      ℤ)

Tactic:
rw [eval, ← Products.eval_πs' _ h (Products.prop_of_isGood C _ gl), eval]

Premises used: Profinite.NobelingProof.Products.eval_πs', Profinite.NobelingProof.Products.prop_of_isGood, Profinite.NobelingProof.GoodProducts.eval