awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.unit.app x ≫ h.inverse.map (h.functor.map a) ≫ h.unitInv.app y =
    h.unit.app x ≫ h.inverse.map (h.functor.map b) ≫ h.unitInv.app y
have mp : h.functor.map a = h.functor.map b
Tactic: congr 3
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1})
x y : C
f : x ⟶ y :=
  have hx : x ⟶ h.inverse.obj { as := PUnit.unit } := Eq.mpr ⋯ (h.unit.app x);
  have hy : h.inverse.obj { as := PUnit.unit : Discrete PUnit.{w + 1} } ⟶ y := Eq.mpr ⋯ (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.functor.map a = h.functor.map b
have mp : ULift.down.{w, 0} (h.functor.map a) = ULift.down.{w, 0} (h.functor.map b)
Tactic: apply ULift.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
p : C
⊢ Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1}))
have mpr : ∀ (this : (x y : C) → Unique (x ⟶ y)), Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1}))
Tactic: haveI := fun x y => (h x y).some
-- Lean 4 proof step from Mathlib.CategoryTheory.PUnit (goal)
Goal:
C : Type u
inst : Category.{v, u} C
h : ∀ (x y : C), Nonempty.{max 1 (v + 1)} (Unique (x ⟶ y))
p : C
this : (x y : C) → Unique (x ⟶ y)
⊢ Nonempty (Equivalence.{v, w, u, w} C (Discrete PUnit.{w + 1}))
have mpr : Iso (C := Functor.{v, v, u, u} C C) (𝟭 C)
  (Functor.obj (Functor.const C) { as := PUnit.unit : Discrete PUnit.{w + 1} } ⋙
    Functor.obj (Functor.const (Discrete PUnit.{w + 1})) p)
Tactic: refine
      Nonempty.intro
        (CategoryTheory.Equivalence.mk ((Functor.const _).obj ⟨⟨⟩⟩)
          ((@Functor.const <| Discrete PUnit).obj p) ?_ (by apply Functor.punitExt))
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ Prefunctor.obj (of V) u) (q : u ⟶ v), P p → P (p ≫ Prefunctor.map (of V) q)
b : Paths V
f : a ⟶ b
⊢ P f
have nil : P Quiver.Path.nil
Tactic: induction f with
  | nil => exact id
  | cons _ w h => exact comp _ w h
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ Prefunctor.obj (of V) u) (q : u ⟶ v), P p → P (p ≫ Prefunctor.map (of V) q)
b : Paths V
f : a ⟶ b
nil : P Quiver.Path.nil
⊢ P f
have cons : ∀ {b c : Paths V} (a_1 : Quiver.Path.{v₁, u₁} a b) (w : b ⟶ c) (h : P a_1), P (a_1.cons w)
Tactic: induction f with
  | nil => exact id
  | cons _ w h => exact comp _ w h
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
a : Paths V
f : a ⟶ b
⊢ P f
have generalize : ∀ (k : ℕ) (h : Quiver.Path.length f = k), P f
Tactic: generalize h : f.length = k
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
a : Paths V
f : a ⟶ b
h : Quiver.Path.length f = 0
⊢ P f
have zero : ∀ (h : Quiver.Path.length.{u₁, v₁} (V := V) (a := b) Quiver.Path.nil = 0), P Quiver.Path.nil
Tactic: cases f with
    | nil => exact id
    | cons _ _ => simp at h
Cleared hypotheses: a, f, h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
a : Paths V
f : a ⟶ b
h : Quiver.Path.length f = 0
zero : ∀ (h : Quiver.Path.length.{u₁, v₁} (V := V) (a := b) Quiver.Path.nil = 0), P Quiver.Path.nil
⊢ P f
have zero₁ : ∀ {b_1 : Paths V} (a_1 : Quiver.Path.{v₁, u₁} a b_1) (a_2 : b_1 ⟶ b) (h : (a_1.cons a_2).length = 0), P (a_1.cons a_2)
Tactic: cases f with
    | nil => exact id
    | cons _ _ => simp at h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
