awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 G : Prefunctor.{u_3, u_4, u_1, u_2} U V
e : F = G
X : U
refl : F.obj X = F.obj X
⊢ F.obj X = G.obj X

Tactic:
cases e
-- 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 : U
⊢ F.obj X = F.obj X

Tactic:
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 G : Prefunctor.{u_3, u_4, u_1, u_2} U V
e : F = G
X Y : U
f : X ⟶ Y
subst : Quiver.homOfEq (F.map f) ⋯ ⋯ = F.map f
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f

Tactic:
subst e
-- 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 : X ⟶ Y
⊢ Quiver.homOfEq (F.map f) ⋯ ⋯ = F.map f

Tactic:
simp
-- 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 : X ⟶ Y
X' Y' : U
hX : X = X'
hY : Y = Y'
subst : F.map (Quiver.homOfEq f ⋯ ⋯) = Quiver.homOfEq (F.map f) ⋯ ⋯
⊢ F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) ⋯ ⋯

Tactic:
subst hX hY
-- 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 : X ⟶ Y
⊢ F.map (Quiver.homOfEq f ⋯ ⋯) = Quiver.homOfEq (F.map f) ⋯ ⋯

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Push
Goal:
V : Type u_1
inst : Quiver V
W : Type u_2
σ : V → W
h : Nonempty W
⊢ Nonempty.{u_2 + 1} (Push σ)

Tactic:
h

Premises used: Quiver.Push
-- Module: Mathlib.Combinatorics.Quiver.Push
Goal:
V : Type u_1
inst : Quiver.{u_3, u_1} V
W : Type u_2
σ : V → W
⊢ Prefunctor.obj (of σ) = σ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.Push
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
rw : φ.obj X ⟶ φ.obj Y
⊢ τ (σ X) ⟶ τ (σ Y)

Tactic:
rw [← h X, ← h Y]
-- Module: Mathlib.Combinatorics.Quiver.Push
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
⊢ φ.obj X ⟶ φ.obj Y

Tactic:
exact φ.map f

Premises used: Prefunctor.map
-- Module: Mathlib.Combinatorics.Quiver.Push
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)
⊢ (lift σ φ τ h).obj = τ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.Push
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
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) ⋯
        (Eq.recOn (motive := fun (x : W') (x_1 : φ.obj X = x) ↦ x ⟶ φ.obj Y) ⋯ (φ.map f))
⊢ of σ ⋙q lift σ φ τ h = φ

Tactic:
fapply Prefunctor.ext

Premises used: Prefunctor.ext
-- Module: Mathlib.Combinatorics.Quiver.Push
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
h_obj : (lift σ φ τ h).obj (Prefunctor.obj (of σ) X) = φ.obj X
⊢ (of σ ⋙q lift σ φ τ h).obj X = φ.obj X

Tactic:
simp only [Prefunctor.comp_obj]

Premises used: Prefunctor.comp_obj
-- Module: Mathlib.Combinatorics.Quiver.Push
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
h_obj : φ.obj X = (lift σ φ τ h).obj (Prefunctor.obj (of σ) X)
⊢ (lift σ φ τ h).obj (Prefunctor.obj (of σ) X) = φ.obj X

Tactic:
apply Eq.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Quiver.Push
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
⊢ φ.obj X = (lift σ φ τ h).obj (Prefunctor.obj (of σ) X)

Tactic:
h X
-- Module: Mathlib.Combinatorics.Quiver.Push
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
⊢ φ.obj X = (lift σ φ τ h).obj (Prefunctor.obj (of σ) X)

Tactic:
exact h X
-- Module: Mathlib.Combinatorics.Quiver.Push
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
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) ⋯) ⋯)
⊢ (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))

Tactic:
simp only [Prefunctor.comp_map]

Premises used: Prefunctor.comp_map
-- Module: Mathlib.Combinatorics.Quiver.Push
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
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) ⋯) ⋯ :
      (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj 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) ⋯) ⋯)

Tactic:
apply eq_of_heq

Premises used: eq_of_heq
-- Module: Mathlib.Combinatorics.Quiver.Push
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
h_map :
  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)
⊢ 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)

Tactic:
apply (cast_heq _ _).trans

Premises used: HEq.trans, cast_heq
-- Module: Mathlib.Combinatorics.Quiver.Push
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
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) ⋯) ⋯ :
      (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj 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)

Tactic:
apply (cast_heq _ _).trans

Premises used: HEq.trans, cast_heq
-- Module: Mathlib.Combinatorics.Quiver.Push
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
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) ⋯) ⋯ :
      (of σ ⋙q lift σ φ τ h).obj X ⟶ (of σ ⋙q lift σ φ τ h).obj 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)

Tactic:
iterate 2 apply (cast_heq _ _).trans

Premises used: HEq.trans, cast_heq
-- Module: Mathlib.Combinatorics.Quiver.Push
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 (φ.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)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Quiver.Push
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 σ
h_obj : Φ.obj X = τ X
⊢ Φ.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

Tactic:
simp only
-- Module: Mathlib.Combinatorics.Quiver.Push
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 σ
h_obj h_obj₁ : τ X = τ X
⊢ Φ.obj X = τ X

