-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem hasInitial_of_isCoseparating [LocallySmall.{w} C] [WellPowered.{w} C]
    [HasLimitsOfSize.{w, w} C] {𝒢 : Set C} [Small.{w} 𝒢]
    (h𝒢 : IsCoseparating 𝒢) : HasInitial C

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝ : HasFiniteLimits C
this : HasProductsOfShape (↑𝒢) C
⊢ HasInitial C

Tactic:
haveI := fun A => hasProductsOfShape_of_small.{w} C (ΣG : 𝒢, A ⟶ (G : C))

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasFiniteLimits C
this✝ : HasProductsOfShape (↑𝒢) C
this : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
⊢ HasInitial C

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasFiniteLimits C
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
⊢ HasInitial C

Tactic:
suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C) ⟶ A) by
  exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C)

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasFiniteLimits C
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)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this : HasFiniteLimits C
⊢ HasInitial C

Tactic:
haveI : HasProductsOfShape 𝒢 C := hasProductsOfShape_of_small C 𝒢

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝ : HasFiniteLimits C
this : HasProductsOfShape (↑𝒢) C
⊢ HasInitial C

Proof state:
case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝³ : HasFiniteLimits C
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

Tactic:
exact Subobject.ofLEMk _ (pullback.fst _ _ : pullback s t ⟶ _) bot_le ≫ pullback.snd _ _

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝³ : HasFiniteLimits C
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

Tactic:
exact eq_of_epi_equalizer

Result:
no goals

Proof state:
case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasFiniteLimits C
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

Tactic:
haveI : Mono t := (isCoseparating_iff_mono 𝒢).1 h𝒢 A

Result:
case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝³ : HasFiniteLimits C
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

Proof state:
case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasFiniteLimits C
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

Tactic:
suffices IsSplitEpi (equalizer.ι f g) by exact eq_of_epi_equalizer

Result:
case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
𝒢 : Set C
inst✝ : Small.{w, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasFiniteLimits C
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)