awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W X Y Z : Truncated 2
x : X ⟶ Y
x_1 : Y ⟶ Z
h :
  (mapHomotopyCategory (x ≫ x_1)).toCatHom.toFunctor =
    ((mapHomotopyCategory x).toCatHom ≫ (mapHomotopyCategory x_1).toCatHom).toFunctor
⊢ (mapHomotopyCategory (x ≫ x_1)).toCatHom = (mapHomotopyCategory x).toCatHom ≫ (mapHomotopyCategory x_1).toCatHom

Tactic:
ext1
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W X Y Z : Truncated 2
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ ∀
    (x_2 :
      X.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))),
    (mapHomotopyCategory (x ≫ x_1)).toCatHom.toFunctor.obj (HomotopyCategory.mk x_2) =
      ((mapHomotopyCategory x).toCatHom ≫ (mapHomotopyCategory x_1).toCatHom).toFunctor.obj (HomotopyCategory.mk x_2)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W X Y Z : Truncated 2
x : X ⟶ Y
x_1 : Y ⟶ Z
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀
    ⦃x_2 y :
      X.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x_2 y),
    (mapHomotopyCategory (x ≫ x_1)).toCatHom.toFunctor.map (HomotopyCategory.homMk e) =
      eqToHom ⋯ ≫
        ((mapHomotopyCategory x).toCatHom ≫ (mapHomotopyCategory x_1).toCatHom).toFunctor.map
            (HomotopyCategory.homMk e) ≫
          eqToHom ⋯
⊢ ∀
    ⦃x_2 y :
      X.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x_2 y),
    (mapHomotopyCategory (x ≫ x_1)).toCatHom.toFunctor.map (HomotopyCategory.homMk e) =
      eqToHom ⋯ ≫
        ((mapHomotopyCategory x).toCatHom ≫ (mapHomotopyCategory x_1).toCatHom).toFunctor.map
            (HomotopyCategory.homMk e) ≫
          eqToHom ⋯

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V W X Y Z : Truncated 2
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ (mapHomotopyCategory (x ≫ x_1)).toCatHom.toFunctor =
    ((mapHomotopyCategory x).toCatHom ≫ (mapHomotopyCategory x_1).toCatHom).toFunctor

Tactic:
exact HomotopyCategory.functor_ext (by simp) (by cat_disch)

