Theorem: SimpleGraph.Menger.AB_Walk.minimal_ext (Untitled/Graphs/Menger.lean)

State before:
V : Type u_1
V' : Type u_2
inst✝¹ : Fintype V
inst✝ : Fintype V'
G G₁ G₂ : SimpleGraph V
a : V
A B X Y Z : Finset V
p : AB_Walk G₁ A B
p' : AB_Walk G₂ A B
h : Walk.support p.to_Walk = Walk.support p'.to_Walk
⊢ minimal p ↔ minimal p'
Tactic:
simp_rw [minimal, Walk.init_eq_take_support, Walk.tail_eq_tail_support, h]
State after:
no goals