rw [this]
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ : V
p : EdgePath G x₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
this :
  { τ₀ := τ, τ₁ := Graph.τ G nxt.edge,
      nxt :=
        { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ),
          term_eq := (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) },
      p := p, is_reduced := is_reduced } =
    { τ₀ := τ, τ₁ := τ₁,
      nxt := { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }, p := p,
      is_reduced := is_reduced }
⊢ { τ₀ := τ, τ₁ := Graph.τ G { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := is_reduced' }.nxt.edge,
      nxt :=
        { edge := nxt.edge,
          init_eq := (_ : G.ι { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := is_reduced' }.nxt.edge = τ),
          term_eq :=
            (_ :
              Graph.τ G { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := is_reduced' }.nxt.edge =
                Graph.τ G { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := is_reduced' }.nxt.edge) },
      p := p, is_reduced := is_reduced } ≈
    { τ₀ := τ, τ₁ := τ₁,
      nxt := { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }, p := p,
      is_reduced := is_reduced }
case a
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
τ : V
p : EdgePath G x₀ τ
is_reduced : reduced p
τ₀ τ₁ : V
nxt : EdgeBetween G τ₀ τ₁
p' : EdgePath G x₀ τ₀
is_reduced' : reduced p'
h : τ = G.ι nxt.edge
this :
  { τ₀ := τ, τ₁ := Graph.τ G nxt.edge,
      nxt :=
        { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ),
          term_eq := (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) },
      p := p, is_reduced := is_reduced } =
    { τ₀ := τ, τ₁ := τ₁,
      nxt := { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }, p := p,
      is_reduced := is_reduced }
⊢ { τ₀ := τ, τ₁ := τ₁,
      nxt := { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }, p := p,
      is_reduced := is_reduced } ≈
    { τ₀ := τ, τ₁ := τ₁,
      nxt := { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }, p := p,
      is_reduced := is_reduced }