-- 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
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
⊢ ⊥.ofLEMk (equalizer.ι f g ≫ ⊥.arrow) ⋯ ≫ equalizer.ι f g = 𝟙 (Subobject.underlying.obj ⊥)

Tactic:
ext

Result:
case h.h
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
b✝ : { x // x ∈ 𝒢 }
⊢ ((⊥.ofLEMk (equalizer.ι f g ≫ ⊥.arrow) ⋯ ≫ equalizer.ι f g) ≫ ⊥.arrow) ≫ Pi.π Subtype.val b✝ =
    (𝟙 (Subobject.underlying.obj ⊥) ≫ ⊥.arrow) ≫ Pi.π Subtype.val b✝

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) → Unique (Subobject.underlying.obj ⊥ ⟶ A)

Tactic:
refine fun A => ⟨⟨?_⟩, fun f => ?_⟩

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
⊢ Subobject.underlying.obj ⊥ ⟶ A

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

Proof state:
case h.h
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
b✝ : { x // x ∈ 𝒢 }
⊢ ((⊥.ofLEMk (equalizer.ι f g ≫ ⊥.arrow) ⋯ ≫ equalizer.ι f g) ≫ ⊥.arrow) ≫ Pi.π Subtype.val b✝ =
    (𝟙 (Subobject.underlying.obj ⊥) ≫ ⊥.arrow) ≫ Pi.π Subtype.val b✝

Tactic:
simp

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

Tactic:
have := hasFiniteLimits_of_hasLimitsOfSize 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
⊢ 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
g : Subobject.underlying.obj ⊥ ⟶ A
⊢ IsSplitEpi (equalizer.ι f g)

Tactic:
exact IsSplitEpi.mk' ⟨Subobject.ofLEMk _ (equalizer.ι f g ≫ Subobject.arrow _) bot_le, by
  ext
  simp⟩

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
⊢ Subobject.underlying.obj ⊥ ⟶ A

Tactic:
let s := Pi.lift fun f : ΣG : 𝒢, A ⟶ (G : C) => id (Pi.π (Subtype.val : 𝒢 → C)) f.1

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
⊢ Subobject.underlying.obj ⊥ ⟶ A

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
⊢ Subobject.underlying.obj ⊥ ⟶ A

Tactic:
let t := Pi.lift (@Sigma.snd 𝒢 fun G => A ⟶ (G : C))

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
⊢ Subobject.underlying.obj ⊥ ⟶ A