[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
⊢ 𝟙 (mk' f).obj.left ≫ arrow ((map f).obj ⊤) = arrow (mk' f)
[PROOFSTEP]
simp [id_comp f]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
f : X ⟶ Y
⊢ f ≫ ((forget Y).obj ⊤).hom = 𝟙 ⊤.obj.left ≫ f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ ((fun f => pullback (arrow f) ⋙ map (arrow f)) X✝).obj g ⟶ ((fun f => pullback (arrow f) ⋙ map (arrow f)) Y✝).obj g
[PROOFSTEP]
apply homMk _ _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ (((fun f => pullback (arrow f) ⋙ map (arrow f)) X✝).obj g).obj.left ⟶
    (((fun f => pullback (arrow f) ⋙ map (arrow f)) Y✝).obj g).obj.left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ ?m.19120 ≫ arrow (((fun f => pullback (arrow f) ⋙ map (arrow f)) Y✝).obj g) =
    arrow (((fun f => pullback (arrow f) ⋙ map (arrow f)) X✝).obj g)
[PROOFSTEP]
apply pullback.lift pullback.fst (pullback.snd ≫ k.left) _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.fst ≫ ((forget A).obj g).hom = (pullback.snd ≫ k.left) ≫ arrow Y✝
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.lift pullback.fst (pullback.snd ≫ k.left) ?m.21896 ≫
      arrow (((fun f => pullback (arrow f) ⋙ map (arrow f)) Y✝).obj g) =
    arrow (((fun f => pullback (arrow f) ⋙ map (arrow f)) X✝).obj g)
[PROOFSTEP]
rw [pullback.condition, assoc, w k]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.lift pullback.fst (pullback.snd ≫ k.left)
        (_ : pullback.fst ≫ ((forget A).obj g).hom = (pullback.snd ≫ k.left) ≫ arrow Y✝) ≫
      arrow (((fun f => pullback (arrow f) ⋙ map (arrow f)) Y✝).obj g) =
    arrow (((fun f => pullback (arrow f) ⋙ map (arrow f)) X✝).obj g)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
X✝ Y✝ : MonoOver A
k : X✝ ⟶ Y✝
g : MonoOver A
⊢ pullback.lift pullback.fst (pullback.snd ≫ k.left) (_ : pullback.fst ≫ arrow g = (pullback.snd ≫ k.left) ≫ arrow Y✝) ≫
      pullback.snd ≫ arrow Y✝ =
    pullback.snd ≫ arrow X✝
[PROOFSTEP]
rw [pullback.lift_snd_assoc, assoc, w k]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
f g h : MonoOver A
⊢ (h ⟶ f) → (h ⟶ g) → (h ⟶ (inf.obj f).obj g)
[PROOFSTEP]
intro k₁ k₂
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
f g h : MonoOver A
k₁ : h ⟶ f
k₂ : h ⟶ g
⊢ h ⟶ (inf.obj f).obj g
[PROOFSTEP]
refine' homMk (pullback.lift k₂.left k₁.left _) _
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
f g h : MonoOver A
k₁ : h ⟶ f
k₂ : h ⟶ g
⊢ k₂.left ≫ ((forget A).obj g).hom = k₁.left ≫ arrow f
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
f g h : MonoOver A
k₁ : h ⟶ f
k₂ : h ⟶ g
⊢ pullback.lift k₂.left k₁.left ?refine'_1 ≫ arrow ((inf.obj f).obj g) = arrow h
[PROOFSTEP]
rw [w k₁, w k₂]
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
f g h : MonoOver A
k₁ : h ⟶ f
k₂ : h ⟶ g
⊢ pullback.lift k₂.left k₁.left (_ : k₂.left ≫ ((forget A).obj g).hom = k₁.left ≫ arrow f) ≫ arrow ((inf.obj f).obj g) =
    arrow h
[PROOFSTEP]
erw [pullback.lift_snd_assoc, w k₁]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ f ⟶ (sup.obj f).obj g
[PROOFSTEP]
refine' homMk (coprod.inl ≫ factorThruImage _) _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ (coprod.inl ≫ factorThruImage ((uncurry.obj Over.coprod).obj ((Functor.prod (forget A) (forget A)).obj (f, g))).hom) ≫
      arrow ((sup.obj f).obj g) =
    arrow f
[PROOFSTEP]
erw [Category.assoc, image.fac, coprod.inl_desc]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ ((Functor.prod (forget A) (forget A)).obj (f, g)).fst.hom = arrow f
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ g ⟶ (sup.obj f).obj g
[PROOFSTEP]
refine' homMk (coprod.inr ≫ factorThruImage _) _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ (coprod.inr ≫ factorThruImage ((uncurry.obj Over.coprod).obj ((Functor.prod (forget A) (forget A)).obj (f, g))).hom) ≫
      arrow ((sup.obj f).obj g) =
    arrow g
[PROOFSTEP]
erw [Category.assoc, image.fac, coprod.inr_desc]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ ((Functor.prod (forget A) (forget A)).obj (f, g)).snd.hom = arrow g
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
⊢ (f ⟶ h) → (g ⟶ h) → ((sup.obj f).obj g ⟶ h)
[PROOFSTEP]
intro k₁ k₂
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ (sup.obj f).obj g ⟶ h
[PROOFSTEP]
refine' homMk _ _
[GOAL]
case refine'_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ ((sup.obj f).obj g).obj.left ⟶ h.obj.left
case refine'_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ ?refine'_1 ≫ arrow h = arrow ((sup.obj f).obj g)
[PROOFSTEP]
apply image.lift ⟨_, h.arrow, coprod.desc k₁.left k₂.left, _⟩
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ coprod.desc k₁.left k₂.left ≫ arrow h =
    ((uncurry.obj Over.coprod).obj ((Functor.prod (forget A) (forget A)).obj (f, g))).hom
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ coprod.inl ≫ coprod.desc k₁.left k₂.left ≫ arrow h =
    coprod.inl ≫ ((uncurry.obj Over.coprod).obj ((Functor.prod (forget A) (forget A)).obj (f, g))).hom
[PROOFSTEP]
simp [w k₁]
[GOAL]
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ coprod.inr ≫ coprod.desc k₁.left k₂.left ≫ arrow h =
    coprod.inr ≫ ((uncurry.obj Over.coprod).obj ((Functor.prod (forget A) (forget A)).obj (f, g))).hom
[PROOFSTEP]
simp [w k₂]
[GOAL]
case refine'_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ image.lift (MonoFactorisation.mk h.obj.left (arrow h) (coprod.desc k₁.left k₂.left)) ≫ arrow h =
    arrow ((sup.obj f).obj g)
[PROOFSTEP]
apply image.lift_fac
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
⊢ ∀ (a : Subobject X), a ≤ ⊤
[PROOFSTEP]
refine' Quotient.ind' fun f => _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f : MonoOver X
⊢ Quotient.mk'' f ≤ ⊤
[PROOFSTEP]
exact ⟨MonoOver.leTop f⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
⊢ (underlyingIso (𝟙 B)).hom = arrow ⊤
[PROOFSTEP]
convert underlyingIso_hom_comp_eq_mk (𝟙 B)
[GOAL]
case h.e'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
⊢ (underlyingIso (𝟙 B)).hom = (underlyingIso (𝟙 B)).hom ≫ 𝟙 B
[PROOFSTEP]
simp only [comp_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
⊢ IsIso (arrow ⊤)
[PROOFSTEP]
rw [← underlyingIso_top_hom]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
⊢ IsIso (underlyingIso (𝟙 B)).hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊤
⊢ IsIso f
[PROOFSTEP]
rw [← ofMkLEMk_comp h.le, Category.comp_id]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊤
⊢ IsIso (ofMkLEMk f (𝟙 Y) (_ : mk f ≤ ⊤))
[PROOFSTEP]
exact IsIso.of_iso (isoOfMkEqMk _ _ h)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y : C
P : Subobject Y
⊢ IsIso (arrow P) ↔ P = ⊤
[PROOFSTEP]
rw [isIso_iff_mk_eq_top, mk_arrow]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y : C
⊢ IsIso (arrow ⊤)
[PROOFSTEP]
rw [isIso_arrow_iff_eq_top]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
X : C
⊢ ∀ (a : Subobject X), ⊥ ≤ a
[PROOFSTEP]
refine' Quotient.ind' fun f => _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
X : C
f : MonoOver X
⊢ ⊥ ≤ Quotient.mk'' f
[PROOFSTEP]
exact ⟨MonoOver.botLE f⟩
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
B : C
⊢ (IsInitial.uniqueUpToIso initialIsInitial HasZeroObject.zeroIsInitial).hom ≫ 0 = initial.to B
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
f : A ⟶ B
⊢ Factors ⊥ f → f = 0
[PROOFSTEP]
rintro ⟨h, rfl⟩
[GOAL]
case intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
h : A ⟶ ⊥.obj.left
⊢ h ≫ MonoOver.arrow ⊥ = 0
[PROOFSTEP]
simp only [MonoOver.bot_arrow_eq_zero, Functor.id_obj, Functor.const_obj_obj, MonoOver.bot_left, comp_zero]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
f : A ⟶ B
⊢ f = 0 → Factors ⊥ f
[PROOFSTEP]
rintro rfl
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
⊢ Factors ⊥ 0
[PROOFSTEP]
exact ⟨0, by simp⟩
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
A B : C
⊢ 0 ≫ MonoOver.arrow ⊥ = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊥
⊢ f = 0
[PROOFSTEP]
simpa [h, bot_factors_iff_zero] using mk_factors_self f
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : Mono f
h : f = 0
⊢ (isoZeroOfMonoEqZero h ≪≫ HasZeroObject.zeroIsoInitial).hom ≫ initial.to Y = f
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
h f g : Subobject A
⊢ ∀ (a₁ a₂ a₃ : MonoOver A),
    Quotient.mk'' a₁ ≤ Quotient.mk'' a₂ →
      Quotient.mk'' a₁ ≤ Quotient.mk'' a₃ → Quotient.mk'' a₁ ≤ (inf.obj (Quotient.mk'' a₂)).obj (Quotient.mk'' a₃)
[PROOFSTEP]
rintro f g h ⟨k⟩ ⟨l⟩
[GOAL]
case intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
h✝ f✝ g✝ : Subobject A
f g h : MonoOver A
k : f ⟶ g
l : f ⟶ h
⊢ Quotient.mk'' f ≤ (inf.obj (Quotient.mk'' g)).obj (Quotient.mk'' h)
[PROOFSTEP]
exact ⟨MonoOver.leInf _ _ _ k l⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A B : C
X Y : Subobject B
f : A ⟶ B
⊢ Factors X f ∧ Factors Y f → Factors (X ⊓ Y) f
[PROOFSTEP]
revert X Y
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ {X Y : Subobject B}, Factors X f ∧ Factors Y f → Factors (X ⊓ Y) f
[PROOFSTEP]
apply Quotient.ind₂'
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ (a₁ a₂ : MonoOver B),
    Factors (Quotient.mk'' a₁) f ∧ Factors (Quotient.mk'' a₂) f → Factors (Quotient.mk'' a₁ ⊓ Quotient.mk'' a₂) f
[PROOFSTEP]
rintro X Y ⟨⟨g₁, rfl⟩, ⟨g₂, hg₂⟩⟩
[GOAL]
case h.intro.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A B : C
X Y : MonoOver B
g₁ : A ⟶ X.obj.left
g₂ : A ⟶ Y.obj.left
hg₂ : g₂ ≫ MonoOver.arrow Y = g₁ ≫ MonoOver.arrow X
⊢ Factors (Quotient.mk'' X ⊓ Quotient.mk'' Y) (g₁ ≫ MonoOver.arrow X)
[PROOFSTEP]
exact ⟨_, pullback.lift_snd_assoc _ _ hg₂ _⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
B : C
X Y : Subobject B
⊢ ofLE (X ⊓ Y) X (_ : (inf.obj X).obj Y ≤ X) ≫ MonoOver.arrow (representative.obj X) = arrow (X ⊓ Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
B : C
X Y : Subobject B
⊢ ofLE (X ⊓ Y) Y (_ : (inf.obj X).obj Y ≤ Y) ≫ MonoOver.arrow (representative.obj Y) = arrow (X ⊓ Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
⊢ Factors (Finset.inf s P) f ↔ ∀ (i : I), i ∈ s → Factors (P i) f
[PROOFSTEP]
classical
induction' s using Finset.induction_on with _ _ _ ih
· simp [top_factors]
· simp [ih]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
⊢ Factors (Finset.inf s P) f ↔ ∀ (i : I), i ∈ s → Factors (P i) f
[PROOFSTEP]
induction' s using Finset.induction_on with _ _ _ ih
[GOAL]
case empty
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
⊢ Factors (Finset.inf ∅ P) f ↔ ∀ (i : I), i ∈ ∅ → Factors (P i) f
[PROOFSTEP]
simp [top_factors]
[GOAL]
case insert
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : Factors (Finset.inf s✝ P) f ↔ ∀ (i : I), i ∈ s✝ → Factors (P i) f
⊢ Factors (Finset.inf (insert a✝¹ s✝) P) f ↔ ∀ (i : I), i ∈ insert a✝¹ s✝ → Factors (P i) f
[PROOFSTEP]
simp [ih]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
s : Finset I
P : I → Subobject B
i : I
m : i ∈ s
⊢ Factors (P i) (arrow (Finset.inf s P))
[PROOFSTEP]
classical
revert i m
induction' s using Finset.induction_on with _ _ _ ih
· rintro _ ⟨⟩
· intro _ m
  rw [Finset.inf_insert]
  simp only [Finset.mem_insert] at m 
  rcases m with (rfl | m)
  · rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
    exact factors_comp_arrow _
  · rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
    apply factors_of_factors_right
    exact ih _ m
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
s : Finset I
P : I → Subobject B
i : I
m : i ∈ s
⊢ Factors (P i) (arrow (Finset.inf s P))
[PROOFSTEP]
revert i m
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
s : Finset I
P : I → Subobject B
⊢ ∀ (i : I), i ∈ s → Factors (P i) (arrow (Finset.inf s P))
[PROOFSTEP]
induction' s using Finset.induction_on with _ _ _ ih
[GOAL]
case empty
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
⊢ ∀ (i : I), i ∈ ∅ → Factors (P i) (arrow (Finset.inf ∅ P))
[PROOFSTEP]
rintro _ ⟨⟩
[GOAL]
case insert
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
⊢ ∀ (i : I), i ∈ insert a✝¹ s✝ → Factors (P i) (arrow (Finset.inf (insert a✝¹ s✝) P))
[PROOFSTEP]
intro _ m
[GOAL]
case insert
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ insert a✝¹ s✝
⊢ Factors (P i✝) (arrow (Finset.inf (insert a✝¹ s✝) P))
[PROOFSTEP]
rw [Finset.inf_insert]
[GOAL]
case insert
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ insert a✝¹ s✝
⊢ Factors (P i✝) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
[PROOFSTEP]
simp only [Finset.mem_insert] at m 
[GOAL]
case insert
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ = a✝¹ ∨ i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
[PROOFSTEP]
rcases m with (rfl | m)
[GOAL]
case insert.inl
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
s✝ : Finset I
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
a✝ : ¬i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (P i✝ ⊓ Finset.inf s✝ P))
[PROOFSTEP]
rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
[GOAL]
case insert.inl
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
s✝ : Finset I
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
a✝ : ¬i✝ ∈ s✝
⊢ Factors (P i✝)
    (factorThru (P i✝) (arrow (P i✝ ⊓ Finset.inf s✝ P)) (_ : Factors (P i✝) (arrow (P i✝ ⊓ Finset.inf s✝ P))) ≫
      arrow (P i✝))
[PROOFSTEP]
exact factors_comp_arrow _
[GOAL]
case insert.inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
[PROOFSTEP]
rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
[GOAL]
case insert.inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ s✝
⊢ Factors (P i✝)
    (factorThru (Finset.inf s✝ P) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))
        (_ : Factors (Finset.inf s✝ P) (arrow (P a✝¹ ⊓ Finset.inf s✝ P))) ≫
      arrow (Finset.inf s✝ P))
[PROOFSTEP]
apply factors_of_factors_right
[GOAL]
case insert.inr.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : ∀ (i : I), i ∈ s✝ → Factors (P i) (arrow (Finset.inf s✝ P))
i✝ : I
m : i✝ ∈ s✝
⊢ Factors (P i✝) (arrow (Finset.inf s✝ P))
[PROOFSTEP]
exact ih _ m
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
f₁ : MonoOver A
f₂ : Subobject A
⊢ (inf.obj (Quotient.mk'' f₁)).obj f₂ = (map (MonoOver.arrow f₁)).obj ((pullback (MonoOver.arrow f₁)).obj f₂)
[PROOFSTEP]
induction' f₂ using Quotient.inductionOn' with f₂
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
A : C
f₁ f₂ : MonoOver A
⊢ (inf.obj (Quotient.mk'' f₁)).obj (Quotient.mk'' f₂) =
    (map (MonoOver.arrow f₁)).obj ((pullback (MonoOver.arrow f₁)).obj (Quotient.mk'' f₂))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ (f₁ ⨯ f₂) = f₁ ⊓ f₂
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ (f₁ ⨯ f₂) ≤ f₁ ⊓ f₂
[PROOFSTEP]
refine' le_inf _ _ _ (Limits.prod.fst.le) (Limits.prod.snd.le)
[GOAL]
case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ≤ (f₁ ⨯ f₂)
[PROOFSTEP]
apply leOfHom
[GOAL]
case a.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ⟶ f₁ ⨯ f₂
[PROOFSTEP]
exact prod.lift (inf_le_left _ _).hom (inf_le_right _ _).hom
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₁ f₂ : Subobject Y
⊢ (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂
[PROOFSTEP]
revert f₁
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
⊢ ∀ (f₁ : Subobject Y), (pullback g).obj (f₁ ⊓ f₂) = (pullback g).obj f₁ ⊓ (pullback g).obj f₂
[PROOFSTEP]
apply Quotient.ind'
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (pullback g).obj (Quotient.mk'' a ⊓ f₂) = (pullback g).obj (Quotient.mk'' a) ⊓ (pullback g).obj f₂
[PROOFSTEP]
intro f₁
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj (Quotient.mk'' f₁ ⊓ f₂) = (pullback g).obj (Quotient.mk'' f₁) ⊓ (pullback g).obj f₂
[PROOFSTEP]
erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← pullback_comp, ←
  map_pullback pullback.condition (pullbackIsPullback f₁.arrow g), ← pullback_comp, pullback.condition]
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map pullback.snd).obj ((pullback (pullback.snd ≫ g)).obj f₂) =
    (map (MonoOver.arrow ((MonoOver.pullback g).obj f₁))).obj
      ((pullback (MonoOver.arrow ((MonoOver.pullback g).obj f₁) ≫ g)).obj f₂)
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₁ f₂ : Subobject Y
⊢ (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂
[PROOFSTEP]
revert f₁
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
⊢ ∀ (f₁ : Subobject Y), (map g).obj (f₁ ⊓ f₂) = (map g).obj f₁ ⊓ (map g).obj f₂
[PROOFSTEP]
apply Quotient.ind'
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
⊢ ∀ (a : MonoOver Y), (map g).obj (Quotient.mk'' a ⊓ f₂) = (map g).obj (Quotient.mk'' a) ⊓ (map g).obj f₂
[PROOFSTEP]
intro f₁
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj (Quotient.mk'' f₁ ⊓ f₂) = (map g).obj (Quotient.mk'' f₁) ⊓ (map g).obj f₂
[PROOFSTEP]
erw [inf_def, inf_def, inf_eq_map_pullback', inf_eq_map_pullback', ← map_comp]
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (MonoOver.arrow f₁ ≫ g)).obj ((pullback (MonoOver.arrow f₁)).obj f₂) =
    (map (MonoOver.arrow ((MonoOver.map g).obj f₁))).obj
      ((pullback (MonoOver.arrow ((MonoOver.map g).obj f₁))).obj ((map g).obj f₂))
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map (MonoOver.arrow f₁ ≫ g)).obj ((pullback (MonoOver.arrow f₁)).obj f₂) =
    (map (MonoOver.arrow f₁ ≫ g)).obj ((pullback (MonoOver.arrow f₁ ≫ g)).obj ((map g).obj f₂))
