awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (q.rightSection ≫ π) = 𝟙 (F.obj Z)
rw₁ : F.map (𝟙 Z) = 𝟙 (F.obj Z)
rw₂ rw₃ : Eq.{v₂ + 1} (α := F.obj Z ⟶ F.obj Z) (𝟙 (F.obj Z)) (𝟙 (F.obj Z))
⊢ F.map q.rightSection ≫ F.map π = 𝟙 (F.obj Z)

Tactic:
rw [← F.map_comp, q.rightSection_π, F.map_id]

Premises used: CategoryTheory.IsSplitCoequalizer.rightSection_π, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (q.leftSection ≫ g) = 𝟙 (F.obj Y)
rw₁ : F.map (𝟙 Y) = 𝟙 (F.obj Y)
rw₂ rw₃ : Eq.{v₂ + 1} (α := F.obj Y ⟶ F.obj Y) (𝟙 (F.obj Y)) (𝟙 (F.obj Y))
⊢ F.map q.leftSection ≫ F.map g = 𝟙 (F.obj Y)

Tactic:
rw [← F.map_comp, q.leftSection_bottom, F.map_id]

Premises used: CategoryTheory.IsSplitCoequalizer.leftSection_bottom, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
π : Y ⟶ Z
q : IsSplitCoequalizer f g π
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (q.leftSection ≫ f) = F.map π ≫ F.map q.rightSection
rw₁ : F.map (π ≫ q.rightSection) = F.map π ≫ F.map q.rightSection
rw₂ rw₃ : F.map π ≫ F.map q.rightSection = F.map π ≫ F.map q.rightSection
⊢ F.map q.leftSection ≫ F.map f = F.map π ≫ F.map q.rightSection

Tactic:
rw [← F.map_comp, q.leftSection_top, F.map_comp]

Premises used: CategoryTheory.IsSplitCoequalizer.leftSection_top, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
⊢ t.asCofork.π = h

Tactic:
rfl

Premises used: rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
dsimp : h ≫ t.rightSection ≫ s.π = s.π
⊢ t.asCofork.π ≫ t.rightSection ≫ s.π = s.π

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
rw : t.leftSection ≫ f ≫ s.π = s.π
rw₁ : t.leftSection ≫ g ≫ s.π = s.π
rw₂ rw₃ : s.π = s.π
⊢ h ≫ t.rightSection ≫ s.π = s.π

Tactic:
rw [← t.leftSection_top_assoc, s.condition, t.leftSection_bottom_assoc]

Premises used: CategoryTheory.IsSplitCoequalizer.leftSection_bottom_assoc, CategoryTheory.IsSplitCoequalizer.leftSection_top_assoc, CategoryTheory.Limits.Cofork.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
Z : C
h : Y ⟶ Z
t : IsSplitCoequalizer f g h
s : Cofork f g
m : t.asCofork.pt ⟶ s.pt
hm : t.asCofork.π ≫ m = s.π
⊢ m = t.rightSection ≫ s.π

Tactic:
simp [← hm]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasSplitCoequalizer f g
⊢ HasCoequalizer f g

Tactic:
HasColimit.mk ⟨_, (HasSplitCoequalizer.isSplitCoequalizer f g).isCoequalizer⟩

Premises used: CategoryTheory.HasSplitCoequalizer.isSplitCoequalizer, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.IsSplitCoequalizer.isCoequalizer, CategoryTheory.Limits.ColimitCocone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (ι ≫ f) = F.map ι ≫ F.map g
rw₁ : F.map (ι ≫ g) = F.map ι ≫ F.map g
rw₂ rw₃ : F.map ι ≫ F.map g = F.map ι ≫ F.map g
⊢ F.map ι ≫ F.map f = F.map ι ≫ F.map g

