[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


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J J₁ J₂ : GrothendieckTopology C
h : J₁.sieves = J₂.sieves
⊢ J₁ = J₂
[PROOFSTEP]
cases J₁
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J J₂ : GrothendieckTopology C
sieves✝ : (X : C) → Set (Sieve X)
top_mem'✝ : ∀ (X : C), ⊤ ∈ sieves✝ X
pullback_stable'✝ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝ X → Sieve.pullback f S ∈ sieves✝ Y
transitive'✝ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝ Y) → R ∈ sieves✝ X
h :
  { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝,
        transitive' := transitive'✝ }.sieves =
    J₂.sieves
⊢ { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ } = J₂
[PROOFSTEP]
cases J₂
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
sieves✝¹ : (X : C) → Set (Sieve X)
top_mem'✝¹ : ∀ (X : C), ⊤ ∈ sieves✝¹ X
pullback_stable'✝¹ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝¹ X → Sieve.pullback f S ∈ sieves✝¹ Y
transitive'✝¹ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝¹ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝¹ Y) → R ∈ sieves✝¹ X
sieves✝ : (X : C) → Set (Sieve X)
top_mem'✝ : ∀ (X : C), ⊤ ∈ sieves✝ X
pullback_stable'✝ : ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sieves✝ X → Sieve.pullback f S ∈ sieves✝ Y
transitive'✝ :
  ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sieves✝ X →
      ∀ (R : Sieve X), (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sieves✝ Y) → R ∈ sieves✝ X
h :
  { sieves := sieves✝¹, top_mem' := top_mem'✝¹, pullback_stable' := pullback_stable'✝¹,
        transitive' := transitive'✝¹ }.sieves =
    { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝,
        transitive' := transitive'✝ }.sieves
⊢ { sieves := sieves✝¹, top_mem' := top_mem'✝¹, pullback_stable' := pullback_stable'✝¹, transitive' := transitive'✝¹ } =
    { sieves := sieves✝, top_mem' := top_mem'✝, pullback_stable' := pullback_stable'✝, transitive' := transitive'✝ }
[PROOFSTEP]
congr
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ sieves J X
⊢ R ∈ sieves J X
[PROOFSTEP]
apply J.transitive sjx R fun Y f hf => _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ sieves J X
⊢ ∀ (Y : C) (f : Y ⟶ X), S.arrows f → Sieve.pullback f R ∈ sieves J Y
[PROOFSTEP]
intros Y f hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R ∈ sieves J Y
[PROOFSTEP]
apply covering_of_eq_top
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f R = ⊤
[PROOFSTEP]
rw [← top_le_iff, ← S.pullback_eq_top_of_mem hf]
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
Hss : S ≤ R
sjx : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f S ≤ Sieve.pullback f R
[PROOFSTEP]
apply Sieve.pullback_monotone _ Hss
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
⊢ R ⊓ S ∈ sieves J X
[PROOFSTEP]
apply J.transitive rj _ fun Y f Hf => _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
⊢ ∀ (Y : C) (f : Y ⟶ X), R.arrows f → Sieve.pullback f (R ⊓ S) ∈ sieves J Y
[PROOFSTEP]
intros Y f hf
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ Sieve.pullback f (R ⊓ S) ∈ sieves J Y
[PROOFSTEP]
rw [Sieve.pullback_inter, R.pullback_eq_top_of_mem hf]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S R : Sieve X
J : GrothendieckTopology C
rj : R ∈ sieves J X
sj : S ∈ sieves J X
Y : C
f : Y ⟶ X
hf : R.arrows f
⊢ ⊤ ⊓ Sieve.pullback f S ∈ sieves J Y
[PROOFSTEP]
simp [sj]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
S : Sieve X
⊢ S ∈ sieves J X ↔ Covers J S (𝟙 X)
[PROOFSTEP]
simp [covers_iff]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ Covers J S f
[PROOFSTEP]
rw [Covers, (Sieve.pullback_eq_top_iff_mem f).1 hf]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ ⊤ ∈ sieves J Y
[PROOFSTEP]
apply J.top_mem
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
h : Covers J S f
Z : C
g : Z ⟶ Y
⊢ Covers J S (g ≫ f)
[PROOFSTEP]
rw [covers_iff] at h ⊢
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
h : Sieve.pullback f S ∈ sieves J Y
Z : C
g : Z ⟶ Y
⊢ Sieve.pullback (g ≫ f) S ∈ sieves J Z
[PROOFSTEP]
simp [h, Sieve.pullback_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
⊢ (∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g) → Covers J R f
[PROOFSTEP]
intro k
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
⊢ Covers J R f
[PROOFSTEP]
apply J.transitive h
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄, (Sieve.pullback f S).arrows f_1 → Sieve.pullback f_1 (Sieve.pullback f R) ∈ sieves J Y_1
[PROOFSTEP]
intro Z g hg
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback g (Sieve.pullback f R) ∈ sieves J Z
[PROOFSTEP]
rw [← Sieve.pullback_comp]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : Covers J S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → Covers J R g
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
⊢ Sieve.pullback (g ≫ f) R ∈ sieves J Z
[PROOFSTEP]
apply k (g ≫ f) hg
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R✝ : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
hS : Covers J S f
hR : Covers J R f
⊢ Covers J (S ⊓ R) f
[PROOFSTEP]
simpa [covers_iff] using And.intro hS hR
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
f : Y ⟶ X
hf : S ∈ (fun X => {⊤}) X
⊢ Sieve.pullback f S ∈ (fun X => {⊤}) Y
[PROOFSTEP]
rw [Set.mem_singleton_iff] at hf ⊢
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
f : Y ⟶ X
hf : S = ⊤
⊢ Sieve.pullback f S = ⊤
[PROOFSTEP]
simp [hf]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ (fun X => {⊤}) X
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {⊤}) Y
⊢ R ∈ (fun X => {⊤}) X
[PROOFSTEP]
rw [Set.mem_singleton_iff, ← Sieve.id_mem_iff_eq_top] at hS
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S.arrows (𝟙 X)
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => {⊤}) Y
⊢ R ∈ (fun X => {⊤}) X
[PROOFSTEP]
simpa using hR hS
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ (X : C), ⊤ ∈ (fun X => Set.univ) X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S R : Sieve X✝
J : GrothendieckTopology C
X Y : C
f : Sieve X
⊢ ∀ (f_1 : Y ⟶ X), f ∈ (fun X => Set.univ) X → Sieve.pullback f_1 f ∈ (fun X => Set.univ) Y
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ (fun X => Set.univ) X →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X => Set.univ) Y) → R ∈ (fun X => Set.univ) X
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
T : Set (GrothendieckTopology C)
⊢ ∀ (X : C), ⊤ ∈ sInf (sieves '' T) X
[PROOFSTEP]
rintro X S ⟨⟨_, J, hJ, rfl⟩, rfl⟩
[GOAL]
case intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S R : Sieve X✝
J✝ : GrothendieckTopology C
T : Set (GrothendieckTopology C)
X : C
J : GrothendieckTopology C
hJ : J ∈ T
⊢ ⊤ ∈ (fun f => ↑f X) { val := J.sieves, property := (_ : ∃ a, a ∈ T ∧ a.sieves = J.sieves) }
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
T : Set (GrothendieckTopology C)
⊢ ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X), S ∈ sInf (sieves '' T) X → Sieve.pullback f S ∈ sInf (sieves '' T) Y
[PROOFSTEP]
rintro X Y S hS f _ ⟨⟨_, J, hJ, rfl⟩, rfl⟩
[GOAL]
case intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J✝ : GrothendieckTopology C
T : Set (GrothendieckTopology C)
X Y : C
S : Sieve X
hS : Y ⟶ X
f : S ∈ sInf (sieves '' T) X
J : GrothendieckTopology C
hJ : J ∈ T
⊢ Sieve.pullback hS S ∈ (fun f => ↑f Y) { val := J.sieves, property := (_ : ∃ a, a ∈ T ∧ a.sieves = J.sieves) }
[PROOFSTEP]
apply J.pullback_stable _ (f _ ⟨⟨_, _, hJ, rfl⟩, rfl⟩)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
T : Set (GrothendieckTopology C)
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ sInf (sieves '' T) X →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sInf (sieves '' T) Y) → R ∈ sInf (sieves '' T) X
[PROOFSTEP]
rintro X S hS R h _ ⟨⟨_, J, hJ, rfl⟩, rfl⟩
[GOAL]
case intro.mk.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R✝ : Sieve X✝
J✝ : GrothendieckTopology C
T : Set (GrothendieckTopology C)
X : C
S : Sieve X
hS : S ∈ sInf (sieves '' T) X
R : Sieve X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ sInf (sieves '' T) Y
J : GrothendieckTopology C
hJ : J ∈ T
⊢ R ∈ (fun f => ↑f X) { val := J.sieves, property := (_ : ∃ a, a ∈ T ∧ a.sieves = J.sieves) }
[PROOFSTEP]
apply J.transitive (hS _ ⟨⟨_, _, hJ, rfl⟩, rfl⟩) _ fun Y f hf => h hf _ ⟨⟨_, _, hJ, rfl⟩, rfl⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
⊢ IsGLB s (sInf s)
[PROOFSTEP]
refine' @IsGLB.of_image _ _ _ _ sieves _ _ _ _
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
⊢ ∀ {x y : GrothendieckTopology C}, x.sieves ≤ y.sieves ↔ x ≤ y
[PROOFSTEP]
intros
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
x✝ y✝ : GrothendieckTopology C
⊢ x✝.sieves ≤ y✝.sieves ↔ x✝ ≤ y✝
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
s : Set (GrothendieckTopology C)
⊢ IsGLB (sieves '' s) (sInf s).sieves
[PROOFSTEP]
exact _root_.isGLB_sInf _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ discrete C = ⊤
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ discrete C ≤ ⊤
[PROOFSTEP]
exact @CompleteLattice.le_top _ (completeLatticeOfInf _ isGLB_sInf) (discrete C)
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ⊤ ≤ discrete C
[PROOFSTEP]
intro X S _
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
a✝ : S ∈ sieves ⊤ X
⊢ S ∈ sieves (discrete C) X
[PROOFSTEP]
apply Set.mem_univ
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ trivial C = ⊥
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ trivial C ≤ ⊥
[PROOFSTEP]
intro X S hS
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ sieves (trivial C) X
⊢ S ∈ sieves ⊥ X
[PROOFSTEP]
rw [trivial_covering] at hS
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S = ⊤
⊢ S ∈ sieves ⊥ X
[PROOFSTEP]
apply covering_of_eq_top _ hS
[GOAL]
case a
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ⊥ ≤ trivial C
[PROOFSTEP]
refine' @CompleteLattice.bot_le _ (completeLatticeOfInf _ isGLB_sInf) (trivial C)
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
S : Sieve X
f : Y ⟶ X
⊢ Covers ⊥ S f ↔ S.arrows f
[PROOFSTEP]
rw [covers_iff, bot_covering, ← Sieve.pullback_eq_top_iff_mem]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
S : Sieve X
f : Y ⟶ X
⊢ Covers ⊤ S f
[PROOFSTEP]
simp [covers_iff]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X),
    S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X →
      Sieve.pullback f S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y