[PROOFSTEP]
rw [pullback_comp, pullback_map_self]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
h : ∃ i, i ∈ s ∧ Factors (P i) f
⊢ Factors (Finset.sup s P) f
[PROOFSTEP]
classical
revert h
induction' s using Finset.induction_on with _ _ _ ih
· rintro ⟨_, ⟨⟨⟩, _⟩⟩
· rintro ⟨j, ⟨m, h⟩⟩
  simp only [Finset.sup_insert]
  simp at m 
  rcases m with (rfl | m)
  · exact sup_factors_of_factors_left h
  · exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
h : ∃ i, i ∈ s ∧ Factors (P i) f
⊢ Factors (Finset.sup s P) f
[PROOFSTEP]
revert h
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
⊢ (∃ i, i ∈ s ∧ Factors (P i) f) → Factors (Finset.sup s P) f
[PROOFSTEP]
induction' s using Finset.induction_on with _ _ _ ih
[GOAL]
case empty
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
⊢ (∃ i, i ∈ ∅ ∧ Factors (P i) f) → Factors (Finset.sup ∅ P) f
[PROOFSTEP]
rintro ⟨_, ⟨⟨⟩, _⟩⟩
[GOAL]
case insert
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
⊢ (∃ i, i ∈ insert a✝¹ s✝ ∧ Factors (P i) f) → Factors (Finset.sup (insert a✝¹ s✝) P) f
[PROOFSTEP]
rintro ⟨j, ⟨m, h⟩⟩
[GOAL]
case insert.intro.intro
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
m : j ∈ insert a✝¹ s✝
h : Factors (P j) f
⊢ Factors (Finset.sup (insert a✝¹ s✝) P) f
[PROOFSTEP]
simp only [Finset.sup_insert]
[GOAL]
case insert.intro.intro
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
m : j ∈ insert a✝¹ s✝
h : Factors (P j) f
⊢ Factors (P a✝¹ ⊔ Finset.sup s✝ P) f
[PROOFSTEP]
simp at m 
[GOAL]
case insert.intro.intro
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
h : Factors (P j) f
m : j = a✝¹ ∨ j ∈ s✝
⊢ Factors (P a✝¹ ⊔ Finset.sup s✝ P) f
[PROOFSTEP]
rcases m with (rfl | m)
[GOAL]
case insert.intro.intro.inl
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
s✝ : Finset I
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
h : Factors (P j) f
a✝ : ¬j ∈ s✝
⊢ Factors (P j ⊔ Finset.sup s✝ P) f
[PROOFSTEP]
exact sup_factors_of_factors_left h
[GOAL]
case insert.intro.intro.inr
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : ¬a✝¹ ∈ s✝
ih : (∃ i, i ∈ s✝ ∧ Factors (P i) f) → Factors (Finset.sup s✝ P) f
j : I
h : Factors (P j) f
m : j ∈ s✝
⊢ Factors (P a✝¹ ⊔ Finset.sup s✝ P) f
[PROOFSTEP]
exact sup_factors_of_factors_right (ih ⟨j, ⟨m, h⟩⟩)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : WellPowered C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
j : ↑(↑(equivShrink (Subobject A)) '' s)
⊢ ↑(equivShrink (Subobject A)).symm ↑j ∈ s
[PROOFSTEP]
rcases j with ⟨-, ⟨g, ⟨m, rfl⟩⟩⟩
[GOAL]
case mk.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : WellPowered C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
g : Subobject A
m : g ∈ s
⊢ ↑(equivShrink (Subobject A)).symm
      ↑{ val := ↑(equivShrink (Subobject A)) g,
          property := (_ : ∃ a, a ∈ s ∧ ↑(equivShrink (Subobject A)) a = ↑(equivShrink (Subobject A)) g) } ∈
    s
