awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x : C
simp :
  Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (ComposableArrows.left.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : ComposableArrows C 0) → ComposableArrows C 1)
          (ComposableArrows.mk₀ x)))
      (ComposableArrows.right.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : ComposableArrows C 0) → ComposableArrows C 1)
          (ComposableArrows.mk₀ x))))
    (ComposableArrows.hom
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : ComposableArrows C 0) → ComposableArrows C 1)
          (ComposableArrows.mk₀ x)) :
      Quiver.Hom.{v, u} (V := C)
        (ComposableArrows.left.{v, u} (n := 1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
              (a : ComposableArrows C 0) → ComposableArrows C 1)
            (ComposableArrows.mk₀ x)))
        (ComposableArrows.right.{v, u} (n := 1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
              (a : ComposableArrows C 0) → ComposableArrows C 1)
            (ComposableArrows.mk₀ x))))
    (eqToHom ⋯ :
      Quiver.Hom.{v, u} (V := C)
        (ComposableArrows.left.{v, u} (n := 1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
              (a : ComposableArrows C 0) → ComposableArrows C 1)
            (ComposableArrows.mk₀ x)))
        (ComposableArrows.right.{v, u} (n := 1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
              (a : ComposableArrows C 0) → ComposableArrows C 1)
            (ComposableArrows.mk₀ x))))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (ComposableArrows.left.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0 + 1⦌))
          (ComposableArrows.mk₀ x)))
      (ComposableArrows.right.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0 + 1⦌))
          (ComposableArrows.mk₀ x))))
    (ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
          (a : (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0⦌)) → (fun (X : Type (max u v)) ↦ X) (nerve C _⦋0 + 1⦌))
        (ComposableArrows.mk₀ x)))
    (eqToHom ⋯ ≫ ComposableArrows.hom (ComposableArrows.mk₁ (𝟙 x)) ≫ eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x : C
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C)
      (ComposableArrows.left.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : ComposableArrows C 0) → ComposableArrows C 1)
          (ComposableArrows.mk₀ x)))
      (ComposableArrows.right.{v, u} (n := 1)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : ComposableArrows C 0) → ComposableArrows C 1)
          (ComposableArrows.mk₀ x))))
    (ComposableArrows.hom
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
            (a : ComposableArrows C 0) → ComposableArrows C 1)
          (ComposableArrows.mk₀ x)) :
      Quiver.Hom.{v, u} (V := C)
        (ComposableArrows.left.{v, u} (n := 1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
              (a : ComposableArrows C 0) → ComposableArrows C 1)
            (ComposableArrows.mk₀ x)))
        (ComposableArrows.right.{v, u} (n := 1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
              (a : ComposableArrows C 0) → ComposableArrows C 1)
            (ComposableArrows.mk₀ x))))
    (eqToHom ⋯ :
      Quiver.Hom.{v, u} (V := C)
        (ComposableArrows.left.{v, u} (n := 1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
              (a : ComposableArrows C 0) → ComposableArrows C 1)
            (ComposableArrows.mk₀ x)))
        (ComposableArrows.right.{v, u} (n := 1)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.σ (nerve.{v, u} C) 0) :
              (a : ComposableArrows C 0) → ComposableArrows C 1)
            (ComposableArrows.mk₀ x))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
simp :
  ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
          (a : ComposableArrows C 2) → ComposableArrows C 1)
        (ComposableArrows.mk₂ f g)) =
    f
⊢ ComposableArrows.hom
      ((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⦌))
        (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ f).hom ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 2) :
          (a : ComposableArrows C 2) → ComposableArrows C 1)
        (ComposableArrows.mk₂ f g)) =
    f

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
simp :
  ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
          (a : ComposableArrows C 2) → ComposableArrows C 1)
        (ComposableArrows.mk₂ f g)) =
    g
⊢ ComposableArrows.hom
      ((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⦌))
        (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ g).hom ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
          (a : ComposableArrows C 2) → ComposableArrows C 1)
        (ComposableArrows.mk₂ f g)) =
    g

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
simp :
  ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
          (a : ComposableArrows C 2) → ComposableArrows C 1)
        (ComposableArrows.mk₂ f g)) =
    f ≫ g
⊢ ComposableArrows.hom
      ((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⦌))
        (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ (f ≫ g)).hom ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
          (a : ComposableArrows C 2) → ComposableArrows C 1)
        (ComposableArrows.mk₂ f g)) =
    f ≫ g

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Quiver.IsThin.{u, v} C
n : SimplexCategoryᵒᵖ
x y : (nerve.{v, u} C).obj n
h : x.obj = y.obj
⊢ ∀ (i : Fin ((unop n).len + 1)), x.obj i = y.obj i