Premises used: SSet.Truncated.HomotopyCategory.functor_ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
X Y : Truncated 2
f : X ⟶ Y
⊢ ((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ HomotopyCategory.quotientFunctor Y =
    HomotopyCategory.quotientFunctor X ⋙ mapHomotopyCategory f

Tactic:
rfl

Premises used: SSet.OneTruncation₂, CategoryTheory.Cat.FreeRefl.mk, SSet.Truncated.HomotopyCategory.quotientFunctor, CategoryTheory.Paths, CategoryTheory.Quotient.functor, CategoryTheory.Functor.comp, CategoryTheory.Cat.freeReflMap, CategoryTheory.Cat.FreeRefl.lift, CategoryTheory.Cat.FreeRefl, CategoryTheory.Cat.FreeRefl.lift', CategoryTheory.Quotient.lift, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
V : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
F₁ F₂ : CategoryTheory.Functor.{u, v_1, u, u_1} V.HomotopyCategory D
h : quotientFunctor V ⋙ F₁ = quotientFunctor V ⋙ F₂
⊢ F₁ = F₂

Tactic:
Quotient.lift_unique' _ _ _ h

Premises used: CategoryTheory.Quotient.lift_unique', SSet.Truncated.HomotopyCategory
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
x y : OneTruncation₂ (obj (truncation 2) Δ[0])
⊢ x = default

Tactic:
Unique.uniq _ _

Premises used: Unique.uniq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
x y : OneTruncation₂ (obj (truncation 2) Δ[0])
obtain : default ⟶ y
⊢ x ⟶ y

Tactic:
obtain rfl : x = default := Unique.uniq _ _

Premises used: Inhabited.default, Unique.uniq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
y : OneTruncation₂ (obj (truncation 2) Δ[0])
⊢ y = default

Tactic:
Unique.uniq _ _

Premises used: Unique.uniq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
y : OneTruncation₂ (obj (truncation 2) Δ[0])
obtain : Quiver.Hom (V := OneTruncation₂ (obj (truncation 2) Δ[0])) default default
⊢ default ⟶ y

Tactic:
obtain rfl : y = default := Unique.uniq _ _

Premises used: Inhabited.default, Unique.uniq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
⊢ Quiver.Hom (V := OneTruncation₂ (obj (truncation 2) Δ[0])) default default

Tactic:
exact 𝟙rq instUniqueOneTruncation₂DeltaZero.default

Premises used: Inhabited.default, CategoryTheory.ReflQuiver.id
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
x y : OneTruncation₂ (obj (truncation 2) Δ[0])
x_1 : x ⟶ y
this : Subsingleton.{u_1 + 1}
  (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (obj (truncation 2) Δ[0])
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :=
  instUniqueHomOneTruncation₂ObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk._proof_1
h :
  x_1.edge =
    Truncated.Edge.edge (x₁ := y)
      (Eq.ndrec (a := default) (motive := fun (x : OneTruncation₂ (obj (truncation 2) Δ[0])) ↦ x ⟶ y)
        (Eq.ndrec (motive := fun (y : OneTruncation₂ (obj (truncation 2) Δ[0])) ↦ default ⟶ y) (𝟙rq default) ⋯) ⋯)
⊢ x_1 =
    Eq.ndrec (a := default) (motive := fun (x : OneTruncation₂ (obj (truncation 2) Δ[0])) ↦ x ⟶ y)
      (Eq.ndrec (motive := fun (y : OneTruncation₂ (obj (truncation 2) Δ[0])) ↦ default ⟶ y) (𝟙rq default) ⋯) ⋯

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
x y : OneTruncation₂ (obj (truncation 2) Δ[0])
x_1 : x ⟶ y
this : Subsingleton.{u_1 + 1}
  (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (obj (truncation 2) Δ[0])
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :=
  instUniqueHomOneTruncation₂ObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk._proof_1
⊢ x_1.edge =
    Truncated.Edge.edge (x₁ := y)
      (Eq.ndrec (a := default) (motive := fun (x : OneTruncation₂ (obj (truncation 2) Δ[0])) ↦ x ⟶ y)
        (Eq.ndrec (motive := fun (y : OneTruncation₂ (obj (truncation 2) Δ[0])) ↦ default ⟶ y) (𝟙rq default) ⋯) ⋯)

Tactic:
this.allEq _ _

Premises used: Subsingleton.allEq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
x y : OneTruncation₂ (obj (truncation 2) Δ[0])
x_1 : x ⟶ y
this : Subsingleton.{u_1 + 1}
  (obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (obj (truncation 2) Δ[0])
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ ⋯))) :=
  instUniqueHomOneTruncation₂ObjTruncatedOfNatNatTruncationSimplexCategoryStdSimplexMk._proof_1
⊢ x_1.edge =
    Truncated.Edge.edge (x₁ := y)
      (Eq.ndrec (a := default) (motive := fun (x : OneTruncation₂ (obj (truncation 2) Δ[0])) ↦ x ⟶ y)
        (Eq.ndrec (motive := fun (y : OneTruncation₂ (obj (truncation 2) Δ[0])) ↦ default ⟶ y) (𝟙rq default) ⋯) ⋯)

Tactic:
exact this.allEq _ _

Premises used: Subsingleton.allEq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
X Y : Truncated.HomotopyCategory (obj (truncation 2) Δ[0])
x : X ⟶ Y
⊢ X = Y

Tactic:
subsingleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
⊢ PreservesLimit (empty SSet) hoFunctor

Tactic:
preservesTerminal_of_iso hoFunctor hoFunctor.terminalIso

Premises used: CategoryTheory.Limits.preservesTerminal_of_iso, SSet.hoFunctor.terminalIso, SSet.hoFunctor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
Goal:
⊢ PreservesLimitsOfShape (Discrete PEmpty.{1}) hoFunctor

Tactic:
preservesLimitsOfShape_pempty_of_preservesTerminal _

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
U V : SimplexCategoryᵒᵖ
φ : U ⟶ V
s : Δ[n].obj U
hs :
  Membership.mem (γ := Set (Δ[n].obj U))
    {s : Δ[n].obj U |
      Ne (α := Set (Fin (n + 1)))
        (Set.range (ι := Fin ((unop U).len + 1))
            (⇑(stdSimplex.asOrderHom s) : (a : Fin ((unop U).len + 1)) → Fin (n + 1)) ∪
          {i})
        Set.univ}
    s
h :
  Eq (α := Set (Fin (n + 1)))
    (Set.range (ι := Fin ((unop V).len + 1))
        (⇑(stdSimplex.asOrderHom.{u}
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map φ) :
                  (a : (fun (X : Type u) ↦ X) (Δ[n].obj U)) → (fun (X : Type u) ↦ X) (Δ[n].obj V))
                s)) :
          (a : Fin ((unop V).len + 1)) → Fin (n + 1)) ∪
      {i})
    Set.univ
