-- 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:
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
⊢ f = default

Tactic:
suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by
  apply this

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), f = g

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
⊢ HasInitial C

Tactic:
letI := completeLatticeOfCompleteSemilatticeInf (Subobject (piObj (Subtype.val : 𝒢 → 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))
⊢ 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))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
this : ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g
⊢ f = default

Tactic:
apply this

Result:
no goals

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:
intro g

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
⊢ f = g

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))
this : (A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)
⊢ HasInitial C

Tactic:
exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C)

Result:
no goals