awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
⊢ fibrations SSet = J.rlp

Tactic:
rfl

Premises used: HomotopicalAlgebra.fibrations, CategoryTheory.MorphismProperty.rlp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
f : X ⟶ Y
rw : cofibrations SSet f ↔ Mono f
⊢ Cofibration f ↔ Mono f

Tactic:
rw [HomotopicalAlgebra.cofibration_iff]

Premises used: HomotopicalAlgebra.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
f : X ⟶ Y
⊢ cofibrations SSet f ↔ Mono f

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
f : X ⟶ Y
rw : fibrations SSet f ↔ J.rlp f
⊢ Fibration f ↔ J.rlp f

Tactic:
rw [HomotopicalAlgebra.fibration_iff]

Premises used: HomotopicalAlgebra.fibration_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
f : X ⟶ Y
⊢ fibrations SSet f ↔ J.rlp f

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
f : X ⟶ Y
inst rwa rwa₁ rwa₂ rwa₃ : Cofibration f
⊢ Mono f

Tactic:
rwa [← cofibration_iff]

Premises used: SSet.modelCategoryQuillen.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
f : X ⟶ Y
inst rwa rwa₁ rwa₂ rwa₃ : Mono f
⊢ Cofibration f

Tactic:
rwa [cofibration_iff]

Premises used: SSet.modelCategoryQuillen.cofibration_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
f : X ⟶ Y
hf : Fibration f
n : ℕ
i : Fin (n + 2)
rw : ∀ (hf : J.rlp f) {n : ℕ} (i : Fin (n + 2)), HasLiftingProperty Λ[n + 1, i].ι f
⊢ HasLiftingProperty Λ[n + 1, i].ι f

Tactic:
rw [fibration_iff] at hf

Premises used: SSet.modelCategoryQuillen.fibration_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
f : X ⟶ Y
hf : J.rlp f
n : ℕ
i : Fin (n + 2)
⊢ HasLiftingProperty Λ[n + 1, i].ι f

Tactic:
hf _ (horn_ι_mem_J _ _)

Premises used: SSet.modelCategoryQuillen.horn_ι_mem_J
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
Goal:
X Y : SSet
f : X ⟶ Y
hf : J.rlp f
n : ℕ
i : Fin (n + 2)
⊢ HasLiftingProperty Λ[n + 1, i].ι f

Tactic:
exact hf _ (horn_ι_mem_J _ _)

Premises used: SSet.modelCategoryQuillen.horn_ι_mem_J
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
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
j : Fin (n + 2)
hj : j ≠ i
⊢ ι i j hj ≫ hf.desc ≫ p = ι i j hj ≫ Λ[n + 1, i].ι ≫ b

Tactic:
simpa using comm j hj
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
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
⊢ 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)⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
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
sq : CommSq hf.desc Λ[n + 1, i].ι p b
j : Fin (n + 2)
hj : j ≠ i
⊢ stdSimplex.δ j ≫ sq.lift = f j hj

Tactic:
simp [← ι_ι_assoc i j hj]

Premises used: SSet.horn.ι_ι_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
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
sq : CommSq hf.desc Λ[n + 1, i].ι p b
⊢ sq.lift ≫ p = b

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
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
sq : CommSq hf.desc Λ[n + 1, i].ι p b
⊢ ∃ (φ : Δ[n + 1] ⟶ X), (∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj) ∧ φ ≫ p = b

Tactic:
exact ⟨sq.lift, fun j hj ↦ by simp [← ι_ι_assoc i j hj], by simp⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
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
j : Fin (n + 2)
hj : j ≠ i
⊢ stdSimplex.δ j ≫ hf.lift p b comm = f j hj

Tactic:
((hf.exists_lift p b comm).choose_spec).1 j hj

Premises used: Exists.choose_spec, SSet.horn.IsCompatible.lift, SSet.horn.IsCompatible.exists_lift, And.left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
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
⊢ hf.lift p b comm ≫ p = b

Tactic:
((hf.exists_lift p b comm).choose_spec).2

Premises used: Exists.choose_spec, SSet.horn.IsCompatible.lift, SSet.horn.IsCompatible.exists_lift, And.right
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ : X _⦋0⦌
e : Truncated.Edge (X := Functor.obj (truncation 2) X) x₀ x₁
⊢ (ofTruncated e).edge = e.edge

Tactic:
rfl

Premises used: SSet.Edge.edge, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ : X _⦋0⦌
e : Edge x₀ x₁
⊢ e.toTruncated.edge = e.edge

Tactic:
rfl

