awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V_1 : Type u
inst : Quiver V_1
a b c d : V_1
inst_1 : ∀ (a b : V_1), Subsingleton (a ⟶ b)
V : Type u_1
inst_2 : Quiver.{u_2, u_1} V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths.{u_1, u_2} v w n)
v w : V
p q : Path.{u_2, u_1} v w
a_1 x v' v'' : V
x_1 x_2 : BoundedPaths.{u_1, u_2} a_1 x (n + 1)
a_2 : V
p' : Path.{u_2, u_1} a_1 a_2
α : a_2 ⟶ x
q' : Path.{u_2, u_1} a_1 a_2
β : a_2 ⟶ x
hp : (p'.cons α).length ≤ n + 1
hq : (q'.cons β).length ≤ n + 1
h : α = β
hp' : p'.length ≤ n
hq' : q'.length ≤ n
h'' :
  Eq (α := { p : Path.{u_2, u_1} a_1 a_2 // p.length ≤ n })
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 a_2) ↦ p.length ≤ n) p' hp')
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 a_2) ↦ p.length ≤ n) q' hq')
a₁ :
  (↑(Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ n + 1) (p'.cons α) hp) : Path a_1 x) =
    (↑(Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ n + 1) (q'.cons β) hq) : Path a_1 x)
⊢ Eq (α := BoundedPaths.{u_1, u_2} a_1 x (n + 1))
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ n + 1) (p'.cons α) hp)
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 x) ↦ p.length ≤ n + 1) (q'.cons β) hq)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V_1 : Type u
inst : Quiver V_1
a b c d : V_1
inst_1 : ∀ (a b : V_1), Subsingleton (a ⟶ b)
V : Type u_1
inst_2 : Quiver.{u_2, u_1} V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths.{u_1, u_2} v w n)
v w : V
p q : Path.{u_2, u_1} v w
a_1 x v' v'' : V
x_1 x_2 : BoundedPaths.{u_1, u_2} a_1 x (n + 1)
a_2 : V
p' : Path.{u_2, u_1} a_1 a_2
α : a_2 ⟶ x
q' : Path.{u_2, u_1} a_1 a_2
β : a_2 ⟶ x
hp : (p'.cons α).length ≤ n + 1
hq : (q'.cons β).length ≤ n + 1
h : α = β
hp' : p'.length ≤ n
hq' : q'.length ≤ n
h'' :
  Eq (α := { p : Path.{u_2, u_1} a_1 a_2 // p.length ≤ n })
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 a_2) ↦ p.length ≤ n) p' hp')
    (Subtype.mk (p := fun (p : Path.{u_2, u_1} a_1 a_2) ↦ p.length ≤ n) q' hq')
a₁ : p'.cons β = q'.cons β
a₂ a₃ : q'.cons β = q'.cons β
⊢ p'.cons α = q'.cons β

Tactic:
rw [h, show p' = q' from Subtype.mk.inj h'']

Premises used: Subtype.mk.inj
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F : Prefunctor.{v₁, v₂, u₁, u₂} V W
a : V
⊢ Eq (α := Path.{v₂, u₂} (F.obj a) (F.obj a)) (F.mapPath Path.nil) Path.nil

Tactic:
rfl

Premises used: Prefunctor.mapPath, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F : Prefunctor.{v₁, v₂, u₁, u₂} V W
a b c : V
p : Path.{v₁, u₁} a b
e : b ⟶ c
⊢ F.mapPath (p.cons e) = (F.mapPath p).cons (F.map e)

Tactic:
rfl

Premises used: Prefunctor.mapPath, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F : Prefunctor.{v₁, v₂, u₁, u₂} V W
a b : V
p : Path.{v₁, u₁} a b
c b_1 : V
q : Path.{v₁, u₁} b b_1
e : b_1 ⟶ c
rw rw₁ : ((F.mapPath p).comp (F.mapPath q)).cons (F.map e) = ((F.mapPath p).comp (F.mapPath q)).cons (F.map e)
⊢ (F.mapPath (p.comp q)).cons (F.map e) = ((F.mapPath p).comp (F.mapPath q)).cons (F.map e)

Tactic:
rw [mapPath_comp p q]
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F : Prefunctor.{v₁, v₂, u₁, u₂} V W
a b : V
f : a ⟶ b
⊢ F.mapPath f.toPath = (F.map f).toPath

Tactic:
rfl

Premises used: Quiver.Hom.toPath, Prefunctor.mapPath, rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
a b_1 b b_2 : V
q : Path.{v₁, u₁} a b_2
e : b_2 ⟶ b
dsimp : Path.cons (mapPath (𝟭q V) q) e = q.cons e
⊢ mapPath (𝟭q V) (q.cons e) = q.cons e

Tactic:
dsimp
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
a b_1 b b_2 : V
q : Path.{v₁, u₁} a b_2
e : b_2 ⟶ b
rw rw₁ : q.cons e = q.cons e
⊢ Path.cons (mapPath (𝟭q V) q) e = q.cons e

Tactic:
rw [mapPath_id q]
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F : Prefunctor.{v₁, v₂, u₁, u₂} V W
U : Type u₃
inst_2 : Quiver.{v₃, u₃} U
G : Prefunctor.{v₂, v₃, u₂, u₃} W U
a b : V
⊢ Eq (α := Path.{v₃, u₃} ((F ⋙q G).obj a) ((F ⋙q G).obj a)) ((F ⋙q G).mapPath Path.nil) (G.mapPath (F.mapPath Path.nil))

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F : Prefunctor.{v₁, v₂, u₁, u₂} V W
U : Type u₃
inst_2 : Quiver.{v₃, u₃} U
G : Prefunctor.{v₂, v₃, u₂, u₃} W U
a b b_1 c : V
x : Path.{v₁, u₁} a b_1
y : b_1 ⟶ c
h : (F ⋙q G).mapPath x = G.mapPath (F.mapPath x)
⊢ (F ⋙q G).mapPath (x.cons y) = G.mapPath (F.mapPath (x.cons y))

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Quiver.Path
Goal:
V : Type u₁
inst : Quiver.{v₁, u₁} V
W : Type u₂
inst_1 : Quiver.{v₂, u₂} W
F : Prefunctor.{v₁, v₂, u₁, u₂} V W
U : Type u₃
inst_2 : Quiver.{v₃, u₃} U
G : Prefunctor.{v₂, v₃, u₂, u₃} W U
a b : V
p : Path.{v₁, u₁} a b
nil :
  Eq (α := Path.{v₃, u₃} ((F ⋙q G).obj a) ((F ⋙q G).obj a)) ((F ⋙q G).mapPath Path.nil) (G.mapPath (F.mapPath Path.nil))
cons :
  ∀ {b c : V} (x : Path.{v₁, u₁} a b) (y : b ⟶ c) (h : (F ⋙q G).mapPath x = G.mapPath (F.mapPath x)),
    (F ⋙q G).mapPath (x.cons y) = G.mapPath (F.mapPath (x.cons y))
⊢ (F ⋙q G).mapPath p = G.mapPath (F.mapPath p)

Tactic:
induction p with
  | nil => rfl
  | cons x y h => simp [h]
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
Goal:
V : Type u_1
W : Type u_2
inst : Quiver.{u_3, u_1} V
inst_1 : Quiver.{u_4, u_2} W
obj : V → W
map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)
X : V
⊢ { obj := obj, map := @map : Prefunctor.{u_3, u_4, u_1, u_2} V W }.obj X = obj X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
Goal:
V : Type u_1
W : Type u_2
inst : Quiver.{u_3, u_1} V
inst_1 : Quiver.{u_4, u_2} W
obj : V → W
map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)
X Y : V
f : X ⟶ Y
⊢ { obj := obj, map := @map : Prefunctor.{u_3, u_4, u_1, u_2} V W }.map f = map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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))
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) ⋯
            (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
⊢ F = G

Tactic:
obtain ⟨F_obj, _⟩ := F
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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))
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) ⋯
            (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 }
