awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1 : ComposableArrows.{v, u} C 1 = (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌)
⊢ Eq (α := ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk (f₀₁ ≫ f₁₂)) :
      ComposableArrows.{v, u} C 1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
        h'.simplex :
      (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌))

Tactic:
exact (h'.d₁).symm

Premises used: SSet.Edge.CompStruct.d₁, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1 : ComposableArrows.{v, u} C 1 = (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌)
⊢ Eq (α := ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk f₀₂) :
      ComposableArrows.{v, u} C 1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
        h.simplex :
      (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌))

Tactic:
(h.d₁).symm

Premises used: SSet.Edge.CompStruct.d₁, Eq.symm, SSet.Edge.edge, CategoryTheory.ComposableArrows.mk₁
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1 : ComposableArrows.{v, u} C 1 = (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌)
⊢ Eq (α := ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk f₀₂) :
      ComposableArrows.{v, u} C 1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
        h.simplex :
      (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌))

Tactic:
exact (h.d₁).symm

Premises used: SSet.Edge.CompStruct.d₁, Eq.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₁₂).edge

Tactic:
have h₀ := h.d₀
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₁₂).edge
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₀₁).edge

Tactic:
have h₂ := h.d₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₁₂).edge
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₀₁).edge
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h'.simplex =
    (edgeMk f₁₂).edge

Tactic:
have h'₀ := h'.d₀
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₁₂).edge
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₀₁).edge
h'₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h'.simplex =
    (edgeMk f₁₂).edge
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h'.simplex =
    (edgeMk f₀₁).edge

Tactic:
have h'₂ := h'.d₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₁₂).edge
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₀₁).edge
h'₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h'.simplex =
    (edgeMk f₁₂).edge
h'₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h'.simplex =
    (edgeMk f₀₁).edge
⊢ ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) = ComposableArrows.mk₁ f₁₂

Tactic:
simp only [δ₂_zero, δ₂_two, edgeMk_edge] at h₀ h₂ h'₀ h'₂

Premises used: CategoryTheory.nerve.edgeMk_edge, CategoryTheory.nerve.δ₂_zero, CategoryTheory.nerve.δ₂_two
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₁₂).edge
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₀₁).edge
h'₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h'.simplex =
    (edgeMk f₁₂).edge
h'₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h'.simplex =
    (edgeMk f₀₁).edge
h₁ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) = ComposableArrows.mk₁ f₁₂
⊢ ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁

Tactic:
simp only [δ₂_zero, δ₂_two, edgeMk_edge] at h₀ h₂ h'₀ h'₂

Premises used: CategoryTheory.nerve.edgeMk_edge, CategoryTheory.nerve.δ₂_zero, CategoryTheory.nerve.δ₂_two
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₁₂).edge
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₀₁).edge
h'₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h'.simplex =
    (edgeMk f₁₂).edge
h'₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h'.simplex =
    (edgeMk f₀₁).edge
h₁ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) = ComposableArrows.mk₁ f₁₂
h₃ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
⊢ ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) =
    ComposableArrows.mk₁ f₁₂

Tactic:
simp only [δ₂_zero, δ₂_two, edgeMk_edge] at h₀ h₂ h'₀ h'₂

Premises used: CategoryTheory.nerve.edgeMk_edge, CategoryTheory.nerve.δ₂_zero, CategoryTheory.nerve.δ₂_two
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₁₂).edge
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h.simplex =
    (edgeMk f₀₁).edge
h'₀ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h'.simplex =
    (edgeMk f₁₂).edge
h'₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
        (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
      h'.simplex =
    (edgeMk f₀₁).edge
h₁ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) = ComposableArrows.mk₁ f₁₂
h₃ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
h'₁ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) =
    ComposableArrows.mk₁ f₁₂
⊢ ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁

Tactic:
simp only [δ₂_zero, δ₂_two, edgeMk_edge] at h₀ h₂ h'₀ h'₂

Premises used: CategoryTheory.nerve.edgeMk_edge, CategoryTheory.nerve.δ₂_zero, CategoryTheory.nerve.δ₂_two
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) = ComposableArrows.mk₁ f₁₂
h₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
h'₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) =
    ComposableArrows.mk₁ f₁₂
