[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.2230
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u v : U
⊢ Injective fun f => φ.map f
[PROOFSTEP]
rintro f g he
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.2230
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u v : U
f g : u ⟶ v
he : (fun f => φ.map f) f = (fun f => φ.map f) g
⊢ f = g
[PROOFSTEP]
have : φ.star u (Quiver.Star.mk f) = φ.star u (Quiver.Star.mk g) := by simpa using he
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.2230
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u v : U
f g : u ⟶ v
he : (fun f => φ.map f) f = (fun f => φ.map f) g
⊢ star φ u (Star.mk f) = star φ u (Star.mk g)
[PROOFSTEP]
simpa using he
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.2230
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u v : U
f g : u ⟶ v
he : (fun f => φ.map f) f = (fun f => φ.map f) g
this : star φ u (Star.mk f) = star φ u (Star.mk g)
⊢ f = g
[PROOFSTEP]
simpa using (hφ.star_bijective u).left this
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
hφψ : Prefunctor.IsCovering (φ ⋙q ψ)
φsur : Surjective φ.obj
⊢ Prefunctor.IsCovering ψ
[PROOFSTEP]
refine' ⟨fun v => _, fun v => _⟩
[GOAL]
case refine'_1
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
hφψ : Prefunctor.IsCovering (φ ⋙q ψ)
φsur : Surjective φ.obj
v : V
⊢ Bijective (star ψ v)
[PROOFSTEP]
obtain ⟨u, rfl⟩ := φsur v
[GOAL]
case refine'_2
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
hφψ : Prefunctor.IsCovering (φ ⋙q ψ)
φsur : Surjective φ.obj
v : V
⊢ Bijective (costar ψ v)
[PROOFSTEP]
obtain ⟨u, rfl⟩ := φsur v
[GOAL]
case refine'_1.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
hφψ : Prefunctor.IsCovering (φ ⋙q ψ)
φsur : Surjective φ.obj
u : U
⊢ Bijective (star ψ (φ.obj u))
case refine'_2.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type u_3
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
hφψ : Prefunctor.IsCovering (φ ⋙q ψ)
φsur : Surjective φ.obj
u : U
⊢ Bijective (costar ψ (φ.obj u))
[PROOFSTEP]
exacts [(Bijective.of_comp_iff _ (hφ.star_bijective u)).mp (hφψ.star_bijective u),
  (Bijective.of_comp_iff _ (hφ.costar_bijective u)).mp (hφψ.costar_bijective u)]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
⊢ star (symmetrify φ) u =
    ↑(Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (star φ u) (costar φ u) ∘ ↑(Quiver.symmetrifyStar u)
[PROOFSTEP]
rw [Equiv.eq_symm_comp]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
⊢ ↑(Quiver.symmetrifyStar (φ.obj u)) ∘ star (symmetrify φ) u =
    Sum.map (star φ u) (costar φ u) ∘ ↑(Quiver.symmetrifyStar u)
[PROOFSTEP]
ext ⟨v, f | g⟩
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : u ⟶ v
⊢ (↑(Quiver.symmetrifyStar (φ.obj u)) ∘ star (symmetrify φ) u) { fst := v, snd := Sum.inl f } =
    (Sum.map (star φ u) (costar φ u) ∘ ↑(Quiver.symmetrifyStar u)) { fst := v, snd := Sum.inl f }
[PROOFSTEP]
simp only [Quiver.symmetrifyStar, Function.comp_apply]
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : v ⟶ u
⊢ (↑(Quiver.symmetrifyStar (φ.obj u)) ∘ star (symmetrify φ) u) { fst := v, snd := Sum.inr g } =
    (Sum.map (star φ u) (costar φ u) ∘ ↑(Quiver.symmetrifyStar u)) { fst := v, snd := Sum.inr g }
[PROOFSTEP]
simp only [Quiver.symmetrifyStar, Function.comp_apply]
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : u ⟶ v
⊢ ↑(Equiv.sigmaSumDistrib (fun v => Symmetrify.of.obj (φ.obj u) ⟶ v) fun v => v ⟶ Symmetrify.of.obj (φ.obj u))
      (star (symmetrify φ) u { fst := v, snd := Sum.inl f }) =
    Sum.map (star φ u) (costar φ u)
      (↑(Equiv.sigmaSumDistrib (fun v => Symmetrify.of.obj u ⟶ v) fun v => v ⟶ Symmetrify.of.obj u)
        { fst := v, snd := Sum.inl f })
[PROOFSTEP]
erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply]
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : v ⟶ u
⊢ ↑(Equiv.sigmaSumDistrib (fun v => Symmetrify.of.obj (φ.obj u) ⟶ v) fun v => v ⟶ Symmetrify.of.obj (φ.obj u))
      (star (symmetrify φ) u { fst := v, snd := Sum.inr g }) =
    Sum.map (star φ u) (costar φ u)
      (↑(Equiv.sigmaSumDistrib (fun v => Symmetrify.of.obj u ⟶ v) fun v => v ⟶ Symmetrify.of.obj u)
        { fst := v, snd := Sum.inr g })
[PROOFSTEP]
erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply]
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : u ⟶ v
⊢ Sum.map (Sigma.mk (star (symmetrify φ) u { fst := v, snd := Sum.inl f }).fst)
      (Sigma.mk (star (symmetrify φ) u { fst := v, snd := Sum.inl f }).fst)
      (star (symmetrify φ) u { fst := v, snd := Sum.inl f }).snd =
    Sum.map (star φ u) (costar φ u)
      (Sum.map (Sigma.mk { fst := v, snd := Sum.inl f }.fst) (Sigma.mk { fst := v, snd := Sum.inl f }.fst)
        { fst := v, snd := Sum.inl f }.snd)
