awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
n m : ℕ
⊢ IsIso (X := hoFunctor.obj (Δ[n] ⨯ Δ[m])) (Y := hoFunctor.obj Δ[n] ⨯ hoFunctor.obj Δ[m])
    (prodComparison hoFunctor Δ[n] Δ[m])

Tactic:
IsIso.of_isIso_fac_right (prodComparison_natural.{w}
    hoFunctor (stdSimplex.isoNerve n).hom (stdSimplex.isoNerve m).hom).symm

Premises used: CategoryTheory.IsIso.of_isIso_fac_right, CategoryTheory.Limits.prodComparison_natural, SSet.stdSimplex.isoNerve, Eq.symm, CategoryTheory.Iso.hom, SSet.hoFunctor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
D X : SSet
H :
  ∀ (m : ℕ),
    IsIso (X := hoFunctor.obj (D ⨯ Δ[m])) (Y := hoFunctor.obj D ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor D Δ[m])
rw :
  ∀ (X_1 : CostructuredArrow uliftYoneda.{u, 0, 0} X),
    IsIso (X :=
      Functor.obj
        ((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
          Functor.obj prod.functor D ⋙ hoFunctor)
        X_1)
      (Y :=
      Functor.obj
        ((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
          hoFunctor ⋙ Functor.obj prod.functor (hoFunctor.obj D))
        X_1)
      (NatTrans.app
        (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0})
          (prodComparisonNatTrans hoFunctor D))
        X_1)
⊢ IsIso (C := CostructuredArrow uliftYoneda.{u, 0, 0} X ⥤ Cat) (X :=
    (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙ Functor.obj prod.functor D ⋙ hoFunctor)
    (Y :=
    (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
      hoFunctor ⋙ Functor.obj prod.functor (hoFunctor.obj D))
    (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0})
      (prodComparisonNatTrans hoFunctor D))

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
D X : SSet
H :
  ∀ (m : ℕ),
    IsIso (X := hoFunctor.obj (D ⨯ Δ[m])) (Y := hoFunctor.obj D ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor D Δ[m])
⊢ ∀ (X_1 : CostructuredArrow uliftYoneda.{u, 0, 0} X),
    IsIso (X :=
      Functor.obj
        ((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
          Functor.obj prod.functor D ⋙ hoFunctor)
        X_1)
      (Y :=
      Functor.obj
        ((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
          hoFunctor ⋙ Functor.obj prod.functor (hoFunctor.obj D))
        X_1)
      (NatTrans.app
        (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0})
          (prodComparisonNatTrans hoFunctor D))
        X_1)

Tactic:
fun x ↦ H (x.left).len

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Cat.of, CategoryTheory.Bundled.of, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, CategoryTheory.CostructuredArrow.left, CategoryTheory.Limits.prodComparison, SimplexCategory.len
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
D X : SSet
H :
  ∀ (m : ℕ),
    IsIso (X := hoFunctor.obj (D ⨯ Δ[m])) (Y := hoFunctor.obj D ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor D Δ[m])
⊢ ∀ (X_1 : CostructuredArrow uliftYoneda.{u, 0, 0} X),
    IsIso (X :=
      Functor.obj
        ((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
          Functor.obj prod.functor D ⋙ hoFunctor)
        X_1)
      (Y :=
      Functor.obj
        ((CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
          hoFunctor ⋙ Functor.obj prod.functor (hoFunctor.obj D))
        X_1)
      (NatTrans.app
        (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0})
          (prodComparisonNatTrans hoFunctor D))
        X_1)

Tactic:
exact fun x ↦ H (x.left).len
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
D X : SSet
H :
  ∀ (m : ℕ),
    IsIso (X := hoFunctor.obj (D ⨯ Δ[m])) (Y := hoFunctor.obj D ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor D Δ[m])
⊢ IsIso (C := CostructuredArrow uliftYoneda.{u, 0, 0} X ⥤ Cat) (X :=
    (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙ Functor.obj prod.functor D ⋙ hoFunctor)
    (Y :=
    (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
      hoFunctor ⋙ Functor.obj prod.functor (hoFunctor.obj D))
    (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0})
      (prodComparisonNatTrans hoFunctor D))

