awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
left : x.Nonempty
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} b
have right : ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} b
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
⊢ x.Nonempty
have left : Finset.Nonempty (α := ι) {v}
Tactic: rw [hv]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (hypothesis)
Goal:
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
⊢ Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} t
have x₁ : t = ∅ ∨ t = {v}
Tactic: cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
            | inl h => exact (ht.ne_empty h).elim
            | inr h => exact ⟨v, h⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} b
have left : x.Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
left : x.Nonempty
⊢ x.Nonempty ∧
    ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} b
have right : ∀ ⦃b : Finset ι⦄, b ≤ x → b.Nonempty → Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} b
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
⊢ x.Nonempty
have left : Finset.Nonempty (α := ι) {v}
Tactic: rw [hv]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (hypothesis)
Goal:
ι : Type u_1
x : Finset ι
h : Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} x
v : ι
hv : x = {v}
t : Finset ι
hts : t ≤ x
ht : t.Nonempty
⊢ Membership.mem (γ := Set (Finset ι)) {s : Finset ι | ∃ (v : ι), s = {v}} t
have x₁ : t = ∅ ∨ t = {v}
Tactic: cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
          | inl h => exact (ht.ne_empty h).elim
          | inr h => exact ⟨v, h⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
⊢ IsLUB x (sSup x)
have left : sSup x ∈ upperBounds x
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
left : sSup x ∈ upperBounds x
⊢ IsLUB x (sSup x)
have right : sSup x ∈ lowerBounds (upperBounds x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
K : AbstractSimplicialComplex ι
hK : K ∈ x
⊢ K ≤ sSup x
have left : ∀ ⦃a : Finset ι⦄,
  Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) K) a →
    Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) (sSup x)) a
Tactic: _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
⊢ sSup x ≤ L
have right : ∀ ⦃a : Finset ι⦄,
  Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) (sSup x)) a →
    Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
Tactic: _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (hypothesis)
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
ht : Membership.mem (γ := Set (Finset ι)) (⋃ K ∈ x, K.faces) a
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
have ht₁ : ∃ (i : AbstractSimplicialComplex ι) (_ : i ∈ x), a ∈ i.faces
Tactic: simp only [Set.mem_iUnion] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
ht : ∃ (i : AbstractSimplicialComplex ι) (_ : i ∈ x), a ∈ i.faces
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
have right : ∀ (K : AbstractSimplicialComplex ι) (hK : K ∈ x) (htK : a ∈ K.faces),
  Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
Tactic: obtain ⟨K, hK, htK⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
ht : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} a
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
have right : ∀ (v : ι) (hv : a = {v}), Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
Tactic: obtain ⟨v, hv⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
ht : Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) (sSup x)) a
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
have right : ∀ (ht : Membership.mem (γ := Set (Finset ι)) (⋃ K ∈ x, K.faces) a),
  Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
Tactic: cases ht with
      | inl ht =>
        simp only [Set.mem_iUnion] at ht
        obtain ⟨K, hK, htK⟩ := ht
        exact hL hK htK
      | inr ht =>
        obtain ⟨v, hv⟩ := ht
        exact hv ▸ L.singleton_mem v
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
x : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x
a : Finset ι
ht : Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) (sSup x)) a
right :
  ∀ (ht : Membership.mem (γ := Set (Finset ι)) (⋃ K ∈ x, K.faces) a),
    Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
have right₁ : ∀ (ht : Membership.mem (γ := Set (Finset ι)) {t : Finset ι | ∃ (v : ι), t = {v}} a),
  Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) L) a
Tactic: cases ht with
      | inl ht =>
        simp only [Set.mem_iUnion] at ht
        obtain ⟨K, hK, htK⟩ := ht
        exact hL hK htK
      | inr ht =>
        obtain ⟨v, hv⟩ := ht
        exact hv ▸ L.singleton_mem v
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialComplex.Basic (goal)
Goal:
ι : Type u_1
K : AbstractSimplicialComplex ι
x : Finset ι
ht : Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) ⊥) x
⊢ Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) K) x
have obtain : ∀ (v : ι) (hv : x = {v}), Membership.mem (γ := Set (Finset ι)) ((fun (K : AbstractSimplicialComplex ι) ↦ K.faces) K) x
Tactic: obtain ⟨v, hv⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
J : Type u_1
inst : LinearOrder J
i j : SimplicialThickening J
x y : i ⟶ j
h : ∀ (t : J), t ∈ x.I ↔ t ∈ y.I
⊢ x = y
have I : x.I = y.I
Tactic: apply Path.ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
J : Type u_1
inst : LinearOrder J
X Y : SimplicialThickening J
f : X ⟶ Y
⊢ 𝟙 X ≫ f = f
have h : ∀ (t : J), t ∈ (𝟙 X ≫ f).I ↔ t ∈ f.I
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
J : Type u_1
inst : LinearOrder J
X Y : SimplicialThickening J
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f
have h : ∀ (t : J), t ∈ (f ≫ 𝟙 Y).I ↔ t ∈ f.I
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
J K : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
f : J →o K
i : SimplicialThickening J
⊢ eId SSet i ≫ nerveMap (functorMap f i i) = eId SSet { as := (f : (a : J) → K) i.as }
have w : ∀ (n : SimplexCategoryᵒᵖ) (x : (𝟙_ SSet) (𝒞 := Functor.category).obj n),
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((eId SSet i ≫ nerveMap (functorMap f i i)).app n)).toFun x =
    TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (eId SSet { as := (f : (a : J) → K) i.as }) n))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
