-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices
Goal:
X : SSet
s t : X.S
mp :
  (∃ (f : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex) →
    ∃ (f : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex
mpr :
  (∃ (f : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex) →
    ∃ (f : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex
mp₁ mp₂ mp₃ :
  ∀ (w : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex →
      ∃ (f : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
            t.simplex =
          s.simplex
mpr₁ mpr₂ mpr₃ :
  ∀ (w : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex →
      ∃ (f : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) :
              (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
            t.simplex =
          s.simplex
mp₄ mp₅ mp₆ :
  ∀ (w : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex →
      ∃ (f : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
            t.simplex =
          s.simplex
mpr₄ mpr₅ mpr₆ :
  ∀ (w : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex →
      ∃ (f : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) :
              (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
            t.simplex =
          s.simplex
mp₇ mp₈ :
  ∀ (w : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex →
      ∃ (f : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
            t.simplex =
          s.simplex
mp₉ :
  ∀ (w : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex →
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Opposite.unop w).op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex
mp₁₀ :
  (w : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌) →
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex →
      (⦋s.dim⦌ ⟶ ⦋t.dim⦌)
mp₁₁ :
  ∀ (w : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex →
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Opposite.unop w).op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex
mp₁₂ :
  (w : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌) →
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex →
      (⦋s.dim⦌ ⟶ ⦋t.dim⦌)
mpr₇ mpr₈ :
  ∀ (w : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map w.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex →
      ∃ (f : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) :
              (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
            t.simplex =
          s.simplex
⊢ (∃ (f : Opposite.op ⦋t.dim⦌ ⟶ Opposite.op ⦋s.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex) ↔
    ∃ (f : ⦋s.dim⦌ ⟶ ⦋t.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋t.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋s.dim⦌))
          t.simplex =
        s.simplex

Tactic:
tauto