-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem map_isPath_of_injective (hinj : Function.Injective f) (hp : p.IsPath) :
    (p.map f).IsPath

Proof state:
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.IsPath → (Walk.map f p✝).IsPath
hp : p✝.IsPath ∧ u✝ ∉ p✝.support
⊢ (Walk.map f (cons h✝ p✝)).IsPath

Tactic:
simp only [map_cons, cons_isPath_iff, ih hp.1, support_map, List.mem_map, not_exists, not_and,
  true_and]

Result:
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.IsPath → (Walk.map f p✝).IsPath
hp : p✝.IsPath ∧ u✝ ∉ p✝.support
⊢ ∀ x ∈ p✝.support, ¬f x = f u✝

Proof state:
case cons.refl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.IsPath → (Walk.map f p✝).IsPath
hp : p✝.IsPath ∧ u✝ ∉ p✝.support
hx : u✝ ∈ p✝.support
hf : f u✝ = f u✝
⊢ False

Tactic:
exact hp.2 hx

Result:
no goals

Proof state:
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.IsPath → (Walk.map f p✝).IsPath
hp : (cons h✝ p✝).IsPath
⊢ (Walk.map f (cons h✝ p✝)).IsPath

Tactic:
rw [Walk.cons_isPath_iff] at hp

Result:
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.IsPath → (Walk.map f p✝).IsPath
hp : p✝.IsPath ∧ u✝ ∉ p✝.support
⊢ (Walk.map f (cons h✝ p✝)).IsPath

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
hp : p.IsPath
⊢ (Walk.map f p).IsPath

Tactic:
induction p with
| nil => simp
| cons _ _ ih =>
  rw [Walk.cons_isPath_iff] at hp
  simp only [map_cons, cons_isPath_iff, ih hp.1, support_map, List.mem_map, not_exists, not_and,
    true_and]
  intro x hx hf
  cases hinj hf
  exact hp.2 hx

Result:
no goals

Proof state:
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.IsPath → (Walk.map f p✝).IsPath
hp : p✝.IsPath ∧ u✝ ∉ p✝.support
⊢ ∀ x ∈ p✝.support, ¬f x = f u✝

Tactic:
intro x hx hf

Result:
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.IsPath → (Walk.map f p✝).IsPath
hp : p✝.IsPath ∧ u✝ ∉ p✝.support
x : V
hx : x ∈ p✝.support
hf : f x = f u✝
⊢ False

Proof state:
case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.IsPath → (Walk.map f p✝).IsPath
hp : p✝.IsPath ∧ u✝ ∉ p✝.support
x : V
hx : x ∈ p✝.support
hf : f x = f u✝
⊢ False

Tactic:
cases hinj hf

Result:
case cons.refl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : p✝.IsPath → (Walk.map f p✝).IsPath
hp : p✝.IsPath ∧ u✝ ∉ p✝.support
hx : u✝ ∈ p✝.support
hf : f u✝ = f u✝
⊢ False

Proof state:
case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hinj : Injective ⇑f
u✝ : V
hp : nil.IsPath
⊢ (Walk.map f nil).IsPath

Tactic:
simp

Result:
no goals