awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋1⦌) ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := Opposite.unop (Opposite.op ⦋2⦌)) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋1⦌) ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫
                ((stdSimplex.objEquiv :
                      Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)
                  ((yonedaEquiv : (a : Δ[n + 1 + 1] ⟶ Δ[n + 1 + 1 + 1]) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                    (stdSimplex.δ j))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
have h : Eq (α := Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
              (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      z :
    Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (mkOfSucc k ≫
              ((stdSimplex.objEquiv :
                    Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → ⦋n + 1 + 1⦌ ⟶ ⦋n + 1 + 2⦌)
                ((yonedaEquiv : (a : Δ[n + 1 + 1] ⟶ Δ[n + 1 + 1 + 1]) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                  (stdSimplex.map (SimplexCategory.δ j)))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      z :
    Fin (n + 1 + 2 + 1))
Tactic: dsimp [CosimplicialObject.δ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫
                ((stdSimplex.objEquiv :
                      Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → ⦋n + 1 + 1⦌ ⟶ ⦋n + 1 + 2⦌)
                  ((yonedaEquiv : (a : Δ[n + 1 + 1] ⟶ Δ[n + 1 + 1 + 1]) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                    (stdSimplex.map (SimplexCategory.δ j)))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
have h : Eq (α := Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
              (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      z :
    Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (mkOfSucc k ≫
              ((stdSimplex.objEquiv :
                    Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → ⦋n + 1 + 1⦌ ⟶ ⦋n + 1 + 2⦌)
                ((Equiv.symm stdSimplex.objEquiv :
                    (a : Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 1 + 1⦌) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                  (SimplexCategory.δ j))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      z :
    Fin (n + 1 + 2 + 1))
Tactic: rw [SSet.yonedaEquiv_map]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫
                ((stdSimplex.objEquiv :
                      Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → ⦋n + 1 + 1⦌ ⟶ ⦋n + 1 + 2⦌)
                  ((Equiv.symm stdSimplex.objEquiv :
                      (a : Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 1 + 1⦌) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                    (SimplexCategory.δ j))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
have h : Eq (α := Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
              (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) sorry) : Δ[n + 1 + 2] _⦋2⦌))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      z :
    Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (mkOfSucc k ≫ SimplexCategory.δ j) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      z :
    Fin (n + 1 + 2 + 1))
Tactic: simp only [Equiv.apply_symm_apply, triangle]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫ SimplexCategory.δ j) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
have h : Eq (α := Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
              (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) sorry) : Δ[n + 1 + 2] _⦋2⦌))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      z :
    Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 sorry) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      z :
    Fin (n + 1 + 2 + 1))
Tactic: rw [mkOfSucc_δ_eq heq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 ⋯) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
have h : Eq (α := Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
          (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
            (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
              (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) sorry) : Δ[n + 1 + 2] _⦋2⦌))) :
        Δ[n + 1 + 2] _⦋1⦌) :
      (a : Fin 2) → Fin (n + 1 + 2 + 1))
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 sorry) :
        Δ[n + 1 + 2] _⦋1⦌) :
      (a : Fin 2) → Fin (n + 1 + 2 + 1))
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
            (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
              (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 ⋯) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin 2) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯) : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 ⋯) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