rw :
  ∀
    (h :
      ∀ (x : Fin (n + 1)),
        Membership.mem (γ := Set (Fin (n + 1)))
          (Set.range (ι := Fin ((unop V).len + 1))
              (⇑(stdSimplex.asOrderHom.{u}
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map φ) :
                        (a : (fun (X : Type u) ↦ X) (Δ[n].obj U)) → (fun (X : Type u) ↦ X) (Δ[n].obj V))
                      s)) :
                (a : Fin ((unop V).len + 1)) → Fin (n + 1)) ∪
            {i})
          x)
    (x : Fin (n + 1)),
    Membership.mem (γ := Set (Fin (n + 1)))
      (Set.range (ι := Fin ((unop U).len + 1))
          (⇑(stdSimplex.asOrderHom s) : (a : Fin ((unop U).len + 1)) → Fin (n + 1)) ∪
        {i})
      x
⊢ Eq (α := Set (Fin (n + 1)))
    (Set.range (ι := Fin ((unop U).len + 1)) (⇑(stdSimplex.asOrderHom s) : (a : Fin ((unop U).len + 1)) → Fin (n + 1)) ∪
      {i})
    Set.univ

Tactic:
rw [Set.eq_univ_iff_forall] at h ⊢

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
U V : SimplexCategoryᵒᵖ
φ : U ⟶ V
s : Δ[n].obj U
hs :
  Membership.mem (γ := Set (Δ[n].obj U))
    {s : Δ[n].obj U |
      Ne (α := Set (Fin (n + 1)))
        (Set.range (ι := Fin ((unop U).len + 1))
            (⇑(stdSimplex.asOrderHom s) : (a : Fin ((unop U).len + 1)) → Fin (n + 1)) ∪
          {i})
        Set.univ}
    s
h :
  ∀ (x : Fin (n + 1)),
    Membership.mem (γ := Set (Fin (n + 1)))
      (Set.range (ι := Fin ((unop V).len + 1))
          (⇑(stdSimplex.asOrderHom.{u}
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map φ) :
                    (a : (fun (X : Type u) ↦ X) (Δ[n].obj U)) → (fun (X : Type u) ↦ X) (Δ[n].obj V))
                  s)) :
            (a : Fin ((unop V).len + 1)) → Fin (n + 1)) ∪
        {i})
      x
