awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
t : (range (X := f.sigmaHorn j) (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN t
inl :
  ∀ (c' : f.Cell j) (h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₁ f c')),
    Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₁ f c')
⊢ Cell.type₁ f c = t
have inl₁ : ∀ (c' : f.Cell j) (h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₂ f c')),
  Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₂ f c')
Tactic: obtain ⟨c', rfl | rfl⟩ := f.exists_or_of_range_m_N t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
t : (range (X := f.sigmaHorn j) (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN t
⊢ Cell.type₂ f c = t
have inr : ∀ (c' : f.Cell j) (h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₁ f c')),
  Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₂ f c) (Cell.type₁ f c')
Tactic: obtain ⟨c', rfl | rfl⟩ := f.exists_or_of_range_m_N t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
t : (range (X := f.sigmaHorn j) (f.m j)).N
c : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN t
inr :
  ∀ (c' : f.Cell j) (h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₁ f c')),
    Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₂ f c) (Cell.type₁ f c')
⊢ Cell.type₂ f c = t
have inr₁ : ∀ (c' : f.Cell j) (h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₂ f c')),
  Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₂ f c) (Cell.type₂ f c')
Tactic: obtain ⟨c', rfl | rfl⟩ := f.exists_or_of_range_m_N t
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₁ f c')
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₁ f c')
have h₁ : Eq (α := { x : A.N // x ∈ P.I }) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
  ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s : (↑P.I : Type u))
Tactic: simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₁ f c) = f.mapN (Cell.type₂ f c')
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₂ f c')
have h₁ : (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) = (↑c'.s : A.N)
Tactic: simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₁ f c')
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₂ f c) (Cell.type₁ f c')
have h₁ : (↑c.s : A.N) = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s) : A.N)
Tactic: simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : f.mapN (Cell.type₂ f c) = f.mapN (Cell.type₂ f c')
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₂ f c) (Cell.type₂ f c')
have h₁ : c.s = c'.s
Tactic: simp only [mapN_type₁, mapN_type₂, ← Subcomplex.N.eq_iff_sMk_eq,
      ← Subtype.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c c' : f.Cell j
h :
  Eq (α := { x : A.N // x ∈ P.I }) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
    ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s : (↑P.I : Type u))
⊢ c = c'
have s : c.s = c'.s
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c c' : f.Cell j
h :
  Eq (α := { x : A.N // x ∈ P.I }) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
    ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c'.s : (↑P.I : Type u))
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₁ f c')
have inl : ∀
  (h :
    Eq (α := { x : A.N // x ∈ P.I }) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))
      ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s : (↑P.I : Type u))),
  Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₁ f c) (Cell.type₁ f c)
Tactic: obtain rfl : c = c' := by ext : 1; exact P.p.injective h
Cleared hypotheses: c', h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
c c' : f.Cell j
h : c.s = c'.s
⊢ Eq (α := (range (X := f.sigmaHorn j) (f.m j)).N) (Cell.type₂ f c) (Cell.type₂ f c')
have inr : c = c'
Tactic: congr
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x : SimplexCategoryᵒᵖ
d : ℕ
⊢ IsColimit (F := span (X := f.sigmaHorn j) (f.t j) (f.m j) ⋙ CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌)
    (Functor.mapCocone (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌)
      (PushoutCocone.mk (W := (f.filtration (Order.succ j)).toSSet) (homOfLE ⋯) (f.b j) ⋯))
have refine : IsPushout (Z := Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaHorn j)) (P :=
  Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration (Order.succ j)).toSSet)
  (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.t j))
  (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.m j))
  (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (homOfLE sorry))
  (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.b j))
Tactic: refine (isColimitMapCoconePushoutCoconeEquiv _ _).symm
      (IsPushout.isColimit ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : OrderBot ι
inst_4 : NoMaxOrder ι
inst_5 : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
⊢ IsLUB
    (Set.range (ι := (↑(Set.Iio m) : Type v))
      (Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type v)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : ι) ↦ x1 < x2) (Set.principalSegIio m)) :
              (a : (↑(Set.Iio m) : Type v)) → ι))
            ⋯ ⋙
          ⋯.functor)))
    (Cocone.pt (J := (↑(Set.Iio m) : Type v)) (F :=
      Monotone.functor (f :=
          (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type v)) ↦ x1 < x2) (s := fun (x1 x2 : ι) ↦
                x1 < x2) (Set.principalSegIio m)) :
            (a : (↑(Set.Iio m) : Type v)) → ι))
          ⋯ ⋙
        ⋯.functor)
      (PrincipalSeg.cocone (Set.principalSegIio m) ⋯.functor))
