Theorem: Digraph.Walk.edges_nodup_of_support_nodup (GraphProjects/DigraphConnectivity.lean)

State before:
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v : V
p : Walk G u v
h : List.Nodup (support p)
⊢ List.Nodup (edges p)
Tactic:
induction p with
| nil => simp
| cons _ p' ih =>
  simp only [edges_cons, support_cons, List.nodup_cons] at h ⊢
  exact ⟨fun h' => h.1 (edges_fst_mem_support_of_mem_darts p' h'), ih h.2⟩
State after:
no goals

State before:
case nil
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ : V
h : List.Nodup (support nil)
⊢ List.Nodup (edges nil)
Tactic:
simp
State after:
no goals

State before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : List.Nodup (support p') → List.Nodup (edges p')
h : List.Nodup (support (cons h✝ p'))
⊢ List.Nodup (edges (cons h✝ p'))
Tactic:
simp only [edges_cons, support_cons, List.nodup_cons] at h ⊢
State after:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : List.Nodup (support p') → List.Nodup (edges p')
h : ¬u✝ ∈ support p' ∧ List.Nodup (support p')
⊢ ¬(u✝, v✝) ∈ edges p' ∧ List.Nodup (edges p')

State before:
case cons
V : Type u
V' : Type v
V'' : Type w
G : Digraph V
G' : Digraph V'
G'' : Digraph V''
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p' : Walk G v✝ w✝
ih : List.Nodup (support p') → List.Nodup (edges p')
h : ¬u✝ ∈ support p' ∧ List.Nodup (support p')
⊢ ¬(u✝, v✝) ∈ edges p' ∧ List.Nodup (edges p')
Tactic:
exact ⟨fun h' => h.1 (edges_fst_mem_support_of_mem_darts p' h'), ih h.2⟩
State after:
no goals