[PROOFSTEP]
simp
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.4868
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : v ⟶ u
⊢ Sum.map (Sigma.mk (star (symmetrify φ) u { fst := v, snd := Sum.inr g }).fst)
      (Sigma.mk (star (symmetrify φ) u { fst := v, snd := Sum.inr g }).fst)
      (star (symmetrify φ) u { fst := v, snd := Sum.inr g }).snd =
    Sum.map (star φ u) (costar φ u)
      (Sum.map (Sigma.mk { fst := v, snd := Sum.inr g }.fst) (Sigma.mk { fst := v, snd := Sum.inr g }.fst)
        { fst := v, snd := Sum.inr g }.snd)
[PROOFSTEP]
simp
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
⊢ costar (symmetrify φ) u = ↑(symmetrifyCostar (φ.obj u)).symm ∘ Sum.map (costar φ u) (star φ u) ∘ ↑(symmetrifyCostar u)
[PROOFSTEP]
rw [Equiv.eq_symm_comp]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
⊢ ↑(symmetrifyCostar (φ.obj u)) ∘ costar (symmetrify φ) u = Sum.map (costar φ u) (star φ u) ∘ ↑(symmetrifyCostar u)
[PROOFSTEP]
ext ⟨v, f | g⟩
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : v ⟶ u
⊢ (↑(symmetrifyCostar (φ.obj u)) ∘ costar (symmetrify φ) u) { fst := v, snd := Sum.inl f } =
    (Sum.map (costar φ u) (star φ u) ∘ ↑(symmetrifyCostar u)) { fst := v, snd := Sum.inl f }
[PROOFSTEP]
simp only [Quiver.symmetrifyCostar, Function.comp_apply]
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : u ⟶ v
⊢ (↑(symmetrifyCostar (φ.obj u)) ∘ costar (symmetrify φ) u) { fst := v, snd := Sum.inr g } =
    (Sum.map (costar φ u) (star φ u) ∘ ↑(symmetrifyCostar u)) { fst := v, snd := Sum.inr g }
[PROOFSTEP]
simp only [Quiver.symmetrifyCostar, Function.comp_apply]
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : v ⟶ u
⊢ ↑(Equiv.sigmaSumDistrib (fun u_1 => u_1 ⟶ Symmetrify.of.obj (φ.obj u)) fun u_1 => Symmetrify.of.obj (φ.obj u) ⟶ u_1)
      (costar (symmetrify φ) u { fst := v, snd := Sum.inl f }) =
    Sum.map (costar φ u) (star φ u)
      (↑(Equiv.sigmaSumDistrib (fun u_1 => u_1 ⟶ Symmetrify.of.obj u) fun u_1 => Symmetrify.of.obj u ⟶ u_1)
        { fst := v, snd := Sum.inl f })