Tactic:
have : IsIso (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda X ⋙ uliftYoneda)
      (prodComparisonNatTrans hoFunctor.{u} D)) := by
    rw [NatTrans.isIso_iff_isIso_app]
    exact fun x ↦ H (x.left).len
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
D X : SSet
H :
  ∀ (m : ℕ),
    IsIso (X := hoFunctor.obj (D ⨯ Δ[m])) (Y := hoFunctor.obj D ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor D Δ[m])
this :
  IsIso (C := CostructuredArrow uliftYoneda.{u, 0, 0} X ⥤ Cat) (X :=
    (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙ Functor.obj prod.functor D ⋙ hoFunctor)
    (Y :=
    (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
      hoFunctor ⋙ Functor.obj prod.functor (hoFunctor.obj D))
    (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0})
      (prodComparisonNatTrans hoFunctor D))
⊢ IsIso (X := hoFunctor.obj (D ⨯ X)) (Y := hoFunctor.obj D ⨯ hoFunctor.obj X) (prodComparison hoFunctor D X)

Tactic:
isIso_app_coconePt_of_preservesColimit _ (prodComparisonNatTrans hoFunctor _) _
    (Presheaf.isColimitTautologicalCocone' X)

Premises used: CategoryTheory.Presheaf.isColimitTautologicalCocone', CategoryTheory.Limits.isIso_app_coconePt_of_preservesColimit, CategoryTheory.Cat.of, CategoryTheory.Bundled.of, CategoryTheory.Limits.limit, CategoryTheory.Limits.limit.lift, CategoryTheory.Limits.prodComparison, SSet.hoFunctor, CategoryTheory.Limits.prodComparisonNatTrans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
D X : SSet
H :
  ∀ (m : ℕ),
    IsIso (X := hoFunctor.obj (D ⨯ Δ[m])) (Y := hoFunctor.obj D ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor D Δ[m])
this :
  IsIso (C := CostructuredArrow uliftYoneda.{u, 0, 0} X ⥤ Cat) (X :=
    (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙ Functor.obj prod.functor D ⋙ hoFunctor)
    (Y :=
    (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0}) ⋙
      hoFunctor ⋙ Functor.obj prod.functor (hoFunctor.obj D))
    (Functor.whiskerLeft (CostructuredArrow.proj uliftYoneda.{u, 0, 0} X ⋙ uliftYoneda.{u, 0, 0})
      (prodComparisonNatTrans hoFunctor D))
⊢ IsIso (X := hoFunctor.obj (D ⨯ X)) (Y := hoFunctor.obj D ⨯ hoFunctor.obj X) (prodComparison hoFunctor D X)

Tactic:
exact isIso_app_coconePt_of_preservesColimit _ (prodComparisonNatTrans hoFunctor _) _
    (Presheaf.isColimitTautologicalCocone' X)

Premises used: CategoryTheory.Presheaf.isColimitTautologicalCocone', CategoryTheory.Limits.isIso_app_coconePt_of_preservesColimit, SSet.hoFunctor, CategoryTheory.Limits.prodComparisonNatTrans
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X Y : SSet
m : ℕ
h :
  Eq (α := hoFunctor.obj (X ⨯ Δ[m]) ⟶ hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m])
    (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
      (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
        (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
convert_to :
  IsIso (X := hoFunctor.obj (X ⨯ Δ[m])) (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
    (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
      (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
        (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
⊢ IsIso (X := hoFunctor.obj (X ⨯ Δ[m])) (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m])

Tactic:
convert_to IsIso (hoFunctor.map (prod.braiding _ _).hom ≫
    prodComparison hoFunctor Δ[m] X ≫ (prod.braiding _ _).hom)

Premises used: CategoryTheory.IsIso, SSet.stdSimplex, CategoryTheory.Functor.map, SimplexCategory.mk, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.prod.braiding, CategoryTheory.Iso.hom, CategoryTheory.Limits.prodComparison, CategoryTheory.Functor.obj, SSet.hoFunctor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X Y : SSet
m : ℕ
h :
  Eq (α := (↑(hoFunctor.obj (X ⨯ Δ[m])) : Type u) ⥤ (↑(hoFunctor.obj X) : Type u))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m]) prod.fst))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
        (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
          (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
            (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
        prod.fst))
h₁ :
  Eq (α := (↑(hoFunctor.obj (X ⨯ Δ[m])) : Type u) ⥤ (↑(hoFunctor.obj Δ[m]) : Type u))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m]) prod.snd))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
        (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
          (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
            (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
        prod.snd))
⊢ Eq (α := hoFunctor.obj (X ⨯ Δ[m]) ⟶ hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m])
    (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
      (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
        (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X Y : SSet
m : ℕ
⊢ Eq (α := (↑(hoFunctor.obj (X ⨯ Δ[m])) : Type u) ⥤ (↑(hoFunctor.obj X) : Type u))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m]) prod.fst))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
        (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
          (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
            (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
        prod.fst))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X Y : SSet
m : ℕ
⊢ Eq (α := (↑(hoFunctor.obj (X ⨯ Δ[m])) : Type u) ⥤ (↑(hoFunctor.obj Δ[m]) : Type u))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m]) (prodComparison hoFunctor X Δ[m]) prod.snd))
    (Cat.Hom.toFunctor
      (CategoryStruct.comp (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
        (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
          (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
            (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))
        prod.snd))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X Y : SSet
m : ℕ
this :
  IsIso (X := hoFunctor.obj (Δ[m] ⨯ X)) (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
⊢ IsIso (X := hoFunctor.obj (X ⨯ Δ[m])) (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
    (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
      (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
        (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X Y : SSet
m : ℕ
suffices :
  IsIso (X := hoFunctor.obj (Δ[m] ⨯ X)) (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
⊢ IsIso (X := hoFunctor.obj (X ⨯ Δ[m])) (Y := hoFunctor.obj X ⨯ hoFunctor.obj Δ[m])
    (CategoryStruct.comp (Y := hoFunctor.obj (Δ[m] ⨯ X)) (hoFunctor.map (Iso.hom (prod.braiding X Δ[m])))
      (CategoryStruct.comp (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)
        (Iso.hom (prod.braiding (hoFunctor.obj Δ[m]) (hoFunctor.obj X)))))

Tactic:
suffices IsIso (prodComparison hoFunctor Δ[m] X) by infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X Y : SSet
m : ℕ
⊢ IsIso (X := hoFunctor.obj (Δ[m] ⨯ X)) (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)

Tactic:
isIso_prodComparison_of_stdSimplex _ (isIso_prodComparison_stdSimplex _)

Premises used: CategoryTheory.hoFunctor.isIso_prodComparison_of_stdSimplex, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X Y : SSet
m : ℕ
⊢ IsIso (X := hoFunctor.obj (Δ[m] ⨯ X)) (Y := hoFunctor.obj Δ[m] ⨯ hoFunctor.obj X) (prodComparison hoFunctor Δ[m] X)

Tactic:
exact isIso_prodComparison_of_stdSimplex _ (isIso_prodComparison_stdSimplex _)

Premises used: CategoryTheory.hoFunctor.isIso_prodComparison_of_stdSimplex, CategoryTheory.hoFunctor.isIso_prodComparison_stdSimplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
X Y : SSet
⊢ PreservesLimit (pair X Y) hoFunctor

Tactic:
PreservesLimitPair.of_iso_prod_comparison hoFunctor X Y

Premises used: CategoryTheory.Limits.PreservesLimitPair.of_iso_prod_comparison, SSet.hoFunctor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
Goal:
⊢ PreservesFiniteProducts hoFunctor

Tactic:
PreservesFiniteProducts.of_preserves_binary_and_terminal _

Premises used: CategoryTheory.Limits.PreservesFiniteProducts.of_preserves_binary_and_terminal
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
mp :
  Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      s →
    s.obj i.castSucc = s.obj i.succ
mpr :
  s.obj i.castSucc = s.obj i.succ →
    Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      s
⊢ Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
      s ↔
    s.obj i.castSucc = s.obj i.succ

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
i : Fin (n + 1)
s : nerve X _⦋n⦌
⊢ Eq.{u_1 + 1} (α := X)
    (Functor.obj
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌))
        s)
      i.castSucc)
    (Functor.obj
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌))
        s)
      i.succ)

Tactic:
simp [-nerve_obj, nerve.σ_obj]

Premises used: CategoryTheory.nerve.σ_obj, CategoryTheory.nerve_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
⊢ Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
    (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
        (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
    s

Tactic:
⟨(nerve X).δ i.castSucc s, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, setOf, Exists.intro, CategoryTheory.nerve, Set.range, Fin.castSucc, CategoryTheory.SimplicialObject.δ, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
mpr :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i) :
        (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve X) i.castSucc) :
            (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
          s :
        (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) =
    s
⊢ Membership.mem (γ := Set ((fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
    (Set.range (ι := (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
        (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)))
    s

Tactic:
refine ⟨(nerve X).δ i.castSucc s, ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
mpr :
  ∀ (j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)),
    Functor.obj
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i) :
            (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve X) i.castSucc) :
                (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
              s :
            (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)))
        j =
      s.obj j
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i) :
        (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve X) i.castSucc) :
            (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
          s :
        (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) =
    s

Tactic:
ext j
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
mpr : s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
⊢ Functor.obj
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i) :
          (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve X) i.castSucc) :
              (a : (fun (X : Type u_1) ↦ X) (nerve X _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌))
            s :
          (fun (X : Type u_1) ↦ X) (nerve X _⦋n⦌)))
      j =
    s.obj j

