Theorem: Graph.SubgroupCover.Quot.localSection_composition' (GroupComp/Graph/SubgroupCover.lean)

State before:
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 }⟧
Tactic:
rw [localSection_composition]
State after:
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 }⟧

State before:
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 }⟧
Tactic:
apply Quotient.sound
State after:
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
⊢ { τ₀ := τ, τ₁ := 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 }

State before:
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
⊢ { τ₀ := τ, τ₁ := 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 }
Tactic:
simp [nxt.term_eq]
State after:
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
⊢ { τ₀ := τ, τ₁ := 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 }

State before:
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
⊢ { τ₀ := τ, τ₁ := 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 }
Tactic:
have : (⟨τ, G.τ (nxt.edge),
  ⟨nxt.edge, Eq.symm h, rfl⟩, p, is_reduced⟩ : Edge G x₀) =
  ⟨τ, τ₁,
  ⟨nxt.edge, Eq.symm h, nxt.term_eq⟩, p, is_reduced⟩ := by
  simp [nxt.term_eq, eq_of_edge_eq]
  congr
  rw [nxt.term_eq]
  have l {τ : V}(pf: G.τ nxt.edge = τ) :
    HEq (rfl: G.τ nxt.edge  = G.τ nxt.edge ) pf   := by
    cases pf
    simp
  apply l nxt.term_eq
State after:
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 }

State before:
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 }
Tactic:
rw [this]
State after:
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 }

State before:
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 }
Tactic:
apply @Setoid.refl _ (edgeSetoid H)
State after:
no goals

State before:
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.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 }
Tactic:
simp [nxt.term_eq, eq_of_edge_eq]
State after:
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
⊢ HEq { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) }
    { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }

State before:
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
⊢ HEq { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) }
    { edge := nxt.edge, init_eq := (_ : G.ι nxt.edge = τ), term_eq := (_ : Graph.τ G nxt.edge = τ₁) }
Tactic:
congr
State after:
case e_5.h
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.edge = τ₁

case e_8
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
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)

State before:
case e_5.h
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.edge = τ₁

case e_8
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
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)
Tactic:
rw [nxt.term_eq]
State after:
case e_8
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
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)

State before:
case e_8
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
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)
Tactic:
have l {τ : V}(pf: G.τ nxt.edge = τ) :
  HEq (rfl: G.τ nxt.edge  = G.τ nxt.edge ) pf   := by
  cases pf
  simp
State after:
case e_8
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
l : ∀ {τ : V} (pf : Graph.τ G nxt.edge = τ), HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) pf
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)

State before:
case e_8
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
l : ∀ {τ : V} (pf : Graph.τ G nxt.edge = τ), HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) pf
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = τ₁)
Tactic:
apply l nxt.term_eq
State after:
no goals

State before:
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
τ : V
pf : Graph.τ G nxt.edge = τ
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) pf
Tactic:
cases pf
State after:
case refl
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
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge)

State before:
case refl
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
⊢ HEq (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge) (_ : Graph.τ G nxt.edge = Graph.τ G nxt.edge)
Tactic:
simp
State after:
no goals