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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ underlying.obj (sSup s) ⟶ underlying.obj f

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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ ?f ≫ arrow f = arrow (sSup s)
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ sSup s ≤ f
fapply le_of_comm
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          (MonoFactorisation.mk (underlying.obj f) (arrow f)
            (Sigma.desc fun b =>
              Subtype.casesOn b fun g m =>
                underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m } ≤ f))))) ≫
      arrow f =
    arrow (sSup s)
. dsimp [sSup]
  rw [assoc, image.lift_fac, underlyingIso_hom_comp_eq_mk]
case f.refine'_1
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ (∐ fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) ⟶ underlying.obj f

case f.refine'_2
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ ?f.refine'_1 ≫ arrow f = smallCoproductDesc 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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ underlying.obj (sSup s) ⟶ underlying.obj f
refine'(underlyingIso _).hom ≫ image.lift ⟨_, f.arrow, _, _⟩
case f.refine'_1
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ (b : ↑(↑(equivShrink (Subobject A)) '' s)) → underlying.obj (↑(equivShrink (Subobject A)).symm ↑b) ⟶ underlying.obj f
case f.refine'_1
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ (∐ fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) ⟶ underlying.obj f
refine' Sigma.desc _
case f.refine'_1.mk
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
g : Shrink (Subobject A)
m : g ∈ ↑(equivShrink (Subobject A)) '' s
⊢ underlying.obj (↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m }) ⟶ underlying.obj f
case f.refine'_1
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ (b : ↑(↑(equivShrink (Subobject A)) '' s)) → underlying.obj (↑(equivShrink (Subobject A)).symm ↑b) ⟶ underlying.obj f
rintro ⟨g, m⟩
case f.refine'_1.mk
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
g : Shrink (Subobject A)
m : g ∈ ↑(equivShrink (Subobject A)) '' s
⊢ ↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m } ∈ s
case f.refine'_1.mk
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
g : Shrink (Subobject A)
m : g ∈ ↑(equivShrink (Subobject A)) '' s
⊢ underlying.obj (↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m }) ⟶ underlying.obj f
refine' underlying.map (homOfLE (k _ _))
no goals
case f.refine'_1.mk
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
g : Shrink (Subobject A)
m : g ∈ ↑(equivShrink (Subobject A)) '' s
⊢ ↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m } ∈ s
simpa [symm_apply_mem_iff_mem_image] using m
case f.refine'_2.h
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
b✝ : ↑(↑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b =>
          Subtype.casesOn b fun g m =>
            underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m } ≤ f))) ≫
        arrow f =
    Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫ smallCoproductDesc s
case f.refine'_2
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ (Sigma.desc fun b =>
        Subtype.casesOn b fun g m =>
          underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m } ≤ f))) ≫
      arrow f =
    smallCoproductDesc s
ext
case f.refine'_2.h
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
b✝ : ↑(↑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b => underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑b ≤ f))) ≫ arrow f =
    Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      Sigma.desc fun j => arrow (↑(equivShrink (Subobject A)).symm ↑j)
case f.refine'_2.h
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
b✝ : ↑(↑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b =>
          Subtype.casesOn b fun g m =>
            underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m } ≤ f))) ≫
        arrow f =
    Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫ smallCoproductDesc s
dsimp [smallCoproductDesc]
no goals
case f.refine'_2.h
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
b✝ : ↑(↑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b => underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑b ≤ f))) ≫ arrow f =
    Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      Sigma.desc fun j => arrow (↑(equivShrink (Subobject A)).symm ↑j)
simp
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          (MonoFactorisation.mk (underlying.obj f) (arrow f)
            (Sigma.desc fun b => underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑b ≤ f))))) ≫
      arrow f =
    arrow (mk (image.ι (smallCoproductDesc 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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          (MonoFactorisation.mk (underlying.obj f) (arrow f)
            (Sigma.desc fun b =>
              Subtype.casesOn b fun g m =>
                underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m } ≤ f))))) ≫
      arrow f =
    arrow (sSup s)
dsimp [sSup]
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
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          (MonoFactorisation.mk (underlying.obj f) (arrow f)
            (Sigma.desc fun b => underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑b ≤ f))))) ≫
      arrow f =
    arrow (mk (image.ι (smallCoproductDesc s)))
rw [assoc, image.lift_fac, underlyingIso_hom_comp_eq_mk]