Tactic:
rw [← F.map_comp, q.condition, F.map_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.IsSplitEqualizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (ι ≫ q.leftRetraction) = 𝟙 (F.obj W)
rw₁ : F.map (𝟙 W) = 𝟙 (F.obj W)
rw₂ rw₃ : Eq.{v₂ + 1} (α := F.obj W ⟶ F.obj W) (𝟙 (F.obj W)) (𝟙 (F.obj W))
⊢ F.map ι ≫ F.map q.leftRetraction = 𝟙 (F.obj W)

Tactic:
rw [← F.map_comp, q.ι_leftRetraction, F.map_id]

Premises used: CategoryTheory.IsSplitEqualizer.ι_leftRetraction, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (g ≫ q.rightRetraction) = 𝟙 (F.obj X)
rw₁ : F.map (𝟙 X) = 𝟙 (F.obj X)
rw₂ rw₃ : Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (𝟙 (F.obj X))
⊢ F.map g ≫ F.map q.rightRetraction = 𝟙 (F.obj X)

Tactic:
rw [← F.map_comp, q.bottom_rightRetraction, F.map_id]

Premises used: CategoryTheory.IsSplitEqualizer.bottom_rightRetraction, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
ι : W ⟶ X
q : IsSplitEqualizer f g ι
F : Functor.{v, v₂, u, u₂} C D
rw : F.map (f ≫ q.rightRetraction) = F.map q.leftRetraction ≫ F.map ι
rw₁ : F.map (q.leftRetraction ≫ ι) = F.map q.leftRetraction ≫ F.map ι
rw₂ rw₃ : F.map q.leftRetraction ≫ F.map ι = F.map q.leftRetraction ≫ F.map ι
⊢ F.map f ≫ F.map q.rightRetraction = F.map q.leftRetraction ≫ F.map ι

Tactic:
rw [← F.map_comp, q.top_rightRetraction, F.map_comp]

Premises used: CategoryTheory.IsSplitEqualizer.top_rightRetraction, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
W : C
h : W ⟶ X
t : IsSplitEqualizer f g h
⊢ t.asFork.ι = h

Tactic:
rfl

Premises used: CategoryTheory.Limits.Fork.ι, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
h : W ⟶ X
t : IsSplitEqualizer f g h
s : Fork f g
⊢ (s.ι ≫ t.leftRetraction) ≫ t.asFork.ι = s.ι

Tactic:
simp [- top_rightRetraction, ← t.top_rightRetraction, s.condition_assoc]

Premises used: CategoryTheory.IsSplitEqualizer.top_rightRetraction, CategoryTheory.Limits.Fork.condition_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
W : C
h : W ⟶ X
t : IsSplitEqualizer f g h
s : Fork f g
m : s.pt ⟶ t.asFork.pt
hm : m ≫ t.asFork.ι = s.ι
⊢ m = s.ι ≫ t.leftRetraction

Tactic:
simp [← hm]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
X Y : C
f g : X ⟶ Y
inst_2 : HasSplitEqualizer f g
⊢ HasEqualizer f g

Tactic:
HasLimit.mk ⟨_, (HasSplitEqualizer.isSplitEqualizer f g).isEqualizer⟩

Premises used: CategoryTheory.IsSplitEqualizer.isEqualizer, CategoryTheory.HasSplitEqualizer.isSplitEqualizer, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I : C
hI : IsInitial.{v, u} I
A : C
f : A ⟶ I
⊢ IsIso f

Tactic:
HasStrictInitialObjects.out f hI

Premises used: CategoryTheory.Limits.HasStrictInitialObjects.out
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I : C
hI : IsInitial.{v, u} I
A : C
f g : A ⟶ I
⊢ IsIso f

Tactic:
haveI := hI.isIso_to f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I : C
hI : IsInitial.{v, u} I
A : C
f g : A ⟶ I
this : IsIso f
⊢ IsIso g

Tactic:
haveI := hI.isIso_to g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I : C
hI : IsInitial.{v, u} I
A : C
f g : A ⟶ I
this_1 : IsIso f
this : IsIso g
⊢ f = g

Tactic:
eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.eq_of_inv_eq_inv, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I : C
hI : IsInitial.{v, u} I
A : C
f g : A ⟶ I
this_1 : IsIso f
this : IsIso g
⊢ f = g

Tactic:
exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.eq_of_inv_eq_inv, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I : C
hI : IsInitial.{v, u} I
A : C
⊢ Subsingleton.{v + 1} (A ⟶ I)

Tactic:
⟨hI.strict_hom_ext⟩

Premises used: Subsingleton.intro, CategoryTheory.Limits.IsInitial.strict_hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I X : C
inst_2 : HasBinaryProduct.{v, u} X I
hI : IsInitial.{v, u} I
⊢ IsIso.{v, u} (C := C) (X := prod.{v, u} X I) prod.snd

Tactic:
have := hI.isIso_to (prod.snd : X ⨯ I ⟶ I)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I X : C
inst_2 : HasBinaryProduct.{v, u} X I
hI : IsInitial.{v, u} I
this : IsIso.{v, u} (C := C) (X := prod.{v, u} X I) prod.snd
⊢ prod.{v, u} X I ≅ I

Tactic:
exact asIso prod.snd

Premises used: CategoryTheory.Limits.prod.snd, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I X : C
inst_2 : HasBinaryProduct.{v, u} X I
hI : IsInitial.{v, u} I
⊢ Eq (α := I ⟶ prod.{v, u} X I) (Iso.inv (mulIsInitial X hI)) (hI.to (prod.{v, u} X I))

Tactic:
hI.hom_ext _ _

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I X : C
inst_2 : HasBinaryProduct.{v, u} I X
hI : IsInitial.{v, u} I
⊢ IsIso.{v, u} (C := C) (X := prod.{v, u} I X) prod.fst

Tactic:
have := hI.isIso_to (prod.fst : I ⨯ X ⟶ I)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I X : C
inst_2 : HasBinaryProduct.{v, u} I X
hI : IsInitial.{v, u} I
this : IsIso.{v, u} (C := C) (X := prod.{v, u} I X) prod.fst
⊢ prod.{v, u} I X ≅ I

Tactic:
exact asIso prod.fst

Premises used: CategoryTheory.Limits.prod.fst, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I X : C
inst_2 : HasBinaryProduct.{v, u} I X
hI : IsInitial.{v, u} I
⊢ Eq (α := I ⟶ prod.{v, u} I X) (Iso.inv (isInitialMul X hI)) (hI.to (prod.{v, u} I X))

Tactic:
hI.hom_ext _ _

Premises used: CategoryTheory.Limits.IsInitial.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
I : C
inst_2 : HasInitial.{v, u} C
A : C
f : A ⟶ initial.{v, u} C
⊢ IsIso f

Tactic:
initialIsInitial.isIso_to _

Premises used: CategoryTheory.Limits.IsInitial.isIso_to, CategoryTheory.Limits.initialIsInitial
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
inst_2 : HasInitial.{v, u} C
A : C
f g : A ⟶ initial.{v, u} C
⊢ f = g

Tactic:
initialIsInitial.strict_hom_ext _ _

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.IsInitial.strict_hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
inst_2 : HasInitial.{v, u} C
A : C
⊢ Subsingleton.{v + 1} (A ⟶ initial.{v, u} C)

Tactic:
initialIsInitial.subsingleton_to

Premises used: CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.IsInitial.subsingleton_to
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
inst_2 : HasInitial.{v, u} C
X : C
inst_3 : HasBinaryProduct.{v, u} X (initial.{v, u} C)
⊢ Iso.inv (mulInitial X) = initial.to (prod.{v, u} X (initial.{v, u} C))

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictInitialObjects.{v, u} C
inst_2 : HasInitial.{v, u} C
X : C
inst_3 : HasBinaryProduct.{v, u} (initial.{v, u} C) X
⊢ Iso.inv (initialMul X) = initial.to (prod.{v, u} (initial.{v, u} C) X)

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
h : ∀ (A : C) (f : A ⟶ initial.{v, u} C), IsIso f
I A : C
f : A ⟶ I
hI : IsInitial.{v, u} I
this : IsIso (Y := initial.{v, u} C) (f ≫ hI.to (initial.{v, u} C))
rw :
  CategoryStruct.comp (Y := initial.{v, u} C) (f ≫ hI.to (initial.{v, u} C)) (inv (f ≫ hI.to (initial.{v, u} C))) = 𝟙 A
rw₁ rw₂ : Eq.{v + 1} (α := A ⟶ A) (𝟙 A) (𝟙 A)
⊢ f ≫ CategoryStruct.comp (Y := initial.{v, u} C) (hI.to (initial.{v, u} C)) (inv (f ≫ hI.to (initial.{v, u} C))) = 𝟙 A

Tactic:
rw [← assoc, IsIso.hom_inv_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
I : C
hI : IsTerminal.{v, u} I
A : C
f : I ⟶ A
⊢ IsIso f

Tactic:
HasStrictTerminalObjects.out f hI

Premises used: CategoryTheory.Limits.HasStrictTerminalObjects.out
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
I : C
hI : IsTerminal.{v, u} I
A : C
f g : I ⟶ A
⊢ IsIso f

Tactic:
haveI := hI.isIso_from f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
I : C
hI : IsTerminal.{v, u} I
A : C
f g : I ⟶ A
this : IsIso f
⊢ IsIso g

Tactic:
haveI := hI.isIso_from g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
I : C
hI : IsTerminal.{v, u} I
A : C
f g : I ⟶ A
this_1 : IsIso f
this : IsIso g
⊢ f = g

Tactic:
eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))

