Theorem: Graph.SubgroupCover.relH_symm (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₀)
τ : V
v₁ v₂ : EdgePath G x₀ τ
⊢ relH H v₁ v₂ → relH H v₂ v₁
Tactic:
simp [relH]
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
v₁ v₂ : EdgePath G x₀ τ
⊢ [[v₁ ++ reverse v₂]] ∈ H → [[v₂ ++ reverse v₁]] ∈ H

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
v₁ v₂ : EdgePath G x₀ τ
⊢ [[v₁ ++ reverse v₂]] ∈ H → [[v₂ ++ reverse v₁]] ∈ H
Tactic:
intro h
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
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
⊢ [[v₂ ++ reverse v₁]] ∈ H

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
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
⊢ [[v₂ ++ reverse v₁]] ∈ H
Tactic:
let h': [[v₁ ++ v₂.reverse]].inv ∈ H := inv_mem h
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
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
h' : PathClass.inv [[v₁ ++ reverse v₂]] ∈ H := inv_mem h
⊢ [[v₂ ++ reverse v₁]] ∈ H

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
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
h' : PathClass.inv [[v₁ ++ reverse v₂]] ∈ H := inv_mem h
⊢ [[v₂ ++ reverse v₁]] ∈ H
Tactic:
rw [inv_equiv_reverse,
  reverse_append,  reverse_reverse] at h'
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
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
h' : [[v₂ ++ reverse v₁]] ∈ H
⊢ [[v₂ ++ reverse v₁]] ∈ H

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
v₁ v₂ : EdgePath G x₀ τ
h : [[v₁ ++ reverse v₂]] ∈ H
h' : [[v₂ ++ reverse v₁]] ∈ H
⊢ [[v₂ ++ reverse v₁]] ∈ H
Tactic:
exact h'
State after:
no goals