no goals
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w x : V
p : Walk G u v
q : Walk G v w
r : Walk G w x
⊢ append p (append q r) = append (append p q) r
induction p with
| nil => rfl
| cons h p' ih =>
  dsimp only [append]
  rw [ih]
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 x : V
r : Walk G w x
u✝ : V
q : Walk G u✝ w
⊢ append nil (append q r) = append (append nil q) r
rfl
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w x : V
r : Walk G w x
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p' : Walk G v✝ w✝
ih : ∀ (q : Walk G w✝ w), append p' (append q r) = append (append p' q) r
q : Walk G w✝ w
⊢ cons h (append p' (append q r)) = cons h (append (append p' q) r)
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w x : V
r : Walk G w x
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p' : Walk G v✝ w✝
ih : ∀ (q : Walk G w✝ w), append p' (append q r) = append (append p' q) r
q : Walk G w✝ w
⊢ append (cons h p') (append q r) = append (append (cons h p') q) r
dsimp only [append]
no goals
case cons
V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
u v w x : V
r : Walk G w x
u✝ v✝ w✝ : V
h : Adj G u✝ v✝
p' : Walk G v✝ w✝
ih : ∀ (q : Walk G w✝ w), append p' (append q r) = append (append p' q) r
q : Walk G w✝ w
⊢ cons h (append p' (append q r)) = cons h (append (append p' q) r)
rw [ih]