Theorem: Graph.Subgraph.contains_reverse (GroupComp/Subgraph.lean)

State before:
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v : V
p : EdgePath G u v
⊢ contains H p → contains H (EdgePath.reverse p)
Tactic:
induction p with
  | nil => simp only  [contains_nil, EdgePath.reverse_nil, imp_self]
  | cons e p' ih =>
    rw [EdgePath.reverse_cons]
    simp only [contains_cons, contains_concat, EdgeBetween.bar_eq_bar, and_imp]
    intro he hp'H
    exact ⟨H.edges_bar _ he, ih hp'H⟩
State after:
no goals

State before:
case nil
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ : V
⊢ contains H (EdgePath.nil v✝) → contains H (EdgePath.reverse (EdgePath.nil v✝))
Tactic:
simp only  [contains_nil, EdgePath.reverse_nil, imp_self]
State after:
no goals

State before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ contains H (EdgePath.cons e p') → contains H (EdgePath.reverse (EdgePath.cons e p'))
Tactic:
rw [EdgePath.reverse_cons]
State after:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ contains H (EdgePath.cons e p') → contains H (EdgePath.concat (EdgePath.reverse p') (EdgeBetween.bar e))

State before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ contains H (EdgePath.cons e p') → contains H (EdgePath.concat (EdgePath.reverse p') (EdgeBetween.bar e))
Tactic:
simp only [contains_cons, contains_concat, EdgeBetween.bar_eq_bar, and_imp]
State after:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ e.edge ∈ H.edges → contains H p' → G.bar e.edge ∈ H.edges ∧ contains H (EdgePath.reverse p')

State before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
⊢ e.edge ∈ H.edges → contains H p' → G.bar e.edge ∈ H.edges ∧ contains H (EdgePath.reverse p')
Tactic:
intro he hp'H
State after:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
he : e.edge ∈ H.edges
hp'H : contains H p'
⊢ G.bar e.edge ∈ H.edges ∧ contains H (EdgePath.reverse p')

State before:
case cons
V : Type u_1
E : Type u_2
G : Graph V E
H : Subgraph G
u v v✝ w✝ u✝ : V
e : EdgeBetween G v✝ w✝
p' : EdgePath G w✝ u✝
ih : contains H p' → contains H (EdgePath.reverse p')
he : e.edge ∈ H.edges
hp'H : contains H p'
⊢ G.bar e.edge ∈ H.edges ∧ contains H (EdgePath.reverse p')
Tactic:
exact ⟨H.edges_bar _ he, ih hp'H⟩
State after:
no goals