Theorem: Graph.SubgroupCover.Quot.toFuncV_init (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)), toFuncV H ((groupCover H).ι ebar) = G.ι (toFuncE 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₀), toFuncV H ((groupCover H).ι ⟦a⟧) = G.ι (toFuncE 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₀), toFuncV H ((groupCover H).ι ⟦a⟧) = G.ι (toFuncE H ⟦a⟧)
Tactic:
intro e
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₀)
e : Edge G x₀
⊢ toFuncV H ((groupCover H).ι ⟦e⟧) = G.ι (toFuncE H ⟦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₀)
e : Edge G x₀
⊢ toFuncV H ((groupCover H).ι ⟦e⟧) = G.ι (toFuncE H ⟦e⟧)
Tactic:
rw [initial]
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₀)
e : Edge G x₀
⊢ toFuncV H ⟦(univ G x₀).ι e⟧ = G.ι (toFuncE H ⟦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₀)
e : Edge G x₀
⊢ toFuncV H ⟦(univ G x₀).ι e⟧ = G.ι (toFuncE H ⟦e⟧)
Tactic:
rw [toFuncV_defn, toFuncE_defn]
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₀)
e : Edge G x₀
⊢ ((univ G x₀).ι e).τ = G.ι e.nxt.edge

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₀)
e : Edge G x₀
⊢ ((univ G x₀).ι e).τ = G.ι e.nxt.edge
Tactic:
apply (proj G x₀).toFuncV_init
State after:
no goals