Tactic:
rw [Φ₀]
-- Module: Mathlib.Combinatorics.Quiver.Push
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'
Φ : Push σ ⥤q W'
X Y : V
f : X ⟶ Y
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f) = id (⋯.mpr (⋯.mpr (Φ.map (Prefunctor.map (of σ) f))))

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
X X' : V
hX : X = X'
subst : Eq.{u_2 + 1} (α := X ⟶ X) (Quiver.homOfEq (𝟙rq X) ⋯ ⋯) (𝟙rq X)
⊢ Eq.{u_2 + 1} (α := X' ⟶ X') (Quiver.homOfEq (𝟙rq X) hX hX) (𝟙rq X')

Tactic:
subst hX
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
X : V
⊢ Eq.{u_2 + 1} (α := X ⟶ X) (Quiver.homOfEq (𝟙rq X) ⋯ ⋯) (𝟙rq X)

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : C
⊢ Eq.{v_1 + 1} (α := X ⟶ X) (𝟙rq X) (𝟙 X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V : Type u_1
W : Type u_2
inst : ReflQuiver.{u_3, u_1} V
inst_1 : ReflQuiver.{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.ReflQuiver
Goal:
V : Type u_1
W : Type u_2
inst : ReflQuiver.{u_3, u_1} V
inst_1 : ReflQuiver.{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.ReflQuiver
Goal:
V : Type u
inst : ReflQuiver.{v₁, u} V
W : Type u₂
inst_1 : ReflQuiver.{v₂, u₂} W
F G : ReflPrefunctor.{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))
    (map_id :
      ∀ (X : V),
        { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
          𝟙rq ({ obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X))
    (h_obj :
      ∀ (X : V), { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = G.obj X)
    (h_map :
      ∀ (X Y : V) (f : X ⟶ Y),
        { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{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, map_id := map_id : ReflPrefunctor.{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, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W } = G
⊢ F = G

Tactic:
obtain ⟨⟨F_obj⟩⟩ := F
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V : Type u
inst : ReflQuiver.{v₁, u} V
W : Type u₂
inst_1 : ReflQuiver.{v₂, u₂} W
G : ReflPrefunctor.{v₁, v₂, u, u₂} V W
F_obj : V → W
map : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id :
  ∀ (X : V),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
      𝟙rq ({ obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
h_obj : ∀ (X : V), { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = G.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{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, map_id := map_id : ReflPrefunctor.{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))
    (map_id_1 :
      ∀ (X : V),
        { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
          𝟙rq ({ obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X))
    (h_obj :
      ∀ (X : V),
        { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X =
          { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X)
    (h_map :
      ∀ (X Y : V) (f : X ⟶ Y),
        { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f =
          Eq.recOn (motive :=
            fun (x : W)
              (x_1 :
                { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
            { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) ⋯
            (Eq.recOn (motive :=
              fun (x : W)
                (x_1 :
                  { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
              x ⟶ { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y) ⋯
              ({ obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f))),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W } =
      { obj := G_obj, map := @map_1, map_id := map_id_1 }
⊢ { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W } = G

Tactic:
obtain ⟨⟨G_obj⟩⟩ := G
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V : Type u
inst : ReflQuiver.{v₁, u} V
W : Type u₂
inst_1 : ReflQuiver.{v₂, u₂} W
F_obj : V → W
map : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id :
  ∀ (X : V),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
      𝟙rq ({ obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
G_obj : V → W
map_1 : {X Y : V} → (X ⟶ Y) → (G_obj X ⟶ G_obj Y)
map_id_1 :
  ∀ (X : V),
    { obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
      𝟙rq ({ obj := G_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X =
      { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f =
      Eq.recOn (motive :=
        fun (x : W)
          (x_1 : { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
        { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) ⋯
        (Eq.recOn (motive :=
          fun (x : W)
            (x_1 : { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
          x ⟶ { obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y) ⋯
          ({ obj := G_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f))
⊢ F_obj = G_obj

Tactic:
(Set.eqOn_univ F_obj G_obj).mp fun _ _ ↦ h_obj _

Premises used: Set.eqOn_univ, Iff.mp
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V : Type u
inst : ReflQuiver.{v₁, u} V
W : Type u₂
inst_1 : ReflQuiver.{v₂, u₂} W
F_obj : V → W
map : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id :
  ∀ (X : V),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
      𝟙rq ({ obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
map_1 : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id_1 :
  ∀ (X : V),
    { obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
      𝟙rq ({ obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X =
      { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f =
      Eq.recOn (motive :=
        fun (x : W)
          (x_1 : { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
        { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) ⋯
        (Eq.recOn (motive :=
          fun (x : W)
            (x_1 : { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
          x ⟶ { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y) ⋯
          ({ obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f))
e_toPrefunctor : @map = @map_1
⊢ { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W } =
    { obj := F_obj, map := @map_1, map_id := map_id_1 }

Tactic:
congr
-- Module: Mathlib.Combinatorics.Quiver.ReflQuiver
Goal:
V : Type u
inst : ReflQuiver.{v₁, u} V
W : Type u₂
inst_1 : ReflQuiver.{v₂, u₂} W
F_obj : V → W
map : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id :
  ∀ (X : V),
    { obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
      𝟙rq ({ obj := F_obj, map := @map : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
map_1 : {X Y : V} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id_1 :
  ∀ (X : V),
    { obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.map (𝟙rq X) =
      𝟙rq ({ obj := F_obj, map := @map_1 : Prefunctor.{v₁, v₂, u, u₂} V W }.obj X)
h_obj :
  ∀ (X : V),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X =
      { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y),
    { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f =
      Eq.recOn (motive :=
        fun (x : W)
          (x_1 : { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y = x) ↦
        { obj := F_obj, map := @map, map_id := map_id : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X ⟶ x) ⋯
        (Eq.recOn (motive :=
          fun (x : W)
            (x_1 : { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj X = x) ↦
          x ⟶ { obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.obj Y) ⋯
          ({ obj := F_obj, map := @map_1, map_id := map_id_1 : ReflPrefunctor.{v₁, v₂, u, u₂} V W }.map f))
e_toPrefunctor : ∀ (X Y : V) (f : X ⟶ Y), map f = map_1 f
⊢ @map = @map_1

Tactic:
funext X Y f