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

State before:
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
h : Morphism G₃ G₄
g : Morphism G₂ G₃
f : Morphism G₁ G₂
⊢ comp h (comp g f) = comp (comp h g) f
Tactic:
cases h
State after:
case mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
g : Morphism G₂ G₃
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 { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
      (comp g f) =
    comp
      (comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ } g)
      f

State before:
case mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
g : Morphism G₂ G₃
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 { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
      (comp g f) =
    comp
      (comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ } g)
      f
Tactic:
cases g
State after:
case mk.mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
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)
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 { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
      (comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
        f) =
    comp
      (comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
        { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ })
      f

State before:
case mk.mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f✝ : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
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)
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 { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
      (comp { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }
        f) =
    comp
      (comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
        { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ })
      f
Tactic:
cases f
State after:
case mk.mk.mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
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)
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)
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 { toFuncV := toFuncV✝², toFuncE := toFuncE✝², toFuncV_init := toFuncV_init✝², toFuncE_bar := toFuncE_bar✝² }
      (comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
        { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }) =
    comp
      (comp { toFuncV := toFuncV✝², toFuncE := toFuncE✝², toFuncV_init := toFuncV_init✝², toFuncE_bar := toFuncE_bar✝² }
        { 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.mk.mk
V₁ : Type u_7
E₁ : Type u_8
V₂ : Type u_5
E₂ : Type u_6
V : Type u
E : Type v
G₁ : Graph V₁ E₁
G₂ : Graph V₂ E₂
f : Morphism G₁ G₂
V₃ : Type u_1
E₃ : Type u_2
V✝ : Type u_3
E✝ : Type u_4
G₄ : Graph V✝ E✝
G₃ : Graph V₃ E₃
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)
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)
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 { toFuncV := toFuncV✝², toFuncE := toFuncE✝², toFuncV_init := toFuncV_init✝², toFuncE_bar := toFuncE_bar✝² }
      (comp { toFuncV := toFuncV✝¹, toFuncE := toFuncE✝¹, toFuncV_init := toFuncV_init✝¹, toFuncE_bar := toFuncE_bar✝¹ }
        { toFuncV := toFuncV✝, toFuncE := toFuncE✝, toFuncV_init := toFuncV_init✝, toFuncE_bar := toFuncE_bar✝ }) =
    comp
      (comp { toFuncV := toFuncV✝², toFuncE := toFuncE✝², toFuncV_init := toFuncV_init✝², toFuncE_bar := toFuncE_bar✝² }
        { 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