-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
Goal:
p q n : ℕ
z : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌
hn : p + q = n
a b : Fin (n + 1)
hab :
  Eq (α := Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              z :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        a :
      Fin (p + 1) × Fin (q + 1))
    (((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
              z :
            Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
          (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
        b :
      Fin (p + 1) × Fin (q + 1))
h :
  ∀ (x : Fin (n + 1)),
    (⟨(↑((z.1 : (a : Fin (n + 1)) → Fin (p + 1)) x) : ℕ) + (↑((z.2 : (a : Fin (n + 1)) → Fin (q + 1)) x) : ℕ), ⋯⟩ :
        Fin (n + 1)) =
      x
refine_2 :
  (↑(((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                      (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
                    z :
                  Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
                (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
              a).1 :
        ℕ) +
      (↑(((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                      (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
                    z :
                  Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
                (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
              a).2 :
        ℕ) =
    (↑(((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                      (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
                    z :
                  Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
                (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
              b).1 :
        ℕ) +
      (↑(((((objEquiv : tensorObj (𝒞 := Functor.category) Δ[p] Δ[q] _⦋n⦌ ≃ (Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))) :
                      (a : (Δ[p] ⊗ Δ[q]) _⦋n⦌) → Fin (n + 1) →o Fin (p + 1) × Fin (q + 1))
                    z :
                  Fin (n + 1) →o Fin (p + 1) × Fin (q + 1)) :
                (a : Fin (n + 1)) → Fin (p + 1) × Fin (q + 1))
              b).2 :
        ℕ)
⊢ (↑(⟨(↑((z.1 : (a : Fin (n + 1)) → Fin (p + 1)) a) : ℕ) + (↑((z.2 : (a : Fin (n + 1)) → Fin (q + 1)) a) : ℕ), ⋯⟩ :
          Fin (n + 1)) :
      ℕ) =
    (↑(⟨(↑((z.1 : (a : Fin (n + 1)) → Fin (p + 1)) b) : ℕ) + (↑((z.2 : (a : Fin (n + 1)) → Fin (q + 1)) b) : ℕ), ⋯⟩ :
          Fin (n + 1)) :
      ℕ)

Tactic:
change ((objEquiv z a).1 : ℕ) + (objEquiv z a).2 = (objEquiv z b).1 + (objEquiv z b).2

Premises used: Fin.val, Prod.fst, SSet.prodStdSimplex.objEquiv, Prod.snd, DFunLike.coe