[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ (u ⟶ v) = (u' ⟶ v')
[PROOFSTEP]
{rw [hu, hv]
}
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ (u ⟶ v) = (u' ⟶ v')
[PROOFSTEP]
rw [hu, hv]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ cast hu hv e = _root_.cast (_ : (u ⟶ v) = (u' ⟶ v')) e
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u' v' : U
e : u' ⟶ v'
⊢ cast (_ : u' = u') (_ : v' = v') e = _root_.cast (_ : (u' ⟶ v') = (u' ⟶ v')) e
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' u'' v'' : U
e : u ⟶ v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ cast hu' hv' (cast hu hv e) = cast (_ : u = u'') (_ : v = v'') e
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u'' v'' : U
e : u'' ⟶ v''
⊢ cast (_ : u'' = u'') (_ : v'' = v'') (cast (_ : u'' = u'') (_ : v'' = v'') e) = cast (_ : u'' = u'') (_ : v'' = v'') e
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
⊢ HEq (cast hu hv e) e
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u' v' : U
e : u' ⟶ v'
⊢ HEq (cast (_ : u' = u') (_ : v' = v') e) e
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ cast hu hv e = e' ↔ HEq e e'
[PROOFSTEP]
rw [Hom.cast_eq_cast]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ _root_.cast (_ : (u ⟶ v) = (u' ⟶ v')) e = e' ↔ HEq e e'
[PROOFSTEP]
exact _root_.cast_eq_iff_heq
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ e' = cast hu hv e ↔ HEq e' e
[PROOFSTEP]
rw [eq_comm, Hom.cast_eq_iff_heq]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
e : u ⟶ v
e' : u' ⟶ v'
⊢ HEq e e' ↔ HEq e' e
[PROOFSTEP]
exact ⟨HEq.symm, HEq.symm⟩
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ Path u v = Path u' v'
[PROOFSTEP]
rw [hu, hv]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ cast hu hv p = _root_.cast (_ : Path u v = Path u' v') p
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u' v' : U
p : Path u' v'
⊢ cast (_ : u' = u') (_ : v' = v') p = _root_.cast (_ : Path u' v' = Path u' v') p
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' u'' v'' : U
p : Path u v
hu : u = u'
hv : v = v'
hu' : u' = u''
hv' : v' = v''
⊢ cast hu' hv' (cast hu hv p) = cast (_ : u = u'') (_ : v = v'') p
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u'' v'' : U
p : Path u'' v''
⊢ cast (_ : u'' = u'') (_ : v'' = v'') (cast (_ : u'' = u'') (_ : v'' = v'') p) = cast (_ : u'' = u'') (_ : v'' = v'') p
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u u' : U
hu : u = u'
⊢ cast hu hu nil = nil
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
u' : U
⊢ cast (_ : u' = u') (_ : u' = u') nil = nil
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ HEq (cast hu hv p) p
[PROOFSTEP]
rw [Path.cast_eq_cast]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
⊢ HEq (_root_.cast (_ : Path u v = Path u' v') p) p
[PROOFSTEP]
exact _root_.cast_heq _ _
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
p' : Path u' v'
⊢ cast hu hv p = p' ↔ HEq p p'
[PROOFSTEP]
rw [Path.cast_eq_cast]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v u' v' : U
hu : u = u'
hv : v = v'
p : Path u v
p' : Path u' v'
⊢ _root_.cast (_ : Path u v = Path u' v') p = p' ↔ HEq p p'
[PROOFSTEP]
exact _root_.cast_eq_iff_heq
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v w u' w' : U
p : Path u v
e : v ⟶ w
hu : u = u'
hw : w = w'
⊢ cast hu hw (cons p e) = cons (cast hu (_ : v = v) p) (Hom.cast (_ : v = v) hw e)
[PROOFSTEP]
subst_vars
[GOAL]
U : Type u_1
inst✝ : Quiver U
v u' w' : U
p : Path u' v
e : v ⟶ w'
⊢ cast (_ : u' = u') (_ : w' = w') (cons p e) =
    cons (cast (_ : u' = u') (_ : v = v) p) (Hom.cast (_ : v = v) (_ : w' = w') e)
[PROOFSTEP]
rfl
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ Path.cast (_ : u = u) (_ : v = v') p = p'
[PROOFSTEP]
rw [Path.cast_eq_iff_heq]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ HEq p p'
[PROOFSTEP]
exact heq_of_cons_eq_cons h
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ Hom.cast (_ : v = v') (_ : w = w) e = e'
[PROOFSTEP]
rw [Hom.cast_eq_iff_heq]
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : cons p e = cons p' e'
⊢ HEq e e'
[PROOFSTEP]
exact hom_heq_of_cons_eq_cons h
[GOAL]
U : Type u_1
inst✝ : Quiver U
u v : U
p : Path u v
hzero : length p = 0
⊢ Path.cast (_ : u = v) (_ : v = v) p = nil
[PROOFSTEP]
cases p
[GOAL]
case nil
U : Type u_1
inst✝ : Quiver U
u : U
hzero : length nil = 0
⊢ Path.cast (_ : u = u) (_ : u = u) nil = nil
[PROOFSTEP]
rfl
[GOAL]
case cons
U : Type u_1
inst✝ : Quiver U
u v b✝ : U
a✝¹ : Path u b✝
a✝ : b✝ ⟶ v
hzero : length (cons a✝¹ a✝) = 0
⊢ Path.cast (_ : u = v) (_ : v = v) (cons a✝¹ a✝) = nil
[PROOFSTEP]
simp only [Nat.succ_ne_zero, length_cons] at hzero 
