awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
x : X _⦋n⦌
⊢ Eq (α := X _⦋n + 1 + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x) (op ⦋n + 1 + 1⦌)) :
              (a : Δ[n] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[n] i.castSucc) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n + 1 + 1⦌)
                ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
                  Δ[n] _⦋n + 1⦌) :
              Δ[n] _⦋n + 1 + 1⦌),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[1] i.castSucc) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n + 1 + 1⦌)
            (stdSimplex.objMk₁ j.castSucc.succ)).1 :
      X _⦋n + 1 + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌))
                  (op ⦋n + 1 + 1⦌)) :
              (a : Δ[n + 1] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                (SimplexCategory.σ j.succ) :
              Δ[n + 1] _⦋n + 1 + 1⦌),
          stdSimplex.objMk₁ j.castSucc.succ.succ).1 :
      X _⦋n + 1 + 1⦌)
have h : Eq (α := X _⦋n + 1 + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.succ).op) : (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i).op) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x :
        X _⦋n + 1⦌) :
    X _⦋n + 1 + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.succ).op) : (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌) :
    X _⦋n + 1 + 1⦌)
Tactic: simp [SimplexCategory.σ_comp_σ hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
⊢ (↾fun (x : X _⦋n⦌) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
            (a : (fun (X : Type u) ↦ X) ((Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                j) :
            (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
      σ Y i.succ =
    σ X i ≫
      ↾fun (x : X _⦋n + 1⦌) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                (op ⦋n + 1 + 1⦌)) :
            (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                j.castSucc) :
            (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)
have h : ∀ (x : X _⦋n⦌),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X _⦋n⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                    j) :
                (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
          σ Y i.succ))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (σ X i ≫
          ↾fun (x : X _⦋n + 1⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                    (op ⦋n + 1 + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                    j.castSucc) :
                (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)))
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : X _⦋n⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                    j) :
                (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌)) ≫
          σ Y i.succ))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (σ X i ≫
          ↾fun (x : X _⦋n + 1⦌) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X) x ▷ Δ[1] ≫ H.h)
                    (op ⦋n + 1 + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) ((Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n + 1 + 1⦌))
              (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                      (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
                    j.castSucc) :
                (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌)))
      x
have h : Eq (α := Y _⦋n + 1 + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x ▷ Δ[1] ≫ H.h) (op ⦋n + 1 + 1⦌)) :
        (a : (Δ[n] ⊗ Δ[1]) _⦋n + 1 + 1⦌) → Y _⦋n + 1 + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ (tensorObj (𝒞 := Functor.category) Δ[n] Δ[1]) i.succ) :
            (a : (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) → (Δ[n] ⊗ Δ[1]) _⦋n + 1 + 1⦌)
          (↑((prodStdSimplex.nonDegenerateEquiv₁ :
                  (a : Fin (n + 1)) → (↑((Δ[n] ⊗ Δ[1]).nonDegenerate (n + 1)) : Type u))
                j) :
            (Δ[n] ⊗ Δ[1]) _⦋n + 1⦌) :
        tensorObj (𝒞 := Functor.category) Δ[n] Δ[1] _⦋n + 1 + 1⦌) :
    Y _⦋n + 1 + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌) ▷
                Δ[1] ≫
              H.h)
            (op ⦋n + 1 + 1⦌)) :
        (a : (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) → Y _⦋n + 1 + 1⦌)
      (↑((prodStdSimplex.nonDegenerateEquiv₁ :
              (a : Fin (n + 1 + 1)) → (↑((Δ[n + 1] ⊗ Δ[1]).nonDegenerate (n + 1 + 1)) : Type u))
            j.castSucc) :
        (Δ[n + 1] ⊗ Δ[1]) _⦋n + 1 + 1⦌) :
    Y _⦋n + 1 + 1⦌)
