Theorem: GroupLabelledGraph.pathClassLabel_append (GroupComp/GroupLabelledGraph.lean)

State before:
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
⊢ ∀ (p : u ⟶ v) (p' : v ⟶ w), pathClassLabel 𝓖 (p ≫ p') = pathClassLabel 𝓖 p * pathClassLabel 𝓖 p'
Tactic:
apply Quot.ind
State after:
case mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
⊢ ∀ (a : Graph.EdgePath Γ u v) (p' : v ⟶ w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a ≫ p') =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a) * pathClassLabel 𝓖 p'

State before:
case mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
⊢ ∀ (a : Graph.EdgePath Γ u v) (p' : v ⟶ w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a ≫ p') =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a) * pathClassLabel 𝓖 p'
Tactic:
intro p
State after:
case mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
⊢ ∀ (p' : v ⟶ w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ p') =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 p'

State before:
case mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
⊢ ∀ (p' : v ⟶ w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ p') =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 p'
Tactic:
apply Quot.ind
State after:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
⊢ ∀ (a : Graph.EdgePath Γ v w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ Quot.mk Graph.EdgePath.Reduction a) =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a)

State before:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
⊢ ∀ (a : Graph.EdgePath Γ v w),
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ Quot.mk Graph.EdgePath.Reduction a) =
      pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction a)
Tactic:
intro p'
State after:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
p' : Graph.EdgePath Γ v w
⊢ pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ Quot.mk Graph.EdgePath.Reduction p') =
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p')

State before:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
p' : Graph.EdgePath Γ v w
⊢ pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p ≫ Quot.mk Graph.EdgePath.Reduction p') =
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p')
Tactic:
show 𝓖.pathLabel (_ ++ _) = _
State after:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
p' : Graph.EdgePath Γ v w
⊢ pathLabel 𝓖 (p ++ p') =
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p')

State before:
case mk.mk
V : Type u_1
E : Type u_2
G : Type u_3
Γ : Graph V E
inst✝ : Group G
u✝ v✝ w✝ : V
g h : G
𝓖 : GroupLabelledGraph Γ G
u v w : V
p : Graph.EdgePath Γ u v
p' : Graph.EdgePath Γ v w
⊢ pathLabel 𝓖 (p ++ p') =
    pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p) * pathClassLabel 𝓖 (Quot.mk Graph.EdgePath.Reduction p')
Tactic:
simp only [pathLabel_append, pathClassLabel]
State after:
no goals