have h₁ : Eq (α := Fin (n + 1 + 2 + 1))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
          (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
            (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
              (↑(horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) sorry) : Δ[n + 1 + 2] _⦋2⦌))) :
        Δ[n + 1 + 2] _⦋1⦌) :
      (a : Fin 2) → Fin (n + 1 + 2 + 1))
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, sorry⟩))
  ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌) (intervalEdge (↑k : ℕ) 2 sorry) :
        Δ[n + 1 + 2] _⦋1⦌) :
      (a : Fin 2) → Fin (n + 1 + 2 + 1))
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, sorry⟩))
Tactic: fin_cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
⊢ (coproducts.{w, v, u} (ofHoms g)).pushouts f
have refine : coproducts.{w, v, u} (ofHoms g) c.m
Tactic: refine ⟨_, _, _, _, _, ?_, c.isPushout⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
x : Discrete c.ι
i : c.ι
⊢ Eq (α :=
    Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) { as := i : Discrete c.ι } ⟶ c.cofan₂.pt)
    (c.cofan₁.ι.app { as := i } ≫ c.m)
    (c.cofan₁.ι.app { as := i : Discrete c.ι } ≫
      c.isColimit₁.desc
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun (x : Discrete c.ι) ↦
                match (motive :=
                  (x : Discrete c.ι) →
                    Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                      (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                  x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι })
have rw : Eq (α := Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) { as := i : Discrete c.ι } ⟶ c.cofan₂.pt)
  (c.cofan₁.ι.app { as := i } ≫ c.m)
  (NatTrans.app
    (Cocone.ι
      { pt := c.cofan₂.pt,
        ι :=
          (Discrete.natTrans fun (x : Discrete c.ι) ↦
              match (motive :=
                (x : Discrete c.ι) →
                  Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                    (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                x with
              | { as := i } => g (c.π i)) ≫
            c.cofan₂.ι })
    { as := i })
Tactic: rw [IsColimit.fac]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
⊢ coproducts.{w, v, u} (ofHoms g) c.m
have this : c.m =
  c.isColimit₁.desc
    { pt := c.cofan₂.pt,
      ι :=
        (Discrete.natTrans fun (x : Discrete c.ι) ↦
            match (motive :=
              (x : Discrete c.ι) →
                Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                  (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
              x with
            | { as := i } => g (c.π i)) ≫
          c.cofan₂.ι }
Tactic: have : c.m = c.isColimit₁.desc
      (Cocone.mk _ (Discrete.natTrans (fun ⟨i⟩ ↦ by exact g (c.π i)) ≫ c.cofan₂.ι)) :=
    c.isColimit₁.hom_ext (fun ⟨i⟩ ↦ by rw [IsColimit.fac]; exact c.hm i)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
this :
  c.m =
    c.isColimit₁.desc
      { pt := c.cofan₂.pt,
        ι :=
          (Discrete.natTrans fun (x : Discrete c.ι) ↦
              match (motive :=
                (x : Discrete c.ι) →
                  Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                    (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                x with
              | { as := i } => g (c.π i)) ≫
            c.cofan₂.ι }
⊢ coproducts.{w, v, u} (ofHoms g) c.m
have rw : ∃ (J : Type w),
  colimitsOfShape.{v, u, w, w} (ofHoms g) (Discrete J) (Y := c.cofan₂.pt)
    (c.isColimit₁.desc
        { pt := c.cofan₂.pt,
          ι :=
            (Discrete.natTrans fun (x : Discrete c.ι) ↦
                match (motive :=
                  (x : Discrete c.ι) →
                    Quiver.Hom.{v, u} (V := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                      (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                  x with
                | { as := i } => g (c.π i)) ≫
              c.cofan₂.ι } :
      c.cofan₁.pt ⟶
        Cocone.pt (F := Discrete.functor fun (i : c.ι) ↦ A (c.π i))
          { pt := c.cofan₂.pt,
            ι :=
              (Discrete.natTrans fun (x : Discrete c.ι) ↦
                  match (motive :=
                    (x : Discrete c.ι) →
                      Quiver.Hom.{v, u} (V := C)
                        (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
                        (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ B (c.π i)) x))
                    x with
                  | { as := i } => g (c.π i)) ≫
                c.cofan₂.ι })
Tactic: rw [this, coproducts_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ φ = φ'
have apply : c.g₂ ≫ φ = c.g₂ ≫ φ'
Tactic: apply c.isPushout.hom_ext h₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
Z : C
φ φ' : X₂ ⟶ Z
h₀ : f ≫ φ = f ≫ φ'
h : ∀ (i : c.ι), c.cell i ≫ φ = c.cell i ≫ φ'
⊢ c.g₂ ≫ φ = c.g₂ ≫ φ'
have h₁ : ∀ (i : c.ι), c.cofan₂.inj i ≫ c.g₂ ≫ φ = c.cofan₂.inj i ≫ c.g₂ ≫ φ'
Tactic: apply Cofan.IsColimit.hom_ext c.isColimit₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells (goal)
Goal:
C : Type u
inst : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
c : AttachCells.{w, t, v, u} g f
α' : Type t'
A' B' : α' → C
g' : (i' : α') → A' i' ⟶ B' i'
a : α → α'
ha : (i : α) → Arrow.mk (g i) ≅ Arrow.mk (X := A' (a i)) (g' (a i))
e : Iso (C := CategoryTheory.Functor.{w, v, w, u} (Discrete c.ι) C) (Discrete.functor fun (i : c.ι) ↦ A (c.π i))
  (Discrete.functor fun (i : c.ι) ↦ A' (a (c.π i))) :=
  Discrete.natIso fun (x : Discrete c.ι) ↦
    match (motive :=
      (x : Discrete c.ι) →
        Iso.{v, u} (C := C) (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A (c.π i)) x)
          (Functor.obj.{w, v, w, u} (Discrete.functor fun (i : c.ι) ↦ A' (a (c.π i))) x))
      x with
    | { as := i } => Functor.mapIso Arrow.leftFunc (ha (c.π i))
⊢ IsColimit.{w, v, w, u} (J := Discrete c.ι) (F := Discrete.functor fun (i : c.ι) ↦ A' ((a ∘ c.π) i))
    (Cofan.mk c.cofan₁.pt fun (i : c.ι) ↦
      CategoryTheory.Functor.map Arrow.leftFunc (Iso.inv (ha (c.π i))) ≫ c.cofan₁.inj i)
have refine : ∀ (i : c.ι),
  c.cofan₁.inj i ≫ Iso.hom (Iso.refl c.cofan₁.pt) =
    Cofan.inj
      ((Cocone.precompose e.hom).obj
        (Cofan.mk c.cofan₁.pt fun (i : c.ι) ↦
          CategoryTheory.Functor.map Arrow.leftFunc (Iso.inv (ha (c.π i))) ≫ c.cofan₁.inj i))
      i
Tactic: refine (IsColimit.precomposeHomEquiv e _).1
      (IsColimit.ofIsoColimit c.isColimit₁ (Cofan.ext (Iso.refl _) (fun i ↦ ?_)))