-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem map_injective_of_injective {f : G →g G'} (hinj : Function.Injective f) (u v : V) :
    Function.Injective (Walk.map f : G.Walk u v → G'.Walk (f u) (f v))

Proof state:
case cons.cons.refl.h
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : G.Walk v✝ w✝
ih : ∀ ⦃p' : G.Walk v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : f v✝ = f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ Walk.map f p✝¹ = Walk.map f p✝

Tactic:
simpa using h.2

Result:
no goals

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

Tactic:
cases p' with
| nil => simp at h
| cons _ _ =>
  simp only [map_cons, cons.injEq] at h
  cases hinj h.1
  simp only [cons.injEq, heq_iff_eq, true_and]
  apply ih
  simpa using h.2

Result:
no goals

Proof state:
case cons.cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ ⦃p' : G.Walk v✝¹ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : Walk.map f (cons h✝¹ p✝¹) = Walk.map f (cons h✝ p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝

Tactic:
simp only [map_cons, cons.injEq] at h

Result:
case cons.cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ ⦃p' : G.Walk v✝¹ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : f v✝¹ = f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝

Proof state:
case cons.cons.refl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : G.Walk v✝ w✝
ih : ∀ ⦃p' : G.Walk v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : f v✝ = f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝

Tactic:
simp only [cons.injEq, heq_iff_eq, true_and]

Result:
case cons.cons.refl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : G.Walk v✝ w✝
ih : ∀ ⦃p' : G.Walk v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : f v✝ = f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ p✝¹ = p✝

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

Tactic:
intro p p' h

Result:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v : V
p p' : G.Walk u v
h : Walk.map f p = Walk.map f p'
⊢ p = p'

Proof state:
case cons.nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ u✝
ih : ∀ ⦃p' : G.Walk v✝ u✝⦄, Walk.map f p✝ = Walk.map f p' → p✝ = p'
h : Walk.map f (cons h✝ p✝) = Walk.map f nil
⊢ cons h✝ p✝ = nil

Tactic:
simp at h

Result:
no goals

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

Tactic:
simp at h

Result:
no goals

Proof state:
case cons.cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ ⦃p' : G.Walk v✝¹ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : f v✝¹ = f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝

Tactic:
cases hinj h.1

Result:
case cons.cons.refl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : G.Walk v✝ w✝
ih : ∀ ⦃p' : G.Walk v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : f v✝ = f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ cons h✝¹ p✝¹ = cons h✝ p✝

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

Tactic:
cases p'

Result:
case nil.nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ : V
h : Walk.map f nil = Walk.map f nil
⊢ nil = nil

case nil.cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ u✝
h : Walk.map f nil = Walk.map f (cons h✝ p✝)
⊢ nil = cons h✝ p✝

Proof state:
case cons.cons.refl
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : G.Walk v✝ w✝
ih : ∀ ⦃p' : G.Walk v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : f v✝ = f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ p✝¹ = p✝

Tactic:
apply ih

Result:
case cons.cons.refl.h
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ v✝ w✝ : V
h✝¹ : G.Adj u✝ v✝
p✝¹ : G.Walk v✝ w✝
ih : ∀ ⦃p' : G.Walk v✝ w✝⦄, Walk.map f p✝¹ = Walk.map f p' → p✝¹ = p'
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
h : f v✝ = f v✝ ∧ HEq (Walk.map f p✝¹) (Walk.map f p✝)
⊢ Walk.map f p✝¹ = Walk.map f p✝

Proof state:
case nil.nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective ⇑f
u v u✝ : V
h : Walk.map f nil = Walk.map f nil
⊢ nil = nil

Tactic:
rfl

Result:
no goals