case f
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f ⟶ underlying.obj (sSup s)

case w
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ?f ≫ arrow (sSup s) = arrow f
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ f ≤ sSup s
fapply le_of_comm
case f
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f =
    underlying.obj
      (↑(equivShrink (Subobject A)).symm
        ↑{ val := ↑(equivShrink (Subobject A)) f,
            property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) })
case f
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f ⟶ underlying.obj (sSup s)
refine' eqToHom _ ≫ Sigma.ι _ ⟨equivShrink (Subobject A) f, by simpa [Set.mem_image] using hf⟩
  ≫ factorThruImage _ ≫ (underlyingIso _).inv
no goals
case f
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f =
    underlying.obj
      (↑(equivShrink (Subobject A)).symm
        ↑{ val := ↑(equivShrink (Subobject A)) f,
            property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) })
exact (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _).symm)
no goals
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s
simpa [Set.mem_image] using hf
no goals
case w
C : Type u₁
inst✝⁴ : Category C
X Y Z : C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ (eqToHom
          (_ :
            underlying.obj f =
              underlying.obj
                (↑(equivShrink (Subobject A)).symm
                  ↑{ val := ↑(equivShrink (Subobject A)) f,
                      property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) })) ≫
        Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j))
            { val := ↑(equivShrink (Subobject A)) f,
              property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) } ≫
          factorThruImage (smallCoproductDesc s) ≫ (underlyingIso (image.ι (smallCoproductDesc s))).inv) ≫
      arrow (sSup s) =
    arrow f
simp [sSup, smallCoproductDesc]