[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (fun X Y x => τ X ⟶ τ Y) (σ X) (σ Y) (PushQuiver.arrow f)
[PROOFSTEP]
dsimp only
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ τ (σ X) ⟶ τ (σ Y)
[PROOFSTEP]
rw [← h X, ← h Y]
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ φ.obj X ⟶ φ.obj Y
[PROOFSTEP]
exact φ.map f
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ of σ ⋙q lift σ φ τ h = φ
[PROOFSTEP]
fapply Prefunctor.ext
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (of σ ⋙q lift σ φ τ h).obj X = φ.obj X
[PROOFSTEP]
simp only [Prefunctor.comp_obj]
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ (lift σ φ τ h).obj ((of σ).obj X) = φ.obj X
[PROOFSTEP]
apply Eq.symm
[GOAL]
case h_obj.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X : V
⊢ φ.obj X = (lift σ φ τ h).obj ((of σ).obj X)
[PROOFSTEP]
exact h X
[GOAL]
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
⊢ ∀ (X Y : V) (f : X ⟶ Y),
    (of σ ⋙q lift σ φ τ h).map f =
      Eq.recOn (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y)
        (Eq.recOn (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) (φ.map f))
[PROOFSTEP]
rintro X Y f
[GOAL]
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (of σ ⋙q lift σ φ τ h).map f =
    Eq.recOn (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y)
      (Eq.recOn (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) (φ.map f))
[PROOFSTEP]
simp only [Prefunctor.comp_map]
[GOAL]
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ (lift σ φ τ h).map ((of σ).map f) =
    (_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f
[PROOFSTEP]
apply eq_of_heq
[GOAL]
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((lift σ φ τ h).map ((of σ).map f))
    ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
[PROOFSTEP]
iterate 2 apply (cast_heq _ _).trans
[GOAL]
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((lift σ φ τ h).map ((of σ).map f))
    ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
[PROOFSTEP]
apply (cast_heq _ _).trans
[GOAL]
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))
    ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
