case mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
hinj : Injective ↑f
u v : V
p : Walk G u v
hp : Walk.IsPath p
p' : Walk G u v
hp' : Walk.IsPath p'
h : Path.map f hinj { val := p, property := hp } = Path.map f hinj { val := p', property := hp' }
⊢ { val := p, property := hp } = { val := p', property := hp' }
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
hinj : Injective ↑f
u v : V
⊢ Injective (Path.map f hinj)
rintro ⟨p, hp⟩ ⟨p', hp'⟩ h
case mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
hinj : Injective ↑f
u v : V
p : Walk G u v
hp : Walk.IsPath p
p' : Walk G u v
hp' : Walk.IsPath p'
h : Walk.map f p = Walk.map f p'
⊢ { val := p, property := hp } = { val := p', property := hp' }
case mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
hinj : Injective ↑f
u v : V
p : Walk G u v
hp : Walk.IsPath p
p' : Walk G u v
hp' : Walk.IsPath p'
h : Path.map f hinj { val := p, property := hp } = Path.map f hinj { val := p', property := hp' }
⊢ { val := p, property := hp } = { val := p', property := hp' }
simp only [Path.map, Subtype.coe_mk, Subtype.mk.injEq] at h
no goals
case mk.mk
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
hinj : Injective ↑f
u v : V
p : Walk G u v
hp : Walk.IsPath p
p' : Walk G u v
hp' : Walk.IsPath p'
h : Walk.map f p = Walk.map f p'
⊢ { val := p, property := hp } = { val := p', property := hp' }
simp [Walk.map_injective_of_injective hinj u v h]