awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
x₀ x₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
y₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge x₀ y₁
h : e.edge = e'.edge
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
        (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
          (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
      e.edge =
    y₁
⊢ x₁ = y₁
have rw₁ : Eq (α :=
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
        (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
          (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
      e.edge :
    (fun (X : Type u) ↦ X)
      (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
        (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
          (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
      e'.edge :
    (fun (X : Type u) ↦ X)
      (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
Tactic: rw [← e.tgt_eq, ← e'.tgt_eq, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
x₀ x₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
y₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge x₀ y₁
h : e.edge = e'.edge
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
        (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
          (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
      e.edge =
    y₁
rw₁ :
  Eq (α :=
    V.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
            (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
        e.edge :
      (fun (X : Type u) ↦ X)
        (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
            (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
        e'.edge :
      (fun (X : Type u) ↦ X)
        (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
⊢ x₁ = y₁
have rw₂ : Eq (α :=
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
        (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
          (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
      e'.edge :
    (fun (X : Type u) ↦ X)
      (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 0 Edge._proof_1 Edge._proof_3).op) :
        (a : (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0 + 1⦌, property := Edge._proof_3 }))) →
          (fun (X : Type u) ↦ X) (V.obj (op { obj := ⦋0⦌, property := Edge._proof_1 })))
      e'.edge :
    (fun (X : Type u) ↦ X)
      (V.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
Tactic: rw [← e.tgt_eq, ← e'.tgt_eq, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
x₀ x₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e : Edge x₀ x₁
y₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge x₀ y₁
h : e.edge = e'.edge
⊢ Arrow.mk (homMk e) = Arrow.mk (homMk e')
have obtain : ∀ (e' : Edge x₀ x₁) (h : e.edge = e'.edge), Arrow.mk (homMk e) = Arrow.mk (homMk e')
Tactic: obtain rfl : x₁ = y₁ := by rw [← e.tgt_eq, ← e'.tgt_eq, h]
Cleared hypotheses: y₁, e', h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
x₀ x₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e e' : Edge x₀ x₁
h : e.edge = e'.edge
⊢ Arrow.mk (homMk e) = Arrow.mk (homMk e')
have obtain : ∀ (h : e.edge = e.edge), Arrow.mk (homMk e) = Arrow.mk (homMk e)
Tactic: obtain rfl : e = e' := by aesop
Cleared hypotheses: e', h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
x :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ homMk (Edge.id x) = 𝟙 (mk x)
have rw : 𝟙 ((quotientFunctor V).obj (Cat.FreeRefl.mk x)) = 𝟙 (mk x)
Tactic: rw [homMk, ← OneTruncation₂.reflQuiver_id, Cat.FreeRefl.homMk_id,
    CategoryTheory.Functor.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
⊢ morphismPropertyHomMk V =
    MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V)
have h : ∀ ⦃X Y : V.HomotopyCategory⦄ (f : X ⟶ Y),
  morphismPropertyHomMk V f ↔
    MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V) f
Tactic: ext _ _ f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
X Y : V.HomotopyCategory
f : X ⟶ Y
⊢ morphismPropertyHomMk V f ↔
    MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V) f
have h : morphismPropertyHomMk V f →
  MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
X Y : V.HomotopyCategory
f : X ⟶ Y
h :
  morphismPropertyHomMk V f →
    MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V) f
⊢ morphismPropertyHomMk V f ↔
    MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V) f
have h₁ : MorphismProperty.strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V) f →
  morphismPropertyHomMk V f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
x y : V.HomotopyCategory
f : x ⟶ y
h : ⊤ f
⊢ (morphismPropertyHomMk V).multiplicativeClosure f
have obtain : ∀ (f : x.as (r := OneTruncation₂.HoRel₂ V) ⟶ y.as (r := OneTruncation₂.HoRel₂ V)),
  ⊤ ((quotientFunctor V).map f) → (morphismPropertyHomMk V).multiplicativeClosure ((quotientFunctor V).map f)
Tactic: obtain ⟨f, rfl⟩ := (quotientFunctor _).map_surjective f
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as (r := OneTruncation₂.HoRel₂ V) ⟶ y.as (r := OneTruncation₂.HoRel₂ V)
h : ⊤ ((quotientFunctor V).map f)
⊢ (morphismPropertyHomMk V).multiplicativeClosure ((quotientFunctor V).map f)
have rw : (strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V)).multiplicativeClosure
  ((quotientFunctor V).map f)
Tactic: rw [morphismPropertyHomMk_eq_strictMap]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as (r := OneTruncation₂.HoRel₂ V) ⟶ y.as (r := OneTruncation₂.HoRel₂ V)
h : ⊤ ((quotientFunctor V).map f)
⊢ (strictMap (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)) (quotientFunctor V)).multiplicativeClosure
    ((quotientFunctor V).map f)
have refine : strictMap (multiplicativeClosure (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V))) (quotientFunctor V)
  ((quotientFunctor V).map f)
Tactic: refine strictMap_multiplicativeClosure_le _ _ _ ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
x y : V.HomotopyCategory
f : x.as (r := OneTruncation₂.HoRel₂ V) ⟶ y.as (r := OneTruncation₂.HoRel₂ V)
h : ⊤ ((quotientFunctor V).map f)
⊢ strictMap (multiplicativeClosure (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V))) (quotientFunctor V)
    ((quotientFunctor V).map f)
have rw : strictMap ⊤ (quotientFunctor V) ((quotientFunctor V).map f)
Tactic: rw [Cat.FreeRefl.multiplicativeClosure_morphismPropertyHomMk]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst : W.IsMultiplicative
hW :
  ∀
    {x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))}
    (e : Edge x y), W (homMk e)
⊢ ⊤ ≤ W
have rw : morphismPropertyHomMk V ≤ W
Tactic: rw [← multiplicativeClosure_morphismPropertyHomMk,
      MorphismProperty.multiplicativeClosure_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (hypothesis)
Goal:
V W : Truncated 2
D : Type u_1
inst : Category.{v_1, u_1} D
F G : CategoryTheory.Functor.{u, v_1, u, u_1} V.HomotopyCategory D
φ :
  (x :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
            OneTruncation₂._proof_1))) →
    F.obj (mk x) ⟶ G.obj (mk x)
hφ :
  ∀
    ⦃x y :
      V.obj
        (op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))⦄
    (e : Edge x y), F.map (homMk e) ≫ φ y = φ x ≫ G.map (homMk e)
x x_1 : V.HomotopyCategory
f : x ⟶ x_1
⊢ F.map f ≫ φ (Quotient.as (r := Cat.FreeReflRel (OneTruncation₂ V)) x_1.1) =
    φ (Quotient.as (r := Cat.FreeReflRel (OneTruncation₂ V)) x.1) ≫ G.map f
have this : Eq.{u + 1} (α := MorphismProperty V.HomotopyCategory)
  (MorphismProperty.naturalityProperty.{u, v_1, u, u_1} (D := D) (F₁ := F) (F₂ := G) fun (x : V.HomotopyCategory) ↦
    φ (Quotient.as (r := Cat.FreeReflRel (OneTruncation₂ V)) x.1))
  ⊤
Tactic: have : MorphismProperty.naturalityProperty (fun (x : V.HomotopyCategory) ↦ φ _) = ⊤ :=
      morphismProperty_eq_top (fun e ↦ hφ e)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V W X : Truncated 2
inst :
  Subsingleton.{u + 1}
    (X.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
x y : X.HomotopyCategory
⊢ x = y
have obtain : ∀
  (x :
    X.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))),
  mk x = y
Tactic: obtain ⟨x, rfl⟩ := x.mk_surjective
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V W X : Truncated 2
inst :
  Subsingleton.{u + 1}
    (X.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
y : X.HomotopyCategory
x :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ mk x = y
have obtain : ∀
  (y :
    X.obj
      (op
        (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))),
  mk x = mk y
Tactic: obtain ⟨y, rfl⟩ := y.mk_surjective
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V W X : Truncated 2
inst :
  Subsingleton.{u + 1}
    (X.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
x y :
  X.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
⊢ mk x = mk y
have obtain : mk x = mk x
Tactic: obtain rfl := Subsingleton.elim x y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V W x : Truncated 2
⊢ (mapHomotopyCategory (𝟙 x)).toCatHom = 𝟙 (Cat.of x.HomotopyCategory)
have h : (mapHomotopyCategory (𝟙 x)).toCatHom.toFunctor = Cat.Hom.toFunctor (𝟙 (Cat.of x.HomotopyCategory))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V W X Y Z : Truncated 2
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ (mapHomotopyCategory (x ≫ x_1)).toCatHom = (mapHomotopyCategory x).toCatHom ≫ (mapHomotopyCategory x_1).toCatHom
have h : (mapHomotopyCategory (x ≫ x_1)).toCatHom.toFunctor =
  ((mapHomotopyCategory x).toCatHom ≫ (mapHomotopyCategory x_1).toCatHom).toFunctor
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
x y : OneTruncation₂ (obj (truncation 2) Δ[0])
⊢ x ⟶ y
have obtain : default ⟶ y
Tactic: obtain rfl : x = default := Unique.uniq _ _
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
y : OneTruncation₂ (obj (truncation 2) Δ[0])
⊢ default ⟶ y
have obtain : Quiver.Hom (V := OneTruncation₂ (obj (truncation 2) Δ[0])) default default
Tactic: obtain rfl : y = default := Unique.uniq _ _
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
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 =
    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) ⋯) ⋯
have 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) sorry) sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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
⊢ 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
have 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
Tactic: rw [Set.eq_univ_iff_forall] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
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)
⊢ 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
have 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
Tactic: apply Or.imp _ id (h j)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Λ[n, i] = ⨆ (j : (↑{i}ᶜ : Type)), stdSimplex.face {(↑j : Fin (n + 1))}ᶜ
have 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
Tactic: ext m j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
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
have 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
Tactic: simp [stdSimplex.face_obj, horn, Set.eq_univ_iff_forall]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ HasDimensionLT.{u} Λ[n, i].toSSet n
have rw : ∀ (i_1 : (↑{i}ᶜ : Type)), HasDimensionLT.{u} (Subcomplex.toSSet (X := Δ[n]) (stdSimplex.face {(↑i_1 : Fin (n + 1))}ᶜ)) n
Tactic: rw [horn_eq_iSup, hasDimensionLT_iSup_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≠ j
⊢ stdSimplex.face {i}ᶜ ≤ Λ[n, j]
have rw : LE.le.{u} (α := Δ[n].Subcomplex) (stdSimplex.face {i}ᶜ)
  (⨆ (j_1 : (↑{j}ᶜ : Type)), stdSimplex.face {(↑j_1 : Fin (n + 1))}ᶜ)
Tactic: rw [horn_eq_iSup]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 3)
⊢ Eq (α := Set (Δ[n + 2] _⦋0⦌)) (Λ[n + 2, i].obj (op ⦋0⦌)) ⊤
have 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
Tactic: ext j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (goal)
Goal:
n : ℕ
i : Fin (n + 3)
j : Δ[n + 2] _⦋0⦌
⊢ Membership.mem (γ := Set (Δ[n + 2] _⦋0⦌)) (Λ[n + 2, i].obj (op ⦋0⦌)) j ↔ Membership.mem (γ := Set (Δ[n + 2] _⦋0⦌)) ⊤ j
have h : ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1
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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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
⊢ False
have this : Finset.card (α := Fin (n + 3)) Finset.univ ≤ S.card
Tactic: have := Finset.card_le_card hS.symm.le
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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
⊢ False
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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}
⊢ False
have this₁ : n + 3 ≤ 2
Tactic: have := this.trans Finset.card_le_two
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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}
⊢ ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1
have hS : ¬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
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Horn (hypothesis)
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
⊢ ∃ (i_1 : Fin (n + 2 + 1)), ¬i_1 = i ∧ ∀ (i : Fin 1), ¬(j : (a : Fin 1) → Fin (n + 2 + 1)) i = i_1
have hS₁ : ∃ (x : Fin (n + 3)), x ∉ S
Tactic: rw [Finset.eq_univ_iff_forall, not_forall] at hS
Cleared hypotheses: hS