-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit (goal)
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 :
      ℤ)
⊢ 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 :
      ℤ)
have 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 :
    ℤ)
Tactic: rw [eval, ← Products.eval_πs' _ h (Products.prop_of_isGood C _ gl), eval]