Theorem: Graph.SubgroupCover.relH_refl (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 : EdgePath G x₀ τ
⊢ 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 : EdgePath G x₀ τ
⊢ CategoryTheory.CategoryStruct.id x₀ ∈ 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 : EdgePath G x₀ τ
⊢ CategoryTheory.CategoryStruct.id x₀ ∈ H
Tactic:
apply one_mem
State after:
no goals