Tactic: simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.σ_naturality_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
⊢ Eq (α := X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x) (op ⦋n + 1 + 1⦌)) :
            (a : Δ[n] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[n] i.succ) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n + 1 + 1⦌)
              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
                Δ[n] _⦋n + 1⦌) :
            Δ[n] _⦋n + 1 + 1⦌),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n + 1 + 1⦌)
          (stdSimplex.objMk₁ j.castSucc.succ)) :
      X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌))
                (op ⦋n + 1 + 1⦌)) :
            (a : Δ[n + 1] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
              (SimplexCategory.σ j.castSucc) :
            Δ[n + 1] _⦋n + 1 + 1⦌),
        stdSimplex.objMk₁ j.castSucc.castSucc.succ) :
      X _⦋n + 1 + 1⦌ × Δ[1] _⦋n + 1 + 1⦌)
have h : Eq (α := X _⦋n + 1 + 1⦌)
  (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x) (op ⦋n + 1 + 1⦌)) :
            (a : Δ[n] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[n] i.succ) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n + 1 + 1⦌)
              ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
                Δ[n] _⦋n + 1⦌) :
            Δ[n] _⦋n + 1 + 1⦌),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n + 1 + 1⦌)
          (stdSimplex.objMk₁ j.castSucc.succ)).1 :
    X _⦋n + 1 + 1⦌)
  (((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X)
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌))
                (op ⦋n + 1 + 1⦌)) :
            (a : Δ[n + 1] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
          ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
              (SimplexCategory.σ j.castSucc) :
            Δ[n + 1] _⦋n + 1 + 1⦌),
        stdSimplex.objMk₁ j.castSucc.castSucc.succ).1 :
    X _⦋n + 1 + 1⦌)
Tactic: ext k : 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homotopy (goal)
Goal:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
x : X _⦋n⦌
⊢ Eq (α := X _⦋n + 1 + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app ((Equiv.symm yonedaEquiv : (a : X _⦋n⦌) → Δ[n] ⟶ X) x) (op ⦋n + 1 + 1⦌)) :
              (a : Δ[n] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[n] i.succ) : (a : Δ[n] _⦋n + 1⦌) → Δ[n] _⦋n + 1 + 1⦌)
                ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n + 1⦌) (SimplexCategory.σ j) :
                  Δ[n] _⦋n + 1⦌) :
              Δ[n] _⦋n + 1 + 1⦌),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (σ Δ[1] i.succ) : (a : Δ[1] _⦋n + 1⦌) → Δ[1] _⦋n + 1 + 1⦌)
            (stdSimplex.objMk₁ j.castSucc.succ)).1 :
      X _⦋n + 1 + 1⦌)
    (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  ((Equiv.symm yonedaEquiv : (a : X _⦋n + 1⦌) → Δ[n + 1] ⟶ X)
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌))
                  (op ⦋n + 1 + 1⦌)) :
              (a : Δ[n + 1] _⦋n + 1 + 1⦌) → X _⦋n + 1 + 1⦌)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n + 1 + 1⦌ ⟶ ⦋n + 1⦌) → Δ[n + 1] _⦋n + 1 + 1⦌)
                (SimplexCategory.σ j.castSucc) :
              Δ[n + 1] _⦋n + 1 + 1⦌),
          stdSimplex.objMk₁ j.castSucc.castSucc.succ).1 :
      X _⦋n + 1 + 1⦌)
have h : Eq (α := X _⦋n + 1 + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.castSucc).op) :
        (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ i).op) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x :
        X _⦋n + 1⦌) :
    X _⦋n + 1 + 1⦌)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.σ j.castSucc).op) :
        (a : X _⦋n + 1⦌) → X _⦋n + 1 + 1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ X i) : (a : X _⦋n⦌) → X _⦋n + 1⦌) x : X _⦋n + 1⦌) :
    X _⦋n + 1 + 1⦌)
Tactic: simp [← SimplexCategory.σ_comp_σ hij, SSet.yonedaEquiv_symm_app_objEquiv_symm.{u}]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
S T : Truncated 2
f : S ⟶ T
x : OneTruncation₂ S
⊢ Truncated.Edge.map (𝟙rq x) f =
    𝟙rq
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
          (a : (fun (X : Type u_1) ↦ X) (S.obj (op { obj := ⦋0⦌, property := _proof_1 }))) →
            (fun (X : Type u_1) ↦ X) (T.obj (op { obj := ⦋0⦌, property := _proof_1 })))
        x)