⊢ { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W } = G

Tactic:
obtain ⟨G_obj, _⟩ := G
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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))
h : ∀ (X : V), F_obj X = G_obj X
⊢ F_obj = G_obj

Tactic:
ext X
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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))
X : V
⊢ F_obj X = G_obj X

Tactic:
apply h_obj
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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))
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) ⋯
            (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) ⋯
              ({ 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 }
⊢ { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W } = { obj := G_obj, map := @map_1 }

Tactic:
obtain rfl : F_obj = G_obj := by
    ext X
    apply h_obj

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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))
e_map : @map = @map_1
⊢ { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W } = { obj := F_obj, map := @map_1 }

Tactic:
congr
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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))
e_map : ∀ (X Y : V) (f : X ⟶ Y), map f = map_1 f
⊢ @map = @map_1

Tactic:
funext X Y f
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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))
X Y : V
f : X ⟶ Y
⊢ map f = map_1 f

Tactic:
simpa using h_map X Y f
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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) ⋯ ⋯
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) ⋯ ⋯),
    { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = G
⊢ F = G

Tactic:
obtain ⟨Fobj, Fmap⟩ := F
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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) ⋯ ⋯
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) ⋯ ⋯),
    { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = { obj := Gobj, map := @Gmap }
⊢ { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = G

Tactic:
obtain ⟨Gobj, Gmap⟩ := G
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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) ⋯ ⋯
⊢ Fobj = Gobj

Tactic:
funext h_obj

Premises used: funext
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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) ⋯ ⋯
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) ⋯ ⋯),
    { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = { obj := Fobj, map := @Gmap }
⊢ { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = { obj := Gobj, map := @Gmap }

Tactic:
obtain rfl : Fobj = Gobj := funext h_obj

Premises used: funext, rfl
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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) ⋯ ⋯
simp : @Fmap = @Gmap
⊢ { obj := Fobj, map := @Fmap : Prefunctor.{u_1, u_2, u, u} V W } = { obj := Fobj, map := @Gmap }

Tactic:
simp only [mk.injEq, heq_eq_eq, true_and]

Premises used: heq_eq_eq, Prefunctor.mk.injEq, true_and
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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) ⋯ ⋯
h : ∀ (X Y : V) (f : X ⟶ Y), Fmap f = Gmap f
⊢ @Fmap = @Gmap

