rw [localSection_composition]
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
⊢ localSection H ⟦{ τ := τ, p := p, is_reduced := is_reduced }⟧
      ((groupCoverProj H).toFuncE ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := is_reduced' }⟧) h =
    ⟦{ τ₀ := τ, τ₁ := τ₁,
        nxt := { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) },
        p := p, is_reduced := is_reduced }⟧
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
⊢ ⟦{ τ₀ := τ, τ₁ := Graph.τ G { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := is_reduced' }.nxt.edge,
        nxt :=
          { edge := { τ₀ := τ₀, τ₁ := τ₁, nxt := nxt, p := p', is_reduced := is_reduced' }.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 }⟧