[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : SingleObj α ⥤q SingleObj β
g : SingleObj β ⥤q SingleObj γ
⊢ ↑toPrefunctor.symm (f ⋙q g) = ↑toPrefunctor.symm g ∘ ↑toPrefunctor.symm f
[PROOFSTEP]
simp only [Equiv.symm_apply_eq, toPrefunctor_comp, Equiv.apply_symm_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
x : SingleObj α
p : Path (star α) x
⊢ listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : x = star α) p
[PROOFSTEP]
induction' p with y z p a ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
x : SingleObj α
⊢ listToPath (pathToList Path.nil) = Path.cast (_ : star α = star α) (_ : star α = star α) Path.nil
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : SingleObj α
p : Path (star α) y
a : y ⟶ z
ih : listToPath (pathToList p) = Path.cast (_ : star α = star α) (_ : y = star α) p
⊢ listToPath (pathToList (Path.cons p a)) = Path.cast (_ : star α = star α) (_ : z = star α) (Path.cons p a)
[PROOFSTEP]
dsimp at *
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
x y z : SingleObj α
p : Path (star α) y
a : y ⟶ z
ih : listToPath (pathToList p) = p
⊢ Path.cons (listToPath (pathToList p)) a = Path.cons p a
[PROOFSTEP]
rw [ih]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l : List α
⊢ pathToList (listToPath l) = l
[PROOFSTEP]
induction' l with a l ih
[GOAL]
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ pathToList (listToPath []) = []
[PROOFSTEP]
rfl
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ pathToList (listToPath (a :: l)) = a :: l
[PROOFSTEP]
change a :: pathToList (listToPath l) = a :: l
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: pathToList (listToPath l) = a :: l
[PROOFSTEP]
rw [ih]