Tactic:
ext X Y f
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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) ⋯ ⋯
X Y : V
f : X ⟶ Y
⊢ Fmap f = Gmap f

Tactic:
simpa only [Quiver.homOfEq_rfl] using h_map X Y f

Premises used: Quiver.homOfEq_rfl
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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
⊢ F.comp (id V) = F

Tactic:
rfl

Premises used: Prefunctor.comp, rfl
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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
⊢ comp (id U) F = F

Tactic:
rfl

Premises used: Prefunctor.comp, rfl
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
Goal:
U : Type u_1
V : Type u_2
W : Type u_3
Z : Type u_4
inst : Quiver.{u_5, u_1} U
inst_1 : Quiver.{u_6, u_2} V
inst_2 : Quiver.{u_7, u_3} W
inst_3 : Quiver.{u_8, u_4} Z
F : Prefunctor.{u_5, u_6, u_1, u_2} U V
G : Prefunctor.{u_6, u_7, u_2, u_3} V W
H : Prefunctor.{u_7, u_8, u_3, u_4} W Z
⊢ (F.comp G).comp H = F.comp (G.comp H)

Tactic:
rfl

Premises used: Prefunctor.comp, rfl
-- Module: Mathlib.Combinatorics.Quiver.Prefunctor
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
rw rw₁ : F.map g = F.map g
⊢ F.map f = F.map g

Tactic:
rw [h]