C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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
intro P f hf q hq
case i
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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

case w
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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
⊢ ?i.hom ≫ f = homMk (Subobject.arrow (projectSubobject (Subobject.mk f)))
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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
fapply Subobject.mk_eq_mk_of_comm
case i.g
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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

case i.w
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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 ?i.g.hom = P.hom) _auto✝
case i
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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
fapply isoMk
no goals
case i.g
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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
exact Subobject.underlyingIso _
no goals
case i.w
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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✝
exact (cancel_mono (T.map f.right)).1 (by dsimp; simpa [← T.map_comp] using hq)
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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
dsimp
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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
simpa [← T.map_comp] using hq
no goals
case w
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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)))
exact ext _ _ (by dsimp; simp)
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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)
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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
dsimp
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category 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)
simp