internlm/Lean-Github huggingface dataset:
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a.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₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra✝ :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra✝
contra : [[p ++ reverse (p:+e)]] ∈ H ∧ e = EdgeBetween.bar e
⊢ False
Tactic:
let c := contra.2
Proof state after:
case a.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₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra✝ :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra✝
contra : [[p ++ reverse (p:+e)]] ∈ H ∧ e = EdgeBetween.bar e
c : e = EdgeBetween.bar e := contra.right
⊢ False
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a.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₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra✝ :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra✝
contra : [[p ++ reverse (p:+e)]] ∈ H ∧ e = EdgeBetween.bar e
c : e = EdgeBetween.bar e := contra.right
⊢ False
Tactic:
have : e.bar.edge = e.edge := by rw [← c]
Proof state after:
case a.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₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra✝ :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra✝
contra : [[p ++ reverse (p:+e)]] ∈ H ∧ e = EdgeBetween.bar e
c : e = EdgeBetween.bar e := contra.right
this : (EdgeBetween.bar e).edge = e.edge
⊢ False
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a.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₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra✝ :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra✝
contra : [[p ++ reverse (p:+e)]] ∈ H ∧ e = EdgeBetween.bar e
c : e = EdgeBetween.bar e := contra.right
this : (EdgeBetween.bar e).edge = e.edge
⊢ False
Tactic:
simp at this
Proof state after:
case a.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₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra✝ :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra✝
contra : [[p ++ reverse (p:+e)]] ∈ H ∧ e = EdgeBetween.bar e
c : e = EdgeBetween.bar e := contra.right
this : G.bar e.edge = e.edge
⊢ False
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a.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₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra✝ :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra✝
contra : [[p ++ reverse (p:+e)]] ∈ H ∧ e = EdgeBetween.bar e
c : e = EdgeBetween.bar e := contra.right
this : G.bar e.edge = e.edge
⊢ False
Tactic:
let nfp := G.bar_ne_self e.edge
Proof state after:
case a.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₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra✝ :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra✝
contra : [[p ++ reverse (p:+e)]] ∈ H ∧ e = EdgeBetween.bar e
c : e = EdgeBetween.bar e := contra.right
this : G.bar e.edge = e.edge
nfp : e.edge ≠ G.bar e.edge := G.bar_ne_self e.edge
⊢ False
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof state before:
case a.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₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra✝ :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra✝
contra : [[p ++ reverse (p:+e)]] ∈ H ∧ e = EdgeBetween.bar e
c : e = EdgeBetween.bar e := contra.right
this : G.bar e.edge = e.edge
nfp : e.edge ≠ G.bar e.edge := G.bar_ne_self e.edge
⊢ False
Tactic:
simp [this] at nfp
Proof state after:
no goals
Theorem: Graph.SubgroupCover.Quot.bar_ne_self
Proof 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₀ τ₀
pf : reduced p
e : EdgeBetween G τ₀ τ₀
contra✝ :
  { τ₀ := τ₀, τ₁ := τ₀, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₀, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : τ₀ = τ₀ := terminal₀_eq_of_r H contra✝
contra : [[p ++ reverse (p:+e)]] ∈ H ∧ e = EdgeBetween.bar e
c : e = EdgeBetween.bar e := contra.right
⊢ (EdgeBetween.bar e).edge = e.edge
Tactic:
rw [← c]
Proof state after:
no goals
Theorem: Graph.SubgroupCover.Quot.toFuncV_init
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (ebar : Quotient (edgeSetoid H)), toFuncV H ((groupCover H).ι ebar) = G.ι (toFuncE H ebar)
Tactic:
apply Quotient.ind
Proof 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₀)
⊢ ∀ (a : Edge G x₀), toFuncV H ((groupCover H).ι ⟦a⟧) = G.ι (toFuncE H ⟦a⟧)
Theorem: Graph.SubgroupCover.Quot.toFuncV_init
Proof 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₀)
⊢ ∀ (a : Edge G x₀), toFuncV H ((groupCover H).ι ⟦a⟧) = G.ι (toFuncE H ⟦a⟧)
Tactic:
intro e
Proof 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₀)
e : Edge G x₀
⊢ toFuncV H ((groupCover H).ι ⟦e⟧) = G.ι (toFuncE H ⟦e⟧)
Theorem: Graph.SubgroupCover.Quot.toFuncV_init
Proof 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₀)
e : Edge G x₀
⊢ toFuncV H ((groupCover H).ι ⟦e⟧) = G.ι (toFuncE H ⟦e⟧)
Tactic:
rw [initial]
Proof 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₀)
e : Edge G x₀
⊢ toFuncV H ⟦(univ G x₀).ι e⟧ = G.ι (toFuncE H ⟦e⟧)
Theorem: Graph.SubgroupCover.Quot.toFuncV_init
Proof 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₀)
e : Edge G x₀
⊢ toFuncV H ⟦(univ G x₀).ι e⟧ = G.ι (toFuncE H ⟦e⟧)
Tactic:
rw [toFuncV_defn, toFuncE_defn]
Proof 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₀)
e : Edge G x₀
⊢ ((univ G x₀).ι e).τ = G.ι e.nxt.edge
Theorem: Graph.SubgroupCover.Quot.toFuncV_init
Proof 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₀)
e : Edge G x₀
⊢ ((univ G x₀).ι e).τ = G.ι e.nxt.edge
Tactic:
apply (proj G x₀).toFuncV_init
Proof state after:
no goals
Theorem: Graph.SubgroupCover.Quot.toFuncE_bar
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ ∀ (ebar : Quotient (edgeSetoid H)), toFuncE H ((groupCover H).bar ebar) = G.bar (toFuncE H ebar)
Tactic:
apply Quotient.ind
Proof 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₀)
⊢ ∀ (a : Edge G x₀), toFuncE H ((groupCover H).bar ⟦a⟧) = G.bar (toFuncE H ⟦a⟧)
Theorem: Graph.SubgroupCover.Quot.toFuncE_bar
Proof 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₀)
⊢ ∀ (a : Edge G x₀), toFuncE H ((groupCover H).bar ⟦a⟧) = G.bar (toFuncE H ⟦a⟧)
Tactic:
intro e
Proof 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₀)
e : Edge G x₀
⊢ toFuncE H ((groupCover H).bar ⟦e⟧) = G.bar (toFuncE H ⟦e⟧)
Theorem: Graph.SubgroupCover.Quot.toFuncE_bar
Proof 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₀)
e : Edge G x₀
⊢ toFuncE H ((groupCover H).bar ⟦e⟧) = G.bar (toFuncE H ⟦e⟧)
Tactic:
rw [toFuncE_defn, bar_eq_barn']
Proof 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₀)
e : Edge G x₀
⊢ toFuncE H ⟦(univ G x₀).bar e⟧ = G.bar e.nxt.edge
Theorem: Graph.SubgroupCover.Quot.toFuncE_bar
Proof 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₀)
e : Edge G x₀
⊢ toFuncE H ⟦(univ G x₀).bar e⟧ = G.bar e.nxt.edge
Tactic:
apply (proj G x₀).toFuncE_bar
Proof state after:
no goals
Theorem: Graph.SubgroupCover.projections_compose
Proof state before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
⊢ Morphism.comp (groupCoverProj H) (univGroupProj H) = proj G x₀
Tactic:
ext
Proof state after:
case toFuncV.h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x✝ : Vert G x₀
⊢ (Morphism.comp (groupCoverProj H) (univGroupProj H)).toFuncV x✝ = (proj G x₀).toFuncV x✝

case toFuncE.h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x✝ : Edge G x₀
⊢ (Morphism.comp (groupCoverProj H) (univGroupProj H)).toFuncE x✝ = (proj G x₀).toFuncE x✝
Theorem: Graph.SubgroupCover.projections_compose
Proof state before:
case toFuncV.h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x✝ : Vert G x₀
⊢ (Morphism.comp (groupCoverProj H) (univGroupProj H)).toFuncV x✝ = (proj G x₀).toFuncV x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.SubgroupCover.projections_compose
Proof state before:
case toFuncE.h
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
H : Subgroup (π₁ G x₀)
x✝ : Edge G x₀
⊢ (Morphism.comp (groupCoverProj H) (univGroupProj H)).toFuncE x✝ = (proj G x₀).toFuncE x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
Proof 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]
Proof 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 }⟧
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
Proof 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
Proof 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 }
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
Proof 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]
Proof 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 }
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
Proof 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
Proof 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 }
Theorem: Graph.SubgroupCover.Quot.localSection_composition'
Proof 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]
Proof 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 }