have h : (Truncated.Edge.map (𝟙rq x) f).edge =
  Truncated.Edge.edge (x₀ :=
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f.app
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                Truncated.Edge._proof_1))) :
        (a : (fun (X : Type u_1) ↦ X) (S.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 }))) →
          (fun (X : Type u_1) ↦ X) (T.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
      x)
    (x₁ :=
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (f.app
            (op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌
                Truncated.Edge._proof_1))) :
        (a : (fun (X : Type u_1) ↦ X) (S.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 }))) →
          (fun (X : Type u_1) ↦ X) (T.obj (op { obj := ⦋0⦌, property := Truncated.Edge._proof_1 })))
      x)
    (𝟙rq
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (f.app (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))) :
          (a : (fun (X : Type u_1) ↦ X) (S.obj (op { obj := ⦋0⦌, property := _proof_1 }))) →
            (fun (X : Type u_1) ↦ X) (T.obj (op { obj := ⦋0⦌, property := _proof_1 })))
        x))
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
X : Truncated 2
x₁ y₁ x₂ y₂ : OneTruncation₂ X
f : x₁ ⟶ y₁
hx : x₁ = x₂
hy : y₁ = y₂
⊢ (Quiver.homOfEq f hx hy).edge = f.edge
have subst : (Quiver.homOfEq f sorry sorry).edge = f.edge
Tactic: subst hx hy
Cleared hypotheses: x₂, y₂, hx, hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
x y : V.HomotopyCategory
h :
  x.as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V)) =
    y.as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V))
⊢ x = y
have obtain : ∀
  (x :
    V.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
  (h :
    (mk x).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V)) =
      y.as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V))),
  mk x = y
Tactic: obtain ⟨x, rfl⟩ := x.mk_surjective
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
y : V.HomotopyCategory
x :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
h :
  (mk x).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V)) =
    y.as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V))
⊢ mk x = y
have obtain : ∀
  (y :
    V.obj
      (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1)))
  (h :
    (mk x).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V)) =
      (mk y).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V))),
  mk x = mk y
Tactic: obtain ⟨y, rfl⟩ := y.mk_surjective
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat (goal)
Goal:
V : Truncated 2
x y :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
h :
  (mk x).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V)) =
    (mk y).as (r := OneTruncation₂.HoRel₂ V).as (r := Cat.FreeReflRel (OneTruncation₂ V))
⊢ mk x = mk y
have obtain : mk x = mk x
Tactic: obtain rfl : x = y := h
Cleared hypotheses: y, 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₀ y₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge y₀ y₁
h : e.edge = e'.edge
⊢ x₀ = y₀
have rw : (ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 1 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₀
Tactic: rw [← e.src_eq, ← e'.src_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₀ y₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge y₀ y₁
h : e.edge = e'.edge
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 1 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 (δ₂ 1 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 (δ₂ 1 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.src_eq, ← e'.src_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₀ y₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge y₀ y₁
h : e.edge = e'.edge
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (V.map (δ₂ 1 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 (δ₂ 1 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 (δ₂ 1 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 (δ₂ 1 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 (δ₂ 1 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.src_eq, ← e'.src_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₀ y₁ :
  V.obj
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ OneTruncation₂._proof_1))
e' : Edge y₀ y₁
h : e.edge = e'.edge
⊢ Arrow.mk (homMk e) = Arrow.mk (homMk e')
have obtain : ∀ (e' : Edge x₀ y₁) (h : e.edge = e'.edge), Arrow.mk (homMk e) = Arrow.mk (homMk e')
Tactic: obtain rfl : x₀ = y₀ := by rw [← e.src_eq, ← e'.src_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 : 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
⊢ x₁ = y₁
have 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₁
Tactic: rw [← e.tgt_eq, ← e'.tgt_eq, h]