[PROOFSTEP]
simpa using m
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : WellPowered C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ ∀ (j : ↑(↑(equivShrink (Subobject A)) '' s)),
    (fun j => underlying.map (homOfLE (_ : f ≤ ↑(equivShrink (Subobject A)).symm ↑j))) j ≫
        (wideCospan s).map (WidePullbackShape.Hom.term j) =
      arrow f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
j : WidePullbackShape ↑(↑(equivShrink (Subobject A)) '' s)
⊢ u ≫ limit.π (wideCospan s) j = v ≫ limit.π (wideCospan s) j
[PROOFSTEP]
cases j
[GOAL]
case none
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
⊢ u ≫ limit.π (wideCospan s) none = v ≫ limit.π (wideCospan s) none
[PROOFSTEP]
exact h
[GOAL]
case some
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val✝ : ↑(↑(equivShrink (Subobject A)) '' s)
⊢ u ≫ limit.π (wideCospan s) (some val✝) = v ≫ limit.π (wideCospan s) (some val✝)
[PROOFSTEP]
apply (cancel_mono ((equivShrink (Subobject A)).symm _).arrow).1
[GOAL]
case some
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val✝ : ↑(↑(equivShrink (Subobject A)) '' s)
⊢ (u ≫ limit.π (wideCospan s) (some val✝)) ≫ arrow (↑(equivShrink (Subobject A)).symm ↑val✝) =
    (v ≫ limit.π (wideCospan s) (some val✝)) ≫ arrow (↑(equivShrink (Subobject A)).symm ↑val✝)
