awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
rw : f = (f ≫ hi.inv) ≫ hi.hom
rw₁ :
  ∀ (j : Discrete PEmpty.{w + 1}),
    (f ≫ hi.inv) ≫ c₁.π.app j =
      NatTrans.app
        (Cone.π
          { pt := c.pt,
            π :=
              { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
                NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) F₁ } })
        j
⊢ f =
    hl.lift
        { pt := c.pt,
          π :=
            { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
              NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) F₁ } } ≫
      hi.hom

Tactic:
rw [← hl.uniq _ (f ≫ hi.inv) _]

Premises used: CategoryTheory.Limits.IsLimit.uniq, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f = (f ≫ hi.inv) ≫ hi.hom

Tactic:
simp only [Category.assoc, Iso.inv_hom_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cone F₁
hl : IsLimit c₁
c₂ : Cone F₂
hi : c₁.pt ≅ c₂.pt
c : Cone F₂
f : c.pt ⟶ c₂.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    (f ≫ hi.inv) ≫ c₁.π.app j =
      NatTrans.app
        (Cone.π
          { pt := c.pt,
            π :=
              { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
                NatTrans (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) F₁ } })
        j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
x : IsLimit c₁
⊢ isLimitChangeEmptyCone C (isLimitChangeEmptyCone C x c₂ h) c₁ h.symm = x

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
x : IsLimit c₂
⊢ isLimitChangeEmptyCone C (isLimitChangeEmptyCone C x c₁ h.symm) c₂ h = x

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
⊢ ∀ ⦃X Y : Discrete PEmpty.{w + 1}⦄ (f : X ⟶ Y),
    Eq (α := F₁.obj X ⟶ Functor.obj.{w, v₁, w, u₁} (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) Y)
      (F₁.map f ≫
        id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w + 1}) ↦ F₁.obj x ⟶ c.pt) Y
            fun (as : PEmpty.{w + 1}) ↦ ⋯.elim))
      (id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w + 1}) ↦ F₁.obj x ⟶ c.pt) X
            fun (as : PEmpty.{w + 1}) ↦ ⋯.elim) ≫
        Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
dsimp :
  f =
    hi.inv ≫
      hl.desc
        { pt := c.pt,
          ι :=
            { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
              NatTrans F₁ (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) } }
⊢ f =
    hi.inv ≫
      hl.desc
        { pt := c.pt,
          ι :=
            {
              app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦
                id
                  (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w + 1}) ↦ F₁.obj x ⟶ c.pt) X_1
                    fun (as : PEmpty.{w + 1}) ↦ ⋯.elim),
              naturality := ⋯ : NatTrans F₁ (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) } }

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
rw : f = hi.inv ≫ hi.hom ≫ f
rw₁ :
  ∀ (j : Discrete PEmpty.{w + 1}),
    c₁.ι.app j ≫ hi.hom ≫ f =
      NatTrans.app
        (Cocone.ι
          { pt := c.pt,
            ι :=
              { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
                NatTrans F₁ (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) } })
        j
⊢ f =
    hi.inv ≫
      hl.desc
        { pt := c.pt,
          ι :=
            { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
              NatTrans F₁ (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) } }

Tactic:
rw [← hl.uniq _ (hi.hom ≫ f) _]

Premises used: CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f = hi.inv ≫ hi.hom ≫ f

