Theorem: Graph.SubgroupCover.edge_eq_of_r (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₀)
⊢ ∀ {e₁ e₂ : Edge G x₀}, Setoid.r e₁ e₂ → e₁.nxt.edge = e₂.nxt.edge
Tactic:
intro ⟨τ₀, τ₁, e, p, _⟩ ⟨τ₀', τ₁', e', p', _⟩
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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₀' τ₁' : V
e' : EdgeBetween G τ₀' τ₁'
p' : EdgePath G x₀ τ₀'
is_reduced✝ : reduced p'
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₀' τ₁' : V
e' : EdgeBetween G τ₀' τ₁'
p' : EdgePath G x₀ τ₀'
is_reduced✝ : reduced p'
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Tactic:
if c:τ₀=τ₀' ∧ τ₁ = τ₁' then
  cases c.left
  cases c.right
  simp [Setoid.r, relH]
  intro _ h
  rw [h]
else
  simp [Setoid.r, relH, c]
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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₀' τ₁' : V
e' : EdgeBetween G τ₀' τ₁'
p' : EdgePath G x₀ τ₀'
is_reduced✝ : reduced p'
c : τ₀ = τ₀' ∧ τ₁ = τ₁'
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Tactic:
cases c.left
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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₁' : V
e' : EdgeBetween G τ₀ τ₁'
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
c : τ₀ = τ₀ ∧ τ₁ = τ₁'
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀, τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀, τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₁' : V
e' : EdgeBetween G τ₀ τ₁'
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
c : τ₀ = τ₀ ∧ τ₁ = τ₁'
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀, τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀, τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Tactic:
cases c.right
State after:
case refl.refl
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₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀, τ₁ := τ₁, nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀, τ₁ := τ₁, nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge

State before:
case refl.refl
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₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀, τ₁ := τ₁, nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀, τ₁ := τ₁, nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Tactic:
simp [Setoid.r, relH]
State after:
case refl.refl
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₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
⊢ [[p ++ reverse p']] ∈ H → e = e' → e.edge = e'.edge

State before:
case refl.refl
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₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
⊢ [[p ++ reverse p']] ∈ H → e = e' → e.edge = e'.edge
Tactic:
intro _ h
State after:
case refl.refl
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₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
a✝ : [[p ++ reverse p']] ∈ H
h : e = e'
⊢ e.edge = e'.edge

State before:
case refl.refl
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₀ τ₀
is_reduced✝¹ : reduced p
p' : EdgePath G x₀ τ₀
is_reduced✝ : reduced p'
e' : EdgeBetween G τ₀ τ₁
c : τ₀ = τ₀ ∧ τ₁ = τ₁
a✝ : [[p ++ reverse p']] ∈ H
h : e = e'
⊢ e.edge = e'.edge
Tactic:
rw [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
e : EdgeBetween G τ₀ τ₁
p : EdgePath G x₀ τ₀
is_reduced✝¹ : reduced p
τ₀' τ₁' : V
e' : EdgeBetween G τ₀' τ₁'
p' : EdgePath G x₀ τ₀'
is_reduced✝ : reduced p'
c : ¬(τ₀ = τ₀' ∧ τ₁ = τ₁')
⊢ Setoid.r { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ } →
    { τ₀ := τ₀, τ₁ := τ₁, nxt := e, p := p, is_reduced := is_reduced✝¹ }.nxt.edge =
      { τ₀ := τ₀', τ₁ := τ₁', nxt := e', p := p', is_reduced := is_reduced✝ }.nxt.edge
Tactic:
simp [Setoid.r, relH, c]
State after:
no goals