Tactic:
rw [nerve.σ_obj, nerve.δ_obj]

Premises used: CategoryTheory.nerve.σ_obj, CategoryTheory.nerve.δ_obj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
pos : ∀ (h₁ : i.castSucc < j), s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
neg : ∀ (h₁ : ¬i.castSucc < j), s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j

Tactic:
by_cases h₁ : i.castSucc < j

Premises used: Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
h₁ : i.castSucc < j
pos : ∀ (j : Fin (n + 1)) (h₁ : i.castSucc < j.succ), s.obj (i.castSucc.succAbove (i.predAbove j.succ)) = s.obj j.succ
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j

Tactic:
obtain ⟨j, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt h₁)

Premises used: Fin.eq_succ_of_ne_zero, Fin.ne_zero_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin (n + 1)
h₁ : i.castSucc < j.succ
pos : s.obj (i.castSucc.succAbove (j.succ.pred ⋯)) = s.obj j.succ
pos₁ : s.obj (i.castSucc.succAbove j) = s.obj j.succ
pos₂ pos₃ : s.obj j.succ = s.obj j.succ
⊢ s.obj (i.castSucc.succAbove (i.predAbove j.succ)) = s.obj j.succ

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _ h₁, Fin.pred_succ,
        Fin.succAbove_of_le_castSucc _ _ (Fin.le_castSucc_iff.2 h₁)]