[PROOFSTEP]
intro X Y S h H Z f
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
h : Y ⟶ X
H : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
Z : C
f : Z ⟶ Y
⊢ ∃ Z_1 g, (Sieve.pullback h S).arrows (g ≫ f)
[PROOFSTEP]
rcases H (f ≫ h) with ⟨W, g, H'⟩
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
h : Y ⟶ X
H : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
Z : C
f : Z ⟶ Y
W : C
g : W ⟶ Z
H' : S.arrows (g ≫ f ≫ h)
⊢ ∃ Z_1 g, (Sieve.pullback h S).arrows (g ≫ f)
[PROOFSTEP]
exact ⟨W, g, by simpa⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y : C
S : Sieve X
h : Y ⟶ X
H : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
Z : C
f : Z ⟶ Y
W : C
g : W ⟶ Z
H' : S.arrows (g ≫ f ≫ h)
⊢ (Sieve.pullback h S).arrows (g ≫ f)
[PROOFSTEP]
simpa
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
            S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y) →
          R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
[PROOFSTEP]
intro X S H₁ R H₂ Y f
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
R : Sieve X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y
Y : C
f : Y ⟶ X
⊢ ∃ Z g, R.arrows (g ≫ f)
[PROOFSTEP]
rcases H₁ f with ⟨Z, g, H₃⟩
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
R : Sieve X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
⊢ ∃ Z g, R.arrows (g ≫ f)
[PROOFSTEP]
rcases H₂ H₃ (𝟙 Z) with ⟨W, h, H₄⟩
[GOAL]
case intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
R : Sieve X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
W : C
h : W ⟶ Z
H₄ : (Sieve.pullback (g ≫ f) R).arrows (h ≫ 𝟙 Z)
⊢ ∃ Z g, R.arrows (g ≫ f)
[PROOFSTEP]
exact ⟨W, h ≫ g, by simpa using H₄⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
X : C
S : Sieve X
H₁ : S ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) X
R : Sieve X
H₂ :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)) Y
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ Y
H₃ : S.arrows (g ≫ f)
W : C
h : W ⟶ Z
H₄ : (Sieve.pullback (g ≫ f) R).arrows (h ≫ 𝟙 Z)
⊢ R.arrows ((h ≫ g) ≫ f)
[PROOFSTEP]
simpa using H₄
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
hro : RightOreCondition C
⊢ ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X),
    S ∈ (fun X S => ∃ Y f, S.arrows f) X → Sieve.pullback f S ∈ (fun X S => ∃ Y f, S.arrows f) Y
