no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w : V
p : Walk G u v
⊢ Walk.toSubgraph (reverse p) = Walk.toSubgraph p
induction p with
| nil => simp
| cons _ _ _ =>
  simp only [*, Walk.toSubgraph, reverse_cons, toSubgraph_append, subgraphOfAdj_symm]
  rw [sup_comm]
  congr
  ext <;> simp [-Set.bot_eq_empty]
no goals
case nil
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ : V
⊢ Walk.toSubgraph (reverse nil) = Walk.toSubgraph nil
simp
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : Walk.toSubgraph (reverse p✝) = Walk.toSubgraph p✝
⊢ Walk.toSubgraph p✝ ⊔ (subgraphOfAdj G (_ : Adj G u✝ v✝) ⊔ SimpleGraph.singletonSubgraph G u✝) =
    subgraphOfAdj G h✝ ⊔ Walk.toSubgraph p✝
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : Walk.toSubgraph (reverse p✝) = Walk.toSubgraph p✝
⊢ Walk.toSubgraph (reverse (cons h✝ p✝)) = Walk.toSubgraph (cons h✝ p✝)
simp only [*, Walk.toSubgraph, reverse_cons, toSubgraph_append, subgraphOfAdj_symm]
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : Walk.toSubgraph (reverse p✝) = Walk.toSubgraph p✝
⊢ subgraphOfAdj G (_ : Adj G u✝ v✝) ⊔ SimpleGraph.singletonSubgraph G u✝ ⊔ Walk.toSubgraph p✝ =
    subgraphOfAdj G h✝ ⊔ Walk.toSubgraph p✝
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : Walk.toSubgraph (reverse p✝) = Walk.toSubgraph p✝
⊢ Walk.toSubgraph p✝ ⊔ (subgraphOfAdj G (_ : Adj G u✝ v✝) ⊔ SimpleGraph.singletonSubgraph G u✝) =
    subgraphOfAdj G h✝ ⊔ Walk.toSubgraph p✝
rw [sup_comm]
case cons.e_a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : Walk.toSubgraph (reverse p✝) = Walk.toSubgraph p✝
⊢ subgraphOfAdj G (_ : Adj G u✝ v✝) ⊔ SimpleGraph.singletonSubgraph G u✝ = subgraphOfAdj G h✝
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : Walk.toSubgraph (reverse p✝) = Walk.toSubgraph p✝
⊢ subgraphOfAdj G (_ : Adj G u✝ v✝) ⊔ SimpleGraph.singletonSubgraph G u✝ ⊔ Walk.toSubgraph p✝ =
    subgraphOfAdj G h✝ ⊔ Walk.toSubgraph p✝
congr
no goals
case cons.e_a
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w u✝ v✝ w✝ : V
h✝ : Adj G u✝ v✝
p✝ : Walk G v✝ w✝
p_ih✝ : Walk.toSubgraph (reverse p✝) = Walk.toSubgraph p✝
⊢ subgraphOfAdj G (_ : Adj G u✝ v✝) ⊔ SimpleGraph.singletonSubgraph G u✝ = subgraphOfAdj G h✝
ext <;> simp [-Set.bot_eq_empty]