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 : SimpleGraph V
hp : ∀ (e : Sym2 V), e ∈ edges p → e ∈ edgeSet H
⊢ ∀ (e : Sym2 V), e ∈ edges p → e ∈ edgeSet H
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 : SimpleGraph V
hp : ∀ (e : Sym2 V), e ∈ edges p → e ∈ edgeSet H
⊢ ∀ (e : Sym2 V), e ∈ edges (reverse p) → e ∈ edgeSet H
simp only [edges_reverse, List.mem_reverse']
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 : SimpleGraph V
hp : ∀ (e : Sym2 V), e ∈ edges p → e ∈ edgeSet H
⊢ ∀ (e : Sym2 V), e ∈ edges p → e ∈ edgeSet H
exact hp
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 : SimpleGraph V
hp : ∀ (e : Sym2 V), e ∈ edges p → e ∈ edgeSet H
⊢ reverse (Walk.transfer p H hp) =
    Walk.transfer (reverse p) H (_ : ∀ (e : Sym2 V), e ∈ edges (reverse p) → e ∈ edgeSet H)
induction p with
| nil => simp
| cons _ _ ih => simp only [transfer_append, Walk.transfer, reverse_nil, reverse_cons, ih]
no goals
case nil
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 : SimpleGraph V
u✝ : V
hp : ∀ (e : Sym2 V), e ∈ edges nil → e ∈ edgeSet H
⊢ reverse (Walk.transfer nil H hp) =
    Walk.transfer (reverse nil) H (_ : ∀ (e : Sym2 V), e ∈ edges (reverse nil) → e ∈ edgeSet H)
simp
no goals
case cons
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 : SimpleGraph V
u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
ih :
  ∀ (hp : ∀ (e : Sym2 V), e ∈ edges p✝ → e ∈ edgeSet H),
    reverse (Walk.transfer p✝ H hp) =
      Walk.transfer (reverse p✝) H (_ : ∀ (e : Sym2 V), e ∈ edges (reverse p✝) → e ∈ edgeSet H)
hp : ∀ (e : Sym2 V), e ∈ edges (cons h✝ p✝) → e ∈ edgeSet H
⊢ reverse (Walk.transfer (cons h✝ p✝) H hp) =
    Walk.transfer (reverse (cons h✝ p✝)) H (_ : ∀ (e : Sym2 V), e ∈ edges (reverse (cons h✝ p✝)) → e ∈ edgeSet H)
simp only [transfer_append, Walk.transfer, reverse_nil, reverse_cons, ih]