Theorem: SimpleGraph.tata (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
q : Walk G c d
h1 : a = c
h2 : b = d
⊢ Walk.copy p h1 h2 = q ↔ p = Walk.copy q (_ : c = a) (_ : d = b)
Tactic:
constructor <;> rintro rfl <;> simp
State after:
no goals