k : ℕ
h' : ∀ {a : Paths V} (f : a ⟶ b) (h : Quiver.Path.length f = k), P f
a : Paths V
f : a ⟶ b
h : Quiver.Path.length f = k + 1
⊢ P f
have succ : ∀ (c : V) (f : a ⟶ c) (q : Quiver.Path.{v₁, u₁} c b) (hq : q.length = k) (h : (f.toPath.comp q).length = k + 1),
  P (f.toPath.comp q)
Tactic: obtain ⟨c, f, q, hq, rfl⟩ := f.eq_toPath_comp_of_length_eq_succ h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
a : Paths V
f : a ⟶ b
k : ℕ
h : Quiver.Path.length f = k
⊢ P f
have zero : ∀ {a : Paths V} (f : a ⟶ b) (h : Quiver.Path.length f = 0), P f
Tactic: induction k generalizing f a with
  | zero => cases f with
    | nil => exact id
    | cons _ _ => simp at h
  | succ k h' =>
    obtain ⟨c, f, q, hq, rfl⟩ := f.eq_toPath_comp_of_length_eq_succ h
    exact comp _ _ (h' _ hq)
Cleared hypotheses: a, f, k, h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
b : Paths V
P : {a : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 b)
comp : ∀ {u v : V} (p : Prefunctor.obj (of V) v ⟶ b) (q : u ⟶ v), P p → P (Prefunctor.map (of V) q ≫ p)
a : Paths V
f : a ⟶ b
k : ℕ
h : Quiver.Path.length f = k
zero : ∀ {a : Paths V} (f : a ⟶ b) (h : Quiver.Path.length f = 0), P f
⊢ P f
have succ : ∀ (k : ℕ) (h' : ∀ {a : Paths V} (f : a ⟶ b) (h : Quiver.Path.length f = k), P f) {a : Paths V} (f : a ⟶ b)
  (h : Quiver.Path.length f = k + 1), P f
Tactic: induction k generalizing f a with
  | zero => cases f with
    | nil => exact id
    | cons _ _ => simp at h
  | succ k h' =>
    obtain ⟨c, f, q, hq, rfl⟩ := f.eq_toPath_comp_of_length_eq_succ h
    exact comp _ _ (h' _ hq)
Cleared hypotheses: a, f, k, h
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 (Prefunctor.obj (of V) v))
comp :
  ∀ {u v w : V} (p : u ⟶ v) (q : Prefunctor.obj (of V) v ⟶ Prefunctor.obj (of V) w),
    P q → P (Prefunctor.map (of V) p ≫ q)
a b : Paths V
⊢ ∀ (f : a ⟶ b), P f
have revert : ∀ {a : Paths V} (f : a ⟶ b), P f
Tactic: revert a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
⊢ Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj Y)
    (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
        (f ≫ Quiver.Path.nil) :
      φ.obj X ⟶ φ.obj Y)
    (CategoryStruct.comp (Y := φ.obj Y)
        (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
          Quiver.Path.nil) :
      φ.obj X ⟶ φ.obj Y)
have nil : Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj Y)
  (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
      (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
      (f ≫ Quiver.Path.nil) :
    φ.obj X ⟶ φ.obj Y)
  (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
      (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f :
    φ.obj X ⟶ φ.obj Y)
Tactic: rw [Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (hypothesis)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
b c : Paths V
g' : Quiver.Path.{v₁, u₁} Y b
p : b ⟶ c
ih :
  Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj b)
    (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) (f ≫ g') :
      φ.obj X ⟶ φ.obj b)
    (CategoryStruct.comp (Y := φ.obj Y)
        (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g') :
      φ.obj X ⟶ φ.obj b)
⊢ Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj c)
    (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
        (f ≫ g'.cons p) :
      φ.obj X ⟶ φ.obj c)
    (CategoryStruct.comp (Y := φ.obj Y)
        (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
          (g'.cons p)) :
      φ.obj X ⟶ φ.obj c)
have this : f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p
Tactic: have : f ≫ Quiver.Path.cons g' p = (f ≫ g').cons p := by apply Quiver.Path.comp_cons
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
b c : Paths V
g' : Quiver.Path.{v₁, u₁} Y b
p : b ⟶ c
ih :
  Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj b)
    (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) (f ≫ g') :
      φ.obj X ⟶ φ.obj b)
    (CategoryStruct.comp (Y := φ.obj Y)
        (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g') :
      φ.obj X ⟶ φ.obj b)
this : f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p
⊢ Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj c)
    (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
        (f ≫ g'.cons p) :
      φ.obj X ⟶ φ.obj c)
    (CategoryStruct.comp (Y := φ.obj Y)
        (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
          (g'.cons p)) :
      φ.obj X ⟶ φ.obj c)
have cons : Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj c)
  (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
      (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
      (Quiver.Path.cons (f ≫ g') p) :
    φ.obj X ⟶ φ.obj c)
  (CategoryStruct.comp (Y := φ.obj Y)
      (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
      (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
        (g'.cons p)) :
    φ.obj X ⟶ φ.obj c)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
b c : Paths V
g' : Quiver.Path.{v₁, u₁} Y b
p : b ⟶ c
ih :
  Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj b)
    (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) (f ≫ g') :
      φ.obj X ⟶ φ.obj b)
    (CategoryStruct.comp (Y := φ.obj Y)
        (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g') :
      φ.obj X ⟶ φ.obj b)
this : f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p
⊢ Eq (α := φ.obj X ⟶ φ.obj c)
    (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) (f ≫ g') ≫
      φ.map p)
    (CategoryStruct.comp (Y := φ.obj Y)
      (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
      (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g' ≫
        φ.map p))
have cons : Eq (α := φ.obj X ⟶ φ.obj c)
  (CategoryStruct.comp (Y := φ.obj Y)
      (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
      (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g') ≫
    φ.map p)
  (CategoryStruct.comp (Y := φ.obj Y)
    (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
      (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
    (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g' ≫
      φ.map p))
Tactic: rw [ih, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y Z : Paths V
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj Z)
    (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) (f ≫ g) :
      φ.obj X ⟶ φ.obj Z)
    (CategoryStruct.comp (Y := φ.obj Y)
        (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
        (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
          (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f) g) :
      φ.obj X ⟶ φ.obj Z)
have nil : Eq.{v_1 + 1} (α := φ.obj X ⟶ φ.obj Y)
  (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
      (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
      (f ≫ Quiver.Path.nil) :
    φ.obj X ⟶ φ.obj Y)
  (CategoryStruct.comp (Y := φ.obj Y)
      (Quiver.Path.rec (motive := fun (Y : V) (x : Quiver.Path.{v₁, u₁} X Y) ↦ φ.obj X ⟶ φ.obj Y) (𝟙 (φ.obj X))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} X b) (f : b ⟶ c) (ihp : φ.obj X ⟶ φ.obj b) ↦ ihp ≫ φ.map f) f)
      (Quiver.Path.rec (motive := fun (Y_1 : V) (x : Quiver.Path.{v₁, u₁} Y Y_1) ↦ φ.obj Y ⟶ φ.obj Y_1) (𝟙 (φ.obj Y))
        (fun {b c : V} (x : Quiver.Path.{v₁, u₁} Y b) (f : b ⟶ c) (ihp : φ.obj Y ⟶ φ.obj b) ↦ ihp ≫ φ.map f)
        Quiver.Path.nil) :
    φ.obj X ⟶ φ.obj Y)
Tactic: induction g with
    | nil =>
      rw [Category.comp_id]
      rfl
    | cons g' p ih =>
      have : f ≫ Quiver.Path.cons g' p = (f ≫ g').cons p := by apply Quiver.Path.comp_cons
      rw [this]
      simp only at ih ⊢
      rw [ih, Category.assoc]
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y : V
f : X ⟶ Y
⊢ (lift φ).map f.toPath = φ.map f
have dsimp : 𝟙 (φ.obj X) ≫ φ.map f = φ.map f
Tactic: dsimp [Quiver.Hom.toPath, lift]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
⊢ of V ⋙q (lift φ).toPrefunctor = φ
have h_obj : ∀ (X : V), (of V ⋙q (lift φ).toPrefunctor).obj X = φ.obj X
Tactic: fapply Prefunctor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
h_obj : ∀ (X : V), (of V ⋙q (lift φ).toPrefunctor).obj X = φ.obj X
⊢ of V ⋙q (lift φ).toPrefunctor = φ
have h_map : ∀ (X Y : V) (f : X ⟶ Y),
  (of V ⋙q (lift φ).toPrefunctor).map f =
    Eq.recOn (motive := fun (x : C) (x_1 : φ.obj Y = x) ↦ (of V ⋙q (lift φ).toPrefunctor).obj X ⟶ x) sorry
      (Eq.recOn (motive := fun (x : C) (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) sorry (φ.map f))
Tactic: fapply Prefunctor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
X Y : V
f : X ⟶ Y
⊢ (of V ⋙q (lift φ).toPrefunctor).map f =
    Eq.recOn (motive := fun (x : C) (x_1 : φ.obj Y = x) ↦ (of V ⋙q (lift φ).toPrefunctor).obj X ⟶ x) ⋯
      (Eq.recOn (motive := fun (x : C) (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) ⋯ (φ.map f))
have h_map : ∀ (φo : V → C) (φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)),
  (of V ⋙q (lift { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }).toPrefunctor).map f =
    Eq.recOn (motive := fun (x : C) (x_1 : { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj Y = x) ↦
      (of V ⋙q (lift { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }).toPrefunctor).obj X ⟶ x) sorry
      (Eq.recOn (motive := fun (x : C) (x_1 : { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj X = x) ↦
        x ⟶ { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj Y) sorry
        ({ obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.map f))
Tactic: rcases φ with ⟨φo, φm⟩
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
⊢ (of V ⋙q (lift { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }).toPrefunctor).map f =
    Eq.recOn (motive := fun (x : C) (x_1 : { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj Y = x) ↦
      (of V ⋙q (lift { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }).toPrefunctor).obj X ⟶ x) ⋯
      (Eq.recOn (motive := fun (x : C) (x_1 : { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj X = x) ↦
        x ⟶ { obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.obj Y) ⋯
        ({ obj := φo, map := @φm : Prefunctor.{v₁, v_1, u₁, u_1} V C }.map f))
have h_map : 𝟙 (φo X) ≫ φm f = φm f
Tactic: dsimp [lift, Quiver.Hom.toPath]
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
φ : Prefunctor.{v₁, v_1, u₁, u_1} V C
Φ : Paths V ⥤ C
hΦ : of V ⋙q Φ.toPrefunctor = φ
⊢ Φ = lift φ
have subst_vars : Φ = lift (of V ⋙q Φ.toPrefunctor)
Tactic: subst_vars
Cleared hypotheses: φ, hΦ
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ Φ = lift (of V ⋙q Φ.toPrefunctor)
have h_obj : ∀ (X : Paths V), Φ.obj X = (lift (of V ⋙q Φ.toPrefunctor)).obj X
Tactic: fapply Functor.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.PathCategory.Basic (goal)
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
C : Type u_1
inst_1 : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
h_obj : ∀ (X : Paths V), Φ.obj X = (lift (of V ⋙q Φ.toPrefunctor)).obj X
⊢ Φ = lift (of V ⋙q Φ.toPrefunctor)
have h_map : autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom sorry ≫ (lift (of V ⋙q Φ.toPrefunctor)).map f ≫ eqToHom sorry)
  Functor.ext._auto_1
Tactic: fapply Functor.ext