simp only [cons.injEq, heq_iff_eq, true_and_iff]
case cons.cons.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ ⦃p' : Walk G v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : ↑f v✝ = ↑f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝
case cons.cons.refl
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
f✝ : G →g G'
f' : G' →g G''
u✝¹ v✝¹ u' v' : V
p : Walk G u✝¹ v✝¹
f : G →g G'
hinj : Injective ↑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : Walk G v✝ w✝
ih : ∀ ⦃p' : Walk G v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : Walk G v✝ w✝
h : ↑f v✝ = ↑f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ p✝¹ = p✝