Theorem: Graph.SubgroupCover.Quot.bar_ne_self (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₀)
⊢ ∀ (ebar : Quotient (edgeSetoid H)), ebar ≠ bar H ebar
Tactic:
apply Quotient.ind
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₀), ⟦a⟧ ≠ bar H ⟦a⟧

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₀), ⟦a⟧ ≠ bar H ⟦a⟧
Tactic:
intro ⟨τ₀, τ₁, e, p, pf⟩
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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
⊢ ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ ≠
    bar H ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧

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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
⊢ ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ ≠
    bar H ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧
Tactic:
simp [bar_eq_barn, Edge.bar_eq_bar]
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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
⊢ ¬⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ =
      ⟦{ τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }⟧

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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
⊢ ¬⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ =
      ⟦{ τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }⟧
Tactic:
intro contra
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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ =
    ⟦{ τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }⟧
⊢ False

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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  ⟦{ τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }⟧ =
    ⟦{ τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }⟧
⊢ False
Tactic:
rw [@Quotient.eq _ (edgeSetoid H)] at contra
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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
⊢ False

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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
⊢ False
Tactic:
let lem := terminal₀_eq_of_r H contra
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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }.τ₀ =
  { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }.τ₀ :=
  terminal₀_eq_of_r H contra
⊢ False

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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
contra :
  { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf } ≈
    { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }
lem : { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := pf }.τ₀ =
  { τ₀ := τ₁, τ₁ := τ₀, nxt := EdgeBetween.bar e, p := p:+e, is_reduced := (_ : reduced (p:+e)) }.τ₀ :=
  terminal₀_eq_of_r H contra
⊢ False
Tactic:
simp only at lem
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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
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
⊢ False

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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
pf : reduced p
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
⊢ False
Tactic:
cases lem
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
⊢ False

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
⊢ False
Tactic:
simp [HasEquiv.Equiv, Setoid.r, relH] at contra
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
⊢ False

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
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

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]
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

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
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

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
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

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
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₀ τ₀
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]
State after:
no goals