[PROOFSTEP]
rw [assoc, assoc]
[GOAL]
case some
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val✝ : ↑(↑(equivShrink (Subobject A)) '' s)
⊢ u ≫ limit.π (wideCospan s) (some val✝) ≫ arrow (↑(equivShrink (Subobject A)).symm ↑val✝) =
    v ≫ limit.π (wideCospan s) (some val✝) ≫ arrow (↑(equivShrink (Subobject A)).symm ↑val✝)
[PROOFSTEP]
erw [limit.w (wideCospan s) (WidePullbackShape.Hom.term _)]
[GOAL]
case some
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
val✝ : ↑(↑(equivShrink (Subobject A)) '' s)
⊢ u ≫ limit.π (wideCospan s) none = v ≫ limit.π (wideCospan s) none
[PROOFSTEP]
exact h
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ sInf s ≤ f
[PROOFSTEP]
fapply le_of_comm
[GOAL]
case f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj (sInf s) ⟶ underlying.obj f
[PROOFSTEP]
exact
  (underlyingIso _).hom ≫
    Limits.limit.π (wideCospan s)
        (some ⟨equivShrink (Subobject A) f, Set.mem_image_of_mem (equivShrink (Subobject A)) hf⟩) ≫
      eqToHom (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _))
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ((underlyingIso (widePullbackι s)).hom ≫
        limit.π (wideCospan s)
            (some
              { val := ↑(equivShrink (Subobject A)) f,
                property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) }) ≫
          eqToHom
            (_ :
              underlying.obj
                  (↑(equivShrink (Subobject A)).symm
                    ↑{ val := ↑(equivShrink (Subobject A)) f,
                        property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) }) =
                underlying.obj f)) ≫
      arrow f =
    arrow (sInf s)