J K : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
f : J →o K
i j k : SimplicialThickening J
⊢ eComp SSet i j k ≫ nerveMap (functorMap f i k) =
    (nerveMap (functorMap f i j) ⊗ₘ nerveMap (functorMap f j k)) ≫
      eComp SSet { as := (f : (a : J) → K) i.as } { as := (f : (a : J) → K) j.as } { as := (f : (a : J) → K) k.as }
have w : ∀ (n : SimplexCategoryᵒᵖ)
  (x :
    Functor.obj
      (tensorObj (𝒞 := Functor.category) (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j)
        (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ j k))
      n),
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((eComp SSet i j k ≫ nerveMap (functorMap f i k)).app n)).toFun x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((nerveMap (functorMap f i j) ⊗ₘ nerveMap (functorMap f j k)) ≫
            eComp SSet { as := (f : (a : J) → K) i.as : SimplicialThickening K }
              { as := (f : (a : J) → K) j.as : SimplicialThickening K }
              { as := (f : (a : J) → K) k.as : SimplicialThickening K })
          n))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
J : Type u
inst : LinearOrder J
⊢ Eq (α := EnrichedFunctor SSet (SimplicialThickening J) (SimplicialThickening J)) (functor OrderHom.id)
    (EnrichedFunctor.id SSet (SimplicialThickening J))
have refine : ∀ (i j : SimplicialThickening J),
  Eq (α :=
    Quiver.Hom (V := SSet) (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j)
      (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _
        (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) i)
        (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) j)))
    (CategoryStruct.comp (Y :=
      @Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ (EnrichedFunctor.obj (functor OrderHom.id) i)
        (EnrichedFunctor.obj (functor OrderHom.id) j))
      (EnrichedFunctor.map (functor OrderHom.id) i j) (eqToHom sorry))
    (EnrichedFunctor.map (EnrichedFunctor.id SSet (SimplicialThickening J)) i j)
Tactic: refine EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
J : Type u
inst : LinearOrder J
i j : SimplicialThickening J
⊢ Eq (α :=
    Quiver.Hom (V := SSet) (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j)
      (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _
        (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) i)
        (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) j)))
    (CategoryStruct.comp (Y :=
      @Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ (EnrichedFunctor.obj (functor OrderHom.id) i)
        (EnrichedFunctor.obj (functor OrderHom.id) j))
      (EnrichedFunctor.map (functor OrderHom.id) i j) (eqToHom ⋯))
    (EnrichedFunctor.map (EnrichedFunctor.id SSet (SimplicialThickening J)) i j)
have w : ∀ (n : SimplexCategoryᵒᵖ) (x : Functor.obj (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j) n),
  Eq (α :=
    Functor.obj
      (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _
        (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) i)
        (EnrichedFunctor.obj (EnrichedFunctor.id SSet (SimplicialThickening J)) j))
      n)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (CategoryStruct.comp (Y :=
            @Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ (EnrichedFunctor.obj (functor OrderHom.id) i)
              (EnrichedFunctor.obj (functor OrderHom.id) j))
            (EnrichedFunctor.map (functor OrderHom.id) i j) (eqToHom sorry))
          n))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app (EnrichedFunctor.map (EnrichedFunctor.id SSet (SimplicialThickening J)) i j) n))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
J K L : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
inst_2 : LinearOrder L
f : J →o K
g : K →o L
⊢ functor (g.comp f) = EnrichedFunctor.comp SSet (functor f) (functor g)
have refine : ∀ (i j : SimplicialThickening J),
  (functor (g.comp f)).map i j ≫ eqToHom sorry = (EnrichedFunctor.comp SSet (functor f) (functor g)).map i j
