-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Simplices (goal)
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
⊢ (∃ (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
have 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
Tactic: tauto