awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi g
⊢ StrongEpi f

Tactic:
StrongEpi.of_arrow_iso e.symm

Premises used: CategoryTheory.StrongEpi.of_arrow_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongEpi f
⊢ StrongEpi g

Tactic:
exacts [StrongEpi.of_arrow_iso e, StrongEpi.of_arrow_iso e.symm]

Premises used: CategoryTheory.StrongEpi.of_arrow_iso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
mp : StrongMono f → StrongMono g
mpr : StrongMono g → StrongMono f
⊢ StrongMono f ↔ StrongMono g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ StrongMono g

Tactic:
StrongMono.of_arrow_iso e

Premises used: CategoryTheory.StrongMono.of_arrow_iso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono g
⊢ StrongMono f

Tactic:
StrongMono.of_arrow_iso e.symm

Premises used: CategoryTheory.StrongMono.of_arrow_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
A B A' B' : C
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
h : StrongMono f
⊢ StrongMono g

Tactic:
exacts [StrongMono.of_arrow_iso e, StrongMono.of_arrow_iso e.symm]

Premises used: CategoryTheory.StrongMono.of_arrow_iso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst_1 : Mono f
inst_2 : StrongEpi f
⊢ 𝟙 P ≫ f = f ≫ 𝟙 Q

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst_1 : Mono f
inst_2 : StrongEpi f
⊢ f ≫ CommSq.lift (A := P) (Y := Q) (f := 𝟙 P) (i := f) (p := f) (g := 𝟙 Q) ⋯ = 𝟙 P ∧
    CommSq.lift (A := P) (Y := Q) (f := 𝟙 P) (i := f) (p := f) (g := 𝟙 Q) ⋯ ≫ f = 𝟙 Q

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst_1 : Epi f
inst_2 : StrongMono f
⊢ 𝟙 P ≫ f = f ≫ 𝟙 Q

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
f : P ⟶ Q
inst_1 : Epi f
inst_2 : StrongMono f
⊢ f ≫ CommSq.lift (A := P) (Y := Q) (f := 𝟙 P) (i := f) (p := f) (g := 𝟙 Q) ⋯ = 𝟙 P ∧
    CommSq.lift (A := P) (Y := Q) (f := 𝟙 P) (i := f) (p := f) (g := 𝟙 Q) ⋯ ≫ f = 𝟙 Q

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
inst_1 : StrongEpiCategory.{v, u} C
f : P ⟶ Q
inst_2 : Epi f
⊢ StrongEpi f

Tactic:
StrongEpiCategory.strongEpi_of_epi _

Premises used: CategoryTheory.StrongEpiCategory.strongEpi_of_epi
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
Goal:
C : Type u
inst : Category.{v, u} C
P Q : C
inst_1 : StrongMonoCategory.{v, u} C
f : P ⟶ Q
inst_2 : Mono f
⊢ StrongMono f

Tactic:
StrongMonoCategory.strongMono_of_mono _

