awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
obtain :
  ∀ (d : ℕ) (x : X _⦋d⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace y),
    IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
      ((Equiv.symm opEquiv : (a : X.S) → X.op.S) y)
⊢ IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) x)
    ((Equiv.symm opEquiv : (a : X.S) → X.op.S) y)

Tactic:
obtain ⟨d, x, rfl⟩ := x.mk_surjective

Premises used: SSet.S.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
y : X.S
d : ℕ
x : X _⦋d⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace y
obtain :
  ∀ (d' : ℕ) (y : X _⦋d'⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d', simplex := y }),
    IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
      ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d', simplex := y : X.S })
⊢ IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
    ((Equiv.symm opEquiv : (a : X.S) → X.op.S) y)

Tactic:
obtain ⟨d', y, rfl⟩ := y.mk_surjective

Premises used: SSet.S.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
d' : ℕ
y : X _⦋d'⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d', simplex := y }
⊢ d' = d + 1

Tactic:
hxy.dim_eq

Premises used: SSet.S.IsUniquelyCodimOneFace.dim_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
d' : ℕ
y : X _⦋d'⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d', simplex := y }
obtain :
  ∀ (y : X _⦋d + 1⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }),
    IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
      ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d + 1, simplex := y : X.S })
⊢ IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
    ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d', simplex := y : X.S })

Tactic:
obtain rfl : d' = d + 1 := hxy.dim_eq

Premises used: SSet.S.IsUniquelyCodimOneFace.dim_eq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
simp :
  ∃! i : Fin (d + 2),
    Eq (α := X.op _⦋d⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
          ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
        X.op _⦋d⦌)
      ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌)
⊢ IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
    ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d + 1, simplex := y : X.S })

Tactic:
simp only [opEquiv_symm_apply, iff]

Premises used: SSet.S.opEquiv_symm_apply, SSet.S.IsUniquelyCodimOneFace.iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ (fun (i : Fin (d + 2)) ↦
      Eq (α := X.op _⦋d⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
            ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
          X.op _⦋d⦌)
        ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌))
    (hxy.index ⋯).rev

Tactic:
simpa using hxy.δ_index rfl

Premises used: SSet.S.IsUniquelyCodimOneFace.δ_index, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
refine :
  ∀ (i : Fin (d + 2))
    (hi :
      (fun (i : Fin (d + 2)) ↦
          Eq (α := X.op _⦋d⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
                ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
              X.op _⦋d⦌)
            ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌))
        i),
    i = (hxy.index ⋯).rev
⊢ ∃! i : Fin (d + 2),
    Eq (α := X.op _⦋d⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
          ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
        X.op _⦋d⦌)
      ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌)

Tactic:
refine ⟨(hxy.index rfl).rev, by simpa using hxy.δ_index rfl, fun i hi ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
i : Fin (d + 2)
hi :
  (fun (i : Fin (d + 2)) ↦
      Eq (α := X.op _⦋d⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
            ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
          X.op _⦋d⦌)
        ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌))
    i
obtain :
  ∀ (i : Fin (d + 2))
    (hi :
      Eq (α := X.op _⦋d⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i.rev) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
            ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
          X.op _⦋d⦌)
        ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌)),
    i.rev = (hxy.index ⋯).rev
⊢ i = (hxy.index ⋯).rev

Tactic:
obtain ⟨i, rfl⟩ := i.rev_surjective

Premises used: Fin.rev_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
i : Fin (d + 2)
hi :
  Eq (α := X.op _⦋d⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i.rev) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
        ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
      X.op _⦋d⦌)
    ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌)
⊢ i.rev = (hxy.index ⋯).rev

Tactic:
simpa [← hxy.δ_eq_iff rfl] using hi

Premises used: SSet.S.IsUniquelyCodimOneFace.δ_eq_iff, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
Y : SSet
e : X ≅ Y
obtain :
  ∀ (d : ℕ) (x : X _⦋d⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace y),
    IsUniquelyCodimOneFace.{u} (X := Y)
      (mk (dim := { dim := d, simplex := x : X.S }.dim)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
              (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
          { dim := d, simplex := x : X.S }.simplex))
      (mk (dim := y.dim)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌))
          y.simplex))
⊢ IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := x.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋x.dim⦌))
        x.simplex))
    (mk (dim := y.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌))
        y.simplex))

Tactic:
obtain ⟨d, x, rfl⟩ := x.mk_surjective

