[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
⊢ HasInitial C
[PROOFSTEP]
let endos := T ⟶ T
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
⊢ HasInitial C
[PROOFSTEP]
let i := wideEqualizer.ι (id : endos → endos)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
⊢ HasInitial C
[PROOFSTEP]
haveI : Nonempty endos := ⟨𝟙 _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
⊢ HasInitial C
[PROOFSTEP]
have : ∀ X : C, Unique (wideEqualizer (id : endos → endos) ⟶ X) :=
  by
  intro X
  refine' ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => _⟩
  let E := equalizer a (i ≫ Classical.choice (hT _))
  let e : E ⟶ wideEqualizer id := equalizer.ι _ _
  let h : T ⟶ E := Classical.choice (hT E)
  have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
    rw [Category.assoc, Category.assoc]
    apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
  rw [Category.comp_id, cancel_mono_id i] at this 
  haveI : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
  rw [← cancel_epi e]
  apply equalizer.condition
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
⊢ (X : C) → Unique (wideEqualizer id ⟶ X)
[PROOFSTEP]
intro X
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
⊢ Unique (wideEqualizer id ⟶ X)
[PROOFSTEP]
refine' ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
⊢ a = default
[PROOFSTEP]
let E := equalizer a (i ≫ Classical.choice (hT _))
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
⊢ a = default
[PROOFSTEP]
let e : E ⟶ wideEqualizer id := equalizer.ι _ _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
⊢ a = default
[PROOFSTEP]
let h : T ⟶ E := Classical.choice (hT E)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
⊢ a = default
[PROOFSTEP]
have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
  rw [Category.assoc, Category.assoc]
  apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
⊢ ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
[PROOFSTEP]
rw [Category.assoc, Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
⊢ i ≫ h ≫ e ≫ i = i ≫ 𝟙 T
[PROOFSTEP]
apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
⊢ a = default
[PROOFSTEP]
rw [Category.comp_id, cancel_mono_id i] at this 
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
⊢ a = default
[PROOFSTEP]
haveI : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝¹ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this✝ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
this : IsSplitEpi e
⊢ a = default
[PROOFSTEP]
rw [← cancel_epi e]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝¹ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice (_ : Nonempty (T ⟶ X)))
h : T ⟶ E := Classical.choice (_ : Nonempty (T ⟶ E))
this✝ : (i ≫ h) ≫ e = 𝟙 (wideEqualizer id)
this : IsSplitEpi e
⊢ e ≫ a = e ≫ default
[PROOFSTEP]
apply equalizer.condition
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
this : (X : C) → Unique (wideEqualizer id ⟶ X)
⊢ HasInitial C
[PROOFSTEP]
exact hasInitial_of_unique (wideEqualizer (id : endos → endos))