Premises used: CategoryTheory.eq_of_inv_eq_inv, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
I : C
hI : IsTerminal.{v, u} I
A : C
f g : I ⟶ A
this_1 : IsIso f
this : IsIso g
⊢ f = g

Tactic:
exact eq_of_inv_eq_inv (hI.hom_ext (inv f) (inv g))

Premises used: CategoryTheory.eq_of_inv_eq_inv, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
I : C
hI : IsTerminal.{v, u} I
A : C
⊢ Subsingleton.{v + 1} (I ⟶ A)

Tactic:
⟨hI.strict_hom_ext⟩

Premises used: Subsingleton.intro, CategoryTheory.Limits.IsTerminal.strict_hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
⊢ IsIso (X := limit F) (limit.π F i)

Tactic:
⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩

Premises used: CategoryTheory.NatTrans.mk, And.intro, Exists.intro, CategoryTheory.Limits.limit.lift, CategoryTheory.IsIso.mk, CategoryTheory.Limits.Cone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
refine_1 : (X : J) → Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj X
refine_2 :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj Y)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
        if h : Y = i then eqToHom ⋯ else (H Y h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) Y))
      ((if h : X = i then eqToHom ⋯ else (H X h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X)) ≫
        F.map f)
refine_3 :
  limit.π F i ≫
      limit.lift F
        { pt := F.1 i,
          π :=
            {
              app := fun (j : J) ↦
                if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
              naturality := ⋯ } } =
    𝟙 (limit F)
