-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
x_1 : Δ[n].obj x
obj :
  (∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) →
    ∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i
obj₁ :
  (∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i) →
    ∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2
obj₂ obj₃ obj₄ :
  ∀ (w : Fin (n + 1)),
    (∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_2 = w) →
      ∃ (i : Fin (n + 1)),
        ∀ (x_2 : Fin ((unop x).len + 1)),
          ¬(SimplexCategory.Hom.toOrderHom
                    (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                  (a : Fin ((unop x).len + 1)) → Fin (n + 1))
                x_2 =
              i
obj₅ obj₆ obj₇ :
  ∀ (w : Fin (n + 1)),
    (∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            w) →
      ∃ (x_2 : Fin (n + 1)),
        ∀ (x_3 : Fin ((unop x).len + 1)),
          ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2
obj₈ obj₉ obj₁₀ :
  ∀ (w : Fin (n + 1)),
    (∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_2 = w) →
      ∃ (i : Fin (n + 1)),
        ∀ (x_2 : Fin ((unop x).len + 1)),
          ¬(SimplexCategory.Hom.toOrderHom
                    (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                  (a : Fin ((unop x).len + 1)) → Fin (n + 1))
                x_2 =
              i
obj₁₁ obj₁₂ obj₁₃ :
  ∀ (w : Fin (n + 1)),
    (∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            w) →
      ∃ (x_2 : Fin (n + 1)),
        ∀ (x_3 : Fin ((unop x).len + 1)),
          ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2
obj₁₄ obj₁₅ :
  ∀ (w : Fin (n + 1)),
    (∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_2 = w) →
      ∃ (i : Fin (n + 1)),
        ∀ (x_2 : Fin ((unop x).len + 1)),
          ¬(SimplexCategory.Hom.toOrderHom
                    (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                  (a : Fin ((unop x).len + 1)) → Fin (n + 1))
                x_2 =
              i
obj₁₆ obj₁₇ :
  ∀ (w : Fin (n + 1)),
    (∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            w) →
      ∃ (x_2 : Fin (n + 1)),
        ∀ (x_3 : Fin ((unop x).len + 1)),
          ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2
⊢ (∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) ↔
    ∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i

Tactic:
tauto