Theorem: SimpleGraph.Walk.transportable_to_of_le (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✝
V : Type u_3
G G' : SimpleGraph V
a b : V
p : Walk G a b
G_le : G ≤ G'
⊢ transportable_to G' p
Tactic:
induction p with
| nil => simp [transportable_to]
| cons h p ih => simpa [transportable_to, G_le h] using ih
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✝
V : Type u_3
G G' : SimpleGraph V
a b : V
p : Walk G a b
G_le : G ≤ G'
u✝ : V
⊢ transportable_to G' nil
Tactic:
simp [transportable_to]
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✝
V : Type u_3
G G' : SimpleGraph V
a b : V
p✝ : Walk G a b
G_le : G ≤ G'
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p : Walk G v✝ w✝
ih : transportable_to G' p
⊢ transportable_to G' (cons h p)
Tactic:
simpa [transportable_to, G_le h] using ih
State after:
no goals