Theorem: Graph.liftTerminal_eq_of_homotopic (GroupComp/Graph/Covering.lean)

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h : p.toFuncV v₁ = v₂
e₁ e₂ : EdgePath G₂ v₂ w₂
red : [[e₁]] = [[e₂]]
⊢ liftTerminal p v₁ h e₁ = liftTerminal p v₁ h e₂
Tactic:
simp [liftTerminal]
State after:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h : p.toFuncV v₁ = v₂
e₁ e₂ : EdgePath G₂ v₂ w₂
red : [[e₁]] = [[e₂]]
⊢ (liftClass p v₁ v₂ w₂ h e₁).τ = (liftClass p v₁ v₂ w₂ h e₂).τ

State before:
V : Type u
E : Type v
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
p : Morphism G₁ G₂
inst✝ : CoveringMap p
v₁ : V₁
v₂ w₂ : V₂
h : p.toFuncV v₁ = v₂
e₁ e₂ : EdgePath G₂ v₂ w₂
red : [[e₁]] = [[e₂]]
⊢ (liftClass p v₁ v₂ w₂ h e₁).τ = (liftClass p v₁ v₂ w₂ h e₂).τ
Tactic:
rw [liftClass_eq_of_homotopic _ _ _ red]
State after:
no goals