mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi (F.map f) ↔ Epi f

Tactic:
constructor

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi (F.map f) → Epi f

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
hF₁ : F.PreservesEpimorphisms
hF₂ : F.ReflectsEpimorphisms
⊢ Epi f → Epi (F.map f)
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
⊢ StrongEpi (F.map f) ↔ StrongEpi f

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
⊢ StrongEpi (F.map f) → StrongEpi f

case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
⊢ StrongEpi f → StrongEpi (F.map f)
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (C ≌ Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (C ≌ Discrete PUnit.{w + 1}) → Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))

case mpr
C : Type u
inst✝ : Category.{v, u} C
⊢ (Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))) → Nonempty (C ≌ Discrete PUnit.{w + 1})
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
⊢ lift F c ≫ limMap α = lift G ((Cone.postcompose α).obj c)

Tactic:
ext

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ (lift F c ≫ limMap α) ≫ π G j✝ = lift G ((Cone.postcompose α).obj c) ≫ π G j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
⊢ lift F c ≫ pre F E = lift (E ⋙ F) (Cone.whisker E c)

Tactic:
ext

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
j✝ : K
⊢ (lift F c ≫ pre F E) ≫ π (E ⋙ F) j✝ = lift (E ⋙ F) (Cone.whisker E c) ≫ π (E ⋙ F) j✝
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X : D
hX : IsTerminal X
X✝ : C ⥤ D
m✝ : X✝ ⟶ (const C).obj X
⊢ m✝ = { app := fun Z ↦ hX.from (X✝.obj Z), naturality := ⋯ }

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X : D
hX : IsTerminal X
X✝ : C ⥤ D
m✝ : X✝ ⟶ (const C).obj X
x✝ : C
⊢ m✝.app x✝ = { app := fun Z ↦ hX.from (X✝.obj Z), naturality := ⋯ }.app x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X : D
hX : IsInitial X
Y✝ : C ⥤ D
m✝ : (const C).obj X ⟶ Y✝
⊢ m✝ = { app := fun Z ↦ hX.to (Y✝.obj Z), naturality := ⋯ }

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
X : D
hX : IsInitial X
Y✝ : C ⥤ D
m✝ : (const C).obj X ⟶ Y✝
x✝ : C
⊢ m✝.app x✝ = { app := fun Z ↦ hX.to (Y✝.obj Z), naturality := ⋯ }.app x✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
⊢ G.map (lift F c) ≫ post F G = lift (F ⋙ G) (G.mapCone c)

Tactic:
ext

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ (G.map (lift F c) ≫ post F G) ≫ π (F ⋙ G) j✝ = lift (F ⋙ G) (G.mapCone c) ≫ π (F ⋙ G) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
⊢ H.map (post F G) ≫ post (F ⋙ G) H = post F (G ⋙ H)

Tactic:
ext

Goal state after:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ (H.map (post F G) ≫ post (F ⋙ G) H) ≫ π ((F ⋙ G) ⋙ H) j✝ = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E

Tactic:
ext

Goal state after:
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ (G.map (pre F E) ≫ post (E ⋙ F) G) ≫ π ((E ⋙ F) ⋙ G) j✝ = (post F G ≫ pre (F ⋙ G) E) ≫ π ((E ⋙ F) ⋙ G) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasLimitsOfShape K C
E : K ⥤ J
⊢ lim.map α ≫ pre G E = pre F E ≫ lim.map (E.whiskerLeft α)

Tactic:
ext

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasLimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ (lim.map α ≫ pre G E) ≫ π (E ⋙ G) j✝ = (pre F E ≫ lim.map (E.whiskerLeft α)) ≫ π (E ⋙ G) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasLimitsOfShape J D
H : C ⥤ D
⊢ H.map (limMap α) ≫ post G H = post F H ≫ limMap (whiskerRight α H)

Tactic:
ext

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasLimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ (H.map (limMap α) ≫ post G H) ≫ π (G ⋙ H) j✝ = (post F H ≫ limMap (whiskerRight α H)) ≫ π (G ⋙ H) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J' C