[PROOFSTEP]
erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply]
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : u ⟶ v
⊢ ↑(Equiv.sigmaSumDistrib (fun u_1 => u_1 ⟶ Symmetrify.of.obj (φ.obj u)) fun u_1 => Symmetrify.of.obj (φ.obj u) ⟶ u_1)
      (costar (symmetrify φ) u { fst := v, snd := Sum.inr g }) =
    Sum.map (costar φ u) (star φ u)
      (↑(Equiv.sigmaSumDistrib (fun u_1 => u_1 ⟶ Symmetrify.of.obj u) fun u_1 => Symmetrify.of.obj u ⟶ u_1)
        { fst := v, snd := Sum.inr g })
[PROOFSTEP]
erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply]
[GOAL]
case h.mk.inl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
f : v ⟶ u
⊢ Sum.map (Sigma.mk (costar (symmetrify φ) u { fst := v, snd := Sum.inl f }).fst)
      (Sigma.mk (costar (symmetrify φ) u { fst := v, snd := Sum.inl f }).fst)
      (costar (symmetrify φ) u { fst := v, snd := Sum.inl f }).snd =
    Sum.map (costar φ u) (star φ u)
      (Sum.map (Sigma.mk { fst := v, snd := Sum.inl f }.fst) (Sigma.mk { fst := v, snd := Sum.inl f }.fst)
        { fst := v, snd := Sum.inl f }.snd)
[PROOFSTEP]
simp
[GOAL]
case h.mk.inr
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.8284
inst✝ : Quiver W
ψ : V ⥤q W
u : U
v : Symmetrify U
g : u ⟶ v
⊢ Sum.map (Sigma.mk (costar (symmetrify φ) u { fst := v, snd := Sum.inr g }).fst)
      (Sigma.mk (costar (symmetrify φ) u { fst := v, snd := Sum.inr g }).fst)
      (costar (symmetrify φ) u { fst := v, snd := Sum.inr g }).snd =
    Sum.map (costar φ u) (star φ u)
      (Sum.map (Sigma.mk { fst := v, snd := Sum.inr g }.fst) (Sigma.mk { fst := v, snd := Sum.inr g }.fst)
        { fst := v, snd := Sum.inr g }.snd)
[PROOFSTEP]
simp
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
⊢ Prefunctor.IsCovering (symmetrify φ)
[PROOFSTEP]
refine' ⟨fun u => _, fun u => _⟩
[GOAL]
case refine'_1
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (star (symmetrify φ) u)
[PROOFSTEP]
simp only [φ.symmetrifyStar, φ.symmetrifyCostar, EquivLike.comp_bijective]
[GOAL]
case refine'_2
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (costar (symmetrify φ) u)
[PROOFSTEP]
simp only [φ.symmetrifyStar, φ.symmetrifyCostar, EquivLike.comp_bijective]
[GOAL]
case refine'_1
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (Sum.map (star φ u) (costar φ u) ∘ ↑(Quiver.symmetrifyStar u))
[PROOFSTEP]
erw [EquivLike.bijective_comp]
[GOAL]
case refine'_2
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (Sum.map (costar φ u) (star φ u) ∘ ↑(symmetrifyCostar u))
[PROOFSTEP]
erw [EquivLike.bijective_comp]
[GOAL]
case refine'_1
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (Sum.map (star φ u) (costar φ u))
[PROOFSTEP]
simp [hφ.star_bijective u, hφ.costar_bijective u]
[GOAL]
case refine'_2
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.11700
inst✝ : Quiver W
ψ : V ⥤q W
hφ : Prefunctor.IsCovering φ
u : Symmetrify U
⊢ Bijective (Sum.map (costar φ u) (star φ u))
[PROOFSTEP]
simp [hφ.star_bijective u, hφ.costar_bijective u]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u : U
⊢ Injective (pathStar φ u)
[PROOFSTEP]
dsimp [Prefunctor.pathStar, Quiver.PathStar.mk]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u : U
⊢ Injective fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }
[PROOFSTEP]
rintro ⟨v₁, p₁⟩
[GOAL]
case mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ : U
p₁ : Path u v₁
⊢ ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := v₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := v₁, snd := p₁ } = a₂
[PROOFSTEP]
induction' p₁ with x₁ y₁ p₁ e₁ ih
[GOAL]
case mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ : U
⊢ ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := u, snd := Path.nil } = a₂
[PROOFSTEP]
rintro ⟨y₂, p₂⟩
[GOAL]
case mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
⊢ ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := y₁, snd := Path.cons p₁ e₁ } = a₂
[PROOFSTEP]
rintro ⟨y₂, p₂⟩
[GOAL]
case mk.nil.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ : U
p₂ : Path u y₂
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := p₂ } →
    { fst := u, snd := Path.nil } = { fst := y₂, snd := p₂ }
