awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n)
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
    (stdSimplex.face {i}ᶜ)
have rw : LE.le.{u} (α := Δ[n + 1].Subcomplex)
  (Subcomplex.ofSimplex (n := n)
    ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
  (Subcomplex.ofSimplex (n := n)
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i)))
Tactic: rw [stdSimplex.face_singleton_compl, yonedaEquiv_map]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
i : Fin (n + 2)
rw :
  LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n)
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
    (Subcomplex.ofSimplex (n := n)
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i)))
⊢ LE.le.{u} (α := Δ[n + 1].Subcomplex)
    (Subcomplex.ofSimplex (n := n)
      ((yonedaEquiv : (a : Δ[n] ⟶ Δ[n + 1]) → Δ[n + 1] _⦋n⦌) (stdSimplex.map (SimplexCategory.δ i))))
    (stdSimplex.face {i}ᶜ)
have rw₁ : LE.le.{u} (α := Δ[n + 1].Subcomplex)
  (Subcomplex.ofSimplex (n := n)
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i)))
  (Subcomplex.ofSimplex (n := n)
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i)))
Tactic: rw [stdSimplex.face_singleton_compl, yonedaEquiv_map]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ (stdSimplex.faceSingletonComplIso i).inv ≫ ι i = faceι i
have rw : ι i = (stdSimplex.faceSingletonComplIso i).hom ≫ faceι i
Tactic: rw [← cancel_epi (stdSimplex.faceSingletonComplIso i).hom, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ Mono (ι i)
have rw : Mono (faceι i)
Tactic: rw [← mono_comp_iff_of_isIso (stdSimplex.faceSingletonComplIso i).inv,
    faceSingletonComplIso_inv_ι]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
X : SSet
f g : Subcomplex.toSSet (X := Δ[n + 1]) ∂Δ[n + 1] ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
⊢ f = g
have w : ∀ (m : SimplexCategoryᵒᵖ) (x : Δ[n + 1].obj m)
  (hx : Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x) x hx) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x) x hx)
Tactic: ext m ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (hypothesis)
Goal:
n : ℕ
X : SSet
f g : Subcomplex.toSSet (X := Δ[n + 1]) ∂Δ[n + 1] ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
m : SimplexCategoryᵒᵖ
x : Δ[n + 1].obj m
hx : Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x) x hx) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x) x hx)
have hx₁ : ∃ (i : Fin (n + 1 + 1)) (f : unop m ⟶ ⦋n⦌),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map f.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
      ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) : Δ[n + 1] _⦋n⦌) =
    x
Tactic: simp only [boundary_eq_iSup, stdSimplex.face_singleton_compl, Subfunctor.iSup_obj,
    Set.mem_iUnion, Subcomplex.mem_ofSimplex_obj_iff, op_unop] at hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
n : ℕ
X : SSet
f g : Subcomplex.toSSet (X := Δ[n + 1]) ∂Δ[n + 1] ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
m : SimplexCategoryᵒᵖ
x : Δ[n + 1].obj m
hx_1 : Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x
hx :
  ∃ (i : Fin (n + 1 + 1)) (f : unop m ⟶ ⦋n⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map f.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
        ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) : Δ[n + 1] _⦋n⦌) =
      x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x) x hx_1) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x) x hx_1)
have w : ∀ (i : Fin (n + 1 + 1)) (y : unop m ⟶ ⦋n⦌)
  (hx :
    Membership.mem (α := Δ[n + 1].obj m) (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) :
            Δ[n + 1] _⦋n⦌) :
        Δ[n + 1].obj m)),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) :
            Δ[n + 1] _⦋n⦌))
        hx) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app m)).toFun
      (Subtype.mk (p := fun (x : Δ[n + 1].obj m) ↦
        Membership.mem (γ := Set (Δ[n + 1].obj m)) (Subfunctor.obj ∂Δ[n + 1] m) x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1].map y.op) : (a : Δ[n + 1] _⦋n⦌) → Δ[n + 1].obj m)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n⦌) (SimplexCategory.δ i) :
            Δ[n + 1] _⦋n⦌))
        hx)