Tactic:
constructor

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
⊢ autoParam (∀ (F : J' ⥤ C), HasLimit F) HasLimitsOfShape.has_limit._autoParam
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : Small.{u₁, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
⊢ HasLimitsOfShape J C

Tactic:
have := HasLimitsOfSize.has_limits_of_shape (C := C) (ShrinkHoms (Shrink.{u₁} J))

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasLimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : Small.{u₁, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
this : HasLimitsOfShape (ShrinkHoms.{u₁} (Shrink.{u₁, u₂} J)) C
⊢ HasLimitsOfShape J C
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
x✝¹ x✝ : WidePullbackShape J
⊢ Subsingleton (x✝¹ ⟶ x✝)

Tactic:
constructor

Goal state after:
J : Type w
x✝¹ x✝ : WidePullbackShape J
⊢ ∀ (a b : x✝¹ ⟶ x✝), a = b
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
⊢ pre F E ≫ desc F c = desc (E ⋙ F) (Cocone.whisker E c)

Tactic:
ext

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimit F
E : K ⥤ J
inst✝ : HasColimit (E ⋙ F)
c : Cocone F
j✝ : K
⊢ ι (E ⋙ F) j✝ ≫ pre F E ≫ desc F c = ι (E ⋙ F) j✝ ≫ desc (E ⋙ F) (Cocone.whisker E c)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
⊢ post F G ≫ G.map (desc F c) = desc (F ⋙ G) (G.mapCocone c)

Tactic:
ext

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ ι (F ⋙ G) j✝ ≫ post F G ≫ G.map (desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
⊢ pre F E ≫ colim.map α = colim.map (E.whiskerLeft α) ≫ pre G E

Tactic:
ext

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ ι (E ⋙ F) j✝ ≫ pre F E ≫ colim.map α = ι (E ⋙ F) j✝ ≫ colim.map (E.whiskerLeft α) ≫ pre G E
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
⊢ post F H ≫ H.map (colim.map α) = colim.map (whiskerRight α H) ≫ post G H

Tactic:
ext

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ ι (F ⋙ H) j✝ ≫ post F H ≫ H.map (colim.map α) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
x✝¹ x✝ : WidePushoutShape J
⊢ Subsingleton (x✝¹ ⟶ x✝)

Tactic:
constructor

Goal state after:
J : Type w
x✝¹ x✝ : WidePushoutShape J
⊢ ∀ (a b : x✝¹ ⟶ x✝), a = b
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J' C

Tactic:
constructor

Goal state after:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u
inst✝² : Category.{v, u} C
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasColimitsOfShape J C
⊢ autoParam (∀ (F : J' ⥤ C), HasColimit F) HasColimitsOfShape.has_colimit._autoParam
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
g : β → C
inst✝ : HasCoproduct f
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
⊢ HasCoproduct g

Tactic:
have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
    Discrete.natIso (fun ⟨j⟩ => iso j)

Goal state after:
β : Type w
α✝ : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α✝ → C
g : β → C
inst✝ : HasCoproduct f
e : β ≃ α✝
iso : (j : β) → g j ≅ f (e j)
α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f
⊢ HasCoproduct g
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
g : β → C
inst✝ : HasProduct f
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
⊢ HasProduct g

Tactic:
have α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f :=
    Discrete.natIso (fun ⟨j⟩ => iso j)

Goal state after:
β : Type w
α✝ : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α✝ → C
g : β → C
inst✝ : HasProduct f
e : β ≃ α✝
iso : (j : β) → g j ≅ f (e j)
α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f
⊢ HasProduct g
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case e'_5
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
⊢ (Sigma.desc fun a ↦ Sigma.ι f a) = 𝟙 (∐ f)

Tactic:
ext

Goal state after:
case e'_5
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
b✝ : β
⊢ (Sigma.ι f b✝ ≫ Sigma.desc fun a ↦ Sigma.ι f a) = Sigma.ι f b✝ ≫ 𝟙 (∐ f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
⊢ (map fun a ↦ 𝟙 (f a)) = 𝟙 (∏ᶜ f)

Tactic:
ext

Goal state after:
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
b✝ : α
⊢ (map fun a ↦ 𝟙 (f a)) ≫ π f b✝ = 𝟙 (∏ᶜ f) ≫ π f b✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
⊢ map q ≫ map q' = map fun a ↦ q a ≫ q' a

Tactic:
ext

Goal state after:
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
b✝ : α
⊢ (map q ≫ map q') ≫ π h b✝ = (map fun a ↦ q a ≫ q' a) ≫ π h b✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
⊢ (map' id fun a ↦ 𝟙 (f a)) = 𝟙 (∏ᶜ f)

Tactic:
ext

Goal state after:
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
b✝ : α
⊢ (map' id fun a ↦ 𝟙 (f a)) ≫ π f b✝ = 𝟙 (∏ᶜ f) ≫ π f b✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
p' : γ → β
q : (b : β) → f (p b) ⟶ g b
q' : (c : γ) → g (p' c) ⟶ h c
⊢ map' p q ≫ map' p' q' = map' (p ∘ p') fun c ↦ q (p' c) ≫ q' c

Tactic:
ext

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
p' : γ → β
q : (b : β) → f (p b) ⟶ g b
q' : (c : γ) → g (p' c) ⟶ h c
b✝ : γ
⊢ (map' p q ≫ map' p' q') ≫ π h b✝ = (map' (p ∘ p') fun c ↦ q (p' c) ≫ q' c) ≫ π h b✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (b : β) → f (p b) ⟶ g b
q' : (b : β) → g b ⟶ h b
⊢ map' p q ≫ map q' = map' p fun b ↦ q b ≫ q' b

Tactic:
ext

Goal state after:
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (b : β) → f (p b) ⟶ g b
q' : (b : β) → g b ⟶ h b
b✝ : β
⊢ (map' p q ≫ map q') ≫ π h b✝ = (map' p fun b ↦ q b ≫ q' b) ≫ π h b✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (a : α) → f a ⟶ g a
q' : (b : β) → g (p b) ⟶ h b
⊢ map q ≫ map' p q' = map' p fun b ↦ q (p b) ≫ q' b

Tactic:
ext

Goal state after:
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (a : α) → f a ⟶ g a
q' : (b : β) → g (p b) ⟶ h b
b✝ : β
⊢ (map q ≫ map' p q') ≫ π h b✝ = (map' p fun b ↦ q (p b) ≫ q' b) ≫ π h b✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F) = 𝟙 (limit F)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X : Discrete α ⥤ C
inst✝ : HasProduct fun j ↦ X.obj { as := j }
s : Cone X
m : s.pt ⟶ (Pi.cone X).pt
hm : ∀ (j : Discrete α), m ≫ (Pi.cone X).π.app j = s.π.app j
⊢ m = Pi.lift fun j ↦ s.π.app { as := j }

Tactic:
ext

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X : Discrete α ⥤ C
inst✝ : HasProduct fun j ↦ X.obj { as := j }
s : Cone X
m : s.pt ⟶ (Pi.cone X).pt
hm : ∀ (j : Discrete α), m ≫ (Pi.cone X).π.app j = s.π.app j
b✝ : α
⊢ m ≫ Pi.π (fun j ↦ X.obj { as := j }) b✝ = (Pi.lift fun j ↦ s.π.app { as := j }) ≫ Pi.π (fun j ↦ X.obj { as := j }) b✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F) = 𝟙 (limit F)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
⊢ colimit.desc F (coconeOfDiagramTerminal I F) ≫ colimit.ι F j = 𝟙 (colimit F)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
j✝ : J
⊢ colimit.ι F j✝ ≫ colimit.desc F (coconeOfDiagramTerminal I F) ≫ colimit.ι F j = colimit.ι F j✝ ≫ 𝟙 (colimit F)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
⊢ (map fun a ↦ 𝟙 (f a)) = 𝟙 (∐ f)

Tactic:
ext

Goal state after:
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
b✝ : α
⊢ (ι f b✝ ≫ map fun a ↦ 𝟙 (f a)) = ι f b✝ ≫ 𝟙 (∐ f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
⊢ map q ≫ map q' = map fun a ↦ q a ≫ q' a

Tactic:
ext

Goal state after:
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
b✝ : α
⊢ ι f b✝ ≫ map q ≫ map q' = ι f b✝ ≫ map fun a ↦ q a ≫ q' a
Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = 𝟙 (colimit F)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ colimit.ι F j✝ ≫ colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = colimit.ι F j✝ ≫ 𝟙 (colimit F)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
⊢ (map' id fun a ↦ 𝟙 (f a)) = 𝟙 (∐ f)

Tactic:
ext

Goal state after:
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
b✝ : α
⊢ (ι f b✝ ≫ map' id fun a ↦ 𝟙 (f a)) = ι f b✝ ≫ 𝟙 (∐ f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
p' : β → γ
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h (p' b)
⊢ map' p q ≫ map' p' q' = map' (p' ∘ p) fun a ↦ q a ≫ q' (p a)

Tactic:
ext

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
p' : β → γ
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h (p' b)
b✝ : α
⊢ ι f b✝ ≫ map' p q ≫ map' p' q' = ι f b✝ ≫ map' (p' ∘ p) fun a ↦ q a ≫ q' (p a)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h b
⊢ map' p q ≫ map q' = map' p fun a ↦ q a ≫ q' (p a)

Tactic:
ext

Goal state after:
β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h b
b✝ : α
⊢ ι f b✝ ≫ map' p q ≫ map q' = ι f b✝ ≫ map' p fun a ↦ q a ≫ q' (p a)