[PROOFSTEP]
cases' p₂ with x₂ _ p₂ e₂
[GOAL]
case mk.cons.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ : U
p₂ : Path u y₂
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := p₂ } →
    { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := p₂ }
[PROOFSTEP]
cases' p₂ with x₂ _ p₂ e₂
[GOAL]
case mk.nil.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ : U
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } →
    { fst := u, snd := Path.nil } = { fst := u, snd := Path.nil }
[PROOFSTEP]
intro h
[GOAL]
case mk.nil.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := Path.cons p₂ e₂ } →
    { fst := u, snd := Path.nil } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
intro h
[GOAL]
case mk.cons.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } →
    { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := u, snd := Path.nil }
[PROOFSTEP]
intro h
[GOAL]
case mk.cons.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
      (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := Path.cons p₂ e₂ } →
    { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
intro h
[GOAL]
case mk.nil.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ : U
h :
  (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil }
⊢ { fst := u, snd := Path.nil } = { fst := u, snd := Path.nil }
[PROOFSTEP]
simp only [Prefunctor.pathStar_apply, Prefunctor.mapPath_nil, Prefunctor.mapPath_cons, Sigma.mk.inj_iff] at h 
[GOAL]
case mk.nil.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h :
  (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := Path.cons p₂ e₂ }
⊢ { fst := u, snd := Path.nil } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
simp only [Prefunctor.pathStar_apply, Prefunctor.mapPath_nil, Prefunctor.mapPath_cons, Sigma.mk.inj_iff] at h 
[GOAL]
case mk.cons.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
h :
  (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := u, snd := Path.nil }
[PROOFSTEP]
simp only [Prefunctor.pathStar_apply, Prefunctor.mapPath_nil, Prefunctor.mapPath_cons, Sigma.mk.inj_iff] at h 
[GOAL]
case mk.cons.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h :
  (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₁, snd := Path.cons p₁ e₁ } =
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := y₂, snd := Path.cons p₂ e₂ }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
simp only [Prefunctor.pathStar_apply, Prefunctor.mapPath_nil, Prefunctor.mapPath_cons, Sigma.mk.inj_iff] at h 
[GOAL]
case mk.nil.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ : U
h : True
⊢ { fst := u, snd := Path.nil } = { fst := u, snd := Path.nil }
[PROOFSTEP]
rfl
[GOAL]
case mk.nil.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h : φ.obj u = φ.obj y₂ ∧ HEq Path.nil (Path.cons (mapPath φ p₂) (φ.map e₂))
⊢ { fst := u, snd := Path.nil } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
exfalso
[GOAL]
case mk.nil.mk.cons.h
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h : φ.obj u = φ.obj y₂ ∧ HEq Path.nil (Path.cons (mapPath φ p₂) (φ.map e₂))
⊢ False
[PROOFSTEP]
cases' h with h h'
[GOAL]
case mk.nil.mk.cons.h.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h : φ.obj u = φ.obj y₂
h' : HEq Path.nil (Path.cons (mapPath φ p₂) (φ.map e₂))
⊢ False
[PROOFSTEP]
rw [← Path.eq_cast_iff_heq rfl h.symm, Path.cast_cons] at h' 
[GOAL]
case mk.nil.mk.cons.h.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h : φ.obj u = φ.obj y₂
h' :
  Path.nil =
    Path.cons (Path.cast (_ : φ.obj u = φ.obj u) (_ : φ.obj x₂ = φ.obj x₂) (mapPath φ p₂))
      (Hom.cast (_ : φ.obj x₂ = φ.obj x₂) (_ : φ.obj y₂ = φ.obj u) (φ.map e₂))