have dsimp : IsLUB
  (Set.range (ι := (↑(Set.Iio m) : Type v))
    (Functor.obj
      (Monotone.functor (f :=
          (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type v)) ↦ x1 < x2) (s := fun (x1 x2 : ι) ↦
                x1 < x2) (Set.principalSegIio m)) :
            (a : (↑(Set.Iio m) : Type v)) → ι))
          sorry ⋙
        sorry.functor)))
  (f.filtration m)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : OrderBot ι
inst_4 : NoMaxOrder ι
inst_5 : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
⊢ IsLUB
    (Set.range (ι := (↑(Set.Iio m) : Type v))
      (Functor.obj
        (Monotone.functor (f :=
            (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type v)) ↦ x1 < x2) (s :=
                  fun (x1 x2 : ι) ↦ x1 < x2) (Set.principalSegIio m)) :
              (a : (↑(Set.Iio m) : Type v)) → ι))
            ⋯ ⋙
          ⋯.functor)))
    (f.filtration m)
have rw : IsLUB
  (Set.range (ι := (↑(Set.Iio m) : Type v))
    (Functor.obj
      (Monotone.functor (f :=
          (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio m) : Type v)) ↦ x1 < x2) (s := fun (x1 x2 : ι) ↦
                x1 < x2) (Set.principalSegIio m)) :
            (a : (↑(Set.Iio m) : Type v)) → ι))
          sorry ⋙
        sorry.functor)))
  (⨆ (i : (↑(Set.Iio m) : Type v)), f.filtration (↑i : ι))
Tactic: rw [← f.iSup_filtration_iio m hm]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
inst_2 : SuccOrder ι
inst_3 : OrderBot ι
inst_4 : NoMaxOrder ι
inst_5 : WellFoundedLT ι
⊢ IsLUB (Set.range ⋯.functor.obj) ⊤
have rw : IsLUB (Set.range sorry.functor.obj) (⨆ (i : ι), f.filtration i)
Tactic: rw [← f.iSup_filtration]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Basic (goal)
Goal:
X Y : SSet
y : Y _⦋0⦌
x x_1 : SimplexCategoryᵒᵖ
x_2 : x ⟶ x_1
⊢ (X.map x_2 ≫
      ↾fun (x : X.obj x_1) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) → (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x_1))))
          y) =
    (↾fun (x_3 : X.obj x) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0))) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) → (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x))))
          y) ≫
      Y.map x_2
have h : ∀ (x_3 : X.obj x),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map x_2 ≫
          ↾fun (x : X.obj x_1) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) →
                  (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x_1))))
              y))
      x_3 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_4 : X.obj x) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) → (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x))))
              y) ≫
          Y.map x_2))
      x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Basic (goal)
Goal:
X Y : SSet
y : Y _⦋0⦌
x x_1 : SimplexCategoryᵒᵖ
x_2 : x ⟶ x_1
x_3 : X.obj x
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map x_2 ≫
          ↾fun (x : X.obj x_1) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) →
                  (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x_1))))
              y))
      x_3 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x_4 : X.obj x) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0))) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋0⦌)) → (fun (X : Type u) ↦ X) (Y.obj (Opposite.op (Opposite.unop x))))
              y) ≫
          Y.map x_2))
      x_3
have h : Eq (α := Y.obj x_1)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
        (a : Y _⦋0⦌) → Y.obj x_1)
      y :
    Y.obj x_1)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map x_2) : (a : Y.obj x) → Y.obj x_1)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0))) :
            (a : Y _⦋0⦌) → Y.obj x)
          y :
        Y.obj x) :
    Y.obj x_1)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Basic (goal)
Goal:
X Y : SSet
y : Y _⦋0⦌
x x_1 : SimplexCategoryᵒᵖ
x_2 : x ⟶ x_1
x_3 : X.obj x
⊢ Eq (α := Y.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
          (a : Y _⦋0⦌) → Y.obj x_1)
        y :
      Y.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map x_2) : (a : Y.obj x) → Y.obj x_1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0))) :
              (a : Y _⦋0⦌) → Y.obj x)
            y :
          Y.obj x) :
      Y.obj x_1)
have h : Eq (α := Y.obj x_1)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x_1).const ⦋0⦌ 0))) :
        (a : Y _⦋0⦌) → Y.obj x_1)
      y :
    Y.obj x_1)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (Quiver.Hom.op ((Opposite.unop x).const ⦋0⦌ 0) ≫ x_2)) :
        (a : Y _⦋0⦌) → Y.obj x_1)
      y :
    Y.obj x_1)