Tactic: refine EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
J K L : Type u
inst : LinearOrder J
inst_1 : LinearOrder K
inst_2 : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
⊢ (functor (g.comp f)).map i j ≫ eqToHom ⋯ = (EnrichedFunctor.comp SSet (functor f) (functor g)).map i j
have w : ∀ (n : SimplexCategoryᵒᵖ) (x : Functor.obj (@Hom _ Functor.category Monoidal.functorCategoryMonoidal _ _ i j) n),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app ((functor (g.comp f)).map i j ≫ eqToHom sorry) n)) x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((EnrichedFunctor.comp SSet (functor f) (functor g)).map i j).app n)).toFun
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
i : SimplexCategoryᵒᵖ
⊢ ↾EnrichedFunctor.comp SSet
        (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (Quiver.Hom.unop (𝟙 i))).uliftMap) =
    𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C)
have h : ∀ (x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet
            (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (Quiver.Hom.unop (𝟙 i))).uliftMap)))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
i : SimplexCategoryᵒᵖ
x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet
            (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (Quiver.Hom.unop (𝟙 i))).uliftMap)))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x
have h : EnrichedFunctor.comp SSet (SimplicialThickening.functor OrderHom.id) x =
  (ConcreteCategory.hom (FC := TypeCat.Fun)
        (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
    x
Tactic: change EnrichedFunctor.comp SSet (SimplicialThickening.functor OrderHom.id) _ = _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
i : SimplexCategoryᵒᵖ
x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C
⊢ EnrichedFunctor.comp SSet (SimplicialThickening.functor OrderHom.id) x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
      x
have h : EnrichedFunctor.comp SSet
    (EnrichedFunctor.id SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1))))) x =
  (ConcreteCategory.hom (FC := TypeCat.Fun)
        (𝟙 (EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop i).len + 1)))) C))).toFun
    x
Tactic: rw [SimplicialThickening.functor_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
X Y Z : SimplexCategoryᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X).len + 1)))) C ⟶
      EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop Z).len + 1)))) C)
    (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (f ≫ g).unop).uliftMap))
    (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
      ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap))
have h : ∀ (x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X).len + 1)))) C),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet
            (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (f ≫ g).unop).uliftMap)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
          ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
X Y Z : SimplexCategoryᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X).len + 1)))) C
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet
            (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom (f ≫ g).unop).uliftMap)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
          ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)))
      x
have h : EnrichedFunctor.comp SSet
    (SimplicialThickening.functor
      ((SimplexCategory.Hom.toOrderHom f.unop).uliftMap.comp (SimplexCategory.Hom.toOrderHom g.unop).uliftMap))
    x =
  TypeCat.Fun.toFun
    (ConcreteCategory.hom (FC := TypeCat.Fun)
      (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
        ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)))
    x
Tactic: change EnrichedFunctor.comp SSet (SimplicialThickening.functor
      (f.unop.toOrderHom.uliftMap.comp g.unop.toOrderHom.uliftMap)) _ = _
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialNerve (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : SimplicialCategory.{v, u} C
X Y Z : SimplexCategoryᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
x : EnrichedFunctor SSet (SimplicialThickening (ULift.{v, 0} (Fin ((Opposite.unop X).len + 1)))) C
⊢ EnrichedFunctor.comp SSet
      (SimplicialThickening.functor
        ((SimplexCategory.Hom.toOrderHom f.unop).uliftMap.comp (SimplexCategory.Hom.toOrderHom g.unop).uliftMap))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
          ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)))
      x
have h : EnrichedFunctor.comp SSet
    (EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)
      (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap))
    x =
  TypeCat.Fun.toFun
    (ConcreteCategory.hom (FC := TypeCat.Fun)
      (↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom f.unop).uliftMap) ≫
        ↾EnrichedFunctor.comp SSet (SimplicialThickening.functor (SimplexCategory.Hom.toOrderHom g.unop).uliftMap)))
    x
Tactic: rw [SimplicialThickening.functor_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.δ j.succ ≫ X.δ i = X.δ i.castSucc ≫ X.δ j
have dsimp : X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ i).op =
  X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ j).op
Tactic: dsimp [δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.δ j ≫ X.δ i = X.δ i.castSucc ≫ X.δ (j.pred ⋯)
have dsimp : X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ i).op =
  X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ (j.pred sorry)).op
Tactic: dsimp [δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ X.δ j.succ ≫ X.δ (i.castLT ⋯) = X.δ i ≫ X.δ j
have dsimp : X.map (SimplexCategory.δ j.succ).op ≫ X.map (SimplexCategory.δ (i.castLT sorry)).op =
  X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.δ j).op
Tactic: dsimp [δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i
have dsimp : X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ i).op =
  X.map (SimplexCategory.δ i.succ).op ≫ X.map (SimplexCategory.δ i).op
Tactic: dsimp [δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : SimplicialObject.{v, u} C
n : ℕ
j : Fin (n + 3)
i : Fin (n + 2)
H : j = i.castSucc
⊢ X.δ j ≫ X.δ i = X.δ i.succ ≫ X.δ i
have subst : X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i
Tactic: subst H
Cleared hypotheses: j, H