Tactic:
simp only [Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
h : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    c₁.ι.app j ≫ hi.hom ≫ f =
      NatTrans.app
        (Cocone.ι
          { pt := c.pt,
            ι :=
              { app := fun (X_1 : Discrete PEmpty.{w + 1}) ↦ ⋯.elim, naturality := ⋯ :
                NatTrans F₁ (Functor.obj (Functor.const (Discrete PEmpty.{w + 1})) c.pt) } })
        j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
x : IsColimit c₁
⊢ isColimitChangeEmptyCocone C (isColimitChangeEmptyCocone C x c₂ h) c₁ h.symm = x

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
x : IsColimit c₂
⊢ isColimitChangeEmptyCocone C (isColimitChangeEmptyCocone C x c₁ h.symm) c₂ h = x

Tactic:
simp only [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : InitialMonoClass.{v₁, u₁} C
I X : C
hI : IsInitial.{v₁, u₁} I
f : I ⟶ X
rw : Mono (hI.to X)
⊢ Mono f

Tactic:
rw [hI.hom_ext f (hI.to X)]

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.IsInitial.to
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : InitialMonoClass.{v₁, u₁} C
I X : C
hI : IsInitial.{v₁, u₁} I
f : I ⟶ X
⊢ Mono (hI.to X)

Tactic:
apply InitialMonoClass.isInitial_mono_from

Premises used: CategoryTheory.Limits.InitialMonoClass.isInitial_mono_from
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : C
hI : IsInitial.{v₁, u₁} I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial.{v₁, u₁} I'
rw : Mono ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)
⊢ Mono (hI'.to X)

Tactic:
rw [hI'.hom_ext (hI'.to X) ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)]

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.IsInitial.uniqueUpToIso, CategoryTheory.Limits.IsInitial.to, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : C
hI : IsInitial.{v₁, u₁} I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial.{v₁, u₁} I'
⊢ Mono ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)

Tactic:
apply mono_comp

Premises used: CategoryTheory.mono_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I T : C
hI : IsInitial.{v₁, u₁} I
hT : IsTerminal.{v₁, u₁} T
h : Mono (hI.to T)
⊢ InitialMonoClass.{v₁, u₁} C