Premises used: Iff.mpr, Fin.succAbove_of_le_castSucc, Fin.predAbove_of_castSucc_lt, Fin.pred_succ, Fin.le_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
h₁ : ¬i.castSucc < j
⊢ j ≤ i.castSucc

Tactic:
simp only [not_lt] at h₁

Premises used: not_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
h : s.obj i.castSucc = s.obj i.succ
j : Fin ((Opposite.unop (Opposite.op ⦋n + 1⦌)).len + 1)
h₁ : j ≤ i.castSucc
⊢ s.obj (i.castSucc.succAbove (i.predAbove j)) = s.obj j

Tactic:
grind [→ Fin.succAbove_of_castSucc_lt,
        → Fin.predAbove_of_le_castSucc, Fin.castSucc_castPred, Fin.castPred_castSucc,
        Fin.succAbove_castSucc_self, → LE.le.lt_or_eq]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Fin.succAbove_castSucc_self, LE.le.lt_or_eq, Iff.not, Fin.castSucc_lt_last, Fin.castSucc_castPred, Fin.predAbove_of_le_castSucc, Fin.succAbove_of_castSucc_lt, LT.lt.ne
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate
Goal:
X : Type u_1
inst : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
hi : s.obj i.castSucc = s.obj i.succ
simp :
  ∃ (i : Fin (n + 1)),
    Membership.mem (γ := Set (ComposableArrows X (n + 1)))
      (Set.range (ι := ComposableArrows X n)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve X) i)) :
          (a : ComposableArrows X n) → ComposableArrows X (n + 1)))
      s
⊢ Membership.mem (γ := Set (nerve X _⦋n + 1⦌)) ((nerve X).degenerate (n + 1)) s

Tactic:
simp only [nerve_obj, SSet.degenerate_eq_iUnion_range_σ, Set.mem_iUnion]

Premises used: Set.mem_iUnion, CategoryTheory.nerve_obj, SSet.degenerate_eq_iUnion_range_σ