[PROOFSTEP]
rintro X Y S h ⟨Z, f, hf⟩
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X Y : C
S : Sieve X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
⊢ Sieve.pullback h S ∈ (fun X S => ∃ Y f, S.arrows f) Y
[PROOFSTEP]
rcases hro h f with ⟨W, g, k, comm⟩
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X Y : C
S : Sieve X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
W : C
g : W ⟶ Y
k : W ⟶ Z
comm : g ≫ h = k ≫ f
⊢ Sieve.pullback h S ∈ (fun X S => ∃ Y f, S.arrows f) Y
[PROOFSTEP]
refine' ⟨_, g, _⟩
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X Y : C
S : Sieve X
h : Y ⟶ X
Z : C
f : Z ⟶ X
hf : S.arrows f
W : C
g : W ⟶ Y
k : W ⟶ Z
comm : g ≫ h = k ≫ f
⊢ (Sieve.pullback h S).arrows g
[PROOFSTEP]
simp [comm, hf]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S R : Sieve X
J : GrothendieckTopology C
hro : RightOreCondition C
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ (fun X S => ∃ Y f, S.arrows f) X →
      ∀ (R : Sieve X),
        (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∃ Y f, S.arrows f) Y) →
          R ∈ (fun X S => ∃ Y f, S.arrows f) X