[PROOFSTEP]
apply (cast_heq _ _).trans
[GOAL]
case h_map.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq (φ.map f) ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f)
[PROOFSTEP]
apply HEq.symm
[GOAL]
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((_ : φ.obj Y = (of σ ⋙q lift σ φ τ h).obj Y) ▸ (_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
[PROOFSTEP]
apply (eqRec_heq _ _).trans
[GOAL]
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ HEq ((_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
[PROOFSTEP]
have : ∀ {α γ} {β : α → γ → Sort _} {a a'} (p : a = a') g (b : β a g), HEq (p ▸ b) b :=
  by
  intros
  subst_vars
  rfl
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ ∀ {α : Sort ?u.2529} {γ : Sort ?u.2531} {β : α → γ → Sort ?u.2533} {a a' : α} (p : a = a') (g : γ) (b : β a g),
    HEq (p ▸ b) b
[PROOFSTEP]
intros
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2529
γ✝ : Sort ?u.2531
β✝ : α✝ → γ✝ → Sort ?u.2533
a✝ a'✝ : α✝
p✝ : a✝ = a'✝
g✝ : γ✝
b✝ : β✝ a✝ g✝
⊢ HEq (p✝ ▸ b✝) b✝
[PROOFSTEP]
subst_vars
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
α✝ : Sort ?u.2529
γ✝ : Sort ?u.2531
β✝ : α✝ → γ✝ → Sort ?u.2533
a'✝ : α✝
g✝ : γ✝
b✝ : β✝ a'✝ g✝
⊢ HEq ((_ : a'✝ = a'✝) ▸ b✝) b✝
[PROOFSTEP]
rfl
[GOAL]
case h_map.h.h
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
this :
  ∀ {α : Sort ?u.2529} {γ : Sort ?u.2531} {β : α → γ → Sort ?u.2533} {a a' : α} (p : a = a') (g : γ) (b : β a g),
    HEq (p ▸ b) b
⊢ HEq ((_ : φ.obj X = (of σ ⋙q lift σ φ τ h).obj X) ▸ φ.map f) (φ.map f)
[PROOFSTEP]
apply this
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ Φ = lift σ φ τ h
[PROOFSTEP]
dsimp only [of, lift]
[GOAL]
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q 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 x => τ X ⟶ τ Y) fun X Y f =>
          id
            (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
              (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }
[PROOFSTEP]
fapply Prefunctor.ext
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X : Push σ),
    Φ.obj X =
      { obj := τ,
            map :=
              @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                id
                  (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                    (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
        X
[PROOFSTEP]
intro X
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X =
    { obj := τ,
          map :=
            @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
              id
                (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                  (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
      X
[PROOFSTEP]
simp only
[GOAL]
case h_obj
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X : Push σ
⊢ Φ.obj X = τ X
[PROOFSTEP]
rw [Φ₀]
[GOAL]
case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn
        (_ :
          { obj := τ,
                  map :=
                    @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                      id
                        (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                          (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
              Y =
            Φ.obj Y)
        (Eq.recOn
          (_ :
            { obj := τ,
                    map :=
                      @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                        id
                          (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                            (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
                X =
              Φ.obj X)
          ({ obj := τ,
                map :=
                  @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                    id
                      (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                        (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.map
            f))
[PROOFSTEP]
rintro _ _ ⟨⟩
[GOAL]
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
⊢ Φ.map (PushQuiver.arrow f✝) =
    Eq.recOn
      (_ :
        { obj := τ,
                map :=
                  @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                    id
                      (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                        (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
            (σ Y✝) =
          Φ.obj (σ Y✝))
      (Eq.recOn
        (_ :
          { obj := τ,
                  map :=
                    @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                      id
                        (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                          (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.obj
              (σ X✝) =
            Φ.obj (σ X✝))
        ({ obj := τ,
              map :=
                @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f =>
                  id
                    (Eq.mpr (_ : (τ (σ X) ⟶ τ (σ Y)) = (φ.obj X ⟶ τ (σ Y)))
                      (Eq.mpr (_ : (φ.obj X ⟶ τ (σ Y)) = (φ.obj X ⟶ φ.obj Y)) (φ.map f))) }.map
          (PushQuiver.arrow f✝)))
[PROOFSTEP]
subst_vars
[GOAL]
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
Φ : Push σ ⥤q W'
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f✝) =
    Eq.recOn
      (_ :
        { obj := Φ.obj,
                map :=
                  @PushQuiver.rec V inst✝¹ W σ (fun X Y x => Φ.obj X ⟶ Φ.obj Y) fun X Y f =>
                    id
                      (Eq.mpr (_ : (Φ.obj (σ X) ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)))
                        (Eq.mpr (_ : ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ (of σ ⋙q Φ).obj Y))
                          ((of σ ⋙q Φ).map f))) }.obj
            (σ Y✝) =
          Φ.obj (σ Y✝))
      (Eq.recOn
        (_ :
          { obj := Φ.obj,
                  map :=
                    @PushQuiver.rec V inst✝¹ W σ (fun X Y x => Φ.obj X ⟶ Φ.obj Y) fun X Y f =>
                      id
                        (Eq.mpr (_ : (Φ.obj (σ X) ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)))
                          (Eq.mpr (_ : ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ (of σ ⋙q Φ).obj Y))
                            ((of σ ⋙q Φ).map f))) }.obj
              (σ X✝) =
            Φ.obj (σ X✝))
        ({ obj := Φ.obj,
              map :=
                @PushQuiver.rec V inst✝¹ W σ (fun X Y x => Φ.obj X ⟶ Φ.obj Y) fun X Y f =>
                  id
                    (Eq.mpr (_ : (Φ.obj (σ X) ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)))
                      (Eq.mpr (_ : ((of σ ⋙q Φ).obj X ⟶ Φ.obj (σ Y)) = ((of σ ⋙q Φ).obj X ⟶ (of σ ⋙q Φ).obj Y))
                        ((of σ ⋙q Φ).map f))) }.map
          (PushQuiver.arrow f✝)))
[PROOFSTEP]
simp only [Prefunctor.comp_map, cast_eq]
[GOAL]
case h_map.arrow
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
Φ : Push σ ⥤q W'
X✝ Y✝ : V
f✝ : X✝ ⟶ Y✝
h : ∀ (x : V), (of σ ⋙q Φ).obj x = Φ.obj (σ x)
⊢ Φ.map (PushQuiver.arrow f✝) =
    id
      (Eq.mpr (_ : (Φ.obj (σ X✝) ⟶ Φ.obj (σ Y✝)) = ((of σ ⋙q Φ).obj X✝ ⟶ Φ.obj (σ Y✝)))
        (Eq.mpr (_ : ((of σ ⋙q Φ).obj X✝ ⟶ Φ.obj (σ Y✝)) = ((of σ ⋙q Φ).obj X✝ ⟶ (of σ ⋙q Φ).obj Y✝))
          (Φ.map ((of σ).map f✝))))
[PROOFSTEP]
rfl