Premises used: SSet.S.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
y : X.S
Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace y
obtain :
  ∀ (d' : ℕ) (y : X _⦋d'⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d', simplex := y }),
    IsUniquelyCodimOneFace.{u} (X := Y)
      (mk (dim := { dim := d, simplex := x : X.S }.dim)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
              (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
          { dim := d, simplex := x : X.S }.simplex))
      (mk (dim := { dim := d', simplex := y : X.S }.dim)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d', simplex := y : X.S }.dim⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d', simplex := y }.dim⦌)) →
              (fun (X : Type u) ↦ X) (Y _⦋{ dim := d', simplex := y }.dim⦌))
          { dim := d', simplex := y : X.S }.simplex))
⊢ IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := { dim := d, simplex := x : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d, simplex := x : X.S }.simplex))
    (mk (dim := y.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌))
        y.simplex))

Tactic:
obtain ⟨d', y, rfl⟩ := y.mk_surjective

Premises used: SSet.S.mk_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
d' : ℕ
y : X _⦋d'⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d', simplex := y }
⊢ d' = d + 1

Tactic:
hxy.dim_eq

Premises used: SSet.S.IsUniquelyCodimOneFace.dim_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
d' : ℕ
y : X _⦋d'⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d', simplex := y }
obtain :
  ∀ (y : X _⦋d + 1⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }),
    IsUniquelyCodimOneFace.{u} (X := Y)
      (mk (dim := { dim := d, simplex := x : X.S }.dim)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
              (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
          { dim := d, simplex := x : X.S }.simplex))
      (mk (dim := { dim := d + 1, simplex := y : X.S }.dim)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
              (fun (X : Type u) ↦ X) (Y _⦋{ dim := d + 1, simplex := y }.dim⦌))
          { dim := d + 1, simplex := y : X.S }.simplex))
⊢ IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := { dim := d, simplex := x : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d, simplex := x : X.S }.simplex))
    (mk (dim := { dim := d', simplex := y : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d', simplex := y : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d', simplex := y }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d', simplex := y }.dim⦌))
        { dim := d', simplex := y : X.S }.simplex))

Tactic:
obtain rfl : d' = d + 1 := hxy.dim_eq

Premises used: SSet.S.IsUniquelyCodimOneFace.dim_eq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
rw :
  ∀
    (hxy :
      ∃! i : Fin (d + 2),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
              (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
            y =
          x),
    ∃! i : Fin ({ dim := d, simplex := x : X.S }.dim + 2),
      Eq (α := (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x : X.S }.dim⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Y i) :
              (a : (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim + 1⦌)) →
                (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌)) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                    (fun (X : Type u) ↦ X) (Y _⦋{ dim := d + 1, simplex := y }.dim⦌))
                { dim := d + 1, simplex := y : X.S }.simplex :
              (fun (X : Type u) ↦ X) (Y _⦋{ dim := d + 1, simplex := y : X.S }.dim⦌)) :
          (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x : X.S }.dim⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
                (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
            { dim := d, simplex := x : X.S }.simplex :
          (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x : X.S }.dim⦌))
⊢ IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := { dim := d, simplex := x : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d, simplex := x : X.S }.simplex))
    (mk (dim := { dim := d + 1, simplex := y : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d + 1, simplex := y }.dim⦌))
        { dim := d + 1, simplex := y : X.S }.simplex))

Tactic:
rw [iff] at hxy ⊢

Premises used: SSet.S.IsUniquelyCodimOneFace.iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy :
  ∃! i : Fin (d + 2),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
        y =
      x
⊢ ∃! i : Fin ({ dim := d, simplex := x : X.S }.dim + 2),
    Eq (α := (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x : X.S }.dim⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Y i) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim + 1⦌)) →
              (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌)) :
                (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                  (fun (X : Type u) ↦ X) (Y _⦋{ dim := d + 1, simplex := y }.dim⦌))
              { dim := d + 1, simplex := y : X.S }.simplex :
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d + 1, simplex := y : X.S }.dim⦌)) :
        (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x : X.S }.dim⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
              (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
          { dim := d, simplex := x : X.S }.simplex :
        (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x : X.S }.dim⦌))

Tactic:
simpa [← SSet.δ_naturality_apply, dsimp% (e.app (Opposite.op ⦋d⦌)).toEquiv.apply_eq_iff_eq]

Premises used: CategoryTheory.Iso.toEquiv, SSet.δ_naturality_apply, SimplexCategory.mk, Opposite.op, CategoryTheory.Iso.app, Equiv.apply_eq_iff_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X Y : SSet
e : X ≅ Y
x y : X.S
hxy' :
  IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := x.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋x.dim⦌))
        x.simplex))
    (mk (dim := y.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌))
        y.simplex))
⊢ x.IsUniquelyCodimOneFace y

Tactic:
simpa using hxy'.of_iso e.symm

Premises used: SSet.S.IsUniquelyCodimOneFace.of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
⊢ Eq (α := Set A.op.N) ((⇑N.opEquiv : (a : A.op.N) → A.N) ⁻¹' P.I ∩ (⇑N.opEquiv : (a : A.op.N) → A.N) ⁻¹' P.II) ∅

Tactic:
simp [← Set.preimage_inter, P.inter]

Premises used: Set.preimage_inter, SSet.Subcomplex.Pairing.inter
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
⊢ Eq (α := Set A.op.N) ((⇑N.opEquiv : (a : A.op.N) → A.N) ⁻¹' P.I ∪ (⇑N.opEquiv : (a : A.op.N) → A.N) ⁻¹' P.II) Set.univ