[PROOFSTEP]
rintro X S ⟨Y, f, hf⟩ R h
[GOAL]
case intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X : C
S : Sieve X
Y : C
f : Y ⟶ X
hf : S.arrows f
R : Sieve X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∃ Y f, S.arrows f) Y
⊢ R ∈ (fun X S => ∃ Y f, S.arrows f) X
[PROOFSTEP]
rcases h hf with ⟨Z, g, hg⟩
[GOAL]
case intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R✝ : Sieve X✝
J : GrothendieckTopology C
hro : RightOreCondition C
X : C
S : Sieve X
Y : C
f : Y ⟶ X
hf : S.arrows f
R : Sieve X
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ (fun X S => ∃ Y f, S.arrows f) Y
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
⊢ R ∈ (fun X S => ∃ Y f, S.arrows f) X
[PROOFSTEP]
exact ⟨_, _, hg⟩
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S✝ R : Sieve X
J : GrothendieckTopology C
src✝ : Preorder (Cover J X) := inferInstance
S : Cover J X
Y : C
f : Y ⟶ X
x✝ : ((fun a => ↑a) S).arrows f
⊢ ((fun a => ↑a) ⊤).arrows f
[PROOFSTEP]
tauto
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S✝ R : Sieve X
J : GrothendieckTopology C
src✝ : Preorder (Cover J X) := inferInstance
S T : Cover J X
h1 : S ≤ T
h2 : T ≤ S
Y : C
f : Y ⟶ X
⊢ (sieve S).arrows f → (sieve T).arrows f
[PROOFSTEP]
apply h1
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S✝ R : Sieve X
J : GrothendieckTopology C
src✝ : Preorder (Cover J X) := inferInstance
S T : Cover J X
h1 : S ≤ T
h2 : T ≤ S
Y : C
f : Y ⟶ X
⊢ (sieve T).arrows f → (sieve S).arrows f
[PROOFSTEP]
apply h2
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
f : Y ⟶ X
S : Cover J X
I : Relation (pullback S f)
⊢ I.g₁ ≫ I.f₁ ≫ f = I.g₂ ≫ I.f₂ ≫ f
[PROOFSTEP]
simp [reassoc_of% I.w]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y✝ : C
S✝ R : Sieve X
J : GrothendieckTopology C
S : Cover J X
Y : C
f : Y ⟶ X
⊢ (sieve (pullback S (𝟙 X))).arrows f ↔ (sieve S).arrows f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝¹ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X Y✝ Z : C
S : Cover J X
f✝ : Z ⟶ Y✝
g : Y✝ ⟶ X
Y : C
f : Y ⟶ Z
⊢ (sieve (pullback S (f✝ ≫ g))).arrows f ↔ (sieve (pullback (pullback S g) f✝)).arrows f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Cover J X
T : (I : Arrow S) → Cover J I.Y
⊢ bind S T ≤ S
[PROOFSTEP]
rintro Y f ⟨Z, e1, e2, h1, _, h3⟩
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Cover J X
T : (I : Arrow S) → Cover J I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (sieve S).arrows e2
left✝ : ((fun Y f hf => sieve (T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ ((fun a => ↑a) S).arrows f
[PROOFSTEP]
rw [← h3]
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Cover J X
T : (I : Arrow S) → Cover J I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (sieve S).arrows e2
left✝ : ((fun Y f hf => sieve (T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ ((fun a => ↑a) S).arrows (e1 ≫ e2)
[PROOFSTEP]
apply Sieve.downward_closed
[GOAL]
case intro.intro.intro.intro.intro.x
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : Cover J X
T : (I : Arrow S) → Cover J I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (sieve S).arrows e2
left✝ : ((fun Y f hf => sieve (T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ ((fun a => ↑a) S).arrows e2
[PROOFSTEP]
exact h1
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
⊢ ∀ (b : (index S P).R),
    (fun I => P.map I.f.op) (Limits.MulticospanIndex.fstTo (index S P) b) ≫ Limits.MulticospanIndex.fst (index S P) b =
      (fun I => P.map I.f.op) (Limits.MulticospanIndex.sndTo (index S P) b) ≫ Limits.MulticospanIndex.snd (index S P) b
[PROOFSTEP]
intro I
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
I : (index S P).R
⊢ (fun I => P.map I.f.op) (Limits.MulticospanIndex.fstTo (index S P) I) ≫ Limits.MulticospanIndex.fst (index S P) I =
    (fun I => P.map I.f.op) (Limits.MulticospanIndex.sndTo (index S P) I) ≫ Limits.MulticospanIndex.snd (index S P) I
[PROOFSTEP]
dsimp [index]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
I : (index S P).R
⊢ P.map I.f₁.op ≫ P.map I.g₁.op = P.map I.f₂.op ≫ P.map I.g₂.op
[PROOFSTEP]
simp only [← P.map_comp, ← op_comp, I.w]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
inst✝ : Limits.HasMultiequalizer (index S P)
⊢ ∀ (b : (index S P).R),
    (fun I => P.map I.f.op) (Limits.MulticospanIndex.fstTo (index S P) b) ≫ Limits.MulticospanIndex.fst (index S P) b =
      (fun I => P.map I.f.op) (Limits.MulticospanIndex.sndTo (index S P) b) ≫ Limits.MulticospanIndex.snd (index S P) b
[PROOFSTEP]
intro I
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
inst✝ : Limits.HasMultiequalizer (index S P)
I : (index S P).R
⊢ (fun I => P.map I.f.op) (Limits.MulticospanIndex.fstTo (index S P) I) ≫ Limits.MulticospanIndex.fst (index S P) I =
    (fun I => P.map I.f.op) (Limits.MulticospanIndex.sndTo (index S P) I) ≫ Limits.MulticospanIndex.snd (index S P) I
[PROOFSTEP]
dsimp only [index, Relation.fst, Relation.snd]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
S : Cover J X
P : Cᵒᵖ ⥤ D
inst✝ : Limits.HasMultiequalizer (index S P)
I : (index S P).R
⊢ P.map I.f₁.op ≫ P.map I.g₁.op = P.map I.f₂.op ≫ P.map I.g₂.op
[PROOFSTEP]
simp only [← P.map_comp, ← op_comp, I.w]


[GOAL]
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
⊢ ((biproduct.map fun j => (F j).p) ≫ biproduct.map fun j => (F j).p) = biproduct.map fun j => (F j).p
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j✝¹ j✝ : J
⊢ biproduct.ι (fun j => (F j).X) j✝ ≫
      ((biproduct.map fun j => (F j).p) ≫ biproduct.map fun j => (F j).p) ≫ biproduct.π (fun j => (F j).X) j✝¹ =
    biproduct.ι (fun j => (F j).X) j✝ ≫ (biproduct.map fun j => (F j).p) ≫ biproduct.π (fun j => (F j).X) j✝¹
[PROOFSTEP]
simp only [assoc, biproduct.map_π, biproduct.map_π_assoc, idem]
[GOAL]
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j : J
⊢ (biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j =
    (mk (⨁ fun j => (F j).X) (biproduct.map fun j => (F j).p)).p ≫
      ((biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j) ≫ (F j).p
[PROOFSTEP]
simp only [assoc, biproduct.bicone_π, biproduct.map_π, biproduct.map_π_assoc, (F j).idem]
[GOAL]
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j : J
⊢ (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p) =
    (F j).p ≫
      (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p) ≫
        (mk (⨁ fun j => (F j).X) (biproduct.map fun j => (F j).p)).p
[PROOFSTEP]
simp only [biproduct.ι_map, assoc, idem_assoc]
[GOAL]
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
⊢ (fun j => Hom.mk (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p)) j ≫
      (fun j => Hom.mk ((biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j)) j' =
    if h : j = j' then eqToHom (_ : F j = F j') else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : j = j'
⊢ (fun j => Hom.mk (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p)) j ≫
      (fun j => Hom.mk ((biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j)) j' =
    eqToHom (_ : F j = F j')
[PROOFSTEP]
subst h
[GOAL]
case pos
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j : J
⊢ (fun j => Hom.mk (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p)) j ≫
      (fun j => Hom.mk ((biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j)) j =
    eqToHom (_ : F j = F j)
[PROOFSTEP]
simp only [biproduct.ι_map, biproduct.bicone_π, biproduct.map_π, eqToHom_refl, id_eq, hom_ext_iff, comp_f, assoc,
  bicone_ι_π_self_assoc, idem]
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : ¬j = j'
⊢ (fun j => Hom.mk (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p)) j ≫
      (fun j => Hom.mk ((biproduct.map fun j => (F j).p) ≫ Bicone.π (biproduct.bicone fun j => (F j).X) j)) j' =
    0
[PROOFSTEP]
dsimp
[GOAL]
case neg
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
F : J → Karoubi C
j j' : J
h : ¬j = j'
⊢ Hom.mk (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p) ≫
      Hom.mk ((biproduct.map fun j => (F j).p) ≫ biproduct.π (fun j => (F j).X) j') =
    Hom.mk 0
[PROOFSTEP]
simp only [hom_ext_iff, biproduct.ι_map, biproduct.map_π, comp_f, assoc, ne_eq, biproduct.ι_π_ne_assoc _ h, comp_zero,
  zero_comp]
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
⊢ HasBiproduct F
[PROOFSTEP]
apply hasBiproduct_of_total (Biproducts.bicone F)
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
⊢ (Finset.sum Finset.univ fun j => Bicone.π (Biproducts.bicone F) j ≫ Bicone.ι (Biproducts.bicone F) j) =
    𝟙 (Biproducts.bicone F).pt
[PROOFSTEP]
simp only [hom_ext_iff]
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
⊢ (Finset.sum Finset.univ fun j => Bicone.π (Biproducts.bicone F) j ≫ Bicone.ι (Biproducts.bicone F) j).f =
    (𝟙 (Biproducts.bicone F).pt).f
[PROOFSTEP]
refine' biproduct.hom_ext' _ _ (fun j => _)
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
⊢ biproduct.ι (fun j => (F j).X) j ≫
      (Finset.sum Finset.univ fun j => Bicone.π (Biproducts.bicone F) j ≫ Bicone.ι (Biproducts.bicone F) j).f =
    biproduct.ι (fun j => (F j).X) j ≫ (𝟙 (Biproducts.bicone F).pt).f
[PROOFSTEP]
simp only [Biproducts.bicone_pt_X, sum_hom, comp_f, Biproducts.bicone_π_f, biproduct.bicone_π, biproduct.map_π,
  Biproducts.bicone_ι_f, biproduct.ι_map, assoc, idem_assoc, id_eq, Biproducts.bicone_pt_p, comp_sum]
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
⊢ (Finset.sum Finset.univ fun j_1 =>
      biproduct.ι (fun j => (F j).X) j ≫
        biproduct.π (fun b => (F b).X) j_1 ≫ (F j_1).p ≫ biproduct.ι (fun j => (F j).X) j_1) =
    (F j).p ≫ biproduct.ι (fun j => (F j).X) j
[PROOFSTEP]
rw [Finset.sum_eq_single j]
[GOAL]
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
⊢ biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun b => (F b).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j =
    (F j).p ≫ biproduct.ι (fun j => (F j).X) j
[PROOFSTEP]
simp only [bicone_ι_π_self_assoc]
[GOAL]
case h₀
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
⊢ ∀ (b : Fin n),
    b ∈ Finset.univ →
      b ≠ j →
        biproduct.ι (fun j => (F j).X) j ≫
            biproduct.π (fun b => (F b).X) b ≫ (F b).p ≫ biproduct.ι (fun j => (F j).X) b =
          0
[PROOFSTEP]
intro b _ hb
[GOAL]
case h₀
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j b : Fin n
a✝ : b ∈ Finset.univ
hb : b ≠ j
⊢ biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun b => (F b).X) b ≫ (F b).p ≫ biproduct.ι (fun j => (F j).X) b = 0
[PROOFSTEP]
simp only [biproduct.ι_π_ne_assoc _ hb.symm, zero_comp]
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
⊢ ¬j ∈ Finset.univ →
    biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun b => (F b).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j = 0
[PROOFSTEP]
intro hj
[GOAL]
case h₁
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteBiproducts C
n : ℕ
F : Fin n → Karoubi C
j : Fin n
hj : ¬j ∈ Finset.univ
⊢ biproduct.ι (fun j => (F j).X) j ≫ biproduct.π (fun b => (F b).X) j ≫ (F j).p ≫ biproduct.ι (fun j => (F j).X) j = 0
[PROOFSTEP]
simp only [Finset.mem_univ, not_true] at hj
[GOAL]
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ decompId_i P ≫ decompId_p (complement P) = 0
[PROOFSTEP]
simp only [instAddCommGroupHom_zero, hom_ext_iff, complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p,
  comp_sub, comp_id, idem, sub_self]
[GOAL]
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ decompId_i (complement P) ≫ decompId_p P = 0
[PROOFSTEP]
simp only [instAddCommGroupHom_zero, hom_ext_iff, complement_X, comp_f, decompId_i_f, complement_p, decompId_p_f,
  sub_comp, id_comp, idem, sub_self]
[GOAL]
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (BinaryBicone.mk (mk P.X (𝟙 P.X)) (decompId_p P) (decompId_p (complement P)) (decompId_i P)
            (decompId_i (complement P))).fst ≫
        (BinaryBicone.mk (mk P.X (𝟙 P.X)) (decompId_p P) (decompId_p (complement P)) (decompId_i P)
            (decompId_i (complement P))).inl +
      (BinaryBicone.mk (mk P.X (𝟙 P.X)) (decompId_p P) (decompId_p (complement P)) (decompId_i P)
            (decompId_i (complement P))).snd ≫
        (BinaryBicone.mk (mk P.X (𝟙 P.X)) (decompId_p P) (decompId_p (complement P)) (decompId_i P)
            (decompId_i (complement P))).inr =
    𝟙
      (BinaryBicone.mk (mk P.X (𝟙 P.X)) (decompId_p P) (decompId_p (complement P)) (decompId_i P)
          (decompId_i (complement P))).pt
[PROOFSTEP]
simp only [id_eq, complement_X, comp_f, decompId_i_f, decompId_p_f, complement_p, instAddCommGroupHom_add, idem,
  comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel'_right]
[GOAL]
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.desc (decompId_i P) (decompId_i (complement P)) ≫ biprod.lift (decompId_p P) (decompId_p (complement P)) =
    𝟙 (P ⊞ complement P)
[PROOFSTEP]
apply biprod.hom_ext'
[GOAL]
case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.inl ≫
      biprod.desc (decompId_i P) (decompId_i (complement P)) ≫ biprod.lift (decompId_p P) (decompId_p (complement P)) =
    biprod.inl ≫ 𝟙 (P ⊞ complement P)
[PROOFSTEP]
rw [biprod.inl_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc, add_right_eq_self, ← assoc]
[GOAL]
case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (decompId_i P ≫ decompId_p (complement P)) ≫ biprod.inr = 0
[PROOFSTEP]
refine' (_ =≫ _).trans zero_comp
[GOAL]
case h₀
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ decompId_i P ≫ decompId_p (complement P) = 0
[PROOFSTEP]
ext
[GOAL]
case h₀.h
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (decompId_i P ≫ decompId_p (complement P)).f = 0.f
[PROOFSTEP]
simp only [comp_f, toKaroubi_obj_X, decompId_i_f, decompId_p_f, complement_p, comp_sub, comp_id, idem, sub_self,
  instAddCommGroupHom_zero]
[GOAL]
case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.inr ≫
      biprod.desc (decompId_i P) (decompId_i (complement P)) ≫ biprod.lift (decompId_p P) (decompId_p (complement P)) =
    biprod.inr ≫ 𝟙 (P ⊞ complement P)
[PROOFSTEP]
rw [biprod.inr_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc, add_left_eq_self, ← assoc]
[GOAL]
case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (decompId_i (complement P) ≫ decompId_p P) ≫ biprod.inl = 0
[PROOFSTEP]
refine' (_ =≫ _).trans zero_comp
[GOAL]
case h₁
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ decompId_i (complement P) ≫ decompId_p P = 0
[PROOFSTEP]
ext
[GOAL]
case h₁.h
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ (decompId_i (complement P) ≫ decompId_p P).f = 0.f
[PROOFSTEP]
simp only [complement_X, comp_f, decompId_i_f, complement_p, decompId_p_f, sub_comp, id_comp, idem, sub_self,
  instAddCommGroupHom_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
P : Karoubi C
⊢ biprod.lift (decompId_p P) (decompId_p (complement P)) ≫ biprod.desc (decompId_i P) (decompId_i (complement P)) =
    𝟙 ((toKaroubi C).obj P.X)
[PROOFSTEP]
simp only [biprod.lift_desc, instAddCommGroupHom_add, toKaroubi_obj_X, comp_f, decompId_p_f, decompId_i_f, idem,
  complement_X, complement_p, comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel'_right, id_eq,
  toKaroubi_obj_p]