Tactic: obtain ⟨i, ⟨y, rfl⟩⟩ := hx
Cleared hypotheses: x, hx_1, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Boundary (goal)
Goal:
X : SSet
f g : Subcomplex.toSSet (X := Δ[0]) ∂Δ[0] ⟶ X
⊢ f = g
have w : ∀ (n : SimplexCategoryᵒᵖ) (x : Δ[0].obj n) (hx : Membership.mem (γ := Set (Δ[0].obj n)) (Subfunctor.obj ∂Δ[0] n) x),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app n)).toFun
      (Subtype.mk (p := fun (x : Δ[0].obj n) ↦ Membership.mem (γ := Set (Δ[0].obj n)) (Subfunctor.obj ∂Δ[0] n) x) x
        hx) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app n)).toFun
      (Subtype.mk (p := fun (x : Δ[0].obj n) ↦ Membership.mem (γ := Set (Δ[0].obj n)) (Subfunctor.obj ∂Δ[0] n) x) x hx)
Tactic: ext _ ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
⊢ J Λ[n, i].ι
have zero : ∀ [NeZero (R := ℕ) 0] (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), J Λ[0, i].ι
Tactic: obtain _ | n := n
Cleared hypotheses: n, inst, i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
zero : ∀ [NeZero (R := ℕ) 0] (i : Fin (HAdd.hAdd (α := ℕ) 0 1)), J Λ[0, i].ι
⊢ J Λ[n, i].ι
have succ : ∀ (n : ℕ) [NeZero (n + 1)] (i : Fin (n + 1 + 1)), J Λ[n + 1, i].ι
Tactic: obtain _ | n := n
Cleared hypotheses: n, inst, i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations (goal)
Goal:
n : ℕ
inst : NeZero (n + 1)
i : Fin (n + 1 + 1)
⊢ J Λ[n + 1, i].ι
have succ : ∃ (i_1 : ℕ),
  ofHoms (X := fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].toSSet) (Y := fun (i : Fin (i_1 + 2)) ↦ Δ[i_1 + 1])
    (fun (i : Fin (i_1 + 2)) ↦ Λ[i_1 + 1, i].ι) Λ[n + 1, i].ι
Tactic: simp only [J, iSup_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations (hypothesis)
Goal:
X Y : SSet
f : X ⟶ Y
h : J f
⊢ monomorphisms SSet f
have h₁ : ∃ (i : ℕ),
  ofHoms (X := fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].toSSet) (Y := fun (i_1 : Fin (i + 2)) ↦ Δ[i + 1])
    (fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].ι) f
Tactic: simp only [J, iSup_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations (goal)
Goal:
X Y : SSet
f : X ⟶ Y
h :
  ∃ (i : ℕ),
    ofHoms (X := fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].toSSet) (Y := fun (i_1 : Fin (i + 2)) ↦ Δ[i + 1])
      (fun (i_1 : Fin (i + 2)) ↦ Λ[i + 1, i_1].ι) f
⊢ monomorphisms SSet f
have obtain : ∀ (n : ℕ) ⦃X Y : SSet.{u}⦄ (i : Fin (n + 2)), monomorphisms SSet Λ[n + 1, i].ι
Tactic: obtain ⟨n, ⟨i⟩⟩ := h
Cleared hypotheses: X, Y, f, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations (goal)
Goal:
X Y : SSet
f : X ⟶ Y
⊢ Cofibration f ↔ Mono f
have rw : cofibrations SSet f ↔ Mono f
Tactic: rw [HomotopicalAlgebra.cofibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations (goal)
Goal:
X Y : SSet
f : X ⟶ Y
⊢ Fibration f ↔ J.rlp f
have rw : fibrations SSet f ↔ J.rlp f
Tactic: rw [HomotopicalAlgebra.fibration_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations (goal)
Goal:
X Y : SSet
f : X ⟶ Y
hf : Fibration f
n : ℕ
i : Fin (n + 2)
⊢ HasLiftingProperty Λ[n + 1, i].ι f
have rw : ∀ (hf : J.rlp f) {n : ℕ} (i : Fin (n + 2)), HasLiftingProperty Λ[n + 1, i].ι f
Tactic: rw [fibration_iff] at hf
Cleared hypotheses: hf, n, i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations (hypothesis)
Goal:
X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
Y : SSet
p : X ⟶ Y
inst : Fibration p
b : Δ[n + 1] ⟶ Y
comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ p = stdSimplex.δ j ≫ b
⊢ ∃ (φ : Δ[n + 1] ⟶ X), (∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj) ∧ φ ≫ p = b
have sq : CommSq hf.desc Λ[n + 1, i].ι p b
Tactic: have sq : CommSq hf.desc Λ[n + 1, i].ι p b :=
    ⟨horn.hom_ext' (fun j hj ↦ by simpa using comm j hj)⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
Goal:
X Y : Truncated 2
x : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
f : X ⟶ Y
⊢ (id x).map f =
    id
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app
              (Opposite.op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) →
            (fun (X : Type u) ↦ X) (Y.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })))
        x)
