C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this : HasProductsOfShape (↑𝒢) C
⊢ HasInitial C
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
⊢ HasInitial C
haveI : HasProductsOfShape 𝒢 C := hasProductsOfShape_of_small C 𝒢
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝ : HasProductsOfShape (↑𝒢) C
this : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
⊢ HasInitial C
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this : HasProductsOfShape (↑𝒢) C
⊢ HasInitial C
haveI := fun A => hasProductsOfShape_of_small.{v₁} C (ΣG : 𝒢, A ⟶ (G : C))
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
⊢ HasInitial C
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝ : HasProductsOfShape (↑𝒢) C
this : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
⊢ HasInitial C
letI := completeLatticeOfCompleteSemilatticeInf (Subobject (piObj (Subtype.val : 𝒢 → C)))
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
⊢ (A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
⊢ HasInitial C
suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C) ⟶ A) by
  exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C)
case refine'_1
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
⊢ Subobject.underlying.obj ⊥ ⟶ A

case refine'_2
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
⊢ f = default
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
⊢ (A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)
refine' fun A => ⟨⟨_⟩, fun f => _⟩
no goals
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasProductsOfShape (↑𝒢) C
this✝¹ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this✝ : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
this : (A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)
⊢ HasInitial C
exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C)
case refine'_1
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
s : ∏ Subtype.val ⟶ ∏ fun f => ↑f.fst := Pi.lift fun f => id (Pi.π Subtype.val) f.fst
⊢ Subobject.underlying.obj ⊥ ⟶ A
case refine'_1
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
⊢ Subobject.underlying.obj ⊥ ⟶ A
let s := Pi.lift fun f : ΣG : 𝒢, A ⟶ (G : C) => id (Pi.π (Subtype.val : 𝒢 → C)) f.1
case refine'_1
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
s : ∏ Subtype.val ⟶ ∏ fun f => ↑f.fst := Pi.lift fun f => id (Pi.π Subtype.val) f.fst
t : A ⟶ ∏ fun b => ↑b.fst := Pi.lift Sigma.snd
⊢ Subobject.underlying.obj ⊥ ⟶ A
case refine'_1
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
s : ∏ Subtype.val ⟶ ∏ fun f => ↑f.fst := Pi.lift fun f => id (Pi.π Subtype.val) f.fst
⊢ Subobject.underlying.obj ⊥ ⟶ A
let t := Pi.lift (@Sigma.snd 𝒢 fun G => A ⟶ (G : C))
case refine'_1
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasProductsOfShape (↑𝒢) C
this✝¹ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this✝ : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
s : ∏ Subtype.val ⟶ ∏ fun f => ↑f.fst := Pi.lift fun f => id (Pi.π Subtype.val) f.fst
t : A ⟶ ∏ fun b => ↑b.fst := Pi.lift Sigma.snd
this : Mono t
⊢ Subobject.underlying.obj ⊥ ⟶ A
case refine'_1
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
s : ∏ Subtype.val ⟶ ∏ fun f => ↑f.fst := Pi.lift fun f => id (Pi.π Subtype.val) f.fst
t : A ⟶ ∏ fun b => ↑b.fst := Pi.lift Sigma.snd
⊢ Subobject.underlying.obj ⊥ ⟶ A
haveI : Mono t := (isCoseparating_iff_mono 𝒢).1 h𝒢 A
no goals
case refine'_1
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasProductsOfShape (↑𝒢) C
this✝¹ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this✝ : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
s : ∏ Subtype.val ⟶ ∏ fun f => ↑f.fst := Pi.lift fun f => id (Pi.π Subtype.val) f.fst
t : A ⟶ ∏ fun b => ↑b.fst := Pi.lift Sigma.snd
this : Mono t
⊢ Subobject.underlying.obj ⊥ ⟶ A
exact Subobject.ofLEMk _ (pullback.fst : pullback s t ⟶ _) bot_le ≫ pullback.snd
case refine'_2
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
⊢ ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g
case refine'_2
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
⊢ f = default
suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A ), f = g by
  apply this
case refine'_2
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
⊢ f = g
case refine'_2
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
⊢ ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g
intro g
case refine'_2
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
⊢ IsSplitEpi (equalizer.ι f g)
case refine'_2
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
⊢ f = g
suffices IsSplitEpi (equalizer.ι f g) by exact eq_of_epi_equalizer
no goals
case refine'_2
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
⊢ IsSplitEpi (equalizer.ι f g)
exact IsSplitEpi.mk' ⟨Subobject.ofLEMk _ (equalizer.ι f g ≫ Subobject.arrow _) bot_le, by
  ext
  simp⟩
no goals
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasProductsOfShape (↑𝒢) C
this✝¹ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this✝ : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
this : ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g
⊢ f = default
apply this
no goals
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasProductsOfShape (↑𝒢) C
this✝¹ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this✝ : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
this : IsSplitEpi (equalizer.ι f g)
⊢ f = g
exact eq_of_epi_equalizer
case h.h
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
b✝ : { x // x ∈ 𝒢 }
⊢ ((Subobject.ofLEMk ⊥ (equalizer.ι f g ≫ Subobject.arrow ⊥)
            (_ : ⊥ ≤ Subobject.mk (equalizer.ι f g ≫ Subobject.arrow ⊥)) ≫
          equalizer.ι f g) ≫
        Subobject.arrow ⊥) ≫
      Pi.π Subtype.val b✝ =
    (𝟙 (Subobject.underlying.obj ⊥) ≫ Subobject.arrow ⊥) ≫ Pi.π Subtype.val b✝
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
⊢ Subobject.ofLEMk ⊥ (equalizer.ι f g ≫ Subobject.arrow ⊥)
        (_ : ⊥ ≤ Subobject.mk (equalizer.ι f g ≫ Subobject.arrow ⊥)) ≫
      equalizer.ι f g =
    𝟙 (Subobject.underlying.obj ⊥)
ext
no goals
case h.h
C : Type u₁
inst✝⁴ : Category C
D : Type u₂
inst✝³ : Category D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
b✝ : { x // x ∈ 𝒢 }
⊢ ((Subobject.ofLEMk ⊥ (equalizer.ι f g ≫ Subobject.arrow ⊥)
            (_ : ⊥ ≤ Subobject.mk (equalizer.ι f g ≫ Subobject.arrow ⊥)) ≫
          equalizer.ι f g) ≫
        Subobject.arrow ⊥) ≫
      Pi.π Subtype.val b✝ =
    (𝟙 (Subobject.underlying.obj ⊥) ≫ Subobject.arrow ⊥) ≫ Pi.π Subtype.val b✝
simp