-- 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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun (x1 x2 : I) ↦ x1 < x2
h :
  ∀ (val : Products I)
    (property : Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) val)
    (x : (↑C : Type u)),
    Eq (α := ℤ)
      (((eval C ∘ (sum_equiv C hsC ho).toFun)
              (Sum.inl
                (Subtype.mk (p := fun (x : Products I) ↦
                  Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                  property)) :
            (a : (↑C : Type u)) → ℤ)
          x :
        ℤ)
      ((Sum.elim
              (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
              (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
              (Sum.inl
                (Subtype.mk (p := fun (x : Products I) ↦
                  Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                  property)) :
            (a : (↑C : Type u)) → ℤ)
          x :
        ℤ)
h₁ :
  ∀ (val : (↑(MaxProducts C ho) : Type u)) (x : (↑C : Type u)),
    Eq (α := ℤ) (((eval C ∘ (sum_equiv C hsC ho).toFun) (Sum.inr val) : (a : (↑C : Type u)) → ℤ) x : ℤ)
      ((Sum.elim
              (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
              (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)) (Sum.inr val) :
            (a : (↑C : Type u)) → ℤ)
          x :
        ℤ)
h₂ :
  ∀ (val : Products I)
    (property : Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) val)
    (x : (↑C : Type u)),
    Eq (α := ℤ)
      (((eval C ∘ (sum_equiv C hsC ho).toFun)
              (Sum.inl
                (Subtype.mk (p := fun (x : Products I) ↦
                  Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                  property)) :
            (a : (↑C : Type u)) → ℤ)
          x :
        ℤ)
      ((Sum.elim
              (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
              (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I))
              (Sum.inl
                (Subtype.mk (p := fun (x : Products I) ↦
                  Membership.mem (γ := Set (Products I)) (GoodProducts (π C fun (x : I) ↦ ord I x < o)) x) val
                  property)) :
            (a : (↑C : Type u)) → ℤ)
          x :
        ℤ)
h₃ :
  ∀ (val : (↑(MaxProducts C ho) : Type u)) (x : (↑C : Type u)),
    Eq (α := ℤ) (((eval C ∘ (sum_equiv C hsC ho).toFun) (Sum.inr val) : (a : (↑C : Type u)) → ℤ) x : ℤ)
      ((Sum.elim
              (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
              (fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)) (Sum.inr val) :
            (a : (↑C : Type u)) → ℤ)
          x :
        ℤ)
⊢ eval C ∘ (sum_equiv C hsC ho).toFun =
    Sum.elim (fun (l : (↑(GoodProducts (π C fun (x : I) ↦ ord I x < o)) : Type u)) ↦ Products.eval C (↑l : Products I))
      fun (l : (↑(MaxProducts C ho) : Type u)) ↦ Products.eval C (↑l : Products I)

Tactic:
ext ⟨_, _⟩ <;> [rfl; rfl]