Theorem: SimpleGraph.support_push_Walk (Untitled/Graphs/Walk.lean)

State before:
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
⊢ Walk.support (push_Walk f p) ⊆ List.map f (Walk.support p)
Tactic:
induction p with
| nil => simp [push_Walk]
| cons h p ih =>
  rename_i u v w
  by_cases h : f u = f v <;> simpa [push_Walk, h] using ih.trans <| List.subset_cons _ _
State after:
no goals

State before:
case nil
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p : Walk G a b
u✝ : V
⊢ Walk.support (push_Walk f Walk.nil) ⊆ List.map f (Walk.support Walk.nil)
Tactic:
simp [push_Walk]
State after:
no goals

State before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : Walk.support (push_Walk f p) ⊆ List.map f (Walk.support p)
⊢ Walk.support (push_Walk f (Walk.cons h p)) ⊆ List.map f (Walk.support (Walk.cons h p))
Tactic:
rename_i u v w
State after:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : Walk.support (push_Walk f p) ⊆ List.map f (Walk.support p)
⊢ Walk.support (push_Walk f (Walk.cons h p)) ⊆ List.map f (Walk.support (Walk.cons h p))

State before:
case cons
V : Type u_1
V' : Type u_2
a b c d : V
G G' : SimpleGraph V
f : V → V'
p✝ : Walk G a b
u v w : V
h : Adj G u v
p : Walk G v w
ih : Walk.support (push_Walk f p) ⊆ List.map f (Walk.support p)
⊢ Walk.support (push_Walk f (Walk.cons h p)) ⊆ List.map f (Walk.support (Walk.cons h p))
Tactic:
by_cases h : f u = f v <;> simpa [push_Walk, h] using ih.trans <| List.subset_cons _ _
State after:
no goals