Tactic:
InitialMonoClass.of_isInitial hI fun X => mono_of_mono_fac (hI.hom_ext (_ ≫ hT.from X) (hI.to T))

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Limits.IsInitial.to, CategoryTheory.Limits.InitialMonoClass.of_isInitial, CategoryTheory.CategoryStruct.comp, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
dsimp : 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k
⊢ Functor.map (Functor.obj (Functor.const J) (F.obj X)) k ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
rw : 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j ≫ k)
rw₁ : F.map (tX.to j') = F.map (tX.to j ≫ k)
rw₂ rw₃ : F.map (tX.to j') = F.map (tX.to j')
⊢ 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k

Tactic:
rw [← F.map_comp, Category.id_comp, tX.hom_ext (tX.to j ≫ k) (tX.to j')]

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.IsInitial.to, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ (coneOfDiagramInitial tX F).π.app j = s.π.app j
simp_rw : m = m ≫ F.map (𝟙 X)
⊢ m = s.π.app X

Tactic:
simp_rw [← w X, coneOfDiagramInitial_π_app, tX.hom_ext (tX.to X) (𝟙 _)]

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.coneOfDiagramInitial_π_app, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.IsInitial.to
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ (coneOfDiagramInitial tX F).π.app j = s.π.app j
⊢ m = m ≫ F.map (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
hX : IsTerminal.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
inst_2 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
dsimp : 𝟙 (F.obj X) ≫ inv (F.map (hX.from j)) = inv (F.map (hX.from i)) ≫ F.map f
⊢ Functor.map (Functor.obj (Functor.const J) (F.obj X)) f ≫ inv (F.map (hX.from j)) = inv (F.map (hX.from i)) ≫ F.map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
hX : IsTerminal.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
inst_2 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ 𝟙 (F.obj X) ≫ inv (F.map (hX.from j)) = inv (F.map (hX.from i)) ≫ F.map f

Tactic:
simp only [IsIso.eq_inv_comp, IsIso.comp_inv_eq, Category.id_comp, ← F.map_comp,
          hX.hom_ext (hX.from i) (f ≫ hX.from j)]

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Functor.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsTerminal.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
dsimp : F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
⊢ F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ Functor.map (Functor.obj (Functor.const J) (F.obj X)) k

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsTerminal.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
j j' : J
k : j ⟶ j'
rw : F.map (k ≫ tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
rw₁ : F.map (k ≫ tX.from j') = F.map (tX.from j)
rw₂ rw₃ : F.map (tX.from j) = F.map (tX.from j)
⊢ F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)

Tactic:
rw [← F.map_comp, Category.comp_id, tX.hom_ext (k ≫ tX.from j') (tX.from j)]

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Category.comp_id, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
tX : IsTerminal.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
s : Cocone F
m : (coconeOfDiagramTerminal tX F).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfDiagramTerminal tX F).ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app X

Tactic:
simp [← w X]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
c : Cocone F
hc : IsColimit c
X : J
hX : IsTerminal.{v, u} X
change : IsIso ((colimitOfDiagramTerminal hX F).coconePointUniqueUpToIso hc).hom
⊢ IsIso (c.ι.app X)

Tactic:
change IsIso (coconePointUniqueUpToIso (colimitOfDiagramTerminal hX F) hc).hom

Premises used: CategoryTheory.IsIso, CategoryTheory.Limits.colimitOfDiagramTerminal, CategoryTheory.Iso.hom, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
c : Cocone F
hc : IsColimit c
X : J
hX : IsTerminal.{v, u} X
⊢ IsIso ((colimitOfDiagramTerminal hX F).coconePointUniqueUpToIso hc).hom

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
hX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
inst_2 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
dsimp : F.map f ≫ inv (F.map (hX.to j)) = inv (F.map (hX.to i)) ≫ 𝟙 (F.obj X)
⊢ F.map f ≫ inv (F.map (hX.to j)) = inv (F.map (hX.to i)) ≫ Functor.map (Functor.obj (Functor.const J) (F.obj X)) f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
X : J
hX : IsInitial.{v, u} X
F : Functor.{v, v₁, u, u₁} J C
inst_2 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
i j : J
f : i ⟶ j
⊢ F.map f ≫ inv (F.map (hX.to j)) = inv (F.map (hX.to i)) ≫ 𝟙 (F.obj X)

Tactic:
simp only [IsIso.eq_inv_comp, IsIso.comp_inv_eq, Category.comp_id, ← F.map_comp,
          hX.hom_ext (hX.to i ≫ f) (hX.to j)]

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.Category.comp_id, CategoryTheory.Limits.IsInitial.to, CategoryTheory.IsIso.comp_inv_eq, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
c : Cone F
hc : IsLimit c
X : J
hX : IsInitial.{v, u} X
change : IsIso (hc.conePointUniqueUpToIso (limitOfDiagramInitial hX F)).hom
⊢ IsIso (c.π.app X)

Tactic:
change IsIso (conePointUniqueUpToIso hc (limitOfDiagramInitial hX F)).hom

Premises used: CategoryTheory.IsIso, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.limitOfDiagramInitial, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
c : Cone F
hc : IsLimit c
X : J
hX : IsInitial.{v, u} X
⊢ IsIso (hc.conePointUniqueUpToIso (limitOfDiagramInitial hX F)).hom

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal.{v₁, u₁} X
hY : IsTerminal.{v₁, u₁} Y
f : X ⟶ Y
⊢ IsIso f

Tactic:
⟨⟨IsTerminal.from hX Y, ?_⟩⟩

Premises used: CategoryTheory.Limits.IsTerminal.from, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal.{v₁, u₁} X
hY : IsTerminal.{v₁, u₁} Y
f : X ⟶ Y
refine : f ≫ hX.from Y = 𝟙 X ∧ hX.from Y ≫ f = 𝟙 Y
⊢ IsIso f

Tactic:
refine ⟨⟨IsTerminal.from hX Y, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal.{v₁, u₁} X
hY : IsTerminal.{v₁, u₁} Y
f : X ⟶ Y
simp : hX.from Y ≫ f = 𝟙 Y
⊢ f ≫ hX.from Y = 𝟙 X ∧ hX.from Y ≫ f = 𝟙 Y

Tactic:
simp only [IsTerminal.comp_from, IsTerminal.from_self, true_and]

Premises used: CategoryTheory.Limits.IsTerminal.comp_from, CategoryTheory.Limits.IsTerminal.from_self, true_and
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal.{v₁, u₁} X
hY : IsTerminal.{v₁, u₁} Y
f : X ⟶ Y
⊢ hX.from Y ≫ f = 𝟙 Y

Tactic:
apply IsTerminal.hom_ext hY

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsInitial.{v₁, u₁} X
hY : IsInitial.{v₁, u₁} Y
f : X ⟶ Y
⊢ IsIso f

Tactic:
⟨⟨IsInitial.to hY X, ?_⟩⟩

Premises used: CategoryTheory.Limits.IsInitial.to, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsInitial.{v₁, u₁} X
hY : IsInitial.{v₁, u₁} Y
f : X ⟶ Y
refine : f ≫ hY.to X = 𝟙 X ∧ hY.to X ≫ f = 𝟙 Y
⊢ IsIso f

Tactic:
refine ⟨⟨IsInitial.to hY X, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsInitial.{v₁, u₁} X
hY : IsInitial.{v₁, u₁} Y
f : X ⟶ Y
simp : f ≫ hY.to X = 𝟙 X
⊢ f ≫ hY.to X = 𝟙 X ∧ hY.to X ≫ f = 𝟙 Y

Tactic:
simp only [IsInitial.to_comp, IsInitial.to_self, and_true]

Premises used: and_true, CategoryTheory.Limits.IsInitial.to_self, CategoryTheory.Limits.IsInitial.to_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
hX : IsInitial.{v₁, u₁} X
hY : IsInitial.{v₁, u₁} Y
f : X ⟶ Y
⊢ f ≫ hY.to X = 𝟙 X

Tactic:
apply IsInitial.hom_ext hX

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X : D
hX : IsTerminal.{v_2, u_2} X
X_1 : Functor.{v_1, v_2, u_1, u_2} C D
m : X_1 ⟶ obj (const C) X
w :
  ∀ (x : C),
    m.app x =
      NatTrans.app
        ((fun (Y : Functor.{v_1, v_2, u_1, u_2} C D) ↦
            ({ app := fun (Z : C) ↦ hX.from (Y.obj Z), naturality := ⋯ } : NatTrans Y (obj (const C) X)))
          X_1)
        x
⊢ m =
    (fun (Y : Functor.{v_1, v_2, u_1, u_2} C D) ↦
        ({ app := fun (Z : C) ↦ hX.from (Y.obj Z), naturality := ⋯ } : NatTrans Y (obj (const C) X)))
      X_1

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X : D
hX : IsTerminal.{v_2, u_2} X
X_1 : Functor.{v_1, v_2, u_1, u_2} C D
m : X_1 ⟶ obj (const C) X
x : C
⊢ m.app x =
    NatTrans.app
      ((fun (Y : Functor.{v_1, v_2, u_1, u_2} C D) ↦
          ({ app := fun (Z : C) ↦ hX.from (Y.obj Z), naturality := ⋯ } : NatTrans Y (obj (const C) X)))
        X_1)
      x

Tactic:
apply hX.hom_ext

Premises used: CategoryTheory.Limits.IsTerminal.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X : D
hX : IsTerminal.{v_2, u_2} X
F : Functor.{v_1, v_2, u_1, u_2} C D
Y : C
⊢ (IsTerminal.from (isTerminalConst C hX) F).app Y = hX.from (F.obj Y)

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsTerminal.from, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X : D
hX : IsInitial.{v_2, u_2} X
Y : Functor.{v_1, v_2, u_1, u_2} C D
m : obj (const C) X ⟶ Y
w :
  ∀ (x : C),
    m.app x =
      NatTrans.app
        ((fun (Y : Functor.{v_1, v_2, u_1, u_2} C D) ↦
            { app := fun (Z : C) ↦ hX.to (Y.obj Z), naturality := ⋯ : NatTrans (obj (const C) X) Y })
          Y)
        x
⊢ m =
    (fun (Y : Functor.{v_1, v_2, u_1, u_2} C D) ↦
        { app := fun (Z : C) ↦ hX.to (Y.obj Z), naturality := ⋯ : NatTrans (obj (const C) X) Y })
      Y

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X : D
hX : IsInitial.{v_2, u_2} X
Y : Functor.{v_1, v_2, u_1, u_2} C D
m : obj (const C) X ⟶ Y
x : C
⊢ m.app x =
    NatTrans.app
      ((fun (Y : Functor.{v_1, v_2, u_1, u_2} C D) ↦
          { app := fun (Z : C) ↦ hX.to (Y.obj Z), naturality := ⋯ : NatTrans (obj (const C) X) Y })
        Y)
      x

Tactic:
apply hX.hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
X : D
hX : IsInitial.{v_2, u_2} X
F : Functor.{v_1, v_2, u_1, u_2} C D
Y : C
⊢ (IsInitial.to (isInitialConst C hX) F).app Y = hX.to (F.obj Y)

Tactic:
rfl

Premises used: CategoryTheory.Limits.IsInitial.to, rfl