[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A T : C
hT : IsTerminal T
inst✝ : Mono (IsTerminal.from hT A)
Z : C
f g : Z ⟶ A
⊢ f = g
[PROOFSTEP]
rw [← cancel_mono (hT.from A)]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A T : C
hT : IsTerminal T
inst✝ : Mono (IsTerminal.from hT A)
Z : C
f g : Z ⟶ A
⊢ f ≫ IsTerminal.from hT A = g ≫ IsTerminal.from hT A
[PROOFSTEP]
apply hT.hom_ext
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f = g
[PROOFSTEP]
rw [← cancel_mono (terminal.from A)]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasTerminal C
inst✝ : Mono (terminal.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ terminal.from A = g ≫ terminal.from A
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ diag A ≫ prod.fst = 𝟙 A
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ prod.fst ≫ diag A = 𝟙 (A ⨯ A)
[PROOFSTEP]
rw [IsSubterminal.def] at hA 
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g
inst✝ : HasBinaryProduct A A
⊢ prod.fst ≫ diag A = 𝟙 (A ⨯ A)
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
⊢ f = g
[PROOFSTEP]
have : (Limits.prod.fst : A ⨯ A ⟶ _) = Limits.prod.snd := by simp [← cancel_epi (diag A)]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
⊢ prod.fst = prod.snd
[PROOFSTEP]
simp [← cancel_epi (diag A)]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : C
inst✝¹ : HasBinaryProduct A A
inst✝ : IsIso (diag A)
Z : C
f g : Z ⟶ A
this : prod.fst = prod.snd
⊢ f = g
[PROOFSTEP]
rw [← prod.lift_fst f g, this, prod.lift_snd]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
⊢ A ⨯ A ≅ A
[PROOFSTEP]
letI := IsSubterminal.isIso_diag hA
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
hA : IsSubterminal A
inst✝ : HasBinaryProduct A A
this : IsIso (diag A) := isIso_diag hA
⊢ A ⨯ A ≅ A
[PROOFSTEP]
apply (asIso (diag A)).symm
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
inst✝ : HasTerminal C
X✝ Y✝ : Subterminals C
f : X✝ ⟶ Y✝
⊢ f ≫
      MonoOver.arrow
        ((fun X => { obj := Over.mk (terminal.from X.obj), property := (_ : Mono (terminal.from X.obj)) }) Y✝) =
    MonoOver.arrow
      ((fun X => { obj := Over.mk (terminal.from X.obj), property := (_ : Mono (terminal.from X.obj)) }) X✝)
[PROOFSTEP]
ext1 ⟨⟨⟩⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
inst✝ : HasTerminal C
X : MonoOver (⊤_ C)
Z : C
f g : Z ⟶ X.obj.left
⊢ f = g
[PROOFSTEP]
rw [← cancel_mono X.arrow]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : C
inst✝ : HasTerminal C
X : MonoOver (⊤_ C)
Z : C
f g : Z ⟶ X.obj.left
⊢ f ≫ MonoOver.arrow X = g ≫ MonoOver.arrow X
[PROOFSTEP]
apply Subsingleton.elim