refine_4 :
  Eq (α := F.obj i ⟶ F.obj i)
    (CategoryStruct.comp (Y := limit F)
        (limit.lift F
          { pt := F.1 i,
            π :=
              {
                app := fun (j : J) ↦
                  if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j),
                naturality := ⋯ } })
        (limit.π F i) :
      F.obj i ⟶ F.obj i)
    (𝟙 (F.obj i) : F.obj i ⟶ F.obj i)
⊢ IsIso (X := limit F) (limit.π F i)

Tactic:
refine ⟨⟨limit.lift _ ⟨_, ⟨?_, ?_⟩⟩, ?_, ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
h : j = i
refl : Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i = F.obj i
⊢ Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j = F.obj j

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
⊢ Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i = F.obj i

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
⊢ (X : J) → Functor.obj (Functor.obj (Functor.const J) (F.1 i)) X ⟶ F.obj X

Tactic:
exact fun j =>
        dite (j = i)
          (fun h => eqToHom (by cases h; rfl))
          fun h => (H _ h).from _

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.eqToHom, dite, Eq
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j k : J
f : j ⟶ k
pos :
  ∀ (h : k = i) (h_1 : j = i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)
neg :
  ∀ (h : k = i) (h_1 : ¬j = i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯)
      ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)
pos₁ :
  ∀ (h : ¬k = i) (h_1 : j = i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
        (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
      (eqToHom ⋯ ≫ F.map f)
neg₁ :
  ∀ (h : ¬k = i) (h_1 : ¬j = i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
        (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
      ((H j h_1).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j) ≫ F.map f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫
      if h : k = i then eqToHom ⋯ else (H k h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) k))
    ((if h : j = i then eqToHom ⋯ else (H j h).from (Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j)) ≫ F.map f)

Tactic:
split_ifs with h h_1 h_1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j k : J
f : j ⟶ k
h : k = i
h_1 : j = i
pos :
  ∀ (f : j ⟶ i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj i)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj k)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
j : J
h_1 : j = i
f : j ⟶ i
pos :
  ∀ (f : i ⟶ i),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) i ⟶ F.obj i)
      (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) (F.1 i)) j ⟶ F.obj i)
    (Functor.map (Functor.obj (Functor.const J) (F.1 i)) f ≫ eqToHom ⋯) (eqToHom ⋯ ≫ F.map f)

Tactic:
cases h_1
-- Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasStrictTerminalObjects.{v, u} C
J : Type v
inst_2 : SmallCategory J
F : J ⥤ C
inst_3 : HasLimit F
i : J
H : (j : J) → j ≠ i → IsTerminal.{v, u} (F.obj j)
inst_4 : Subsingleton.{v + 1} (i ⟶ i)
f : i ⟶ i
⊢ f = 𝟙 i

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim