[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A : StructuredArrow S T
⊢ Subobject A → Subobject A.right
[PROOFSTEP]
refine' Subobject.lift (fun P f hf => Subobject.mk f.right) _
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A : StructuredArrow S T
⊢ ∀ ⦃A_1 B : StructuredArrow S T⦄ (f : A_1 ⟶ A) (g : B ⟶ A) [inst : Mono f] [inst_1 : Mono g] (i : A_1 ≅ B),
    i.hom ≫ g = f → (fun P f hf => Subobject.mk f.right) A_1 f inst = (fun P f hf => Subobject.mk f.right) B g inst_1
[PROOFSTEP]
intro P Q f g hf hg i hi
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ (fun P f hf => Subobject.mk f.right) P f hf = (fun P f hf => Subobject.mk f.right) Q g hg
[PROOFSTEP]
refine' Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i) _
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ ((proj S T).mapIso i).hom ≫ g.right = f.right
[PROOFSTEP]
exact congr_arg CommaMorphism.right hi
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
⊢ (P.hom ≫ T.map (Subobject.underlyingIso (MonoOver.arrow (MonoOver.mk' f)).right).inv) ≫
      T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) =
    A.hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
⊢ (P.hom ≫ T.map (Subobject.underlyingIso f.right).inv) ≫ T.map (Subobject.arrow (Subobject.mk f.right)) = A.hom
[PROOFSTEP]
simp [← T.map_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A : StructuredArrow S T
⊢ ∀ ⦃A_1 : StructuredArrow S T⦄ (f : A_1 ⟶ A) [inst : Mono f]
    {q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))}
    (hq : q ≫ T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) = A.hom),
    liftSubobject (projectSubobject (Subobject.mk f)) hq = Subobject.mk f
[PROOFSTEP]
intro P f hf q hq
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) = A.hom
⊢ liftSubobject (projectSubobject (Subobject.mk f)) hq = Subobject.mk f
[PROOFSTEP]
fapply Subobject.mk_eq_mk_of_comm
[GOAL]
case i
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) = A.hom
⊢ mk q ≅ P
[PROOFSTEP]
fapply isoMk
[GOAL]
case i.g
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) = A.hom
⊢ (mk q).right ≅ P.right
[PROOFSTEP]
exact Subobject.underlyingIso _
[GOAL]
case i.w
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) = A.hom
⊢ autoParam ((mk q).hom ≫ T.map (Subobject.underlyingIso (MonoOver.arrow (MonoOver.mk' f)).right).hom = P.hom) _auto✝
[PROOFSTEP]
exact (cancel_mono (T.map f.right)).1 (by dsimp; simpa [← T.map_comp] using hq)
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) = A.hom
⊢ ((mk q).hom ≫ T.map (Subobject.underlyingIso (MonoOver.arrow (MonoOver.mk' f)).right).hom) ≫ T.map f.right =
    P.hom ≫ T.map f.right
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) = A.hom
⊢ (q ≫ T.map (Subobject.underlyingIso f.right).hom) ≫ T.map f.right = P.hom ≫ T.map f.right
[PROOFSTEP]
simpa [← T.map_comp] using hq
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) = A.hom
⊢ (isoMk (Subobject.underlyingIso (MonoOver.arrow (MonoOver.mk' f)).right)).hom ≫ f =
    homMk (Subobject.arrow (projectSubobject (Subobject.mk f)))
[PROOFSTEP]
exact ext _ _ (by dsimp; simp)
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) = A.hom
⊢ ((isoMk (Subobject.underlyingIso (MonoOver.arrow (MonoOver.mk' f)).right)).hom ≫ f).right =
    (homMk (Subobject.arrow (projectSubobject (Subobject.mk f)))).right
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : (Functor.fromPUnit S).obj A.left ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (Subobject.arrow (projectSubobject (Subobject.mk f))) = A.hom
⊢ (Subobject.underlyingIso f.right).hom ≫ f.right = Subobject.arrow (Subobject.mk f.right)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A : StructuredArrow S T
P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }
⊢ ↑((fun P =>
          { val := projectSubobject P,
            property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
        ((fun P =>
            liftSubobject ↑P
              (_ :
                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) = A.hom))
          P)) =
    ↑P
[PROOFSTEP]
simp only [liftSubobject, homMk_right, projectSubobject_mk, Subobject.mk_arrow, Subtype.coe_eta]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A : StructuredArrow S T
⊢ ∀ {a b : Subobject A},
    ↑{
              toFun := fun P =>
                { val := projectSubobject P,
                  property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
              invFun := fun P =>
                liftSubobject ↑P
                  (_ :
                    Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) =
                      A.hom),
              left_inv :=
                (_ :
                  ∀ (P : Subobject A),
                    liftSubobject (projectSubobject P)
                        (_ :
                          Exists.choose
                                (_ :
                                  ∃ q,
                                    q ≫
                                        T.map
                                          (Subobject.arrow
                                            ↑((fun P =>
                                                  { val := projectSubobject P,
                                                    property :=
                                                      (_ :
                                                        ∃ q,
                                                          q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                                P)) =
                                      A.hom) ≫
                              T.map
                                (Subobject.arrow
                                  ↑((fun P =>
                                        { val := projectSubobject P,
                                          property :=
                                            (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                      P)) =
                            A.hom) =
                      P),
              right_inv :=
                (_ :
                  ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                    (fun P =>
                          { val := projectSubobject P,
                            property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                        ((fun P =>
                            liftSubobject ↑P
                              (_ :
                                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                    T.map (Subobject.arrow ↑P) =
                                  A.hom))
                          P) =
                      P) }
          a ≤
        ↑{
              toFun := fun P =>
                { val := projectSubobject P,
                  property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
              invFun := fun P =>
                liftSubobject ↑P
                  (_ :
                    Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) =
                      A.hom),
              left_inv :=
                (_ :
                  ∀ (P : Subobject A),
                    liftSubobject (projectSubobject P)
                        (_ :
                          Exists.choose
                                (_ :
                                  ∃ q,
                                    q ≫
                                        T.map
                                          (Subobject.arrow
                                            ↑((fun P =>
                                                  { val := projectSubobject P,
                                                    property :=
                                                      (_ :
                                                        ∃ q,
                                                          q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                                P)) =
                                      A.hom) ≫
                              T.map
                                (Subobject.arrow
                                  ↑((fun P =>
                                        { val := projectSubobject P,
                                          property :=
                                            (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                      P)) =
                            A.hom) =
                      P),
              right_inv :=
                (_ :
                  ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                    (fun P =>
                          { val := projectSubobject P,
                            property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                        ((fun P =>
                            liftSubobject ↑P
                              (_ :
                                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                    T.map (Subobject.arrow ↑P) =
                                  A.hom))
                          P) =
                      P) }
          b ↔
      a ≤ b
[PROOFSTEP]
apply Subobject.ind₂
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A : StructuredArrow S T
⊢ ∀ ⦃A_1 B : StructuredArrow S T⦄ (f : A_1 ⟶ A) (g : B ⟶ A) [inst : Mono f] [inst_1 : Mono g],
    ↑{
              toFun := fun P =>
                { val := projectSubobject P,
                  property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
              invFun := fun P =>
                liftSubobject ↑P
                  (_ :
                    Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) =
                      A.hom),
              left_inv :=
                (_ :
                  ∀ (P : Subobject A),
                    liftSubobject (projectSubobject P)
                        (_ :
                          Exists.choose
                                (_ :
                                  ∃ q,
                                    q ≫
                                        T.map
                                          (Subobject.arrow
                                            ↑((fun P =>
                                                  { val := projectSubobject P,
                                                    property :=
                                                      (_ :
                                                        ∃ q,
                                                          q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                                P)) =
                                      A.hom) ≫
                              T.map
                                (Subobject.arrow
                                  ↑((fun P =>
                                        { val := projectSubobject P,
                                          property :=
                                            (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                      P)) =
                            A.hom) =
                      P),
              right_inv :=
                (_ :
                  ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                    (fun P =>
                          { val := projectSubobject P,
                            property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                        ((fun P =>
                            liftSubobject ↑P
                              (_ :
                                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                    T.map (Subobject.arrow ↑P) =
                                  A.hom))
                          P) =
                      P) }
          (Subobject.mk f) ≤
        ↑{
              toFun := fun P =>
                { val := projectSubobject P,
                  property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
              invFun := fun P =>
                liftSubobject ↑P
                  (_ :
                    Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) =
                      A.hom),
              left_inv :=
                (_ :
                  ∀ (P : Subobject A),
                    liftSubobject (projectSubobject P)
                        (_ :
                          Exists.choose
                                (_ :
                                  ∃ q,
                                    q ≫
                                        T.map
                                          (Subobject.arrow
                                            ↑((fun P =>
                                                  { val := projectSubobject P,
                                                    property :=
                                                      (_ :
                                                        ∃ q,
                                                          q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                                P)) =
                                      A.hom) ≫
                              T.map
                                (Subobject.arrow
                                  ↑((fun P =>
                                        { val := projectSubobject P,
                                          property :=
                                            (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                      P)) =
                            A.hom) =
                      P),
              right_inv :=
                (_ :
                  ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                    (fun P =>
                          { val := projectSubobject P,
                            property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                        ((fun P =>
                            liftSubobject ↑P
                              (_ :
                                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                    T.map (Subobject.arrow ↑P) =
                                  A.hom))
                          P) =
                      P) }
          (Subobject.mk g) ↔
      Subobject.mk f ≤ Subobject.mk g
[PROOFSTEP]
intro P Q f g hf hg
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
⊢ ↑{
            toFun := fun P =>
              { val := projectSubobject P,
                property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
            invFun := fun P =>
              liftSubobject ↑P
                (_ :
                  Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) = A.hom),
            left_inv :=
              (_ :
                ∀ (P : Subobject A),
                  liftSubobject (projectSubobject P)
                      (_ :
                        Exists.choose
                              (_ :
                                ∃ q,
                                  q ≫
                                      T.map
                                        (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectSubobject P,
                                                  property :=
                                                    (_ :
                                                      ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                              P)) =
                                    A.hom) ≫
                            T.map
                              (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectSubobject P,
                                        property :=
                                          (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                    P)) =
                          A.hom) =
                    P),
            right_inv :=
              (_ :
                ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                  (fun P =>
                        { val := projectSubobject P,
                          property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                      ((fun P =>
                          liftSubobject ↑P
                            (_ :
                              Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                  T.map (Subobject.arrow ↑P) =
                                A.hom))
                        P) =
                    P) }
        (Subobject.mk f) ≤
      ↑{
            toFun := fun P =>
              { val := projectSubobject P,
                property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
            invFun := fun P =>
              liftSubobject ↑P
                (_ :
                  Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) = A.hom),
            left_inv :=
              (_ :
                ∀ (P : Subobject A),
                  liftSubobject (projectSubobject P)
                      (_ :
                        Exists.choose
                              (_ :
                                ∃ q,
                                  q ≫
                                      T.map
                                        (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectSubobject P,
                                                  property :=
                                                    (_ :
                                                      ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                              P)) =
                                    A.hom) ≫
                            T.map
                              (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectSubobject P,
                                        property :=
                                          (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                    P)) =
                          A.hom) =
                    P),
            right_inv :=
              (_ :
                ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                  (fun P =>
                        { val := projectSubobject P,
                          property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                      ((fun P =>
                          liftSubobject ↑P
                            (_ :
                              Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                  T.map (Subobject.arrow ↑P) =
                                A.hom))
                        P) =
                    P) }
        (Subobject.mk g) ↔
    Subobject.mk f ≤ Subobject.mk g
[PROOFSTEP]
refine' ⟨fun h => Subobject.mk_le_mk_of_comm _ _, fun h => _⟩
[GOAL]
case h.refine'_1
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h :
  ↑{
          toFun := fun P =>
            { val := projectSubobject P,
              property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
          invFun := fun P =>
            liftSubobject ↑P
              (_ :
                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) = A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject A),
                liftSubobject (projectSubobject P)
                    (_ :
                      Exists.choose
                            (_ :
                              ∃ q,
                                q ≫
                                    T.map
                                      (Subobject.arrow
                                        ↑((fun P =>
                                              { val := projectSubobject P,
                                                property :=
                                                  (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                            P)) =
                                  A.hom) ≫
                          T.map
                            (Subobject.arrow
                              ↑((fun P =>
                                    { val := projectSubobject P,
                                      property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                  P)) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                (fun P =>
                      { val := projectSubobject P,
                        property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                    ((fun P =>
                        liftSubobject ↑P
                          (_ :
                            Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                T.map (Subobject.arrow ↑P) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk f) ≤
    ↑{
          toFun := fun P =>
            { val := projectSubobject P,
              property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
          invFun := fun P =>
            liftSubobject ↑P
              (_ :
                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) = A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject A),
                liftSubobject (projectSubobject P)
                    (_ :
                      Exists.choose
                            (_ :
                              ∃ q,
                                q ≫
                                    T.map
                                      (Subobject.arrow
                                        ↑((fun P =>
                                              { val := projectSubobject P,
                                                property :=
                                                  (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                            P)) =
                                  A.hom) ≫
                          T.map
                            (Subobject.arrow
                              ↑((fun P =>
                                    { val := projectSubobject P,
                                      property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                  P)) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                (fun P =>
                      { val := projectSubobject P,
                        property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                    ((fun P =>
                        liftSubobject ↑P
                          (_ :
                            Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                T.map (Subobject.arrow ↑P) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk g)
⊢ P ⟶ Q
[PROOFSTEP]
exact homMk (Subobject.ofMkLEMk _ _ h) ((cancel_mono (T.map g.right)).1 (by simp [← T.map_comp]))
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h :
  ↑{
          toFun := fun P =>
            { val := projectSubobject P,
              property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
          invFun := fun P =>
            liftSubobject ↑P
              (_ :
                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) = A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject A),
                liftSubobject (projectSubobject P)
                    (_ :
                      Exists.choose
                            (_ :
                              ∃ q,
                                q ≫
                                    T.map
                                      (Subobject.arrow
                                        ↑((fun P =>
                                              { val := projectSubobject P,
                                                property :=
                                                  (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                            P)) =
                                  A.hom) ≫
                          T.map
                            (Subobject.arrow
                              ↑((fun P =>
                                    { val := projectSubobject P,
                                      property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                  P)) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                (fun P =>
                      { val := projectSubobject P,
                        property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                    ((fun P =>
                        liftSubobject ↑P
                          (_ :
                            Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                T.map (Subobject.arrow ↑P) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk f) ≤
    ↑{
          toFun := fun P =>
            { val := projectSubobject P,
              property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
          invFun := fun P =>
            liftSubobject ↑P
              (_ :
                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) = A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject A),
                liftSubobject (projectSubobject P)
                    (_ :
                      Exists.choose
                            (_ :
                              ∃ q,
                                q ≫
                                    T.map
                                      (Subobject.arrow
                                        ↑((fun P =>
                                              { val := projectSubobject P,
                                                property :=
                                                  (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                            P)) =
                                  A.hom) ≫
                          T.map
                            (Subobject.arrow
                              ↑((fun P =>
                                    { val := projectSubobject P,
                                      property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                  P)) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                (fun P =>
                      { val := projectSubobject P,
                        property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                    ((fun P =>
                        liftSubobject ↑P
                          (_ :
                            Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                T.map (Subobject.arrow ↑P) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk g)
⊢ (P.hom ≫
        T.map (Subobject.ofMkLEMk (MonoOver.arrow (MonoOver.mk' f)).right (MonoOver.arrow (MonoOver.mk' g)).right h)) ≫
      T.map g.right =
    Q.hom ≫ T.map g.right
[PROOFSTEP]
simp [← T.map_comp]
[GOAL]
case h.refine'_2
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h :
  ↑{
          toFun := fun P =>
            { val := projectSubobject P,
              property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
          invFun := fun P =>
            liftSubobject ↑P
              (_ :
                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) = A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject A),
                liftSubobject (projectSubobject P)
                    (_ :
                      Exists.choose
                            (_ :
                              ∃ q,
                                q ≫
                                    T.map
                                      (Subobject.arrow
                                        ↑((fun P =>
                                              { val := projectSubobject P,
                                                property :=
                                                  (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                            P)) =
                                  A.hom) ≫
                          T.map
                            (Subobject.arrow
                              ↑((fun P =>
                                    { val := projectSubobject P,
                                      property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                  P)) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                (fun P =>
                      { val := projectSubobject P,
                        property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                    ((fun P =>
                        liftSubobject ↑P
                          (_ :
                            Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                T.map (Subobject.arrow ↑P) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk f) ≤
    ↑{
          toFun := fun P =>
            { val := projectSubobject P,
              property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
          invFun := fun P =>
            liftSubobject ↑P
              (_ :
                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) = A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject A),
                liftSubobject (projectSubobject P)
                    (_ :
                      Exists.choose
                            (_ :
                              ∃ q,
                                q ≫
                                    T.map
                                      (Subobject.arrow
                                        ↑((fun P =>
                                              { val := projectSubobject P,
                                                property :=
                                                  (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                            P)) =
                                  A.hom) ≫
                          T.map
                            (Subobject.arrow
                              ↑((fun P =>
                                    { val := projectSubobject P,
                                      property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                  P)) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                (fun P =>
                      { val := projectSubobject P,
                        property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                    ((fun P =>
                        liftSubobject ↑P
                          (_ :
                            Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                T.map (Subobject.arrow ↑P) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk g)
⊢ homMk (Subobject.ofMkLEMk (MonoOver.arrow (MonoOver.mk' f)).right (MonoOver.arrow (MonoOver.mk' g)).right h) ≫ g = f
[PROOFSTEP]
aesop_cat
[GOAL]
case h.refine'_3
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ ↑{
          toFun := fun P =>
            { val := projectSubobject P,
              property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
          invFun := fun P =>
            liftSubobject ↑P
              (_ :
                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) = A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject A),
                liftSubobject (projectSubobject P)
                    (_ :
                      Exists.choose
                            (_ :
                              ∃ q,
                                q ≫
                                    T.map
                                      (Subobject.arrow
                                        ↑((fun P =>
                                              { val := projectSubobject P,
                                                property :=
                                                  (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                            P)) =
                                  A.hom) ≫
                          T.map
                            (Subobject.arrow
                              ↑((fun P =>
                                    { val := projectSubobject P,
                                      property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                  P)) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                (fun P =>
                      { val := projectSubobject P,
                        property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                    ((fun P =>
                        liftSubobject ↑P
                          (_ :
                            Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                T.map (Subobject.arrow ↑P) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk f) ≤
    ↑{
          toFun := fun P =>
            { val := projectSubobject P,
              property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) },
          invFun := fun P =>
            liftSubobject ↑P
              (_ :
                Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫ T.map (Subobject.arrow ↑P) = A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject A),
                liftSubobject (projectSubobject P)
                    (_ :
                      Exists.choose
                            (_ :
                              ∃ q,
                                q ≫
                                    T.map
                                      (Subobject.arrow
                                        ↑((fun P =>
                                              { val := projectSubobject P,
                                                property :=
                                                  (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                            P)) =
                                  A.hom) ≫
                          T.map
                            (Subobject.arrow
                              ↑((fun P =>
                                    { val := projectSubobject P,
                                      property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                                  P)) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, q ≫ T.map (Subobject.arrow P) = A.hom }),
                (fun P =>
                      { val := projectSubobject P,
                        property := (_ : ∃ q, q ≫ T.map (Subobject.arrow (projectSubobject P)) = A.hom) })
                    ((fun P =>
                        liftSubobject ↑P
                          (_ :
                            Exists.choose (_ : ∃ q, q ≫ T.map (Subobject.arrow ↑P) = A.hom) ≫
                                T.map (Subobject.arrow ↑P) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk g)
[PROOFSTEP]
refine' Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).right _
[GOAL]
case h.refine'_3
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasLimits C
inst✝ : PreservesLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (Subobject.ofMkLEMk f g h).right ≫ (MonoOver.arrow (MonoOver.mk' g)).right = (MonoOver.arrow (MonoOver.mk' f)).right
[PROOFSTEP]
exact congr_arg CommaMorphism.right (Subobject.ofMkLEMk_comp h)
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
⊢ Subobject (op A) → Subobject (op A.left)
[PROOFSTEP]
refine' Subobject.lift (fun P f hf => Subobject.mk f.unop.left.op) _
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
⊢ ∀ ⦃A_1 B : (CostructuredArrow S T)ᵒᵖ⦄ (f : A_1 ⟶ op A) (g : B ⟶ op A) [inst : Mono f] [inst_1 : Mono g] (i : A_1 ≅ B),
    i.hom ≫ g = f →
      (fun P f hf => Subobject.mk f.unop.left.op) A_1 f inst = (fun P f hf => Subobject.mk f.unop.left.op) B g inst_1
[PROOFSTEP]
intro P Q f g hf hg i hi
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ (fun P f hf => Subobject.mk f.unop.left.op) P f hf = (fun P f hf => Subobject.mk f.unop.left.op) Q g hg
[PROOFSTEP]
refine' Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i.unop).op (Quiver.Hom.unop_inj _)
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ ((Iso.op ((proj S T).mapIso (Iso.unop i))).hom ≫ g.unop.left.op).unop = f.unop.left.op.unop
[PROOFSTEP]
have := congr_arg Quiver.Hom.unop hi
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
this : (i.hom ≫ g).unop = f.unop
⊢ ((Iso.op ((proj S T).mapIso (Iso.unop i))).hom ≫ g.unop.left.op).unop = f.unop.left.op.unop
[PROOFSTEP]
simpa using congr_arg CommaMorphism.left this
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫
      S.map (Iso.unop (Subobject.underlyingIso (MonoOver.arrow (MonoOver.mk' f)).unop.left.op)).inv ≫ P.unop.hom =
    A.hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map (Subobject.arrow (Subobject.mk f.unop.left.op)).unop ≫
      S.map (Subobject.underlyingIso f.unop.left.op).inv.unop ≫ P.unop.hom =
    A.hom
[PROOFSTEP]
rw [← Category.assoc, ← S.map_comp, ← unop_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
⊢ S.map ((Subobject.underlyingIso f.unop.left.op).inv ≫ Subobject.arrow (Subobject.mk f.unop.left.op)).unop ≫
      P.unop.hom =
    A.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v, u₁} C
D : Type u₂
inst✝¹ : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
⊢ f.unop.left ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop = (Subobject.arrow (Subobject.mk f.unop.left.op)).unop
[PROOFSTEP]
conv_lhs =>
  congr
  rw [← Quiver.Hom.unop_op f.unop.left]
[GOAL]
C : Type u₁
inst✝² : Category.{v, u₁} C
D : Type u₂
inst✝¹ : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
| f.unop.left ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop
[PROOFSTEP]
  congr
  rw [← Quiver.Hom.unop_op f.unop.left]
[GOAL]
C : Type u₁
inst✝² : Category.{v, u₁} C
D : Type u₂
inst✝¹ : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
| f.unop.left ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop
[PROOFSTEP]
  congr
  rw [← Quiver.Hom.unop_op f.unop.left]
[GOAL]
C : Type u₁
inst✝² : Category.{v, u₁} C
D : Type u₂
inst✝¹ : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
| f.unop.left ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop
[PROOFSTEP]
congr
[GOAL]
case a
C : Type u₁
inst✝² : Category.{v, u₁} C
D : Type u₂
inst✝¹ : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
| f.unop.left
case a
C : Type u₁
inst✝² : Category.{v, u₁} C
D : Type u₂
inst✝¹ : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
| (Subobject.underlyingIso f.unop.left.op).hom.unop
[PROOFSTEP]
rw [← Quiver.Hom.unop_op f.unop.left]
[GOAL]
C : Type u₁
inst✝² : Category.{v, u₁} C
D : Type u₂
inst✝¹ : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
inst✝ : Mono f.unop.left.op
⊢ f.unop.left.op.unop ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop =
    (Subobject.arrow (Subobject.mk f.unop.left.op)).unop
[PROOFSTEP]
rw [← unop_comp, Subobject.underlyingIso_hom_comp_eq_mk]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
⊢ ∀ ⦃A_1 : (CostructuredArrow S T)ᵒᵖ⦄ (f : A_1 ⟶ op A) [inst : Mono f]
    {q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right}
    (hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom),
    liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f
[PROOFSTEP]
intro P f hf q hq
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ liftQuotient (projectQuotient (Subobject.mk f)) hq = Subobject.mk f
[PROOFSTEP]
fapply Subobject.mk_eq_mk_of_comm
[GOAL]
case i
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ op (mk q) ≅ P
[PROOFSTEP]
refine' (Iso.op (isoMk _ _) : _ ≅ op (unop P))
[GOAL]
case i.refine'_1
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ P.unop.left ≅ (mk q).left
[PROOFSTEP]
exact (Subobject.underlyingIso f.unop.left.op).unop
[GOAL]
case i.refine'_2
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ S.map (Iso.unop (Subobject.underlyingIso f.unop.left.op)).hom ≫ (mk q).hom = P.unop.hom
[PROOFSTEP]
refine' (cancel_epi (S.map f.unop.left)).1 _
[GOAL]
case i.refine'_2
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ S.map f.unop.left ≫ S.map (Iso.unop (Subobject.underlyingIso f.unop.left.op)).hom ≫ (mk q).hom =
    S.map f.unop.left ≫ P.unop.hom
[PROOFSTEP]
simpa [← Category.assoc, ← S.map_comp] using hq
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ (Iso.op (isoMk (Iso.unop (Subobject.underlyingIso f.unop.left.op)))).hom ≫ f =
    (homMk (Subobject.arrow (projectQuotient (Subobject.mk f))).unop).op
[PROOFSTEP]
exact Quiver.Hom.unop_inj (by aesop_cat)
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (Subobject.underlying.obj (projectQuotient (Subobject.mk f))).unop ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (Subobject.arrow (projectQuotient (Subobject.mk f))).unop ≫ q = A.hom
⊢ ((Iso.op (isoMk (Iso.unop (Subobject.underlyingIso f.unop.left.op)))).hom ≫ f).unop =
    (homMk (Subobject.arrow (projectQuotient (Subobject.mk f))).unop).op.unop
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left
[PROOFSTEP]
conv_lhs =>
  congr
  rw [← Quiver.Hom.unop_op g.unop.left]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
| g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop
[PROOFSTEP]
  congr
  rw [← Quiver.Hom.unop_op g.unop.left]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
| g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop
[PROOFSTEP]
  congr
  rw [← Quiver.Hom.unop_op g.unop.left]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
| g.unop.left ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop
[PROOFSTEP]
congr
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
| g.unop.left
case a
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
| (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop
[PROOFSTEP]
rw [← Quiver.Hom.unop_op g.unop.left]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ g.unop.left.op.unop ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left
[PROOFSTEP]
rw [← unop_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h ≫ g.unop.left.op).unop = f.unop.left
[PROOFSTEP]
simp only [Subobject.ofMkLEMk_comp, Quiver.Hom.unop_op]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }
⊢ ↑((fun P =>
          { val := projectQuotient P,
            property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
        ((fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom))
          P)) =
    ↑P
[PROOFSTEP]
simp only [liftQuotient, Quiver.Hom.unop_op, homMk_left, Quiver.Hom.op_unop, projectQuotient_mk, Subobject.mk_arrow]
[GOAL]
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
⊢ ∀ {a b : Subobject (op A)},
    ↑{
              toFun := fun P =>
                { val := projectQuotient P,
                  property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
              invFun := fun P =>
                liftQuotient ↑P
                  (_ :
                    S.map (Subobject.arrow ↑P).unop ≫
                        Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                      A.hom),
              left_inv :=
                (_ :
                  ∀ (P : Subobject (op A)),
                    liftQuotient (projectQuotient P)
                        (_ :
                          S.map
                                (Subobject.arrow
                                    ↑((fun P =>
                                          { val := projectQuotient P,
                                            property :=
                                              (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                        P)).unop ≫
                              Exists.choose
                                (_ :
                                  ∃ q,
                                    S.map
                                          (Subobject.arrow
                                              ↑((fun P =>
                                                    { val := projectQuotient P,
                                                      property :=
                                                        (_ :
                                                          ∃ q,
                                                            S.map (Subobject.arrow (projectQuotient P)).unop ≫ q =
                                                              A.hom) })
                                                  P)).unop ≫
                                        q =
                                      A.hom) =
                            A.hom) =
                      P),
              right_inv :=
                (_ :
                  ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                    (fun P =>
                          { val := projectQuotient P,
                            property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                        ((fun P =>
                            liftQuotient ↑P
                              (_ :
                                S.map (Subobject.arrow ↑P).unop ≫
                                    Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                                  A.hom))
                          P) =
                      P) }
          a ≤
        ↑{
              toFun := fun P =>
                { val := projectQuotient P,
                  property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
              invFun := fun P =>
                liftQuotient ↑P
                  (_ :
                    S.map (Subobject.arrow ↑P).unop ≫
                        Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                      A.hom),
              left_inv :=
                (_ :
                  ∀ (P : Subobject (op A)),
                    liftQuotient (projectQuotient P)
                        (_ :
                          S.map
                                (Subobject.arrow
                                    ↑((fun P =>
                                          { val := projectQuotient P,
                                            property :=
                                              (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                        P)).unop ≫
                              Exists.choose
                                (_ :
                                  ∃ q,
                                    S.map
                                          (Subobject.arrow
                                              ↑((fun P =>
                                                    { val := projectQuotient P,
                                                      property :=
                                                        (_ :
                                                          ∃ q,
                                                            S.map (Subobject.arrow (projectQuotient P)).unop ≫ q =
                                                              A.hom) })
                                                  P)).unop ≫
                                        q =
                                      A.hom) =
                            A.hom) =
                      P),
              right_inv :=
                (_ :
                  ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                    (fun P =>
                          { val := projectQuotient P,
                            property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                        ((fun P =>
                            liftQuotient ↑P
                              (_ :
                                S.map (Subobject.arrow ↑P).unop ≫
                                    Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                                  A.hom))
                          P) =
                      P) }
          b ↔
      a ≤ b
[PROOFSTEP]
apply Subobject.ind₂
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
⊢ ∀ ⦃A_1 B : (CostructuredArrow S T)ᵒᵖ⦄ (f : A_1 ⟶ op A) (g : B ⟶ op A) [inst : Mono f] [inst_1 : Mono g],
    ↑{
              toFun := fun P =>
                { val := projectQuotient P,
                  property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
              invFun := fun P =>
                liftQuotient ↑P
                  (_ :
                    S.map (Subobject.arrow ↑P).unop ≫
                        Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                      A.hom),
              left_inv :=
                (_ :
                  ∀ (P : Subobject (op A)),
                    liftQuotient (projectQuotient P)
                        (_ :
                          S.map
                                (Subobject.arrow
                                    ↑((fun P =>
                                          { val := projectQuotient P,
                                            property :=
                                              (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                        P)).unop ≫
                              Exists.choose
                                (_ :
                                  ∃ q,
                                    S.map
                                          (Subobject.arrow
                                              ↑((fun P =>
                                                    { val := projectQuotient P,
                                                      property :=
                                                        (_ :
                                                          ∃ q,
                                                            S.map (Subobject.arrow (projectQuotient P)).unop ≫ q =
                                                              A.hom) })
                                                  P)).unop ≫
                                        q =
                                      A.hom) =
                            A.hom) =
                      P),
              right_inv :=
                (_ :
                  ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                    (fun P =>
                          { val := projectQuotient P,
                            property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                        ((fun P =>
                            liftQuotient ↑P
                              (_ :
                                S.map (Subobject.arrow ↑P).unop ≫
                                    Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                                  A.hom))
                          P) =
                      P) }
          (Subobject.mk f) ≤
        ↑{
              toFun := fun P =>
                { val := projectQuotient P,
                  property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
              invFun := fun P =>
                liftQuotient ↑P
                  (_ :
                    S.map (Subobject.arrow ↑P).unop ≫
                        Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                      A.hom),
              left_inv :=
                (_ :
                  ∀ (P : Subobject (op A)),
                    liftQuotient (projectQuotient P)
                        (_ :
                          S.map
                                (Subobject.arrow
                                    ↑((fun P =>
                                          { val := projectQuotient P,
                                            property :=
                                              (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                        P)).unop ≫
                              Exists.choose
                                (_ :
                                  ∃ q,
                                    S.map
                                          (Subobject.arrow
                                              ↑((fun P =>
                                                    { val := projectQuotient P,
                                                      property :=
                                                        (_ :
                                                          ∃ q,
                                                            S.map (Subobject.arrow (projectQuotient P)).unop ≫ q =
                                                              A.hom) })
                                                  P)).unop ≫
                                        q =
                                      A.hom) =
                            A.hom) =
                      P),
              right_inv :=
                (_ :
                  ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                    (fun P =>
                          { val := projectQuotient P,
                            property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                        ((fun P =>
                            liftQuotient ↑P
                              (_ :
                                S.map (Subobject.arrow ↑P).unop ≫
                                    Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                                  A.hom))
                          P) =
                      P) }
          (Subobject.mk g) ↔
      Subobject.mk f ≤ Subobject.mk g
[PROOFSTEP]
intro P Q f g hf hg
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
⊢ ↑{
            toFun := fun P =>
              { val := projectQuotient P,
                property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
            invFun := fun P =>
              liftQuotient ↑P
                (_ :
                  S.map (Subobject.arrow ↑P).unop ≫
                      Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                    A.hom),
            left_inv :=
              (_ :
                ∀ (P : Subobject (op A)),
                  liftQuotient (projectQuotient P)
                      (_ :
                        S.map
                              (Subobject.arrow
                                  ↑((fun P =>
                                        { val := projectQuotient P,
                                          property :=
                                            (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                      P)).unop ≫
                            Exists.choose
                              (_ :
                                ∃ q,
                                  S.map
                                        (Subobject.arrow
                                            ↑((fun P =>
                                                  { val := projectQuotient P,
                                                    property :=
                                                      (_ :
                                                        ∃ q,
                                                          S.map (Subobject.arrow (projectQuotient P)).unop ≫ q =
                                                            A.hom) })
                                                P)).unop ≫
                                      q =
                                    A.hom) =
                          A.hom) =
                    P),
            right_inv :=
              (_ :
                ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                  (fun P =>
                        { val := projectQuotient P,
                          property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                      ((fun P =>
                          liftQuotient ↑P
                            (_ :
                              S.map (Subobject.arrow ↑P).unop ≫
                                  Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                                A.hom))
                        P) =
                    P) }
        (Subobject.mk f) ≤
      ↑{
            toFun := fun P =>
              { val := projectQuotient P,
                property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
            invFun := fun P =>
              liftQuotient ↑P
                (_ :
                  S.map (Subobject.arrow ↑P).unop ≫
                      Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                    A.hom),
            left_inv :=
              (_ :
                ∀ (P : Subobject (op A)),
                  liftQuotient (projectQuotient P)
                      (_ :
                        S.map
                              (Subobject.arrow
                                  ↑((fun P =>
                                        { val := projectQuotient P,
                                          property :=
                                            (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                      P)).unop ≫
                            Exists.choose
                              (_ :
                                ∃ q,
                                  S.map
                                        (Subobject.arrow
                                            ↑((fun P =>
                                                  { val := projectQuotient P,
                                                    property :=
                                                      (_ :
                                                        ∃ q,
                                                          S.map (Subobject.arrow (projectQuotient P)).unop ≫ q =
                                                            A.hom) })
                                                P)).unop ≫
                                      q =
                                    A.hom) =
                          A.hom) =
                    P),
            right_inv :=
              (_ :
                ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                  (fun P =>
                        { val := projectQuotient P,
                          property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                      ((fun P =>
                          liftQuotient ↑P
                            (_ :
                              S.map (Subobject.arrow ↑P).unop ≫
                                  Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                                A.hom))
                        P) =
                    P) }
        (Subobject.mk g) ↔
    Subobject.mk f ≤ Subobject.mk g
[PROOFSTEP]
refine' ⟨fun h => Subobject.mk_le_mk_of_comm _ _, fun h => _⟩
[GOAL]
case h.refine'_1
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h :
  ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk f) ≤
    ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk g)
⊢ P ⟶ Q
[PROOFSTEP]
refine' (homMk (Subobject.ofMkLEMk _ _ h).unop ((cancel_epi (S.map g.unop.left)).1 _)).op
[GOAL]
case h.refine'_1
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h :
  ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk f) ≤
    ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk g)
⊢ S.map g.unop.left ≫
      S.map
          (Subobject.ofMkLEMk (MonoOver.arrow (MonoOver.mk' f)).unop.left.op
              (MonoOver.arrow (MonoOver.mk' g)).unop.left.op h).unop ≫
        (MonoOver.mk' f).obj.left.unop.hom =
    S.map g.unop.left ≫ (MonoOver.mk' g).obj.left.unop.hom
[PROOFSTEP]
dsimp
[GOAL]
case h.refine'_1
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h :
  ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk f) ≤
    ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk g)
⊢ S.map g.unop.left ≫ S.map (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop ≫ P.unop.hom =
    S.map g.unop.left ≫ Q.unop.hom
[PROOFSTEP]
simp only [← S.map_comp_assoc, unop_left_comp_ofMkLEMk_unop, unop_op, CommaMorphism.w, Functor.const_obj_obj,
  right_eq_id, Functor.const_obj_map, Category.comp_id]
[GOAL]
case h.refine'_2
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h :
  ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk f) ≤
    ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk g)
⊢ (homMk
          (Subobject.ofMkLEMk (MonoOver.arrow (MonoOver.mk' f)).unop.left.op
              (MonoOver.arrow (MonoOver.mk' g)).unop.left.op h).unop).op ≫
      g =
    f
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case h.refine'_2.a
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h :
  ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk f) ≤
    ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk g)
⊢ ((homMk
            (Subobject.ofMkLEMk (MonoOver.arrow (MonoOver.mk' f)).unop.left.op
                (MonoOver.arrow (MonoOver.mk' g)).unop.left.op h).unop).op ≫
        g).unop =
    f.unop
[PROOFSTEP]
ext
[GOAL]
case h.refine'_2.a.h
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h :
  ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk f) ≤
    ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk g)
⊢ ((homMk
              (Subobject.ofMkLEMk (MonoOver.arrow (MonoOver.mk' f)).unop.left.op
                  (MonoOver.arrow (MonoOver.mk' g)).unop.left.op h).unop).op ≫
          g).unop.left =
    f.unop.left
[PROOFSTEP]
exact unop_left_comp_ofMkLEMk_unop _
[GOAL]
case h.refine'_3
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk f) ≤
    ↑{
          toFun := fun P =>
            { val := projectQuotient P,
              property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) },
          invFun := fun P =>
            liftQuotient ↑P
              (_ :
                S.map (Subobject.arrow ↑P).unop ≫ Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                  A.hom),
          left_inv :=
            (_ :
              ∀ (P : Subobject (op A)),
                liftQuotient (projectQuotient P)
                    (_ :
                      S.map
                            (Subobject.arrow
                                ↑((fun P =>
                                      { val := projectQuotient P,
                                        property :=
                                          (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                    P)).unop ≫
                          Exists.choose
                            (_ :
                              ∃ q,
                                S.map
                                      (Subobject.arrow
                                          ↑((fun P =>
                                                { val := projectQuotient P,
                                                  property :=
                                                    (_ :
                                                      ∃ q,
                                                        S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                                              P)).unop ≫
                                    q =
                                  A.hom) =
                        A.hom) =
                  P),
          right_inv :=
            (_ :
              ∀ (P : { P // ∃ q, S.map (Subobject.arrow P).unop ≫ q = A.hom }),
                (fun P =>
                      { val := projectQuotient P,
                        property := (_ : ∃ q, S.map (Subobject.arrow (projectQuotient P)).unop ≫ q = A.hom) })
                    ((fun P =>
                        liftQuotient ↑P
                          (_ :
                            S.map (Subobject.arrow ↑P).unop ≫
                                Exists.choose (_ : ∃ q, S.map (Subobject.arrow ↑P).unop ≫ q = A.hom) =
                              A.hom))
                      P) =
                  P) }
      (Subobject.mk g)
[PROOFSTEP]
refine' Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).unop.left.op _
[GOAL]
case h.refine'_3
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.arrow (MonoOver.mk' g)).unop.left.op =
    (MonoOver.arrow (MonoOver.mk' f)).unop.left.op
[PROOFSTEP]
refine' Quiver.Hom.unop_inj _
[GOAL]
case h.refine'_3
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ ((Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.arrow (MonoOver.mk' g)).unop.left.op).unop =
    (MonoOver.arrow (MonoOver.mk' f)).unop.left.op.unop
[PROOFSTEP]
have := congr_arg Quiver.Hom.unop (Subobject.ofMkLEMk_comp h)
[GOAL]
case h.refine'_3
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : Type u₂
inst✝² : Category.{v, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasColimits C
inst✝ : PreservesColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
this : (Subobject.ofMkLEMk f g h ≫ g).unop = f.unop
⊢ ((Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.arrow (MonoOver.mk' g)).unop.left.op).unop =
    (MonoOver.arrow (MonoOver.mk' f)).unop.left.op.unop
[PROOFSTEP]
simpa only [unop_op, Functor.id_obj, Functor.const_obj_obj, MonoOver.mk'_obj, Over.mk_left, MonoOver.mk'_arrow,
  unop_comp, Quiver.Hom.unop_op, comp_left] using congr_arg CommaMorphism.left this