Tactic: rw [← CategoryTheory.comp_apply, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Basic (goal)
Goal:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 2)
x : S _⦋n + 1⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) :
      (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ T i) :
          (a : (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n + 1⦌)) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
have change : Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ S i ≫ f.app (op ⦋n⦌)) :
        (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
      x :
    (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n + 1⦌) ≫ SimplicialObject.δ T i) :
        (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
      x :
    (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
Tactic: change (S.δ i ≫ f.app (op ⦋n⦌)) x = (f.app (op ⦋n + 1⦌) ≫ T.δ i) x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Basic (goal)
Goal:
S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
⊢ Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n + 1⦌)) :
          (a : (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌))
            x :
          (fun (X : Type u_1) ↦ X) (S _⦋n + 1⦌)) :
      (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ T i) :
          (a : (fun (X : Type u_1) ↦ X) (T _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌)) :
              (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n⦌))
            x :
          (fun (X : Type u_1) ↦ X) (T _⦋n⦌)) :
      (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
have change : Eq (α := (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ S i ≫ f.app (op ⦋n + 1⦌)) :
        (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
      x :
    (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op ⦋n⦌) ≫ SimplicialObject.σ T i) :
        (a : (fun (X : Type u_1) ↦ X) (S _⦋n⦌)) → (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
      x :
    (fun (X : Type u_1) ↦ X) (T _⦋n + 1⦌))
Tactic: change (S.σ i ≫ f.app (op ⦋n + 1⦌)) x = (f.app (op ⦋n⦌) ≫ T.σ i) x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
⊢ ∂Δ[n] = ⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ
have obj : ∀ (x : SimplexCategoryᵒᵖ) (x_1 : Δ[n].obj x),
  x_1 ∈ ∂Δ[n].obj x ↔
    Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ) x) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
x_1 : Δ[n].obj x
⊢ x_1 ∈ ∂Δ[n].obj x ↔
    Membership.mem (γ := Set (Δ[n].obj x)) (Subfunctor.obj (⨆ (i : Fin (n + 1)), stdSimplex.face {i}ᶜ) x) x_1
have obj : (∃ (x_2 : Fin (n + 1)),
    ∀ (x_3 : Fin ((unop x).len + 1)),
      ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) ↔
  ∃ (i : Fin (n + 1)),
    ∀ (x_2 : Fin ((unop x).len + 1)),
      ¬(SimplexCategory.Hom.toOrderHom
                (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
              (a : Fin ((unop x).len + 1)) → Fin (n + 1))
            x_2 =
          i
Tactic: simp [stdSimplex.face_obj, boundary, Function.Surjective]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
x_1 : Δ[n].obj x
⊢ (∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) ↔
    ∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i
have obj : (∃ (x_2 : Fin (n + 1)),
    ∀ (x_3 : Fin ((unop x).len + 1)),
      ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) →
  ∃ (i : Fin (n + 1)),
    ∀ (x_2 : Fin ((unop x).len + 1)),
      ¬(SimplexCategory.Hom.toOrderHom
                (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
              (a : Fin ((unop x).len + 1)) → Fin (n + 1))
            x_2 =
          i
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
x : SimplexCategoryᵒᵖ
x_1 : Δ[n].obj x
obj :
  (∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) →
    ∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i
⊢ (∃ (x_2 : Fin (n + 1)),
      ∀ (x_3 : Fin ((unop x).len + 1)),
        ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2) ↔
    ∃ (i : Fin (n + 1)),
      ∀ (x_2 : Fin ((unop x).len + 1)),
        ¬(SimplexCategory.Hom.toOrderHom
                  (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
                (a : Fin ((unop x).len + 1)) → Fin (n + 1))
              x_2 =
            i
have obj₁ : (∃ (i : Fin (n + 1)),
    ∀ (x_2 : Fin ((unop x).len + 1)),
      ¬(SimplexCategory.Hom.toOrderHom
                (((stdSimplex.objEquiv : Δ[n].obj x ≃ (unop x ⟶ ⦋n⦌)) : (a : Δ[n].obj x) → unop x ⟶ ⦋n⦌) x_1) :
              (a : Fin ((unop x).len + 1)) → Fin (n + 1))
            x_2 =
          i) →
  ∃ (x_2 : Fin (n + 1)),
    ∀ (x_3 : Fin ((unop x).len + 1)),
      ¬(stdSimplex.asOrderHom x_1 : (a : Fin ((unop x).len + 1)) → Fin (n + 1)) x_3 = x_2
Tactic: tauto