j : Fin (n + 1)
apply :
  Membership.mem (γ := Set (Fin (n + 1)))
      (Set.range (ι := Fin ((unop V).len + 1))
        (⇑(stdSimplex.asOrderHom.{u}
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map φ) :
                  (a : (fun (X : Type u) ↦ X) (Δ[n].obj U)) → (fun (X : Type u) ↦ X) (Δ[n].obj V))
                s)) :
          (a : Fin ((unop V).len + 1)) → Fin (n + 1)))
      j →
    Membership.mem (γ := Set (Fin (n + 1)))
      (Set.range (ι := Fin ((unop U).len + 1))
        (⇑(stdSimplex.asOrderHom s) : (a : Fin ((unop U).len + 1)) → Fin (n + 1)))
      j
⊢ Membership.mem (γ := Set (Fin (n + 1)))
    (Set.range (ι := Fin ((unop U).len + 1)) (⇑(stdSimplex.asOrderHom s) : (a : Fin ((unop U).len + 1)) → Fin (n + 1)) ∪
      {i})
    j

Tactic:
apply Or.imp _ id (h j)

Premises used: id, Or.imp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
U V : SimplexCategoryᵒᵖ
φ : U ⟶ V
s : Δ[n].obj U
hs :
  Membership.mem (γ := Set (Δ[n].obj U))
    {s : Δ[n].obj U |
      Ne (α := Set (Fin (n + 1)))
        (Set.range (ι := Fin ((unop U).len + 1))
            (⇑(stdSimplex.asOrderHom s) : (a : Fin ((unop U).len + 1)) → Fin (n + 1)) ∪
          {i})
        Set.univ}
    s
h :
  ∀ (x : Fin (n + 1)),
    Membership.mem (γ := Set (Fin (n + 1)))
      (Set.range (ι := Fin ((unop V).len + 1))
          (⇑(stdSimplex.asOrderHom.{u}
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map φ) :
                    (a : (fun (X : Type u) ↦ X) (Δ[n].obj U)) → (fun (X : Type u) ↦ X) (Δ[n].obj V))
                  s)) :
            (a : Fin ((unop V).len + 1)) → Fin (n + 1)) ∪
        {i})
      x
j : Fin (n + 1)
hj :
  Membership.mem (γ := Set (Fin (n + 1)))
    (Set.range (ι := Fin ((unop V).len + 1))
      (⇑(stdSimplex.asOrderHom.{u}
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map φ) :
                (a : (fun (X : Type u) ↦ X) (Δ[n].obj U)) → (fun (X : Type u) ↦ X) (Δ[n].obj V))
              s)) :
        (a : Fin ((unop V).len + 1)) → Fin (n + 1)))
    j
⊢ Membership.mem (γ := Set (Fin (n + 1)))
    (Set.range (ι := Fin ((unop U).len + 1)) (⇑(stdSimplex.asOrderHom s) : (a : Fin ((unop U).len + 1)) → Fin (n + 1)))
    j

Tactic:
Set.range_comp_subset_range _ _ hj

Premises used: Set.range_comp_subset_range
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
U V : SimplexCategoryᵒᵖ
φ : U ⟶ V
s : Δ[n].obj U
hs :
  Membership.mem (γ := Set (Δ[n].obj U))
    {s : Δ[n].obj U |
      Ne (α := Set (Fin (n + 1)))
        (Set.range (ι := Fin ((unop U).len + 1))
            (⇑(stdSimplex.asOrderHom s) : (a : Fin ((unop U).len + 1)) → Fin (n + 1)) ∪
          {i})
        Set.univ}
    s
h :
  ∀ (x : Fin (n + 1)),
    Membership.mem (γ := Set (Fin (n + 1)))
      (Set.range (ι := Fin ((unop V).len + 1))
          (⇑(stdSimplex.asOrderHom.{u}
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map φ) :
                    (a : (fun (X : Type u) ↦ X) (Δ[n].obj U)) → (fun (X : Type u) ↦ X) (Δ[n].obj V))
                  s)) :
            (a : Fin ((unop V).len + 1)) → Fin (n + 1)) ∪
        {i})
      x