[PROOFSTEP]
dsimp [sInf]
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ((underlyingIso (widePullbackι s)).hom ≫
        limit.π (wideCospan s)
            (some
              { val := ↑(equivShrink (Subobject A)) f,
                property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) }) ≫
          eqToHom
            (_ :
              underlying.obj (↑(equivShrink (Subobject A)).symm (↑(equivShrink (Subobject A)) f)) = underlying.obj f)) ≫
      arrow f =
    arrow (mk (widePullbackι s))
[PROOFSTEP]
simp only [Category.comp_id, Category.assoc, ← underlyingIso_hom_comp_eq_mk, Subobject.arrow_congr,
  congrArg_mpr_hom_left, Iso.cancel_iso_hom_left]
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ limit.π (wideCospan s)
        (some
          { val := ↑(equivShrink (Subobject A)) f,
            property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) }) ≫
      eqToHom
          (_ : underlying.obj (↑(equivShrink (Subobject A)).symm (↑(equivShrink (Subobject A)) f)) = underlying.obj f) ≫
        arrow f =
    widePullbackι s
[PROOFSTEP]
convert limit.w (wideCospan s) (WidePullbackShape.Hom.term _)
[GOAL]
case h.e'_2.h.h.e'_7.h
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
e_1✝ : (widePullback s ⟶ A) = (limit (wideCospan s) ⟶ (wideCospan s).obj none)
e_4✝ :
  (wideCospan s).obj
      (some
        { val := ↑(equivShrink (Subobject A)) f,
          property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) }) =
    (wideCospan s).obj
      (some
        { val := ↑(equivShrink (Subobject A)) f,
          property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) })
e_5✝ : A = (wideCospan s).obj none
⊢ eqToHom (_ : underlying.obj (↑(equivShrink (Subobject A)).symm (↑(equivShrink (Subobject A)) f)) = underlying.obj f) ≫
      arrow f =
    (wideCospan s).map
      (WidePullbackShape.Hom.term
        { val := ↑(equivShrink (Subobject A)) f,
          property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) })
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ f ≤ sInf s
[PROOFSTEP]
fapply le_of_comm
[GOAL]
case f
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ underlying.obj f ⟶ underlying.obj (sInf s)
[PROOFSTEP]
exact Limits.limit.lift _ (leInfCone s f k) ≫ (underlyingIso _).inv
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ (underlyingIso (widePullbackι s)).inv) ≫ arrow (sInf s) = arrow f
[PROOFSTEP]
dsimp [sInf]
[GOAL]
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : WellPowered C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → f ≤ g
⊢ (limit.lift (wideCospan s) (leInfCone s f k) ≫ (underlyingIso (widePullbackι s)).inv) ≫ arrow (mk (widePullbackι s)) =
    arrow f
[PROOFSTEP]
rw [assoc, underlyingIso_arrow, widePullbackι, limit.lift_π, leInfCone_π_app_none]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ f ≤ sSup s
[PROOFSTEP]
fapply le_of_comm
[GOAL]
case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f ⟶ underlying.obj (sSup s)
[PROOFSTEP]
refine'
  eqToHom _ ≫
    Sigma.ι _ ⟨equivShrink (Subobject A) f, by simpa [Set.mem_image] using hf⟩ ≫
      factorThruImage _ ≫ (underlyingIso _).inv
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s
[PROOFSTEP]
simpa [Set.mem_image] using hf
[GOAL]
case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f =
    underlying.obj
      (↑(equivShrink (Subobject A)).symm
        ↑{ val := ↑(equivShrink (Subobject A)) f,
            property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) })
