mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : sq.HasLift
⊢ HasLift ?sq

pp: case sq
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : sq.HasLift
⊢ CommSq u (G.map i) p v

Tactic:
]

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : sq.HasLift
⊢ HasLift ?sq

case sq
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : sq.HasLift
⊢ CommSq u (G.map i) p v
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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.PreservesMonomorphisms
inst✝ : G.PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
h : Mono f
⊢ Mono (G.map (F.map f))

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.PreservesMonomorphisms
inst✝ : G.PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
h : Mono f
⊢ Mono (G.map (F.map f))
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 G : C ⥤ D
inst✝¹ : F.PreservesMonomorphisms
f : G ⟶ F
inst✝ : ∀ (X : C), Mono (f.app X)
X Y : C
π : X ⟶ Y
hπ : Mono π
⊢ Mono (f.app X ≫ F.map π)

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝¹ : F.PreservesMonomorphisms
f : G ⟶ F
inst✝ : ∀ (X : C), Mono (f.app X)
X Y : C
π : X ⟶ Y
hπ : Mono π
⊢ Mono (f.app X ≫ F.map π)
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ ⋯.HasLift

Tactic:
]

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
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ ⋯.HasLift
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
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : g = h
⊢ g = h

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : g = h
⊢ g = h
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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
inst✝ : F.Faithful
X Y : C
f : X ⟶ Y
x✝ : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
⊢ F.map h ≫ F.map f = F.map h ≫ F.map f

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ ⋯.HasLift

Tactic:
]

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ ⋯.HasLift
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
inst✝² : F.IsEquivalence
inst✝¹ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
inst✝ : Epi f
⊢ IsSplitEpi (F.inv.map f)

Tactic:
]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : F.IsEquivalence
inst✝¹ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
inst✝ : Epi f
⊢ IsSplitEpi (F.inv.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
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst✝³ : F'.PreservesMonomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty f (F'.map Z)

Tactic:
]

Goal state after:
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
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst✝³ : F'.PreservesMonomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty f (F'.map Z)
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
F' : D ⥤ C
A B : C
adj : F ⊣ F'
X : C
Y : D
f : F.obj X ⟶ Y
hf : Mono ((adj.homEquiv X Y).symm ((adj.homEquiv X Y) f))
inst✝ : F.ReflectsMonomorphisms
⊢ Mono (F.map ((adj.homEquiv X Y) f))

Tactic:
]

Goal state after:
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
F' : D ⥤ C
A B : C
adj : F ⊣ F'
X : C
Y : D
f : F.obj X ⟶ Y
hf : Mono ((adj.homEquiv X Y).symm ((adj.homEquiv X Y) f))
inst✝ : F.ReflectsMonomorphisms
⊢ Mono (F.map ((adj.homEquiv X Y) f))
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: 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
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi (F.inv.map (F.map f))

Tactic:
]

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
a✝ : StrongEpi (F.map f)
e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f))
⊢ StrongEpi (F.inv.map (F.map f))
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.unit.app x ≫ (h.functor ⋙ h.inverse).map a ≫ h.unitInv.app y =
    h.unit.app x ≫ (h.functor ⋙ h.inverse).map b ≫ h.unitInv.app y

Tactic:
]

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
x y : C
f : x ⟶ y :=
  have hx := ⋯.mpr (h.unit.app x);
  have hy := ⋯.mpr (h.unitInv.app y);
  hx ≫ hy
this : ∀ (z : x ⟶ y), z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y
a b : x ⟶ y
⊢ h.unit.app x ≫ (h.functor ⋙ h.inverse).map a ≫ h.unitInv.app y =
    h.unit.app x ≫ (h.functor ⋙ h.inverse).map b ≫ h.unitInv.app y
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : 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
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f = (f ≫ hi.inv) ≫ hi.hom

pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : 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
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    (f ≫ hi.inv) ≫ c₁.π.app j = { pt := c.pt, π := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.π.app j

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : 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
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ f = (f ≫ hi.inv) ≫ hi.hom

C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : 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
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), f ≫ c₂.π.app j = c.π.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    (f ≫ hi.inv) ≫ c₁.π.app j = { pt := c.pt, π := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : 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
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f = hi.inv ≫ hi.hom ≫ f

pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : 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
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    c₁.ι.app j ≫ hi.hom ≫ f = { pt := c.pt, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.ι.app j

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : 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
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f = hi.inv ≫ hi.hom ≫ f

C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : 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
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    c₁.ι.app j ≫ hi.hom ≫ f = { pt := c.pt, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.ι.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono (hI.to X)

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono (hI.to X)
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial I'
⊢ Mono ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (hI.to X)
I' X : C
hI' : IsInitial I'
⊢ Mono ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map (tX.to j') = F.map (tX.to j')

Tactic:
]

Goal state after:
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
j✝ : J
⊢ c.π.app j✝ ≫ α.app j✝ = ((Cone.postcompose α).obj c).π.app j✝

Tactic:
]

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
⊢ c.π.app j✝ ≫ α.app j✝ = ((Cone.postcompose α).obj c).π.app j✝
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map (tX.from j) = F.map (tX.from j)

Tactic:
]

Goal state after:
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)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ π F (E.obj (D.obj j)) = π F ((D ⋙ E).obj j)

Tactic:
]

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)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ π F (E.obj (D.obj j)) = π F ((D ⋙ E).obj 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)
c : Cone F
j✝ : J
⊢ G.map (c.π.app j✝) = (G.mapCone c).π.app j✝

Tactic:
]

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 (c.π.app j✝) = (G.mapCone c).π.app 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)
j✝ : J
⊢ H.map (G.map (π F j✝)) = (G ⋙ H).map (π F j✝)

Tactic:
]

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 (G.map (π F j✝)) = (G ⋙ H).map (π F 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)
j✝ : K
⊢ G.map (π F (E.obj j✝)) = G.map (π F (E.obj j✝))

Tactic:
]

Goal state after:
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
L : (J ⥤ C) ⥤ C
adj : const J ⊣ L
F : J ⥤ C
s : Cone F
j : J
eq : L.map s.π ≫ (adj.counit.app F).app j = (adj.counit.app ((const J).obj s.pt)).app j ≫ s.π.app j
eq' : adj.unit.app s.pt ≫ (adj.counit.app ((const J).obj s.pt)).app j = 𝟙 s.pt
⊢ s.π.app j = s.π.app j

Tactic:
]

Goal state after:
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)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)

Tactic:
]

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)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ 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
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (c.ι.app j✝) = (G.mapCocone c).ι.app j✝

Tactic:
]

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
⊢ G.map (c.ι.app j✝) = (G.mapCocone c).ι.app 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
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasColimit F
G : C ⥤ D
inst✝¹ : HasColimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ H.map (G.map (ι F j)) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)

Tactic:
]

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)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasColimit ((F ⋙ G) ⋙ H)
j : J
⊢ H.map (G.map (ι F j)) = ι ((F ⋙ G) ⋙ H) j ≫ post F (G ⋙ H)
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✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ G.map (ι F (E.obj j)) = (ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E) ≫ post F G

Tactic:
]

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✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ G.map (ι F (E.obj j)) = (ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E) ≫ post F G
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✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
this : HasColimit (E ⋙ F ⋙ G)
⊢ G.map (ι F (E.obj j)) = G.map (ι F (E.obj j))

Tactic:
]

Goal state after:
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
j✝ : K
⊢ α.app (E.obj j✝) ≫ ι G (E.obj j✝) = (E.whiskerLeft α).app j✝ ≫ ι G (E.obj j✝)

Tactic:
]

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
⊢ α.app (E.obj j✝) ≫ ι G (E.obj j✝) = (E.whiskerLeft α).app j✝ ≫ ι G (E.obj 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✝² : 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
⊢ H.map (α.app j✝) ≫ H.map (ι G j✝) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H

Tactic:
]

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
⊢ H.map (α.app j✝) ≫ H.map (ι G j✝) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H
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
j✝ : J
⊢ H.map (α.app j✝) ≫ H.map (ι G j✝) = (whiskerRight α H).app j✝ ≫ H.map (ι G j✝)

Tactic:
]

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
⊢ H.map (α.app j✝) ≫ H.map (ι G j✝) = (whiskerRight α H).app j✝ ≫ H.map (ι 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
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ m = m.unop.op

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
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J), m.unop ≫ t.π.app j = s.unop.π.app j

Tactic:
]

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
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ m = m.unop.op

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
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : J), m.unop ≫ t.π.app j = s.unop.π.app 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
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
j : J
⊢ m.unop ≫ t.π.app j = (t.op.ι.app (Opposite.op j) ≫ m).unop

Tactic:
]

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
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
j : J
⊢ m.unop ≫ t.π.app j = (t.op.ι.app (Opposite.op j) ≫ m).unop