Premises used: SSet.Edge.edge, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ : X _⦋0⦌
e : Edge x₀ x₁
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 1) :
        (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      e.edge =
    x₀

Tactic:
Truncated.Edge.src_eq e

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.δ, SSet.Truncated.Edge.src_eq, OrderEmbedding.toOrderHom, SSet.Edge.edge, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ : X _⦋0⦌
e : Edge x₀ x₁
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      e.edge =
    x₁

Tactic:
Truncated.Edge.tgt_eq e

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.δ, OrderEmbedding.toOrderHom, SSet.Edge.edge, SSet.Truncated.Edge.tgt_eq, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ : X _⦋0⦌
e e' : Edge x₀ x₁
h : e.edge = e'.edge
⊢ e = e'

Tactic:
Truncated.Edge.ext h

Premises used: SSet.Truncated.Edge.ext, SSet.Edge
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ : X _⦋0⦌
edge : X _⦋1⦌
src_eq :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 1) :
        (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      edge =
    x₀
tgt_eq :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋0⦌))
      edge =
    x₁
⊢ (mk edge src_eq tgt_eq).edge = edge

Tactic:
rfl

Premises used: SSet.Edge.edge, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ : X _⦋0⦌
⊢ (id x₀).toTruncated = Truncated.Edge.id x₀

Tactic:
rfl

Premises used: SSet.Edge.id, SSet.Edge.ofTruncated, rfl, SSet.Truncated.Edge.id, SSet.Edge.toTruncated
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ : X _⦋0⦌
⊢ (id x₀).edge =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (X _⦋0 + 1⦌))
      x₀

Tactic:
rfl

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.σ, Fin.predAboveOrderHom, SSet.Edge.edge, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X Y : SSet
x₀ x₁ : X _⦋0⦌
e : Edge x₀ x₁
f : X ⟶ Y
⊢ (e.map f).edge =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋1⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (Y _⦋1⦌))
      e.edge

Tactic:
rfl

Premises used: SSet.Edge.edge, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X Y : SSet
x₀ : X _⦋0⦌
f : X ⟶ Y
⊢ (id x₀).map f =
    id
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋0⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋0⦌)) → (fun (X : Type u) ↦ X) (Y _⦋0⦌))
        x₀)

Tactic:
Truncated.Edge.map_id _ _

Premises used: SSet.Truncated.Edge.map_id, SSet.Edge.map, SSet.Edge, SSet.Edge.id, SSet.Edge.ofTruncated, SSet.Truncated.Edge.id, SSet.Edge.toTruncated
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
s : X _⦋1⦌
⊢ (mk' s).edge = s

Tactic:
rfl

Premises used: SSet.Edge.edge, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
s : X _⦋1⦌
⊢ ∃ (x₀ : X _⦋0⦌) (x₁ : X _⦋0⦌) (e : Edge x₀ x₁), e.edge = s

Tactic:
⟨_, _, mk' s, rfl⟩

Premises used: Exists.intro, SSet.Edge.mk', rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ x₂ : X _⦋0⦌
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 2) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      h.simplex =
    e₀₁.edge

Tactic:
Truncated.Edge.CompStruct.d₂ h

Premises used: SSet.Truncated.Edge.CompStruct.d₂, Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.δ, SSet.Edge.CompStruct.simplex, OrderEmbedding.toOrderHom, SSet.Edge.edge, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ x₂ : X _⦋0⦌
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      h.simplex =
    e₁₂.edge

Tactic:
Truncated.Edge.CompStruct.d₀ h

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.δ, SSet.Edge.CompStruct.simplex, SSet.Truncated.Edge.CompStruct.d₀, OrderEmbedding.toOrderHom, SSet.Edge.edge, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ x₂ : X _⦋0⦌
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 1) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      h.simplex =
    e₀₂.edge

Tactic:
Truncated.Edge.CompStruct.d₁ h

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.δ, SSet.Edge.CompStruct.simplex, OrderEmbedding.toOrderHom, SSet.Truncated.Edge.CompStruct.d₁, SSet.Edge.edge, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ x₂ : X _⦋0⦌
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
simplex : X _⦋2⦌
d₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 2) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      simplex =
    e₀₁.edge
d₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      simplex =
    e₁₂.edge
d₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X 1) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
      simplex =
    e₀₂.edge
⊢ (mk simplex ⋯ ⋯ ⋯).simplex = simplex

Tactic:
rfl

Premises used: SSet.Edge.CompStruct.simplex, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ x₂ : X _⦋0⦌
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h h' : e₀₁.CompStruct e₁₂ e₀₂
eq : h.simplex = h'.simplex
⊢ h = h'

Tactic:
Truncated.Edge.CompStruct.ext eq

Premises used: SSet.Truncated.Edge.CompStruct.ext, SSet.Edge.CompStruct
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
s : X _⦋2⦌
⊢ ∃ (x₀ : X _⦋0⦌) (x₁ : X _⦋0⦌) (x₂ : X _⦋0⦌) (e₀₁ : Edge x₀ x₁) (e₁₂ : Edge x₁ x₂) (e₀₂ : Edge x₀ x₂) (h :
    e₀₁.CompStruct e₁₂ e₀₂), h.simplex = s