[PROOFSTEP]
exact (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _).symm)
[GOAL]
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ (eqToHom
          (_ :
            underlying.obj f =
              underlying.obj
                (↑(equivShrink (Subobject A)).symm
                  ↑{ val := ↑(equivShrink (Subobject A)) f,
                      property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) })) ≫
        Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j))
            { val := ↑(equivShrink (Subobject A)) f,
              property := (_ : ↑(equivShrink (Subobject A)) f ∈ ↑(equivShrink (Subobject A)) '' s) } ≫
          factorThruImage (smallCoproductDesc s) ≫ (underlyingIso (image.ι (smallCoproductDesc s))).inv) ≫
      arrow (sSup s) =
    arrow f
[PROOFSTEP]
simp [sSup, smallCoproductDesc]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : β
h : ↑e.symm x ∈ s
⊢ ↑e (↑e.symm x) = x
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : β
⊢ x ∈ ↑e '' s → ↑e.symm x ∈ s
[PROOFSTEP]
rintro ⟨a, m, rfl⟩
[GOAL]
case intro.intro
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ ↑e.symm (↑e a) ∈ s
[PROOFSTEP]
simpa using m
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ sSup s ≤ f
[PROOFSTEP]
fapply le_of_comm
[GOAL]
case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ underlying.obj (sSup s) ⟶ underlying.obj f
[PROOFSTEP]
refine' (underlyingIso _).hom ≫ image.lift ⟨_, f.arrow, _, _⟩
[GOAL]
case f.refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ (∐ fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) ⟶ underlying.obj f
[PROOFSTEP]
refine' Sigma.desc _
[GOAL]
case f.refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ (b : ↑(↑(equivShrink (Subobject A)) '' s)) → underlying.obj (↑(equivShrink (Subobject A)).symm ↑b) ⟶ underlying.obj f
[PROOFSTEP]
rintro ⟨g, m⟩
[GOAL]
case f.refine'_1.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
g : Shrink (Subobject A)
m : g ∈ ↑(equivShrink (Subobject A)) '' s
⊢ underlying.obj (↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m }) ⟶ underlying.obj f
[PROOFSTEP]
refine' underlying.map (homOfLE (k _ _))
[GOAL]
case f.refine'_1.mk
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
g : Shrink (Subobject A)
m : g ∈ ↑(equivShrink (Subobject A)) '' s
⊢ ↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m } ∈ s
[PROOFSTEP]
simpa using m
[GOAL]
case f.refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ (Sigma.desc fun b =>
        Subtype.casesOn b fun g m =>
          underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m } ≤ f))) ≫
      arrow f =
    smallCoproductDesc s
[PROOFSTEP]
ext
[GOAL]
case f.refine'_2.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
b✝ : ↑(↑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b =>
          Subtype.casesOn b fun g m =>
            underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m } ≤ f))) ≫
        arrow f =
    Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫ smallCoproductDesc s
[PROOFSTEP]
dsimp [smallCoproductDesc]
[GOAL]
case f.refine'_2.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
b✝ : ↑(↑(equivShrink (Subobject A)) '' s)
⊢ Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      (Sigma.desc fun b => underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑b ≤ f))) ≫ arrow f =
    Sigma.ι (fun j => underlying.obj (↑(equivShrink (Subobject A)).symm ↑j)) b✝ ≫
      Sigma.desc fun j => arrow (↑(equivShrink (Subobject A)).symm ↑j)
[PROOFSTEP]
simp
[GOAL]
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          (MonoFactorisation.mk (underlying.obj f) (arrow f)
            (Sigma.desc fun b =>
              Subtype.casesOn b fun g m =>
                underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑{ val := g, property := m } ≤ f))))) ≫
      arrow f =
    arrow (sSup s)
[PROOFSTEP]
dsimp [sSup]
[GOAL]
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ (g : Subobject A), g ∈ s → g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          (MonoFactorisation.mk (underlying.obj f) (arrow f)
            (Sigma.desc fun b => underlying.map (homOfLE (_ : ↑(equivShrink (Subobject A)).symm ↑b ≤ f))))) ≫
      arrow f =
    arrow (mk (image.ι (smallCoproductDesc s)))
[PROOFSTEP]
rw [assoc, image.lift_fac, underlyingIso_hom_comp_eq_mk]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
Z : Subobject (underlying.obj Y)
⊢ ((underlyingIso (arrow Z ≫ arrow Y)).hom ≫ arrow Z) ≫ arrow Y = arrow (mk (arrow Z ≫ arrow Y))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
Z : Subobject (underlying.obj Y)
⊢ (underlyingIso (arrow Z ≫ arrow Y)).hom ≫ arrow Z =
    ofLE (↑((fun Z => { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) }) Z)) Y
      (_ :
        ↑((fun Z => { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) }) Z) ∈
          Set.Iic Y)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
