Theorem: Graph.UniversalCover.Edge.bar_bar (GroupComp/Graph/UniversalCover.lean)

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ bar G x₀ (bar G x₀ e) = e
Tactic:
simp only [bar, EdgeBetween.bar_bar]
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
      is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) } =
    e

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
      is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) } =
    e
Tactic:
ext
State after:
case τ₀
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.τ₀ =
    e.τ₀

case τ₁
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.τ₁ =
    e.τ₁

case nxt
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ HEq
    { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.nxt
    e.nxt

case p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ HEq
    { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.p
    e.p

State before:
case τ₀
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.τ₀ =
    e.τ₀
Tactic:
rfl
State after:
no goals

State before:
case τ₁
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.τ₁ =
    e.τ₁
Tactic:
rfl
State after:
no goals

State before:
case nxt
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ HEq
    { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.nxt
    e.nxt
Tactic:
rfl
State after:
no goals

State before:
case p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ HEq
    { τ₀ := (bar G x₀ e).τ₁, τ₁ := (bar G x₀ e).τ₀, nxt := e.nxt, p := e.p:+e.nxt:+EdgeBetween.bar e.nxt,
        is_reduced := (_ : reduced (e.p:+e.nxt:+EdgeBetween.bar e.nxt)) }.p
    e.p
Tactic:
simp only [Eq.ndrec, id_eq, heq_eq_eq]
State after:
case p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ e.p:+e.nxt:+EdgeBetween.bar e.nxt = e.p

State before:
case p
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ e.p:+e.nxt:+EdgeBetween.bar e.nxt = e.p
Tactic:
apply reducedConcat_cancel_pair
State after:
case p.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ reduced e.p

State before:
case p.hyp
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
⊢ reduced e.p
Tactic:
exact e.is_reduced
State after:
no goals