h'₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
⊢ Eq (α := ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1)
        (Arrow.mk (ComposableArrows.map' h'.simplex 0 1 ComposableArrows.homMk₁._proof_4 _proof_246✝)) :
      ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1)
        (Arrow.mk (ComposableArrows.map' h.simplex 0 1 ComposableArrows.homMk₁._proof_4 _proof_246✝)) :
      ComposableArrows.{v, u} C 1)

Tactic:
simp [-Edge.CompStruct.d₂, h'₂, ← h₂]

Premises used: SSet.Edge.CompStruct.d₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) = ComposableArrows.mk₁ f₁₂
h₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
h'₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) =
    ComposableArrows.mk₁ f₁₂
h'₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
⊢ Eq (α := ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1)
        (Arrow.mk (ComposableArrows.map' h'.simplex 1 2 _proof_246✝ _proof_247✝)) :
      ComposableArrows.{v, u} C 1)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1)
        (Arrow.mk (ComposableArrows.map' h.simplex 1 2 _proof_246✝ _proof_247✝)) :
      ComposableArrows.{v, u} C 1)

Tactic:
simp [-Edge.CompStruct.d₀, h'₀, ← h₀]

Premises used: SSet.Edge.CompStruct.d₀
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
h_1 : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) = ComposableArrows.mk₁ f₁₂
h₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
h'₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) =
    ComposableArrows.mk₁ f₁₂
h'₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
⊢ Eq (α := (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
        h'.simplex :
      (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1 + 1⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋1⦌))
        h.simplex :
      (fun (X : Type (max u v)) ↦ X) (nerve.{v, u} C _⦋1⦌))

Tactic:
exact congr_arg _ (ComposableArrows.ext₂_of_arrow
      (ComposableArrows.arrowEquiv.symm.injective
        (by simp [-Edge.CompStruct.d₂, h'₂, ← h₂]))
      (ComposableArrows.arrowEquiv.symm.injective
        (by simp [-Edge.CompStruct.d₀, h'₀, ← h₀])))

Premises used: CategoryTheory.ComposableArrows.ext₂_of_arrow, CategoryTheory.ComposableArrows.arrowEquiv, congr_arg, Equiv.injective, Equiv.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
⊢ f₀₁ ≫ f₁₂ = f₀₂

Tactic:
(nerve.nonempty_compStruct_iff _ _ _).1 ⟨h⟩

Premises used: CategoryTheory.nerve.nonempty_compStruct_iff, Nonempty.intro, Iff.mp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1 :
  Quiver.Hom.{v, u} (V := C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀ : ComposableArrows.{v, u} C 0) :
        C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂ : ComposableArrows.{v, u} C 0) :
        C) =
    (x₀ ⟶ x₂)
e_3 :
  (nerveEquiv : (a : ComposableArrows C 0) → C)
      ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀ : ComposableArrows.{v, u} C 0) =
    x₀
e_4 :
  (nerveEquiv : (a : ComposableArrows C 0) → C)
      ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₁ : ComposableArrows.{v, u} C 0) =
    x₁
⊢ (homEquiv :
        (a :
            Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀)
              ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁)) →
          (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀) ⟶
            (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁))
      (edgeMk f₀₁) =
    f₀₁

Tactic:
apply homEquiv_edgeMk

Premises used: CategoryTheory.nerve.homEquiv_edgeMk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1 :
  Quiver.Hom.{v, u} (V := C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀ : ComposableArrows.{v, u} C 0) :
        C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂ : ComposableArrows.{v, u} C 0) :
        C) =
    (x₀ ⟶ x₂)
e_4 :
  (nerveEquiv : (a : ComposableArrows C 0) → C)
      ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₁ : ComposableArrows.{v, u} C 0) =
    x₁
e_5 :
  (nerveEquiv : (a : ComposableArrows C 0) → C)
      ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂ : ComposableArrows.{v, u} C 0) =
    x₂
⊢ (homEquiv :
        (a :
            Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁)
              ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂)) →
          (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₁) ⟶
            (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂))
      (edgeMk f₁₂) =
    f₁₂

Tactic:
apply homEquiv_edgeMk

Premises used: CategoryTheory.nerve.homEquiv_edgeMk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
e_1 :
  Quiver.Hom.{v, u} (V := C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₀ : ComposableArrows.{v, u} C 0) :
        C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C)
          ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x₂ : ComposableArrows.{v, u} C 0) :
        C) =
    (x₀ ⟶ x₂)
⊢ (homEquiv :
        (a :
            Edge ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀)
              ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂)) →
          (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₀) ⟶
            (nerveEquiv : (a : ComposableArrows C 0) → C) ((nerveEquiv.symm : (a : C) → ComposableArrows C 0) x₂))
      (edgeMk f₀₂) =
    f₀₂

Tactic:
apply homEquiv_edgeMk

Premises used: CategoryTheory.nerve.homEquiv_edgeMk