no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
d : Dart G
v w : V
h : d.snd = v
p : Walk G v w
⊢ List.Chain (DartAdj G) d (darts p)
induction p generalizing d with
| nil => exact List.Chain.nil
| cons h' p ih => exact List.Chain.cons (by exact h) (ih (by rfl))
no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u✝ : V
d : Dart G
h : d.snd = u✝
⊢ List.Chain (DartAdj G) d (darts nil)
exact List.Chain.nil
no goals
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u✝ v✝ w✝ : V
h' : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {d : Dart G}, d.snd = v✝ → List.Chain (DartAdj G) d (darts p)
d : Dart G
h : d.snd = u✝
⊢ List.Chain (DartAdj G) d (darts (cons h' p))
exact List.Chain.cons (by exact h) (ih (by rfl))
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u✝ v✝ w✝ : V
h' : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {d : Dart G}, d.snd = v✝ → List.Chain (DartAdj G) d (darts p)
d : Dart G
h : d.snd = u✝
⊢ DartAdj G d { toProd := (u✝, v✝), is_adj := h' }
exact h
no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
v w u✝ v✝ w✝ : V
h' : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : ∀ {d : Dart G}, d.snd = v✝ → List.Chain (DartAdj G) d (darts p)
d : Dart G
h : d.snd = u✝
⊢ { toProd := (u✝, v✝), is_adj := h' }.toProd.snd = v✝
rfl