j : Fin (n + 1)
hj :
  Membership.mem (γ := Set (Fin (n + 1)))
    (Set.range (ι := Fin ((unop V).len + 1))
      (⇑(stdSimplex.asOrderHom.{u}
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n].map φ) :
                (a : (fun (X : Type u) ↦ X) (Δ[n].obj U)) → (fun (X : Type u) ↦ X) (Δ[n].obj V))
              s)) :
        (a : Fin ((unop V).len + 1)) → Fin (n + 1)))
    j
⊢ Membership.mem (γ := Set (Fin (n + 1)))
    (Set.range (ι := Fin ((unop U).len + 1)) (⇑(stdSimplex.asOrderHom s) : (a : Fin ((unop U).len + 1)) → Fin (n + 1)))
    j

Tactic:
exact Set.range_comp_subset_range _ _ hj

Premises used: Set.range_comp_subset_range
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : SimplexCategoryᵒᵖ
x : Δ[n].obj m
⊢ x ∈ Λ[n, i].obj m ↔
    Ne (α := Set (Fin (n + 1)))
      (Set.range (ι := Fin ((unop m).len + 1))
          (⇑(stdSimplex.asOrderHom x) : (a : Fin ((unop m).len + 1)) → Fin (n + 1)) ∪
        {i})
      Set.univ

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Not
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
obj :
  ∀ (m : SimplexCategoryᵒᵖ) (j : Δ[n].obj m),
    j ∈ Λ[n, i].obj m ↔
      Membership.mem (γ := Set (Δ[n].obj m))
        (Subfunctor.obj (⨆ (j : (↑{i}ᶜ : Type)), stdSimplex.face {(↑j : Fin (n + 1))}ᶜ) m) j
⊢ Λ[n, i] = ⨆ (j : (↑{i}ᶜ : Type)), stdSimplex.face {(↑j : Fin (n + 1))}ᶜ

Tactic:
ext m j
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : SimplexCategoryᵒᵖ
j : Δ[n].obj m
obj :
  (∃ (x : Fin (n + 1)),
      ¬x = i ∧
        ∀ (x_1 : Fin ((unop m).len + 1)),
          ¬(stdSimplex.asOrderHom j : (a : Fin ((unop m).len + 1)) → Fin (n + 1)) x_1 = x) ↔
    ∃ (i_1 : Fin (n + 1)),
      ¬i_1 = i ∧
        ∀ (x : Fin ((unop m).len + 1)),
          ¬(SimplexCategory.Hom.toOrderHom
                    (((stdSimplex.objEquiv : Δ[n].obj m ≃ (unop m ⟶ ⦋n⦌)) : (a : Δ[n].obj m) → unop m ⟶ ⦋n⦌) j) :
                  (a : Fin ((unop m).len + 1)) → Fin (n + 1))
                x =
              i_1
⊢ j ∈ Λ[n, i].obj m ↔
    Membership.mem (γ := Set (Δ[n].obj m))
      (Subfunctor.obj (⨆ (j : (↑{i}ᶜ : Type)), stdSimplex.face {(↑j : Fin (n + 1))}ᶜ) m) j

