awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
V : Type u
inst : Quiver.{v₁, u} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F G : Prefunctor.{v₁, v₂, u, u₂} V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    F.map f =
      Eq.recOn (motive := fun (x : W) (x_1 : G.obj Y = x) ↦ F.obj X ⟶ x) ⋯
        (Eq.recOn (motive := fun (x : W) (x_1 : G.obj X = x) ↦ x ⟶ G.obj Y) ⋯ (G.map f))
⊢ F = G
have obtain : ∀ (F_obj : V → W) (map : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y))
  (h_obj : ∀ (X : V), { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X = G.obj X)
  (h_map :
    ∀ (X Y : V) (f : X ⟶ Y),
      { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map f =
        Eq.recOn (motive := fun (x : W) (x_1 : G.obj Y = x) ↦
          { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) sorry
          (Eq.recOn (motive := fun (x : W) (x_1 : G.obj X = x) ↦ x ⟶ G.obj Y) sorry (G.map f))),
  { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W } = G
Tactic: obtain ⟨F_obj, _⟩ := F
Cleared hypotheses: F, h_obj, h_map
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
V : Type u
inst : Quiver.{v₁, u} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
G : Prefunctor.{v₁, v₂, u, u₂} V W
F_obj : V → W
map : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj : ∀ (X : V), { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X = G.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map f =
      Eq.recOn (motive := fun (x : W) (x_1 : G.obj Y = x) ↦
        { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) ⋯
        (Eq.recOn (motive := fun (x : W) (x_1 : G.obj X = x) ↦ x ⟶ G.obj Y) ⋯ (G.map f))
⊢ { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W } = G
have obtain : ∀ (G_obj : V → W) (map_1 : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y))
  (h_obj :
    ∀ (X : V),
      { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X =
        { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
  (h_map :
    ∀ (X Y : V) (f : X ⟶ Y),
      { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map f =
        Eq.recOn (motive :=
          fun (x : W) (x_1 : { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
          { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) sorry
          (Eq.recOn (motive :=
            fun (x : W) (x_1 : { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
            x ⟶ { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y) sorry
            ({ obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map f))),
  { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W } = { obj := G_obj, map := @map_1 }
Tactic: obtain ⟨G_obj, _⟩ := G
Cleared hypotheses: G, h_obj, h_map
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
V : Type u
inst : Quiver.{v₁, u} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F_obj : V → W
map : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map_1 : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X =
      { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map f =
      Eq.recOn (motive :=
        fun (x : W) (x_1 : { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
        { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) ⋯
        (Eq.recOn (motive :=
          fun (x : W) (x_1 : { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
          x ⟶ { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y) ⋯
          ({ obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map f))
⊢ F_obj = G_obj
have h : ∀ (X : V), F_obj X = G_obj X
Tactic: ext X
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
V : Type u
inst : Quiver.{v₁, u} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F_obj : V → W
map : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
G_obj : V → W
map_1 : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X =
      { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map f =
      Eq.recOn (motive :=
        fun (x : W) (x_1 : { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
        { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) ⋯
        (Eq.recOn (motive :=
          fun (x : W) (x_1 : { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
          x ⟶ { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y) ⋯
          ({ obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map f))
⊢ { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W } = { obj := G_obj, map := @map_1 }
have obtain : ∀ (map_2 : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y))
  (h_obj :
    ∀ (X : V),
      { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X =
        { obj := F_obj, map := @map_2 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
  (h_map :
    ∀ (X Y : V) (f : X ⟶ Y),
      { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map f =
        Eq.recOn (motive :=
          fun (x : W) (x_1 : { obj := F_obj, map := @map_2 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
          { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) sorry
          (Eq.recOn (motive :=
            fun (x : W) (x_1 : { obj := F_obj, map := @map_2 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
            x ⟶ { obj := F_obj, map := @map_2 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y) sorry
            ({ obj := F_obj, map := @map_2 : Prefunctor.{v₁, v₂, u, u₂} V W }.map f))),
  { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W } = { obj := F_obj, map := @map_2 }
Tactic: obtain rfl : F_obj = G_obj := by
    ext X
    apply h_obj
Cleared hypotheses: G_obj, map_1, h_obj, h_map
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
V : Type u
inst : Quiver.{v₁, u} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F_obj : V → W
map map_1 : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X =
      { obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map f =
      Eq.recOn (motive :=
        fun (x : W) (x_1 : { obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
        { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) ⋯
        (Eq.recOn (motive :=
          fun (x : W) (x_1 : { obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
          x ⟶ { obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y) ⋯
          ({ obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map f))
⊢ { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W } = { obj := F_obj, map := @map_1 }
have e_map : @map = @map_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
V : Type u
inst : Quiver.{v₁, u} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F_obj : V → W
map map_1 : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X =
      { obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map f =
      Eq.recOn (motive :=
        fun (x : W) (x_1 : { obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
        { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) ⋯
        (Eq.recOn (motive :=
          fun (x : W) (x_1 : { obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
          x ⟶ { obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj Y) ⋯
          ({ obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map f))
⊢ @map = @map_1
have e_map : ∀ (X Y : V) (f : X ⟶ Y), map f = map_1 f
Tactic: funext X Y f
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_2, u} W
F G : Prefunctor.{u_1, u_2, u, u} V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ F = G
have obtain : ∀ (Fobj : V → W) (Fmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y))
  (h_obj : ∀ (X : V), { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X = G.obj X)
  (h_map :
    ∀ (X Y : V) (f : X ⟶ Y),
      { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.map f = Quiver.homOfEq (G.map f) sorry sorry),
  { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = G
Tactic: obtain ⟨Fobj, Fmap⟩ := F
Cleared hypotheses: F, h_obj, h_map
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_2, u} W
G : Prefunctor.{u_1, u_2, u, u} V W
Fobj : V → W
Fmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X = G.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = G
have obtain : ∀ (Gobj : V → W) (Gmap : {X Y : V} → (X ⟶ Y) → (Gobj X ⟶ Gobj Y))
  (h_obj :
    ∀ (X : V),
      { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X =
        { obj := Gobj, map := @Gmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X)
  (h_map :
    ∀ (X Y : V) (f : X ⟶ Y),
      { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.map f =
        Quiver.homOfEq ({ obj := Gobj, map := @Gmap : Prefunctor.{u_1, u_2, u, u} V W }.map f) sorry sorry),
  { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = { obj := Gobj, map := @Gmap }
Tactic: obtain ⟨Gobj, Gmap⟩ := G
Cleared hypotheses: G, h_obj, h_map
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_2, u} W
Fobj : V → W
Fmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
Gobj : V → W
Gmap : {X Y : V} → (X ⟶ Y) → (Gobj X ⟶ Gobj Y)
h_obj :
  ∀ (X : V),
    { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X =
      { obj := Gobj, map := @Gmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.map f =
      Quiver.homOfEq ({ obj := Gobj, map := @Gmap : Prefunctor.{u_1, u_2, u, u} V W }.map f) ⋯ ⋯
⊢ { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = { obj := Gobj, map := @Gmap }
have obtain : ∀ (Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y))
  (h_obj :
    ∀ (X : V),
      { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X =
        { obj := Fobj, map := @Gmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X)
  (h_map :
    ∀ (X Y : V) (f : X ⟶ Y),
      { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.map f =
        Quiver.homOfEq ({ obj := Fobj, map := @Gmap : Prefunctor.{u_1, u_2, u, u} V W }.map f) sorry sorry),
  { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = { obj := Fobj, map := @Gmap }
Tactic: obtain rfl : Fobj = Gobj := funext h_obj
Cleared hypotheses: Gobj, Gmap, h_obj, h_map
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_2, u} W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj :
  ∀ (X : V),
    { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X =
      { obj := Fobj, map := @Gmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.map f =
      Quiver.homOfEq ({ obj := Fobj, map := @Gmap : Prefunctor.{u_1, u_2, u, u} V W }.map f) ⋯ ⋯
⊢ { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = { obj := Fobj, map := @Gmap }
have simp : @Fmap = @Gmap
Tactic: simp only [mk.injEq, heq_eq_eq, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_2, u} W
Fobj : V → W
Fmap Gmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj :
  ∀ (X : V),
    { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X =
      { obj := Fobj, map := @Gmap : Prefunctor.{u_1, u_2, u, u} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W }.map f =
      Quiver.homOfEq ({ obj := Fobj, map := @Gmap : Prefunctor.{u_1, u_2, u, u} V W }.map f) ⋯ ⋯
⊢ @Fmap = @Gmap
have h : ∀ (X Y : V) (f : X ⟶ Y), Fmap f = Gmap f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
U : Type u_1
V : Type u_2
inst : Quiver.{u_3, u_1} U
inst_1 : Quiver.{u_4, u_2} V
F : Prefunctor.{u_3, u_4, u_1, u_2} U V
X Y : U
f g : X ⟶ Y
h : f = g
⊢ F.map f = F.map g
have rw : F.map g = F.map g
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
U : Type u_1
V : Type u_2
inst : Quiver.{u_3, u_1} U
inst_1 : Quiver.{u_4, u_2} V
F G : Prefunctor.{u_3, u_4, u_1, u_2} U V
e : F = G
X : U
⊢ F.obj X = G.obj X
have refl : F.obj X = F.obj X
Tactic: cases e
Cleared hypotheses: G, e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
U : Type u_1
V : Type u_2
inst : Quiver.{u_3, u_1} U
inst_1 : Quiver.{u_4, u_2} V
F G : Prefunctor.{u_3, u_4, u_1, u_2} U V
e : F = G
X Y : U
f : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f
have subst : Quiver.homOfEq (F.map f) sorry sorry = F.map f
Tactic: subst e
Cleared hypotheses: G, e
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Prefunctor (goal)
Goal:
U : Type u_1
V : Type u_2
inst : Quiver.{u_3, u_1} U
inst_1 : Quiver.{u_4, u_2} V
F : Prefunctor.{u_3, u_4, u_1, u_2} U V
X Y : U
f : X ⟶ Y
X' Y' : U
hX : X = X'
hY : Y = Y'
⊢ F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) ⋯ ⋯
have subst : F.map (Quiver.homOfEq f sorry sorry) = Quiver.homOfEq (F.map f) sorry sorry
Tactic: subst hX hY
Cleared hypotheses: X', Y', hX, hY
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ τ (σ X) ⟶ τ (σ Y)
have rw : φ.obj X ⟶ φ.obj Y
Tactic: rw [← h X, ← h Y]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ of σ ⋙q lift σ φ τ h = φ
have h_obj : ∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
Tactic: fapply Prefunctor.ext
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
h_obj : ∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
⊢ of σ ⋙q lift σ φ τ h = φ
have h_map : ∀ (X Y : V) (f : X ⟶ Y),
  (of σ ⋙q lift σ φ τ h).map f =
    Eq.recOn (motive := fun (x : W') (x_1 : φ.obj Y = x) ↦ (of σ ⋙q lift σ φ τ h).obj X ⟶ x) sorry
      (Eq.recOn (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) sorry (φ.map f))
Tactic: fapply Prefunctor.ext
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
have h_obj : (lift σ φ τ h).obj (Prefunctor.obj (of σ) X) = φ.obj X
Tactic: simp only [Prefunctor.comp_obj]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (lift σ φ τ h).obj (Prefunctor.obj (of σ) X) = φ.obj X
have h_obj : φ.obj X = (lift σ φ τ h).obj (Prefunctor.obj (of σ) X)
Tactic: apply Eq.symm
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (of σ ⋙q lift σ φ τ h).map f =
    Eq.recOn (motive := fun (x : W') (x_1 : φ.obj Y = x) ↦ (of σ ⋙q lift σ φ τ h).obj X ⟶ x) ⋯
      (Eq.recOn (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) ⋯ (φ.map f))
have h_map : Eq (α := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y) ((lift σ φ τ h).map (Prefunctor.map (of σ) f))
  (Eq.rec (motive := fun (x : W') (x_1 : φ.obj Y = x) ↦ (of σ ⋙q lift σ φ τ h).obj X ⟶ x)
    (Eq.rec (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) (φ.map f) sorry) sorry)
Tactic: simp only [Prefunctor.comp_map]
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ Eq (α := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y) ((lift σ φ τ h).map (Prefunctor.map (of σ) f))
    (Eq.rec (motive := fun (x : W') (x_1 : φ.obj Y = x) ↦ (of σ ⋙q lift σ φ τ h).obj X ⟶ x)
      (Eq.rec (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) (φ.map f) ⋯) ⋯)
have h_map : HEq (α := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y) ((lift σ φ τ h).map (Prefunctor.map (of σ) f))
  (β := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
  (Eq.rec (motive := fun (x : W') (x_1 : φ.obj Y = x) ↦ (of σ ⋙q lift σ φ τ h).obj X ⟶ x)
      (Eq.rec (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) (φ.map f) sorry) sorry :
    (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
Tactic: apply eq_of_heq
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (α := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y) ((lift σ φ τ h).map (Prefunctor.map (of σ) f))
    (β := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
    (Eq.rec (motive := fun (x : W') (x_1 : φ.obj Y = x) ↦ (of σ ⋙q lift σ φ τ h).obj X ⟶ x)
        (Eq.rec (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) (φ.map f) ⋯) ⋯ :
      (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
have h_map : HEq (sorry.mpr (φ.map f)) (β := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
  (Eq.rec (motive := fun (x : W') (x_1 : φ.obj Y = x) ↦ (of σ ⋙q lift σ φ τ h).obj X ⟶ x)
      (Eq.rec (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) (φ.map f) sorry) sorry :
    (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
Tactic: apply (cast_heq _ _).trans
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (⋯.mpr (φ.map f)) (β := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
    (Eq.rec (motive := fun (x : W') (x_1 : φ.obj Y = x) ↦ (of σ ⋙q lift σ φ τ h).obj X ⟶ x)
        (Eq.rec (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) (φ.map f) ⋯) ⋯ :
      (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
have h_map : HEq (φ.map f) (β := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
  (Eq.rec (motive := fun (x : W') (x_1 : φ.obj Y = x) ↦ (of σ ⋙q lift σ φ τ h).obj X ⟶ x)
      (Eq.rec (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) (φ.map f) sorry) sorry :
    (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
Tactic: apply (cast_heq _ _).trans
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (α := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y) ((lift σ φ τ h).map (Prefunctor.map (of σ) f))
    (β := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
    (Eq.rec (motive := fun (x : W') (x_1 : φ.obj Y = x) ↦ (of σ ⋙q lift σ φ τ h).obj X ⟶ x)
        (Eq.rec (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) (φ.map f) ⋯) ⋯ :
      (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
have h_map : HEq (φ.map f) (β := (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
  (Eq.rec (motive := fun (x : W') (x_1 : φ.obj Y = x) ↦ (of σ ⋙q lift σ φ τ h).obj X ⟶ x)
      (Eq.rec (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) (φ.map f) sorry) sorry :
    (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj Y)
Tactic: iterate 2 apply (cast_heq _ _).trans
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ Φ =
    { obj := τ,
      map :=
        @PushQuiver.rec V inst W σ (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ τ X ⟶ τ Y)
          fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr (φ.map f))) }
have h_obj : ∀ (X : Push σ),
  Φ.obj X =
    Prefunctor.obj
      { obj := τ,
        map :=
          @PushQuiver.rec V inst W σ (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ τ X ⟶ τ Y)
            fun (X Y : V) (f : X ⟶ Y) ↦ id (sorry.mpr (sorry.mpr (φ.map f))) }
      X
Tactic: fapply Prefunctor.ext
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X =
    Prefunctor.obj
      { obj := τ,
        map :=
          @PushQuiver.rec V inst W σ (fun (X Y : W) (x : PushQuiver.{u_4, u_1, u_2} σ X Y) ↦ τ X ⟶ τ Y)
            fun (X Y : V) (f : X ⟶ Y) ↦ id (⋯.mpr (⋯.mpr (φ.map f))) }
      X
have h_obj : Φ.obj X = τ X
Tactic: simp only
-- Lean 4 proof step from Mathlib.Combinatorics.Quiver.Push (goal)
Goal:
V : Type u_1
inst : Quiver.{u_4, u_1} V
W : Type u_2
σ : V → W
W' : Type u_3
inst_1 : Quiver.{u_5, u_3} W'
φ : Prefunctor.{u_4, u_5, u_1, u_3} V W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X = τ X
have h_obj : τ X = τ X
Tactic: rw [Φ₀]