Tactic:
Truncated.Edge.CompStruct.exists_of_simplex (X := (truncation 2).obj X) s

Premises used: SSet.Edge.CompStruct.simplex, SSet.Edge.CompStruct, SSet.Truncated.Edge.CompStruct.exists_of_simplex, SSet.Edge, SSet.Edge.toTruncated
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ : X _⦋0⦌
e : Edge x₀ x₁
⊢ (idComp e).simplex =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X 0) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1 + 1⦌))
      e.edge

Tactic:
rfl

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.σ, SSet.Edge.CompStruct.simplex, Fin.predAboveOrderHom, SSet.Edge.edge, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X : SSet
x₀ x₁ : X _⦋0⦌
e : Edge x₀ x₁
⊢ (compId e).simplex =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ X 1) :
        (a : (fun (X : Type u) ↦ X) (X _⦋1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1 + 1⦌))
      e.edge

Tactic:
rfl

Premises used: Quiver.Hom.op, SimplexCategory.mkHom, SimplexCategory.σ, SSet.Edge.CompStruct.simplex, Fin.predAboveOrderHom, SSet.Edge.edge, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
Goal:
X Y : SSet
x₀ x₁ x₂ : X _⦋0⦌
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
f : X ⟶ Y
⊢ (h.map f).simplex =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋2⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋2⦌)) → (fun (X : Type u) ↦ X) (Y _⦋2⦌))
      h.simplex

Tactic:
rfl

Premises used: SSet.Edge.CompStruct.simplex, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X : Truncated 2
s : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))
⊢ ∃ (x₀ :
    X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1)))
    (x₁ :
    X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1)))
    (e : Edge x₀ x₁), e.edge = s

Tactic:
⟨_, _, mk' s, rfl⟩

Premises used: SSet.Truncated.Edge.mk', Exists.intro, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 _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 := _proof_1 })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (σ₂ 0 _proof_3 _proof_1).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) →
              (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0 + 1⦌, property := _proof_3 })))
          x :
        (fun (X : Type u) ↦ X)
          (X.obj
            (Opposite.op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌
                _proof_3)))) =
    x

Tactic:
simp [← Functor.map_comp_apply, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x : X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 _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 := _proof_1 })))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (σ₂ 0 _proof_3 _proof_1).op) :
            (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) →
              (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋0 + 1⦌, property := _proof_3 })))
          x :
        (fun (X : Type u) ↦ X)
          (X.obj
            (Opposite.op
              (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋HAdd.hAdd (α := ℕ) 0 1⦌
                _proof_3)))) =
    x

Tactic:
simp [← Functor.map_comp_apply, ← op_comp]

Premises used: CategoryTheory.op_comp, CategoryTheory.Functor.map_comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x₀ x₁ :
  X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
e : Edge x₀ x₁
f : X ⟶ Y
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (Y.obj
        (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (δ₂ 1 _proof_1 _proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (Y.obj (Opposite.op { obj := ⦋0 + 1⦌, property := _proof_3 }))) →
            (fun (X : Type u) ↦ X) (Y.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (f.app
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := _proof_2 }))) →
                (fun (X : Type u) ↦ X) (Y.obj (Opposite.op { obj := ⦋1⦌, property := _proof_2 })))
            e.edge :
          (fun (X : Type u) ↦ X)
            (Y.obj
              (Opposite.op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))) :
      (fun (X : Type u) ↦ X)
        (Y.obj
          (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))))
    ((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₀ :
      (fun (X : Type u) ↦ X)
        (Y.obj
          (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))))

Tactic:
simp [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
Goal:
X Y : Truncated 2
x₀ x₁ :
  X.obj (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))
e : Edge x₀ x₁
f : X ⟶ Y
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      (Y.obj
        (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map (δ₂ 0 _proof_1 _proof_3).op) :
          (a : (fun (X : Type u) ↦ X) (Y.obj (Opposite.op { obj := ⦋0 + 1⦌, property := _proof_3 }))) →
            (fun (X : Type u) ↦ X) (Y.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (f.app
                  (Opposite.op
                    (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))) :
              (a : (fun (X : Type u) ↦ X) (X.obj (Opposite.op { obj := ⦋1⦌, property := _proof_2 }))) →
                (fun (X : Type u) ↦ X) (Y.obj (Opposite.op { obj := ⦋1⦌, property := _proof_2 })))
            e.edge :
          (fun (X : Type u) ↦ X)
            (Y.obj
              (Opposite.op
                (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2)))) :
      (fun (X : Type u) ↦ X)
        (Y.obj
          (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))))
    ((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₁ :
      (fun (X : Type u) ↦ X)
        (Y.obj
          (Opposite.op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ _proof_1))))

Tactic:
simp [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
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
edge :
  ((id x).map f).edge =
    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))
⊢ (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)

Tactic:
ext