Theorem: Graph.Morphism.id_comp (GroupComp/Graph/Covering.lean)

State before:
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ f : Morphism G₁ G₂
⊢ comp Morphism.id f = f
Tactic:
cases f
State after:
case mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
toFuncV✝ : V₁ → V₂
toFuncE✝ : E₁ → E₂
toFuncV_init✝ : ∀ (e : E₁), toFuncV✝ (G₁.ι e) = G₂.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₁), toFuncE✝ (G₁.bar e) = G₂.bar (toFuncE✝ e)
⊢ comp Morphism.id
      { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ } =
    { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }

State before:
case mk
V₁ : Type u_1
E₁ : Type u_2
V₂ : Type u_3
E₂ : Type u_4
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
toFuncV✝ : V₁ → V₂
toFuncE✝ : E₁ → E₂
toFuncV_init✝ : ∀ (e : E₁), toFuncV✝ (G₁.ι e) = G₂.ι (toFuncE✝ e)
toFuncE_bar✝ : ∀ (e : E₁), toFuncE✝ (G₁.bar e) = G₂.bar (toFuncE✝ e)
⊢ comp Morphism.id
      { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ } =
    { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
Tactic:
rfl
State after:
no goals