[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
⊢ reverse (reverse f) = f
[PROOFSTEP]
apply h.inv'
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g ↔ f = g
[PROOFSTEP]
constructor
[GOAL]
case mp
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g → f = g
[PROOFSTEP]
rintro h
[GOAL]
case mp
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : reverse f = reverse g
⊢ f = g
[PROOFSTEP]
simpa using congr_arg Quiver.reverse h
[GOAL]
case mpr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g
[PROOFSTEP]
rintro h
[GOAL]
case mpr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : f = g
⊢ reverse f = reverse g
[PROOFSTEP]
congr
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
f : a ⟶ b
g : b ⟶ a
⊢ f = reverse g ↔ reverse f = g
[PROOFSTEP]
rw [← reverse_inj, reverse_reverse]
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁷ : Quiver U
inst✝⁶ : Quiver V
inst✝⁵ : Quiver W
inst✝⁴ : HasReverse U
inst✝³ : HasReverse V
inst✝² : HasReverse W
φ : U ⥤q V
ψ : V ⥤q W
inst✝¹ : Prefunctor.MapReverse φ
inst✝ : Prefunctor.MapReverse ψ
u✝ v✝ : U
e : u✝ ⟶ v✝
⊢ (φ ⋙q ψ).map (reverse e) = reverse ((φ ⋙q ψ).map e)
[PROOFSTEP]
simp only [Prefunctor.comp_map, Prefunctor.MapReverse.map_reverse']
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
inst✝ : HasReverse V
a b c : V
p : Path a b
q : Path b c
⊢ reverse (comp p q) = comp (reverse q) (reverse p)
[PROOFSTEP]
induction' q with _ _ _ _ h
[GOAL]
case nil
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
inst✝ : HasReverse V
a b c : V
p : Path a b
⊢ reverse (comp p nil) = comp (reverse nil) (reverse p)
[PROOFSTEP]
simp
[GOAL]
case cons
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
inst✝ : HasReverse V
a b c : V
p : Path a b
b✝ c✝ : V
a✝¹ : Path b b✝
a✝ : b✝ ⟶ c✝
h : reverse (comp p a✝¹) = comp (reverse a✝¹) (reverse p)
⊢ reverse (comp p (cons a✝¹ a✝)) = comp (reverse (cons a✝¹ a✝)) (reverse p)
[PROOFSTEP]
simp [h]
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
p : Path a b
⊢ reverse (reverse p) = p
[PROOFSTEP]
induction' p with _ _ _ _ h
[GOAL]
case nil
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h : HasInvolutiveReverse V
a b : V
⊢ reverse (reverse nil) = nil
[PROOFSTEP]
simp
[GOAL]
case cons
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : reverse (reverse a✝¹) = a✝¹
⊢ reverse (reverse (cons a✝¹ a✝)) = cons a✝¹ a✝
[PROOFSTEP]
rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]
[GOAL]
case cons
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
h✝ : HasInvolutiveReverse V
a b b✝ c✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ c✝
h : reverse (reverse a✝¹) = a✝¹
⊢ comp a✝¹ (Hom.toPath a✝) = cons a✝¹ a✝
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ of ⋙q lift φ = φ
[PROOFSTEP]
fapply Prefunctor.ext
[GOAL]
case h_obj
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X : V), (of ⋙q lift φ).obj X = φ.obj X
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X : V
⊢ (of ⋙q lift φ).obj X = φ.obj X
[PROOFSTEP]
rfl
[GOAL]
case h_map
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
⊢ ∀ (X Y : V) (f : X ⟶ Y),
    (of ⋙q lift φ).map f =
      Eq.recOn (_ : φ.obj Y = (of ⋙q lift φ).obj Y) (Eq.recOn (_ : φ.obj X = (of ⋙q lift φ).obj X) (φ.map f))
[PROOFSTEP]
rintro X Y f
[GOAL]
case h_map
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
φ : V ⥤q V'
X Y : V
f : X ⟶ Y
⊢ (of ⋙q lift φ).map f =
    Eq.recOn (_ : φ.obj Y = (of ⋙q lift φ).obj Y) (Eq.recOn (_ : φ.obj X = (of ⋙q lift φ).obj X) (φ.map f))
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ (lift φ).map (reverse f) = reverse ((lift φ).map f)
[PROOFSTEP]
dsimp [Symmetrify.lift]
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ (match Sum.swap f with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match f with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
[PROOFSTEP]
cases f
[GOAL]
case inl
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ (match Sum.swap (Sum.inl val✝) with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inl val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
[PROOFSTEP]
simp only
[GOAL]
case inl
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ (match Sum.swap (Sum.inl val✝) with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse (φ.map val✝)
[PROOFSTEP]
rfl
[GOAL]
case inr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match Sum.swap (Sum.inr val✝) with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inr val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
[PROOFSTEP]
simp only [reverse_reverse]
[GOAL]
case inr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match Sum.swap (Sum.inr val✝) with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    φ.map val✝
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
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 φ
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
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 Φ)
[PROOFSTEP]
fapply Prefunctor.ext
[GOAL]
case h_obj
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
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
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
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
[PROOFSTEP]
rfl
[GOAL]
case h_map
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
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))
[PROOFSTEP]
rintro X Y f
[GOAL]
case h_map
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
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))
[PROOFSTEP]
cases f
[GOAL]
case h_map.inl
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
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✝)))
[PROOFSTEP]
rfl
[GOAL]
case h_map.inr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝⁴ : Quiver U
inst✝³ : Quiver V
inst✝² : Quiver W
V' : Type u_4
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✝)))
[PROOFSTEP]
exact hΦinv (Sum.inl _)
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
e : u✝ ⟶ v✝
⊢ (Prefunctor.symmetrify φ).map (reverse e) = reverse ((Prefunctor.symmetrify φ).map e)
[PROOFSTEP]
cases e
[GOAL]
case inl
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : u✝ ⟶ v✝
⊢ (Prefunctor.symmetrify φ).map (reverse (Sum.inl val✝)) = reverse ((Prefunctor.symmetrify φ).map (Sum.inl val✝))
[PROOFSTEP]
rfl
[GOAL]
case inr
U : Type u_1
V : Type u_2
W : Type u_3
inst✝³ : Quiver U
inst✝² : Quiver V
inst✝¹ : Quiver W
V' : Type u_4
inst✝ : Quiver V'
φ : U ⥤q V
u✝ v✝ : Symmetrify U
val✝ : v✝ ⟶ u✝
⊢ (Prefunctor.symmetrify φ).map (reverse (Sum.inr val✝)) = reverse ((Prefunctor.symmetrify φ).map (Sum.inr val✝))
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ reverse (reverse (PushQuiver.arrow f)) = PushQuiver.arrow f
[PROOFSTEP]
dsimp [reverse]
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ PushQuiver.arrow (HasReverse.reverse' (HasReverse.reverse' f)) = PushQuiver.arrow f
[PROOFSTEP]
congr
[GOAL]
case e_f
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ HasReverse.reverse' (HasReverse.reverse' f) = f
[PROOFSTEP]
apply h.inv'
[GOAL]
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
⊢ ∀ {u v : V} (e : u ⟶ v), (of σ).map (reverse e) = reverse ((of σ).map e)
[PROOFSTEP]
simp [of_reverse]