⊢ False
[PROOFSTEP]
exact (Path.nil_ne_cons _ _) h'
[GOAL]
case mk.cons.mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
h : φ.obj y₁ = φ.obj u ∧ HEq (Path.cons (mapPath φ p₁) (φ.map e₁)) Path.nil
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := u, snd := Path.nil }
[PROOFSTEP]
exfalso
[GOAL]
case mk.cons.mk.nil.h
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
h : φ.obj y₁ = φ.obj u ∧ HEq (Path.cons (mapPath φ p₁) (φ.map e₁)) Path.nil
⊢ False
[PROOFSTEP]
cases' h with h h'
[GOAL]
case mk.cons.mk.nil.h.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
h : φ.obj y₁ = φ.obj u
h' : HEq (Path.cons (mapPath φ p₁) (φ.map e₁)) Path.nil
⊢ False
[PROOFSTEP]
rw [← Path.cast_eq_iff_heq rfl h, Path.cast_cons] at h' 
[GOAL]
case mk.cons.mk.nil.h.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
h : φ.obj y₁ = φ.obj u
h' :
  Path.cons (Path.cast (_ : φ.obj u = φ.obj u) (_ : φ.obj x₁ = φ.obj x₁) (mapPath φ p₁))
      (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) h (φ.map e₁)) =
    Path.nil
⊢ False
[PROOFSTEP]
exact (Path.cons_ne_nil _ _) h'
[GOAL]
case mk.cons.mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
h : φ.obj y₁ = φ.obj y₂ ∧ HEq (Path.cons (mapPath φ p₁) (φ.map e₁)) (Path.cons (mapPath φ p₂) (φ.map e₂))
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
cases' h with hφy h'
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : HEq (Path.cons (mapPath φ p₁) (φ.map e₁)) (Path.cons (mapPath φ p₂) (φ.map e₂))
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
rw [← Path.cast_eq_iff_heq rfl hφy, Path.cast_cons, Path.cast_rfl_rfl] at h' 
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
have hφx := Path.obj_eq_of_cons_eq_cons h'
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
have hφp := Path.heq_of_cons_eq_cons h'
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : HEq (mapPath φ p₁) (mapPath φ p₂)
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
have hφe := HEq.trans (Hom.cast_heq rfl hφy _).symm (Path.hom_heq_of_cons_eq_cons h')
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : HEq (mapPath φ p₁) (mapPath φ p₂)
hφe : HEq (φ.map e₁) (φ.map e₂)
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
have h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₂, p₂⟩ := by
  simp only [Prefunctor.pathStar_apply, Sigma.mk.inj_iff]; exact ⟨hφx, hφp⟩
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : HEq (mapPath φ p₁) (mapPath φ p₂)
hφe : HEq (φ.map e₁) (φ.map e₂)
⊢ pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₂, snd := p₂ }
[PROOFSTEP]
simp only [Prefunctor.pathStar_apply, Sigma.mk.inj_iff]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : HEq (mapPath φ p₁) (mapPath φ p₂)
hφe : HEq (φ.map e₁) (φ.map e₂)
⊢ φ.obj x₁ = φ.obj x₂ ∧ HEq (mapPath φ p₁) (mapPath φ p₂)
[PROOFSTEP]
exact ⟨hφx, hφp⟩
[GOAL]
case mk.cons.mk.cons.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₂) (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : HEq (mapPath φ p₁) (mapPath φ p₂)
hφe : HEq (φ.map e₁) (φ.map e₂)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₂, snd := p₂ }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₂ e₂ }
[PROOFSTEP]
cases ih h_path_star
[GOAL]
case mk.cons.mk.cons.intro.refl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : HEq (φ.map e₁) (φ.map e₂)
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₁) (φ.map e₂)
hφp : HEq (mapPath φ p₁) (mapPath φ p₁)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₁, snd := p₁ }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₁ e₂ }
[PROOFSTEP]
have h_star : φ.star x₁ ⟨y₁, e₁⟩ = φ.star x₁ ⟨y₂, e₂⟩ := by simp only [Prefunctor.star_apply, Sigma.mk.inj_iff];
  exact ⟨hφy, hφe⟩
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : HEq (φ.map e₁) (φ.map e₂)
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₁) (φ.map e₂)
hφp : HEq (mapPath φ p₁) (mapPath φ p₁)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₁, snd := p₁ }
⊢ star φ x₁ { fst := y₁, snd := e₁ } = star φ x₁ { fst := y₂, snd := e₂ }
[PROOFSTEP]
simp only [Prefunctor.star_apply, Sigma.mk.inj_iff]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : HEq (φ.map e₁) (φ.map e₂)
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₁) (φ.map e₂)
hφp : HEq (mapPath φ p₁) (mapPath φ p₁)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₁, snd := p₁ }
⊢ φ.obj y₁ = φ.obj y₂ ∧ HEq (φ.map e₁) (φ.map e₂)
[PROOFSTEP]
exact ⟨hφy, hφe⟩
[GOAL]
case mk.cons.mk.cons.intro.refl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : HEq (φ.map e₁) (φ.map e₂)
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₁) (φ.map e₂)
hφp : HEq (mapPath φ p₁) (mapPath φ p₁)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₁, snd := p₁ }
h_star : star φ x₁ { fst := y₁, snd := e₁ } = star φ x₁ { fst := y₂, snd := e₂ }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₂, snd := Path.cons p₁ e₂ }
[PROOFSTEP]
cases hφ x₁ h_star
[GOAL]
case mk.cons.mk.cons.intro.refl.refl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.13746
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Injective (star φ u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := x₁, snd := p₁ } =
        (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a₂ →
      { fst := x₁, snd := p₁ } = a₂
hφx : φ.obj x₁ = φ.obj x₁
hφp : HEq (mapPath φ p₁) (mapPath φ p₁)
h_path_star : pathStar φ u { fst := x₁, snd := p₁ } = pathStar φ u { fst := x₁, snd := p₁ }
hφy : φ.obj y₁ = φ.obj y₁
hφe : HEq (φ.map e₁) (φ.map e₁)
h' : Path.cons (mapPath φ p₁) (Hom.cast (_ : φ.obj x₁ = φ.obj x₁) hφy (φ.map e₁)) = Path.cons (mapPath φ p₁) (φ.map e₁)
h_star : star φ x₁ { fst := y₁, snd := e₁ } = star φ x₁ { fst := y₁, snd := e₁ }
⊢ { fst := y₁, snd := Path.cons p₁ e₁ } = { fst := y₁, snd := Path.cons p₁ e₁ }
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
⊢ Surjective (pathStar φ u)
[PROOFSTEP]
dsimp [Prefunctor.pathStar, Quiver.PathStar.mk]
[GOAL]
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
⊢ Surjective fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }
[PROOFSTEP]
rintro ⟨v, p⟩
[GOAL]
case mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
p : Path (φ.obj u) v
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v, snd := p }
[PROOFSTEP]
induction' p with v' v'' p' ev ih
[GOAL]
case mk.nil
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := φ.obj u, snd := Path.nil }
[PROOFSTEP]
use⟨u, Path.nil⟩
[GOAL]
case h
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u, snd := Path.nil } =
    { fst := φ.obj u, snd := Path.nil }
