case nil
C : Type u₁
inst✝ : Category C
X Y Z : C
f : Path X Y
⊢ composePath (Path.comp f Path.nil) = composePath f ≫ composePath Path.nil

case cons
C : Type u₁
inst✝ : Category C
X Y Z : C
f : Path X Y
Y' Z' : C
g : Path Y Y'
e : Y' ⟶ Z'
ih : composePath (Path.comp f g) = composePath f ≫ composePath g
⊢ composePath (Path.comp f (Path.cons g e)) = composePath f ≫ composePath (Path.cons g e)
C : Type u₁
inst✝ : Category C
X Y Z : C
f : Path X Y
g : Path Y Z
⊢ composePath (Path.comp f g) = composePath f ≫ composePath g
induction' g with Y' Z' g e ih
no goals
case nil
C : Type u₁
inst✝ : Category C
X Y Z : C
f : Path X Y
⊢ composePath (Path.comp f Path.nil) = composePath f ≫ composePath Path.nil
simp
no goals
case cons
C : Type u₁
inst✝ : Category C
X Y Z : C
f : Path X Y
Y' Z' : C
g : Path Y Y'
e : Y' ⟶ Z'
ih : composePath (Path.comp f g) = composePath f ≫ composePath g
⊢ composePath (Path.comp f (Path.cons g e)) = composePath f ≫ composePath (Path.cons g e)
simp [ih]