U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ Φ = lift (of ⋙q Φ)
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
Φ : Symmetrify V ⥤q V'
hΦ : of ⋙q Φ = φ
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ Φ = lift φ
subst_vars
case h_obj
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X : Symmetrify V), Φ.obj X = (lift (of ⋙q Φ)).obj X

case h_map
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X Y : Symmetrify V) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
        (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map f))
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ Φ = lift (of ⋙q Φ)
fapply Prefunctor.ext
case h_obj
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X : Symmetrify V
⊢ Φ.obj X = (lift (of ⋙q Φ)).obj X
case h_obj
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X : Symmetrify V), Φ.obj X = (lift (of ⋙q Φ)).obj X
rintro X
no goals
case h_obj
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X : Symmetrify V
⊢ Φ.obj X = (lift (of ⋙q Φ)).obj X
rfl
case h_map
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
f : X ⟶ Y
⊢ Φ.map f =
    Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
      (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map f))
case h_map
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
⊢ ∀ (X Y : Symmetrify V) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
        (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map f))
rintro X Y f
case h_map.inl
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ Φ.map (Sum.inl val✝) =
    Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
      (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map (Sum.inl val✝)))

case h_map.inr
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ Φ.map (Sum.inr val✝) =
    Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
      (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map (Sum.inr val✝)))
case h_map
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
f : X ⟶ Y
⊢ Φ.map f =
    Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
      (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map f))
cases f
no goals
case h_map.inl
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ Φ.map (Sum.inl val✝) =
    Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
      (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map (Sum.inl val✝)))
rfl
no goals
case h_map.inr
U : Type ?u.8739
V : Type u_2
W : Type ?u.8745
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_1
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ Φ.map (Sum.inr val✝) =
    Eq.recOn (_ : (lift (of ⋙q Φ)).obj Y = Φ.obj Y)
      (Eq.recOn (_ : (lift (of ⋙q Φ)).obj X = Φ.obj X) ((lift (of ⋙q Φ)).map (Sum.inr val✝)))
exact hΦinv (Sum.inl _)