Premises used: CategoryTheory.StrongMonoCategory.strongMono_of_mono
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
h : HasLimit F₁
⊢ ∀ ⦃X Y : Discrete PEmpty.{w' + 1}⦄ (f : X ⟶ Y),
    Eq.{v₁ + 1} (α :=
      Functor.obj.{w', v₁, w', u₁} (Functor.obj (Functor.const (Discrete PEmpty.{w' + 1})) (limit F₁)) X ⟶ F₂.obj Y)
      (Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{w' + 1})) (limit F₁)) f ≫
        id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w' + 1}) ↦ limit F₁ ⟶ F₂.obj x) Y
            fun (as : PEmpty.{w' + 1}) ↦ ⋯.elim))
      (id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w' + 1}) ↦ limit F₁ ⟶ F₂.obj x) X
            fun (as : PEmpty.{w' + 1}) ↦ ⋯.elim) ≫
        F₂.map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F₁ : Functor.{w, v₁, w, u₁} (Discrete PEmpty.{w + 1}) C
F₂ : Functor.{w', v₁, w', u₁} (Discrete PEmpty.{w' + 1}) C
h : HasColimit 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})) (colimit F₁)) Y)
      (F₂.map f ≫
        id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w' + 1}) ↦ F₂.obj x ⟶ colimit F₁) Y
            fun (as : PEmpty.{w' + 1}) ↦ ⋯.elim))
      (id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{w' + 1}) ↦ F₂.obj x ⟶ colimit F₁) X
            fun (as : PEmpty.{w' + 1}) ↦ ⋯.elim) ≫
        Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{w' + 1})) (colimit F₁)) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
h : IsTerminal.{v₁, u₁} X
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    Eq.{v₁ + 1} (α := Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) X_1 ⟶ F.obj Y)
      (Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) f ≫
        id (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ X ⟶ F.obj x) Y fun (as : PEmpty.{1}) ↦ ⋯.elim))
      (id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ X ⟶ F.obj x) X_1 fun (as : PEmpty.{1}) ↦
            ⋯.elim) ≫
        F.map f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
h : IsInitial.{v₁, u₁} X
F : Functor.{0, v₁, 0, u₁} (Discrete PEmpty.{1}) C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    Eq (α := F.obj X_1 ⟶ Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) Y)
      (F.map f ≫
        id (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) Y fun (as : PEmpty.{1}) ↦ ⋯.elim))
      (id
          (Discrete.casesOn (motive := fun (x : Discrete PEmpty.{1}) ↦ F.obj x ⟶ X) X_1 fun (as : PEmpty.{1}) ↦
            ⋯.elim) ≫
        Functor.map (Functor.obj (Functor.const (Discrete PEmpty.{1})) X) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasTerminal.{v₁, u₁} C
P : C
f g : P ⟶ terminal.{v₁, u₁} C
⊢ f = g

Tactic:
ext ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasInitial.{v₁, u₁} C
P : C
f g : initial.{v₁, u₁} C ⟶ P
⊢ f = g

Tactic:
ext ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasTerminal.{v₁, u₁} C
P Q : C
f : P ⟶ Q
⊢ Eq (α := P ⟶ terminal.{v₁, u₁} C) (f ≫ «from» Q) («from» P)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasInitial.{v₁, u₁} C
P Q : C
f : P ⟶ Q
⊢ Eq (α := initial.{v₁, u₁} C ⟶ Q) («to» P ≫ f) («to» Q)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y : C
inst_1 : HasTerminal.{v₁, u₁} C
f : terminal.{v₁, u₁} C ⟶ Y
⊢ IsSplitMono f

Tactic:
IsTerminal.isSplitMono_from terminalIsTerminal _

Premises used: CategoryTheory.Limits.terminalIsTerminal, CategoryTheory.Limits.IsTerminal.isSplitMono_from
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
Y : C
inst_1 : HasInitial.{v₁, u₁} C
f : Y ⟶ initial.{v₁, u₁} C
⊢ IsSplitEpi f

Tactic:
IsInitial.isSplitEpi_to initialIsInitial _

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.IsInitial.isSplitEpi_to
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasTerminal.{v₁, u₁} C
⊢ HasInitial.{v₁, u₁} Cᵒᵖ

Tactic:
(initialOpOfTerminal terminalIsTerminal).hasInitial

Premises used: CategoryTheory.Limits.IsInitial.hasInitial, CategoryTheory.Limits.initialOpOfTerminal, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasInitial.{v₁, u₁} C
⊢ HasTerminal.{v₁, u₁} Cᵒᵖ

Tactic:
(terminalOpOfInitial initialIsInitial).hasTerminal

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.IsTerminal.hasTerminal, CategoryTheory.Limits.terminalOpOfInitial
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasInitial.{v₁, u₁} Cᵒᵖ
⊢ HasTerminal.{v₁, u₁} C

Tactic:
(terminalUnopOfInitial initialIsInitial).hasTerminal

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.IsTerminal.hasTerminal, CategoryTheory.Limits.terminalUnopOfInitial
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasTerminal.{v₁, u₁} Cᵒᵖ
⊢ HasInitial.{v₁, u₁} C

Tactic:
(initialUnopOfTerminal terminalIsTerminal).hasInitial

Premises used: CategoryTheory.Limits.IsInitial.hasInitial, CategoryTheory.Limits.initialUnopOfTerminal, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J : Type u_1
inst_1 : Category.{v_1, u_1} J
C : Type u_2
inst_2 : Category.{v_2, u_2} C
inst_3 : HasTerminal.{v_2, u_2} C
⊢ HasLimit.{v_1, u_1, v_2, u_2} (Functor.obj (Functor.const J) (terminal.{v_2, u_2} C))

Tactic:
HasLimit.mk
    { cone :=
        { pt := ⊤_ C
          π := { app := fun _ => terminal.from _ } }
      isLimit := { lift := fun _ => terminal.from _ } }

Premises used: CategoryTheory.Limits.IsLimit.mk, CategoryTheory.Limits.terminal.from, CategoryTheory.Limits.Cone.pt, CategoryTheory.NatTrans.mk, CategoryTheory.Limits.terminal, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Functor.const, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.Cone.mk, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
J : Type u_1
inst_1 : Category.{v_1, u_1} J
C : Type u_2
inst_2 : Category.{v_2, u_2} C
inst_3 : HasInitial.{v_2, u_2} C
⊢ HasColimit.{v_1, u_1, v_2, u_2} (Functor.obj (Functor.const J) (initial.{v_2, u_2} C))

Tactic:
HasColimit.mk
    { cocone :=
        { pt := ⊥_ C
          ι := { app := fun _ => initial.to _ } }
      isColimit := { desc := fun _ => initial.to _ } }

Premises used: CategoryTheory.Limits.IsColimit.mk, CategoryTheory.Limits.Cocone.mk, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.initial.to, CategoryTheory.NatTrans.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Functor.const, CategoryTheory.Limits.initial, CategoryTheory.Functor.obj, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasInitial.{v₁, u₁} C
inst_2 : InitialMonoClass.{v₁, u₁} C
X : C
f : initial.{v₁, u₁} C ⟶ X
⊢ Mono f

Tactic:
initialIsInitial.mono_from f

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.IsInitial.mono_from
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasInitial.{v₁, u₁} C
h : ∀ (X : C), Mono.{v₁, u₁} (X := initial.{v₁, u₁} C) (initial.to X)
⊢ InitialMonoClass.{v₁, u₁} C

Tactic:
InitialMonoClass.of_isInitial initialIsInitial h

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.InitialMonoClass.of_isInitial
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasInitial.{v₁, u₁} C
inst_2 : HasTerminal.{v₁, u₁} C
h : Mono.{v₁, u₁} (X := initial.{v₁, u₁} C) (initial.to (terminal.{v₁, u₁} C))
⊢ InitialMonoClass.{v₁, u₁} C

Tactic:
InitialMonoClass.of_isTerminal initialIsInitial terminalIsTerminal h

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.InitialMonoClass.of_isTerminal, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
inst_2 : HasInitial.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
⊢ HasLimit F

Tactic:
HasLimit.mk { cone := _, isLimit := limitOfDiagramInitial (initialIsInitial) F }

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.coneOfDiagramInitial, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.limitOfDiagramInitial, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
inst_2 : HasTerminal.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ HasLimit F

Tactic:
HasLimit.mk { cone := _, isLimit := limitOfDiagramTerminal (terminalIsTerminal) F }

Premises used: CategoryTheory.Limits.coneOfDiagramTerminal, CategoryTheory.Limits.limitOfDiagramTerminal, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
inst_2 : HasTerminal.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
⊢ HasColimit F

Tactic:
HasColimit.mk { cocone := _, isColimit := colimitOfDiagramTerminal (terminalIsTerminal) F }

Premises used: CategoryTheory.Limits.coconeOfDiagramTerminal, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.colimitOfDiagramTerminal, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
inst_2 : HasInitial.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ HasColimit F

Tactic:
HasColimit.mk { cocone := _, isColimit := colimitOfDiagramInitial (initialIsInitial) F }

Premises used: CategoryTheory.Limits.colimitOfDiagramInitial, CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.coconeOfDiagramInitial
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasLimit F
w :
  ∀ (j_1 : J),
    CategoryStruct.comp (Y := limit F) (limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F)) (limit.π F j_1) =
      𝟙 (limit F) ≫ limit.π F j_1
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F) = 𝟙 (limit F)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasLimit F
j_1 : J
⊢ CategoryStruct.comp (Y := limit F) (limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F)) (limit.π F j_1) =
    𝟙 (limit F) ≫ limit.π F j_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasLimit F
⊢ Eq (α := F.obj j ⟶ F.obj j)
    (CategoryStruct.comp (Y := limit F) (limit.lift F (coneOfDiagramInitial I F)) (limit.π F j) : F.obj j ⟶ F.obj j)
    (𝟙 (F.obj j) : F.obj j ⟶ F.obj j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
inst_2 : HasInitial.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
⊢ IsIso (X := limit F) (Y := F.obj (initial.{v, u} J)) (limit.π F (initial.{v, u} J))

Tactic:
isIso_π_of_isInitial initialIsInitial F

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.isIso_π_of_isInitial
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsTerminal.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasLimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
w :
  ∀ (j_1 : J),
    CategoryStruct.comp (Y := limit F) (limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F)) (limit.π F j_1) =
      𝟙 (limit F) ≫ limit.π F j_1
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F) = 𝟙 (limit F)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsTerminal.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasLimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j_1 : J
⊢ CategoryStruct.comp (Y := limit F) (limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F)) (limit.π F j_1) =
    𝟙 (limit F) ≫ limit.π F j_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsTerminal.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasLimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ Eq (α := F.obj j ⟶ F.obj j)
    (CategoryStruct.comp (Y := limit F) (limit.lift F (coneOfDiagramTerminal I F)) (limit.π F j) : F.obj j ⟶ F.obj j)
    (𝟙 (F.obj j) : F.obj j ⟶ F.obj j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
inst_2 : HasTerminal.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ IsIso (X := limit F) (Y := F.obj (terminal.{v, u} J)) (limit.π F (terminal.{v, u} J))

Tactic:
isIso_π_of_isTerminal terminalIsTerminal F

Premises used: CategoryTheory.Limits.isIso_π_of_isTerminal, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsTerminal.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
⊢ Eq (α := F.obj j ⟶ F.obj j)
    (CategoryStruct.comp (Y := colimit F) (colimit.ι F j) (colimit.desc F (coconeOfDiagramTerminal I F)) :
      F.obj j ⟶ F.obj j)
    (𝟙 (F.obj j) : F.obj j ⟶ F.obj j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsTerminal.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
w :
  ∀ (j_1 : J),
    CategoryStruct.comp (Y := colimit F) (colimit.ι F j_1)
        (CategoryStruct.comp (Y := F.obj j)
          (colimit.desc F (coconeOfDiagramTerminal I F) : colimit F ⟶ (coconeOfDiagramTerminal I F).pt)
          (colimit.ι F j)) =
      colimit.ι F j_1 ≫ 𝟙 (colimit F)
⊢ CategoryStruct.comp (Y := F.obj j)
      (colimit.desc F (coconeOfDiagramTerminal I F) : colimit F ⟶ (coconeOfDiagramTerminal I F).pt) (colimit.ι F j) =
    𝟙 (colimit F)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsTerminal.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
j_1 : J
⊢ CategoryStruct.comp (Y := colimit F) (colimit.ι F j_1)
      (CategoryStruct.comp (Y := F.obj j)
        (colimit.desc F (coconeOfDiagramTerminal I F) : colimit F ⟶ (coconeOfDiagramTerminal I F).pt) (colimit.ι F j)) =
    colimit.ι F j_1 ≫ 𝟙 (colimit F)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
inst_2 : HasTerminal.{v, u} J
F : Functor.{v, v₁, u, u₁} J C
⊢ IsIso (X := F.obj (terminal.{v, u} J)) (Y := colimit F) (colimit.ι F (terminal.{v, u} J))

Tactic:
isIso_ι_of_isTerminal terminalIsTerminal F

Premises used: CategoryTheory.Limits.terminalIsTerminal, CategoryTheory.Limits.isIso_ι_of_isTerminal
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
w :
  ∀ (j_1 : J),
    CategoryStruct.comp (Y := colimit F) (colimit.ι F j_1)
        (CategoryStruct.comp (Y := F.obj j)
          (colimit.desc F (coconeOfDiagramInitial I F) : colimit F ⟶ (coconeOfDiagramInitial I F).pt) (colimit.ι F j)) =
      colimit.ι F j_1 ≫ 𝟙 (colimit F)
⊢ CategoryStruct.comp (Y := F.obj j)
      (colimit.desc F (coconeOfDiagramInitial I F) : colimit F ⟶ (coconeOfDiagramInitial I F).pt) (colimit.ι F j) =
    𝟙 (colimit F)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j_1 : J
⊢ CategoryStruct.comp (Y := colimit F) (colimit.ι F j_1)
      (CategoryStruct.comp (Y := F.obj j)
        (colimit.desc F (coconeOfDiagramInitial I F) : colimit F ⟶ (coconeOfDiagramInitial I F).pt) (colimit.ι F j)) =
    colimit.ι F j_1 ≫ 𝟙 (colimit F)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
refine :
  Eq (α := F.obj j ⟶ F.obj j)
    (CategoryStruct.comp (Y := colimit F) (colimit.ι F j) (colimit.desc F (coconeOfDiagramInitial I F)) :
      F.obj j ⟶ F.obj j)
    (𝟙 (F.obj j) : F.obj j ⟶ F.obj j)
⊢ Eq (α := F.obj j ⟶ F.obj j)
      (CategoryStruct.comp (Y := colimit F) (colimit.ι F j) (colimit.desc F (coconeOfDiagramInitial I F)) :
        F.obj j ⟶ F.obj j)
      (𝟙 (F.obj j) : F.obj j ⟶ F.obj j) ∧
    CategoryStruct.comp (Y := F.obj j)
        (colimit.desc F (coconeOfDiagramInitial I F) : colimit F ⟶ (coconeOfDiagramInitial I F).pt) (colimit.ι F j) =
      𝟙 (colimit F)

Tactic:
refine ⟨?_, by ext; simp⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
simp : inv (F.map (𝟙 j)) = 𝟙 (F.obj j)
⊢ Eq (α := F.obj j ⟶ F.obj j)
    (CategoryStruct.comp (Y := colimit F) (colimit.ι F j) (colimit.desc F (coconeOfDiagramInitial I F)) :
      F.obj j ⟶ F.obj j)
    (𝟙 (F.obj j) : F.obj j ⟶ F.obj j)

Tactic:
simp only [colimit.ι_desc, coconeOfDiagramInitial_pt, coconeOfDiagramInitial_ι_app,
      Functor.const_obj_obj, IsInitial.to_self]

Premises used: CategoryTheory.Limits.IsInitial.to_self, CategoryTheory.Limits.coconeOfDiagramInitial_ι_app, CategoryTheory.Limits.colimit.ι_desc, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Limits.coconeOfDiagramInitial_pt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u
inst_1 : Category.{v, u} J
j : J
I : IsInitial.{v, u} j
F : Functor.{v, v₁, u, u₁} J C
inst_2 : HasColimit F
inst_3 : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ inv (F.map (𝟙 j)) = 𝟙 (F.obj j)

Tactic:
grind