Tactic:
simp [h]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Quiver.IsThin.{u, v} C
n : SimplexCategoryᵒᵖ
x y : (nerve.{v, u} C).obj n
h : x.obj = y.obj
⊢ ∀ (i : ℕ) (hi : i < (unop n).len),
    ComposableArrows.map' x i (i + 1) ⋯ hi = eqToHom ⋯ ≫ ComposableArrows.map' y i (i + 1) ⋯ hi ≫ eqToHom ⋯

Tactic:
subsingleton
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x y : ComposableArrows.{v, u} C 0
e : Edge (X := nerve.{v, u} C) x y
simp :
  ComposableArrows.left e.edge =
    (nerveEquiv : (a : ComposableArrows C 0) → C)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
            (a : nerve C _⦋0 + 1⦌) → nerve C _⦋0⦌)
          e.edge :
        nerve.{v, u} C _⦋0⦌)
⊢ ComposableArrows.left e.edge = (nerveEquiv : (a : ComposableArrows C 0) → C) x

Tactic:
simp only [← e.src_eq]

Premises used: SSet.Edge.src_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x y : ComposableArrows.{v, u} C 0
e : Edge (X := nerve.{v, u} C) x y
⊢ ComposableArrows.left e.edge =
    (nerveEquiv : (a : ComposableArrows C 0) → C)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 1) :
            (a : nerve C _⦋0 + 1⦌) → nerve C _⦋0⦌)
          e.edge :
        nerve.{v, u} C _⦋0⦌)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x y : ComposableArrows.{v, u} C 0
e : Edge (X := nerve.{v, u} C) x y
simp :
  ComposableArrows.right e.edge =
    (nerveEquiv : (a : ComposableArrows C 0) → C)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
            (a : nerve C _⦋0 + 1⦌) → nerve C _⦋0⦌)
          e.edge :
        nerve.{v, u} C _⦋0⦌)
⊢ ComposableArrows.right e.edge = (nerveEquiv : (a : ComposableArrows C 0) → C) y

Tactic:
simp only [← e.tgt_eq]

Premises used: SSet.Edge.tgt_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x y : ComposableArrows.{v, u} C 0
e : Edge (X := nerve.{v, u} C) x y
⊢ ComposableArrows.right e.edge =
    (nerveEquiv : (a : ComposableArrows C 0) → C)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ (nerve.{v, u} C) 0) :
            (a : nerve C _⦋0 + 1⦌) → nerve C _⦋0⦌)
          e.edge :
        nerve.{v, u} C _⦋0⦌)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
x y : ComposableArrows.{v, u} C 0
e : Edge (X := nerve.{v, u} C) x y
⊢ (nerveEquiv : (a : ComposableArrows C 0) → C) x = ComposableArrows.left e.edge

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
x y : ComposableArrows.{v, u} C 0
e : Edge (X := nerve.{v, u} C) x y
⊢ ComposableArrows.right e.edge = (nerveEquiv : (a : ComposableArrows C 0) → C) y

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
x y : ComposableArrows.{v, u} C 0
f :
  Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C)
    ((nerveEquiv : (a : ComposableArrows C 0) → C) y : C)
⊢ (fun (e : Edge (X := nerve.{v, u} C) x y) ↦ eqToHom ⋯ ≫ ComposableArrows.hom e.edge ≫ eqToHom ⋯)
      ((fun
            (f :
              Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C)
                ((nerveEquiv : (a : ComposableArrows C 0) → C) y : C)) ↦
          (Edge.mk (ComposableArrows.mk₁ f) ⋯ ⋯ : Edge (X := nerve.{v, u} C) x y))
        f) =
    f

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x y : ComposableArrows.{v, u} C 0
e : Edge (X := nerve.{v, u} C) x y
⊢ ComposableArrows.mk₁ (X₀ := (nerveEquiv : (a : ComposableArrows C 0) → C) x) (X₁ :=
      (nerveEquiv : (a : ComposableArrows C 0) → C) y)
      ((homEquiv :
          (a : Edge x y) →
            (nerveEquiv : (a : ComposableArrows C 0) → C) x ⟶ (nerveEquiv : (a : ComposableArrows C 0) → C) y)
        e) =
    ComposableArrows.mk₁ (ComposableArrows.hom e.edge)

Tactic:
simp [homEquiv, ComposableArrows.mk₁_eqToHom_comp, ComposableArrows.mk₁_comp_eqToHom]

