C : Type u
inst✝⁴ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ (preComp f (g ≫ h) ≫ preComp g h) ≫ ι h = (eqToHom (_ : f ≫ g ≫ h = (f ≫ g) ≫ h) ≫ preComp (f ≫ g) h) ≫ ι h
C : Type u
inst✝⁴ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ preComp f (g ≫ h) ≫ preComp g h = eqToHom (_ : f ≫ g ≫ h = (f ≫ g) ≫ h) ≫ preComp (f ≫ g) h
apply (cancel_mono (image.ι h)).1
C : Type u
inst✝⁴ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ (lift (MonoFactorisation.mk (image (g ≫ h)) (ι (g ≫ h)) (f ≫ factorThruImage (g ≫ h))) ≫
        lift (MonoFactorisation.mk (image h) (ι h) (g ≫ factorThruImage h))) ≫
      ι h =
    (lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
        lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h))) ≫
      ι h
C : Type u
inst✝⁴ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ (preComp f (g ≫ h) ≫ preComp g h) ≫ ι h = (eqToHom (_ : f ≫ g ≫ h = (f ≫ g) ≫ h) ≫ preComp (f ≫ g) h) ≫ ι h
dsimp [image.preComp, image.eqToHom]
C : Type u
inst✝⁴ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ ι (f ≫ g ≫ h) =
    lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
      lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h)) ≫ ι h
C : Type u
inst✝⁴ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ (lift (MonoFactorisation.mk (image (g ≫ h)) (ι (g ≫ h)) (f ≫ factorThruImage (g ≫ h))) ≫
        lift (MonoFactorisation.mk (image h) (ι h) (g ≫ factorThruImage h))) ≫
      ι h =
    (lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
        lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h))) ≫
      ι h
repeat (rw [Category.assoc,image.lift_fac])
no goals
C : Type u
inst✝⁴ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ ι (f ≫ g ≫ h) =
    lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
      lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h)) ≫ ι h
rw [image.lift_fac,image.lift_fac]
C : Type u
inst✝⁴ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ ι (f ≫ g ≫ h) =
    lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
      lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h)) ≫ ι h
C : Type u
inst✝⁴ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ ι (f ≫ g ≫ h) =
    lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
      lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h)) ≫ ι h
(rw [Category.assoc,image.lift_fac])
C : Type u
inst✝⁴ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ ι (f ≫ g ≫ h) =
    lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
      lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h)) ≫ ι h
C : Type u
inst✝⁴ : Category C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ ι (f ≫ g ≫ h) =
    lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
      lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h)) ≫ ι h
rw [Category.assoc,image.lift_fac]