Z : ↑(Set.Iic Y)
⊢ (underlyingIso (ofLE (↑Z) Y (_ : ↑Z ∈ Set.Iic Y))).hom ≫ arrow ↑Z =
    arrow ((fun Z => mk (ofLE (↑Z) Y (_ : ↑Z ∈ Set.Iic Y))) Z) ≫ arrow Y
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
Z : ↑(Set.Iic Y)
⊢ (underlyingIso (ofLE (↑Z) Y (_ : ↑Z ∈ Set.Iic Y))).hom ≫ arrow ↑Z =
    arrow (mk (ofLE (↑Z) Y (_ : ↑Z ∈ Set.Iic Y))) ≫ arrow Y
[PROOFSTEP]
simp [← Iso.eq_inv_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
⊢ ↑{ toFun := fun Z => { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) },
            invFun := fun Z => mk (ofLE (↑Z) Y (_ : ↑Z ∈ Set.Iic Y)),
            left_inv :=
              (_ :
                ∀ (Z : Subobject (underlying.obj Y)),
                  mk
                      (ofLE
                        (↑((fun Z =>
                              { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) })
                            Z))
                        Y
                        (_ :
                          ↑((fun Z =>
                                  { val := mk (arrow Z ≫ arrow Y),
                                    property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) })
                                Z) ∈
                            Set.Iic Y)) =
                    Z),
            right_inv :=
              (_ :
                ∀ (Z : ↑(Set.Iic Y)),
                  (fun Z => { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) })
                      ((fun Z => mk (ofLE (↑Z) Y (_ : ↑Z ∈ Set.Iic Y))) Z) =
                    Z) }
        W ≤
      ↑{ toFun := fun Z => { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) },
            invFun := fun Z => mk (ofLE (↑Z) Y (_ : ↑Z ∈ Set.Iic Y)),
            left_inv :=
              (_ :
                ∀ (Z : Subobject (underlying.obj Y)),
                  mk
                      (ofLE
                        (↑((fun Z =>
                              { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) })
                            Z))
                        Y
                        (_ :
                          ↑((fun Z =>
                                  { val := mk (arrow Z ≫ arrow Y),
                                    property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) })
                                Z) ∈
                            Set.Iic Y)) =
                    Z),
            right_inv :=
              (_ :
                ∀ (Z : ↑(Set.Iic Y)),
                  (fun Z => { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) })
                      ((fun Z => mk (ofLE (↑Z) Y (_ : ↑Z ∈ Set.Iic Y))) Z) =
                    Z) }
        Z ↔
    W ≤ Z
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
⊢ { val := mk (arrow W ≫ arrow Y), property := (_ : mk (arrow W ≫ arrow Y) ∈ Set.Iic Y) } ≤
      { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) } ↔
    W ≤ Z
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
⊢ { val := mk (arrow W ≫ arrow Y), property := (_ : mk (arrow W ≫ arrow Y) ∈ Set.Iic Y) } ≤
      { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) } →
    W ≤ Z
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
h :
  { val := mk (arrow W ≫ arrow Y), property := (_ : mk (arrow W ≫ arrow Y) ∈ Set.Iic Y) } ≤
    { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) }
⊢ W ≤ Z
[PROOFSTEP]
exact le_of_comm (((underlyingIso _).inv ≫ ofLE _ _ (Subtype.mk_le_mk.mp h) ≫ (underlyingIso _).hom)) (by aesop_cat)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
h :
  { val := mk (arrow W ≫ arrow Y), property := (_ : mk (arrow W ≫ arrow Y) ∈ Set.Iic Y) } ≤
    { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) }
⊢ ((underlyingIso (arrow W ≫ arrow Y)).inv ≫
        ofLE (mk (arrow W ≫ arrow Y)) (mk (arrow Z ≫ arrow Y)) (_ : mk (arrow W ≫ arrow Y) ≤ mk (arrow Z ≫ arrow Y)) ≫
          (underlyingIso (arrow Z ≫ arrow Y)).hom) ≫
      arrow Z =
    arrow W
[PROOFSTEP]
aesop_cat
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
⊢ W ≤ Z →
    { val := mk (arrow W ≫ arrow Y), property := (_ : mk (arrow W ≫ arrow Y) ∈ Set.Iic Y) } ≤
      { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) }
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
h : W ≤ Z
⊢ { val := mk (arrow W ≫ arrow Y), property := (_ : mk (arrow W ≫ arrow Y) ∈ Set.Iic Y) } ≤
    { val := mk (arrow Z ≫ arrow Y), property := (_ : mk (arrow Z ≫ arrow Y) ∈ Set.Iic Y) }
[PROOFSTEP]
exact Subtype.mk_le_mk.mpr (le_of_comm ((underlyingIso _).hom ≫ ofLE _ _ h ≫ (underlyingIso _).inv) (by simp))
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
h : W ≤ Z
⊢ ((underlyingIso (arrow W ≫ arrow Y)).hom ≫ ofLE W Z h ≫ (underlyingIso (arrow Z ≫ arrow Y)).inv) ≫
      arrow (mk (arrow Z ≫ arrow Y)) =
    arrow (mk (arrow W ≫ arrow Y))
[PROOFSTEP]
simp
