Theorem: Graph.UniversalCover.Edge.bar_neq_self (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₀
⊢ e ≠ bar G x₀ e
Tactic:
intro contra
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
⊢ False

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
⊢ False
Tactic:
have : e.p.toList.length =  (bar G x₀ e).p.toList.length
   := by
    rw [← contra]
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (bar G x₀ e).p)
⊢ False

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (bar G x₀ e).p)
⊢ False
Tactic:
simp [bar, Edge.p] at this
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
⊢ False

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
⊢ False
Tactic:
let h' := concat_parity e.p e.nxt
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ ¬Even (List.length (EdgePath.toList e.p)) :=
  concat_parity e.p e.nxt
⊢ False

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ ¬Even (List.length (EdgePath.toList e.p)) :=
  concat_parity e.p e.nxt
⊢ False
Tactic:
rw [this] at h'
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ ¬Even (List.length (EdgePath.toList (e.p:+e.nxt)))
⊢ False

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ ¬Even (List.length (EdgePath.toList (e.p:+e.nxt)))
⊢ False
Tactic:
symm at h'
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : ¬Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ Even (List.length (EdgePath.toList (e.p:+e.nxt)))
⊢ False

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : ¬Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ Even (List.length (EdgePath.toList (e.p:+e.nxt)))
⊢ False
Tactic:
let h'' := not_iff_self  h'
State after:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : ¬Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ Even (List.length (EdgePath.toList (e.p:+e.nxt)))
h'' : False := not_iff_self h'
⊢ False

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
this : List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (e.p:+e.nxt))
h' : ¬Even (List.length (EdgePath.toList (e.p:+e.nxt))) ↔ Even (List.length (EdgePath.toList (e.p:+e.nxt)))
h'' : False := not_iff_self h'
⊢ False
Tactic:
assumption
State after:
no goals

State before:
V : Type u
E : Type v
inst✝¹ : DecidableEq V
inst✝ : DecidableEq E
G : Graph V E
x₀ : V
e : Edge G x₀
contra : e = bar G x₀ e
⊢ List.length (EdgePath.toList e.p) = List.length (EdgePath.toList (bar G x₀ e).p)
Tactic:
rw [← contra]
State after:
no goals