awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (goal)
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⦌))
⊢ 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)
have 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⦌))
Tactic: convert_to (nerve C).δ 1 h'.simplex = (nerve C).δ 1 h.simplex
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (hypothesis)
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₀₂)
⊢ 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⦌))
have 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
Tactic: have h₀ := h.d₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (hypothesis)
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
⊢ 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⦌))
have 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
Tactic: have h₂ := h.d₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (hypothesis)
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
⊢ 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⦌))
have 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
Tactic: have h'₀ := h'.d₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (hypothesis)
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
⊢ 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⦌))
have 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
Tactic: have h'₂ := h'.d₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (hypothesis)
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
⊢ 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⦌))
have h₁ : 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'₂
Cleared hypotheses: h₀, h₂, h'₀, h'₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (hypothesis)
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₁₂
⊢ 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⦌))
have h₃ : 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'₂
Cleared hypotheses: h₀, h₂, h'₀, h'₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (hypothesis)
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₀₁
⊢ 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⦌))
have h'₁ : 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'₂
Cleared hypotheses: h₀, h₂, h'₀, h'₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Nerve (hypothesis)
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₁₂
⊢ 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⦌))
have h'₃ : 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'₂
Cleared hypotheses: h₀, h₂, h'₀, h'₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (hypothesis)
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
y :
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
h' :
  ∀ {a b : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))}
    (e : Edge a b), ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
h₀ :
  ComposableArrows.mk₁ (X₀ :=
      F.obj
        (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 1 Edge._proof_1 Edge._proof_3).op) :
              (a : X.obj (op { obj := ⦋1⦌, property := Edge._proof_3 })) →
                X.obj (op { obj := ⦋0⦌, property := Edge._proof_1 }))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 _proof_2 _proof_5).op) :
                  (a : X.obj (op { obj := ⦋2⦌, property := _proof_5 })) →
                    X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
                h.simplex :
              X.obj
                (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋1⦌ _proof_2))))))
      (F.map
        (homMk
          (Edge.mk'
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (δ₂ 0 _proof_2 _proof_5).op) :
                (a : X.obj (op { obj := ⦋2⦌, property := _proof_5 })) → X.obj (op { obj := ⦋1⦌, property := _proof_2 }))
              h.simplex)))) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
⊢ ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)) = y
have h₁ : ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
  (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
      (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
        ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
    y
Tactic: rw [h.d₀, h'] at h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction (goal)
Goal:
X : Truncated 2
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : X.HomotopyCategory ⥤ C
y :
  Functor.obj (C := (SimplexCategory.Truncated 2)ᵒᵖ) (Functor.obj (truncation 2) (nerve C))
    (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋2⦌ _proof_4))
h' :
  ∀ {a b : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ ⋯))}
    (e : Edge a b), ComposableArrows.mk₁ (F.map (homMk (Edge.mk' e.edge))) = ComposableArrows.mk₁ (F.map (homMk e))
x₀ x₁ x₂ : X.obj (op (ObjectProperty.FullSubcategory.mk (P := fun (a : SimplexCategory) ↦ a.len ≤ 2) ⦋0⦌ Edge._proof_1))
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
h₂ :
  ComposableArrows.mk₁ (F.map (homMk e₀₁)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 2 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
h₀ :
  ComposableArrows.mk₁ (F.map (homMk e₁₂)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryTheory.Functor.map (Functor.obj (truncation 2) (nerve C)) (δ₂ 0 _proof_2 _proof_5).op) :
        (a : ((truncation 2).obj (nerve C)).obj (op { obj := ⦋2⦌, property := _proof_5 })) →
          ((truncation 2).obj (nerve C)).obj (op { obj := ⦋1⦌, property := _proof_2 }))
      y
⊢ ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂)) = y
have refine : spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 (ComposableArrows.mk₂ (F.map (homMk e₀₁)) (F.map (homMk e₁₂))) =
  spine (Functor.obj (truncation 2) (nerve C)) 2 _proof_4 y
Tactic: refine (spine_bijective (X := (truncation 2).obj (nerve C)) _ _).injective ?_