Tactic:
simp [← Set.preimage_union, P.union]

Premises used: Set.preimage_union, SSet.Subcomplex.Pairing.union
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
⊢ ∀ (a : A.op.N),
    Membership.mem (γ := Set A.op.N) ((⇑N.opEquiv : (a : A.op.N) → A.N) ⁻¹' P.II) a ↔
      Membership.mem (α := A.N) P.II
        ((RelIso.toEquiv (r := fun (x1 x2 : A.op.N) ↦ x1 ≤ x2) (s := fun (x1 x2 : A.N) ↦ x1 ≤ x2) N.opEquiv :
              (a : A.op.N) → A.N)
            a :
          A.N)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
⊢ ∀ (a : A.N),
    a ∈ P.I ↔
      Membership.mem (α := A.op.N) (γ := Set A.op.N) ((⇑N.opEquiv : (a : A.op.N) → A.N) ⁻¹' P.I)
        ((RelIso.toEquiv (r := fun (x1 x2 : A.N) ↦ x1 ≤ x2) (s := fun (x1 x2 : A.op.N) ↦ x1 ≤ x2)
                (OrderIso.symm N.opEquiv) :
              (a : A.N) → A.op.N)
            a :
          A.op.N)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : (↑P.II : Type u)
⊢ (OrderIso.symm N.opEquiv : (a : A.N) → A.op.N) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N) ∈ P.op.I

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : (↑P.II : Type u)
⊢ (P.op.p :
        (a : (↑((⇑N.opEquiv : (a : A.op.N) → A.N) ⁻¹' P.II) : Type u)) →
          (↑((⇑N.opEquiv : (a : A.op.N) → A.N) ⁻¹' P.I) : Type u))
      (Subtype.mk (p := fun (x : A.op.N) ↦
        Membership.mem (γ := Set A.op.N) ((⇑N.opEquiv : (a : A.op.N) → A.N) ⁻¹' P.II) x)
        ((OrderIso.symm N.opEquiv : (a : A.N) → A.op.N) (↑x : A.N)) ⋯) =
    Subtype.mk (p := fun (x : A.op.N) ↦ Membership.mem (γ := Set A.op.N) ((⇑N.opEquiv : (a : A.op.N) → A.N) ⁻¹' P.I) x)
      ((OrderIso.symm N.opEquiv : (a : A.N) → A.op.N) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N)) ⋯

Tactic:
rfl

Premises used: SSet.N.mk, Quiver.Hom.op, CategoryTheory.Functor.comp, Nat.pred, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x y : (↑P.II : Type u)
⊢ Eq (α := (↑P.op.II : Type u))
      (Subtype.mk (p := fun (x : A.op.N) ↦ x ∈ P.op.II) ((OrderIso.symm N.opEquiv : (a : A.N) → A.op.N) (↑x : A.N)) ⋯ :
        { x : A.op.N // x ∈ P.op.II })
      (Subtype.mk (p := fun (x : A.op.N) ↦ x ∈ P.op.II) ((OrderIso.symm N.opEquiv : (a : A.N) → A.op.N) (↑y : A.N)) ⋯ :
        { x : A.op.N // x ∈ P.op.II }) ↔
    x = y

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x y : (↑P.II : Type u)
⊢ LT.lt (α := A.op.N)
      ((↑(Subtype.mk (p := fun (x : A.op.N) ↦ x ∈ P.op.II) ((OrderIso.symm N.opEquiv : (a : A.N) → A.op.N) (↑x : A.N))
              ⋯) :
          A.op.N) :
        A.op.N)
      ((↑((P.op.p : (a : (↑P.op.II : Type u)) → (↑P.op.I : Type u))
              (Subtype.mk (p := fun (x : A.op.N) ↦ x ∈ P.op.II)
                ((OrderIso.symm N.opEquiv : (a : A.N) → A.op.N) (↑y : A.N)) ⋯)) :
          A.op.N) :
        A.op.N) ↔
    (↑x : A.N) < (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
⊢ WellFounded P.AncestralRel

Tactic:
have hP := P.wf
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
hP : WellFounded P.AncestralRel
rw :
  ∀ (hP : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }),
    IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.op.II : Type u) // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }
⊢ WellFounded P.op.AncestralRel

Tactic:
rw [wellFounded_iff_isEmpty_descending_chain] at hP ⊢

Premises used: wellFounded_iff_isEmpty_descending_chain
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
hP : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
by_contra! :
  ∀ (this : Nonempty.{u + 1} { f : ℕ → (↑P.op.II : Type u) // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }), False
⊢ IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.op.II : Type u) // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }

Tactic:
by_contra!
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
hP : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
this : Nonempty.{u + 1} { f : ℕ → (↑P.op.II : Type u) // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }
obtain : ∀ (f : ℕ → (↑P.op.II : Type u)) (hf : ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n)), False
⊢ False

Tactic:
obtain ⟨f, hf⟩ := this