no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v : V
p : Walk G u v
h : List.Nodup (support p)
⊢ List.Nodup (darts p)
induction p with
| nil => simp
| cons _ p' ih =>
  simp only [darts_cons, support_cons, List.nodup_cons] at h ⊢
  exact ⟨fun h' => h.1 (dart_fst_mem_support_of_mem_darts p' h'), ih h.2⟩
no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ : V
h : List.Nodup (support nil)
⊢ List.Nodup (darts nil)
simp
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p' : Walk G v✝ w✝
ih : List.Nodup (support p') → List.Nodup (darts p')
h : ¬u✝ ∈ support p' ∧ List.Nodup (support p')
⊢ ¬{ toProd := (u✝, v✝), is_adj := h✝ } ∈ darts p' ∧ List.Nodup (darts p')
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p' : Walk G v✝ w✝
ih : List.Nodup (support p') → List.Nodup (darts p')
h : List.Nodup (support (cons h✝ p'))
⊢ List.Nodup (darts (cons h✝ p'))
simp only [darts_cons, support_cons, List.nodup_cons] at h ⊢
no goals
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p' : Walk G v✝ w✝
ih : List.Nodup (support p') → List.Nodup (darts p')
h : ¬u✝ ∈ support p' ∧ List.Nodup (support p')
⊢ ¬{ toProd := (u✝, v✝), is_adj := h✝ } ∈ darts p' ∧ List.Nodup (darts p')
exact ⟨fun h' => h.1 (dart_fst_mem_support_of_mem_darts p' h'), ih h.2⟩