have edge : ((id x).map f).edge =
  edge (x₀ :=
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f.app
            (Opposite.op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
        (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) →
          (fun (X : Type u) ↦ X) (Y.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })))
      x)
    (id
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app
              (Opposite.op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
          (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) →
            (fun (X : Type u) ↦ X) (Y.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })))
        x))
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
Goal:
X Y : Truncated 2
inst :
  Subsingleton.{u + 1}
    (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))
x y : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
f g : Edge x y
⊢ f = g
have edge : f.edge = g.edge
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
⊢ ∃ (x₀ :
    X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    (x₁ :
    X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    (x₂ :
    X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) (e₀₂ : Edge x₀ x₂) (h : e₀₁.CompStruct e₁₂ e₀₂), h.simplex = s
have refine_1 : Eq (α :=
  (fun (X : Type u) ↦ X)
    (X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 Edge._proof_1 _proof_3).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0 + 1⦌, property := _proof_3 }))) →
          (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 2 Edge._proof_2 _proof_2).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 }))) →
              (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })))
          s :
        (fun (X : Type u) ↦ X)
          (X.obj
            (Opposite.op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ Edge._proof_2)))) :
    (fun (X : Type u) ↦ X)
      (X.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) sorry sorry).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := sorry })))
      s :
    (fun (X : Type u) ↦ X)
      (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ sorry))))
Tactic: refine ⟨X.map (Hom.tr (SimplexCategory.const _ _ 0)).op s,
    X.map (Hom.tr (SimplexCategory.const _ _ 1)).op s,
    X.map (Hom.tr (SimplexCategory.const _ _ 2)).op s,
    .mk _ ?_ ?_, .mk _ ?_ ?_, .mk _ ?_ ?_, .mk s rfl rfl rfl, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (X.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 Edge._proof_1 _proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0 + 1⦌, property := _proof_3 }))) →
            (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 2 Edge._proof_2 _proof_2).op) :
              (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 }))) →
                (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := Edge._proof_2 })))
            s :
          (fun (X : Type u) ↦ X)
            (X.obj
              (Opposite.op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ Edge._proof_2)))) :
      (fun (X : Type u) ↦ X)
        (X.obj
          (Opposite.op
            (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op) :
          (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := ⋯ })))
        s :
      (fun (X : Type u) ↦ X)
        (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))))
have refine_1 : Eq (α :=
  (fun (X : Type u) ↦ X)
    (X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2).op) :
        (a : X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })) →
          X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 }))
      s :
    X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) sorry sorry).op) :
        (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := sorry }))) →
          (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := sorry })))
      s :
    (fun (X : Type u) ↦ X)
      (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ sorry))))
Tactic: rw [← Functor.map_comp_apply, ← op_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (X.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2).op) :
          (a : X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })) →
            X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 }))
        s :
      X.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op) :
          (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := ⋯ }))) →
            (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := ⋯ })))
        s :
      (fun (X : Type u) ↦ X)
        (X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))))
have refine_1 : Eq (α :=
  (x :
      X.obj
        (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))) →
    X.obj
      (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2).op)) :
    (a : X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })) →
      X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 }))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) sorry sorry).op)) :
    (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := sorry }))) →
      (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := sorry })))
Tactic: apply congr_fun
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated (goal)
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))
⊢ Eq (α :=
    (x :
        X.obj
          (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_1))) →
      X.obj
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2).op)) :
      (a : X.obj (Opposite.op { obj := ⦋1 + 1⦌, property := _proof_2 })) →
        X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 }))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) :
      (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋2⦌, property := ⋯ }))) →
        (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := ⋯ })))
have refine_1 : δ₂ 1 Edge._proof_1 _proof_3 ≫ δ₂ 2 Edge._proof_2 _proof_2 = Hom.tr (⦋0⦌.const ⦋2⦌ 0) sorry sorry
Tactic: congr