Premises used: CategoryTheory.ComposableArrows.mk₁_eqToHom_comp, CategoryTheory.ComposableArrows.mk₁_comp_eqToHom, CategoryTheory.nerve.homEquiv
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x y : C
f : x ⟶ y
⊢ (edgeMk f).edge = ComposableArrows.mk₁ f

Tactic:
rfl

Premises used: SSet.Edge.edge, rfl, CategoryTheory.ComposableArrows.mk₁
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x y : C
e :
  Edge (X := nerve.{v, u} C) ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x)
    ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) y)
⊢ x =
    (nerveEquiv : (a : ComposableArrows C 0) → C)
      ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x y : C
e :
  Edge (X := nerve.{v, u} C) ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x)
    ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) y)
⊢ (nerveEquiv : (a : ComposableArrows C 0) → C)
      ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) y : ComposableArrows.{v, u} C 0) =
    y

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve
Goal:
C : Type u
inst : Category.{v, u} C
x : ComposableArrows.{v, u} C 0
obtain :
  ∀ (x : C),
    Eq.{v + 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))
      ((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))
          (Edge.id ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x)) :
        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))
      (𝟙
          ((nerveEquiv : (a : ComposableArrows C 0) → C)
            ((Equiv.symm nerveEquiv : (a : C) → ComposableArrows C 0) x : ComposableArrows.{v, u} C 0)) :
        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))
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C)
      ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C))
    ((homEquiv :
          (a : Edge x x) →
            (nerveEquiv : (a : ComposableArrows C 0) → C) x ⟶ (nerveEquiv : (a : ComposableArrows C 0) → C) x)
        (Edge.id x) :
      Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C))
    (𝟙 ((nerveEquiv : (a : ComposableArrows C 0) → C) x) :
      Quiver.Hom.{v, u} (V := C) ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C)
        ((nerveEquiv : (a : ComposableArrows C 0) → C) x : C))

Tactic:
obtain ⟨x, rfl⟩ := nerveEquiv.symm.surjective x

Premises used: CategoryTheory.nerveEquiv, Equiv.surjective, Equiv.symm, rfl
-- 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₂
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  (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⦌))
      (ComposableArrows.mk₂ f₀₁ f₁₂) =
    (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⦌))
      (ComposableArrows.mk₂ f₀₁ f₁₂) =
    (edgeMk f₁₂).edge

Tactic:
cat_disch
-- 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 : f₀₁ ≫ f₁₂ = f₀₂
rwa rwa₁ rwa₂ rwa₃ : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂))
⊢ (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)

Tactic:
rwa [← h]
-- 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₁₂) ⋯ ⋯ ⋯
refine :
  Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)) →
    ∀ (h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)), f₀₁ ≫ f₁₂ = f₀₂
⊢ Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)) ↔ f₀₁ ≫ f₁₂ = f₀₂

Tactic:
refine ⟨fun ⟨h⟩ ↦ ?_, fun h ↦ ⟨by rwa [← h]⟩⟩
-- 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₀₂)
rw : Arrow.mk (f₀₁ ≫ f₁₂) = Arrow.mk f₀₂
⊢ f₀₁ ≫ f₁₂ = f₀₂

Tactic:
rw [← Arrow.mk_inj]

Premises used: CategoryTheory.Arrow.mk_inj
-- 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₀₂)
a :
  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)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk f₀₂) :
      ComposableArrows.{v, u} C 1)
⊢ Arrow.mk (f₀₁ ≫ f₁₂) = Arrow.mk f₀₂

Tactic:
apply ComposableArrows.arrowEquiv.symm.injective

Premises used: CategoryTheory.ComposableArrows.arrowEquiv, 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₁₂)) :=
  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.{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⦌))
h₂ :
  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⦌))
a :
  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⦌))
⊢ 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)
    ((Equiv.symm ComposableArrows.arrowEquiv : (a : Arrow C) → ComposableArrows C 1) (Arrow.mk f₀₂) :
      ComposableArrows.{v, u} C 1)

Tactic:
convert_to (nerve C).δ 1 h'.simplex = (nerve C).δ 1 h.simplex

Premises used: CategoryTheory.ConcreteCategory.hom, SSet.Edge.CompStruct.simplex, CategoryTheory.nerve, CategoryTheory.SimplicialObject.δ, OfNat.ofNat, DFunLike.coe
-- 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:
(h'.d₁).symm

Premises used: SSet.Edge.CompStruct.d₁, Eq.symm, SSet.Edge.edge, CategoryTheory.ComposableArrows.mk₁