Tactic:
simp [stdSimplex.face_obj, horn, Set.eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall, SSet.stdSimplex.face_obj, SSet.horn
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
m : SimplexCategoryᵒᵖ
j : Δ[n].obj m
⊢ (∃ (x : Fin (n + 1)),
      ¬x = i ∧
        ∀ (x_1 : Fin ((unop m).len + 1)),
          ¬(stdSimplex.asOrderHom j : (a : Fin ((unop m).len + 1)) → Fin (n + 1)) x_1 = x) ↔
    ∃ (i_1 : Fin (n + 1)),
      ¬i_1 = i ∧
        ∀ (x : Fin ((unop m).len + 1)),
          ¬(SimplexCategory.Hom.toOrderHom
                    (((stdSimplex.objEquiv : Δ[n].obj m ≃ (unop m ⟶ ⦋n⦌)) : (a : Δ[n].obj m) → unop m ⟶ ⦋n⦌) j) :
                  (a : Fin ((unop m).len + 1)) → Fin (n + 1))
                x =
              i_1

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 1)
rw :
  ∀ (i_1 : (↑{i}ᶜ : Type)),
    HasDimensionLT.{u} (Subcomplex.toSSet (X := Δ[n]) (stdSimplex.face {(↑i_1 : Fin (n + 1))}ᶜ)) n
⊢ HasDimensionLT.{u} Λ[n, i].toSSet n

Tactic:
rw [horn_eq_iSup, hasDimensionLT_iSup_iff]

Premises used: SSet.horn_eq_iSup, SSet.hasDimensionLT_iSup_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i_1 : Fin (n + 1)
i : (↑{i_1}ᶜ : Type)
⊢ Finset.card (α := Fin (n + 1)) {(↑i : Fin (n + 1))}ᶜ ≤ n

Tactic:
simp [Finset.card_compl]

Premises used: Finset.card_compl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n d : ℕ
s : Δ[n] _⦋d⦌
i : Fin (n + 1)
⊢ Membership.mem (γ := Set (Δ[n] _⦋d⦌)) (Λ[n, i].obj (op ⦋d⦌)) s ↔
    ∃ (j : Fin (n + 1)) (_ : j ≠ i), j ∉ Set.range (ι := Fin (d + 1)) (⇑s : (a : Fin (d + 1)) → Fin (n + 1))

Tactic:
simp [horn_eq_iSup]

Premises used: SSet.horn_eq_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≠ j
rw :
  LE.le.{u} (α := Δ[n].Subcomplex) (stdSimplex.face {i}ᶜ)
    (⨆ (j_1 : (↑{j}ᶜ : Type)), stdSimplex.face {(↑j_1 : Fin (n + 1))}ᶜ)
⊢ stdSimplex.face {i}ᶜ ≤ Λ[n, j]

Tactic:
rw [horn_eq_iSup]

Premises used: SSet.horn_eq_iSup
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≠ j
⊢ LE.le.{u} (α := Δ[n].Subcomplex) (stdSimplex.face {i}ᶜ)
    (⨆ (j_1 : (↑{j}ᶜ : Type)), stdSimplex.face {(↑j_1 : Fin (n + 1))}ᶜ)

Tactic:
le_iSup (fun (k : ({j}ᶜ : Set (Fin (n + 1)))) ↦ stdSimplex.face.{u} {k.1}ᶜ) ⟨i, h⟩

Premises used: Set.Mem, Compl.compl, setOf, SSet.stdSimplex.face, le_iSup, Subtype.mk, Singleton.singleton, Subtype.val
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≠ j
⊢ LE.le.{u} (α := Δ[n].Subcomplex) (stdSimplex.face {i}ᶜ)
    (⨆ (j_1 : (↑{j}ᶜ : Type)), stdSimplex.face {(↑j_1 : Fin (n + 1))}ᶜ)

Tactic:
exact le_iSup (fun (k : ({j}ᶜ : Set (Fin (n + 1)))) ↦ stdSimplex.face.{u} {k.1}ᶜ) ⟨i, h⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
h :
  ∀ (j : Δ[n + 2] _⦋0⦌),
    Membership.mem (γ := Set (Δ[n + 2] _⦋0⦌)) (Λ[n + 2, i].obj (op ⦋0⦌)) j ↔
      Membership.mem (γ := Set (Δ[n + 2] _⦋0⦌)) ⊤ j
⊢ Eq (α := Set (Δ[n + 2] _⦋0⦌)) (Λ[n + 2, i].obj (op ⦋0⦌)) ⊤