[PROOFSTEP]
simp only [Prefunctor.mapPath_nil, eq_self_iff_true, heq_iff_eq, and_self_iff]
[GOAL]
case mk.cons
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v' v'' : V
p' : Path (φ.obj u) v'
ev : v' ⟶ v''
ih : ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v', snd := p' }
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons p' ev }
[PROOFSTEP]
obtain ⟨⟨u', q'⟩, h⟩ := ih
[GOAL]
case mk.cons.intro.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v' v'' : V
p' : Path (φ.obj u) v'
ev : v' ⟶ v''
u' : U
q' : Path u u'
h : (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u', snd := q' } = { fst := v', snd := p' }
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons p' ev }
[PROOFSTEP]
simp only at h 
[GOAL]
case mk.cons.intro.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v' v'' : V
p' : Path (φ.obj u) v'
ev : v' ⟶ v''
u' : U
q' : Path u u'
h : { fst := φ.obj u', snd := mapPath φ q' } = { fst := v', snd := p' }
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons p' ev }
[PROOFSTEP]
obtain ⟨rfl, rfl⟩ := h
[GOAL]
case mk.cons.intro.mk.refl
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v'' : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ v''
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons (mapPath φ q') ev }
[PROOFSTEP]
obtain ⟨⟨u'', eu⟩, k⟩ := hφ u' ⟨_, ev⟩
[GOAL]
case mk.cons.intro.mk.refl.intro.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v'' : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ v''
u'' : U
eu : u' ⟶ u''
k : star φ u' { fst := u'', snd := eu } = { fst := v'', snd := ev }
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons (mapPath φ q') ev }
[PROOFSTEP]
simp only [star_apply, Sigma.mk.inj_iff] at k 
[GOAL]
case mk.cons.intro.mk.refl.intro.mk
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v v'' : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ v''
u'' : U
eu : u' ⟶ u''
k : φ.obj u'' = v'' ∧ HEq (φ.map eu) ev
⊢ ∃ a, (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a = { fst := v'', snd := Path.cons (mapPath φ q') ev }
[PROOFSTEP]
obtain ⟨rfl, k⟩ := k
[GOAL]
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
ev : φ.obj u' ⟶ φ.obj u''
k : HEq (φ.map eu) ev
⊢ ∃ a,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a =
      { fst := φ.obj u'', snd := Path.cons (mapPath φ q') ev }
[PROOFSTEP]
simp only [heq_eq_eq] at k 
[GOAL]
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
ev : φ.obj u' ⟶ φ.obj u''
k : φ.map eu = ev
⊢ ∃ a,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a =
      { fst := φ.obj u'', snd := Path.cons (mapPath φ q') ev }
[PROOFSTEP]
subst k
[GOAL]
case mk.cons.intro.mk.refl.intro.mk.intro
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
⊢ ∃ a,
    (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) a =
      { fst := φ.obj u'', snd := Path.cons (mapPath φ q') (φ.map eu) }
[PROOFSTEP]
use⟨_, q'.cons eu⟩
[GOAL]
case h
U : Type u_1
inst✝² : Quiver U
V : Type u_2
inst✝¹ : Quiver V
φ : U ⥤q V
W : Type ?u.16907
inst✝ : Quiver W
ψ : V ⥤q W
hφ : ∀ (u : U), Surjective (star φ u)
u : U
v : V
u' : U
q' : Path u u'
u'' : U
eu : u' ⟶ u''
⊢ (fun p => { fst := φ.obj p.fst, snd := mapPath φ p.snd }) { fst := u'', snd := Path.cons q' eu } =
    { fst := φ.obj u'', snd := Path.cons (mapPath φ q') (φ.map eu) }
[PROOFSTEP]
simp only [Prefunctor.mapPath_cons, eq_self_iff_true, heq_iff_eq, and_self_iff]
[GOAL]
U : Type ?u.18936
inst✝⁵ : Quiver U
V : Type ?u.18942
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.18964
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : Prefunctor.MapReverse φ
u : U
e : Star u
⊢ (fun e => { fst := e.fst, snd := reverse e.snd }) ((fun e => { fst := e.fst, snd := reverse e.snd }) e) = e
[PROOFSTEP]
simp [Sigma.ext_iff]
[GOAL]
U : Type ?u.18936
inst✝⁵ : Quiver U
V : Type ?u.18942
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.18964
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : Prefunctor.MapReverse φ
u : U
e : Costar u
⊢ (fun e => { fst := e.fst, snd := reverse e.snd }) ((fun e => { fst := e.fst, snd := reverse e.snd }) e) = e
[PROOFSTEP]
simp [Sigma.ext_iff]
[GOAL]
U : Type u_1
inst✝⁵ : Quiver U
V : Type u_2
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.20680
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : MapReverse φ
u : U
⊢ costar φ u = ↑(starEquivCostar (φ.obj u)) ∘ star φ u ∘ ↑(starEquivCostar u).symm
[PROOFSTEP]
ext ⟨v, f⟩
[GOAL]
case h.mk.h₀
U : Type u_1
inst✝⁵ : Quiver U
V : Type u_2
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.20680
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : MapReverse φ
u v : U
f : v ⟶ u
⊢ (costar φ u { fst := v, snd := f }).fst =
    ((↑(starEquivCostar (φ.obj u)) ∘ star φ u ∘ ↑(starEquivCostar u).symm) { fst := v, snd := f }).fst
[PROOFSTEP]
simp
[GOAL]
case h.mk.h₁
U : Type u_1
inst✝⁵ : Quiver U
V : Type u_2
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.20680
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : MapReverse φ
u v : U
f : v ⟶ u
⊢ HEq (costar φ u { fst := v, snd := f }).snd
    ((↑(starEquivCostar (φ.obj u)) ∘ star φ u ∘ ↑(starEquivCostar u).symm) { fst := v, snd := f }).snd
[PROOFSTEP]
simp
[GOAL]
U : Type u_1
inst✝⁵ : Quiver U
V : Type u_2
inst✝⁴ : Quiver V
φ : U ⥤q V
W : Type ?u.22299
inst✝³ : Quiver W
ψ : V ⥤q W
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : MapReverse φ
u : U
⊢ Bijective (costar φ u) ↔ Bijective (star φ u)
[PROOFSTEP]
rw [Prefunctor.costar_conj_star, EquivLike.comp_bijective, EquivLike.bijective_comp]
