no goals
B : Type u
inst✝ : Quiver B
a b c : B
f : Hom a b
g : Hom b c
⊢ normalizeAux nil (Hom.comp f g) = comp (normalizeAux nil f) (normalizeAux nil g)
induction g generalizing a with
| id => rfl
| of => rfl
| comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]
no goals
case id
B : Type u
inst✝ : Quiver B
b c a✝ a : B
f : Hom a a✝
⊢ normalizeAux nil (Hom.comp f (Hom.id a✝)) = comp (normalizeAux nil f) (normalizeAux nil (Hom.id a✝))
rfl
no goals
case of
B : Type u
inst✝ : Quiver B
b c a✝ b✝ : B
f✝ : a✝ ⟶ b✝
a : B
f : Hom a a✝
⊢ normalizeAux nil (Hom.comp f (Hom.of f✝)) = comp (normalizeAux nil f) (normalizeAux nil (Hom.of f✝))
rfl
no goals
case comp
B : Type u
inst✝ : Quiver B
b c a✝ b✝ c✝ : B
g : Hom a✝ b✝
g✝ : Hom b✝ c✝
ihf : ∀ {a : B} (f : Hom a a✝), normalizeAux nil (Hom.comp f g) = comp (normalizeAux nil f) (normalizeAux nil g)
ihg : ∀ {a : B} (f : Hom a b✝), normalizeAux nil (Hom.comp f g✝) = comp (normalizeAux nil f) (normalizeAux nil g✝)
a : B
f : Hom a a✝
⊢ normalizeAux nil (Hom.comp f (Hom.comp g g✝)) = comp (normalizeAux nil f) (normalizeAux nil (Hom.comp g g✝))
erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]