Tactic:
ext j
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
h : ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1
⊢ Membership.mem (γ := Set (Δ[n + 2] _⦋0⦌)) (Λ[n + 2, i].obj (op ⦋0⦌)) j ↔ Membership.mem (γ := Set (Δ[n + 2] _⦋0⦌)) ⊤ j

Tactic:
simp only [horn_eq_iSup, Subfunctor.iSup_obj, Set.iUnion_coe_set,
    Set.mem_compl_iff, Set.mem_singleton_iff, Set.mem_iUnion, stdSimplex.mem_face_iff,
    Nat.reduceAdd, Finset.mem_compl, Finset.mem_singleton, exists_prop, Set.top_eq_univ,
    Set.mem_univ, iff_true]

Premises used: Finset.mem_singleton, Set.mem_iUnion, iff_true, Set.iUnion_coe_set, Nat.reduceAdd, SSet.stdSimplex.mem_face_iff, Finset.mem_compl, exists_prop, Set.top_eq_univ, Set.mem_singleton_iff, SSet.horn_eq_iSup, Set.mem_univ, CategoryTheory.Subfunctor.iSup_obj, Set.mem_compl_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
hS : S = Finset.univ
⊢ Finset.card (α := Fin (n + 3)) Finset.univ ≤ S.card

Tactic:
have := Finset.card_le_card hS.symm.le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
hS : S = Finset.univ
this : Finset.card (α := Fin (n + 3)) Finset.univ ≤ S.card
⊢ n + 3 ≤ Finset.card (α := Fin (n + 3)) {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}

Tactic:
simp only [Finset.card_univ, Fintype.card_fin, S] at this

Premises used: Finset.card_univ, Fintype.card_fin
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
hS : S = Finset.univ
this : n + 3 ≤ Finset.card (α := Fin (n + 3)) {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
⊢ n + 3 ≤ 2

Tactic:
have := this.trans Finset.card_le_two
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
hS : S = Finset.univ
this_1 : n + 3 ≤ Finset.card (α := Fin (n + 3)) {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
this : n + 3 ≤ 2
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
⊢ ¬S = Finset.univ

Tactic:
have hS : ¬ (S = Finset.univ) := fun hS ↦ by
    have := Finset.card_le_card hS.symm.le
    simp only [Finset.card_univ, Fintype.card_fin, S] at this
    have := this.trans Finset.card_le_two
    lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
hS : ¬S = Finset.univ
⊢ ∃ (x : Fin (n + 3)), x ∉ S

Tactic:
rw [Finset.eq_univ_iff_forall, not_forall] at hS

Premises used: Finset.eq_univ_iff_forall, Classical.not_forall
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
hS : ∃ (x : Fin (n + 3)), x ∉ S
h :
  ∀ (k : Fin (n + 3)) (hk : k ∉ S),
    ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1
⊢ ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1

Tactic:
obtain ⟨k, hk⟩ := hS
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
k : Fin (n + 3)
hk : k ∉ S
⊢ ¬k = i ∧ ¬k = (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton, not_or, S] at hk

Premises used: Finset.mem_singleton, Finset.mem_insert, not_or
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
k : Fin (n + 3)
hk : ¬k = i ∧ ¬k = (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0
⊢ ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1

Tactic:
⟨k, hk.1, fun a ↦ ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
k : Fin (n + 3)
hk : ¬k = i ∧ ¬k = (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0
h : ∀ (a : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) a = k
⊢ ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1

Tactic:
refine ⟨k, hk.1, fun a ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
S : Finset (Fin (n + 3)) := {i, (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0}
k : Fin (n + 3)
hk : ¬k = i ∧ ¬k = (j : (a : Fin (0 + 1)) → Fin (n + 2 + 1)) 0
a : Fin 1
h : ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, ⋯⟩) = k
⊢ ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) a = k

Tactic:
fin_cases a