mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
⊢ ∀ ⦃X Y : Discrete PEmpty.{w + 1}⦄ (f : X ⟶ Y),
    ((Functor.const (Discrete PEmpty.{w + 1})).obj c.pt).map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X fun as ↦ ⋯.elim) ≫ F₁.map f

Tactic:
by

Goal state after:
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 =
    hl.lift { pt := c.pt, π := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } } ≫
      hi.hom

Tactic:
by

Goal state after:
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₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.LeftInverse (fun hl ↦ isLimitChangeEmptyCone C hl c₁ h.symm) fun hl ↦ isLimitChangeEmptyCone C hl c₂ h

Tactic:
by

Goal state after:
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₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.RightInverse (fun hl ↦ isLimitChangeEmptyCone C hl c₁ h.symm) fun hl ↦ isLimitChangeEmptyCone C hl c₂ h

Tactic:
by

Goal state after:
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₂
⊢ (X : Discrete PEmpty.{w + 1}) → F₁.obj X ⟶ ((Functor.const (Discrete PEmpty.{w + 1})).obj c.pt).obj X

Tactic:
by

Goal state after:
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₂
⊢ ∀ ⦃X Y : Discrete PEmpty.{w + 1}⦄ (f : X ⟶ Y),
    F₁.map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X fun as ↦ ⋯.elim) ≫ ((Functor.const (Discrete PEmpty.{w + 1})).obj c.pt).map f

Tactic:
by

Goal state after:
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 ≫
      hl.desc { pt := c.pt, ι := { app := fun X_1 ↦ id (Discrete.casesOn X_1 fun as ↦ ⋯.elim), naturality := ⋯ } }

Tactic:
by

Goal state after:
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₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.LeftInverse (fun hl ↦ isColimitChangeEmptyCocone C hl c₁ h.symm) fun hl ↦
    isColimitChangeEmptyCocone C hl c₂ h

Tactic:
by

Goal state after:
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₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.RightInverse (fun hl ↦ isColimitChangeEmptyCocone C hl c₁ h.symm) fun hl ↦
    isColimitChangeEmptyCocone C hl c₂ h

Tactic:
by

Goal state after:
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 f

Tactic:
by

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✝ F : J ⥤ C
inst✝ : HasLimit F
j j' : J
hj : j = j'
⊢ F.obj j = F.obj j'

Tactic:
by

Goal state after:
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'.to X)

Tactic:
by

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 : J ⥤ C
inst✝ : HasLimit F
j j' : J
hj : j = j'
⊢ π F j ≫ eqToHom ⋯ = π F j'

Tactic:
by

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✝ F : J ⥤ C
inst✝ : HasColimit F
j j' : J
hj : j = j'
⊢ F.obj j' = F.obj j

Tactic:
by

Goal state after:
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'
⊢ ((Functor.const J).obj (F.obj X)).map k ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k

Tactic:
by

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 : J ⥤ C
inst✝ : HasColimit F
j j' : J
hj : j = j'
⊢ eqToHom ⋯ ≫ ι F j = ι F j'

Tactic:
by

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 : J ⥤ C
inst✝ : HasLimit F
c : Cone F
j : J
⊢ (coneMorphism c).hom ≫ π F j = c.π.app j

Tactic:
by

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 : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (isoLimitCone t).hom ≫ t.cone.π.app j = π F j

Tactic:
by

Goal state after:
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
s : Cone F
m : s.pt ⟶ (coneOfDiagramInitial tX F).pt
w : ∀ (j : J), m ≫ (coneOfDiagramInitial tX F).π.app j = s.π.app j
⊢ m = s.π.app X

Tactic:
by

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 : J ⥤ C
inst✝ : HasLimit F
t : LimitCone F
j : J
⊢ (isoLimitCone t).inv ≫ π F j = t.cone.π.app j

Tactic:
by

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✝ F G : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit G
α : F ⟶ G
inst✝ : IsIso α
⊢ limMap α ≫ limMap (inv α) = 𝟙 (limit F)

Tactic:
by

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✝ F G : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit G
α : F ⟶ G
inst✝ : IsIso α
⊢ limMap (inv α) ≫ limMap α = 𝟙 (limit G)

Tactic:
by

Goal state after:
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
hX : IsTerminal X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ ∀ ⦃X_1 Y : J⦄ (f : X_1 ⟶ Y),
    ((Functor.const J).obj (F.obj X)).map f ≫ inv (F.map (hX.from Y)) = inv (F.map (hX.from X_1)) ≫ F.map f

Tactic:
by

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
⊢ lift F c ≫ limMap α = lift G ((Cone.postcompose α).obj c)

Tactic:
by

Goal state after:
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 k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ ((Functor.const J).obj (F.obj X)).map k

Tactic:
by

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 : J ⥤ C
inst✝ : HasLimit F
c : Cone F
X : C
f : X ⟶ c.pt
⊢ lift F (c.extend f) = f ≫ lift F c

Tactic:
by

Goal state after:
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
s : Cocone F
m : (coconeOfDiagramTerminal tX F).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfDiagramTerminal tX F).ι.app j ≫ m = s.ι.app j
⊢ m = s.ι.app X

Tactic:
by

Goal state after:
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
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X : J
hX : IsTerminal X
⊢ IsIso (c.ι.app X)

Tactic:
by

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
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ (isoOfEquivalence e w).hom ≫ limit.π G k =
    limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)

Tactic:
by

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
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ (isoOfEquivalence e w).inv ≫ limit.π F j = limit.π G (e.functor.obj j) ≫ w.hom.app j

Tactic:
by

Goal state after:
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
hX : IsInitial X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ ∀ ⦃X_1 Y : J⦄ (f : X_1 ⟶ Y),
    F.map f ≫ inv (F.map (hX.to Y)) = inv (F.map (hX.to X_1)) ≫ ((Functor.const J).obj (F.obj X)).map f

Tactic:
by

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)
k : K
⊢ pre F E ≫ π (E ⋙ F) k = π F (E.obj k)

Tactic:
by

Goal state after:
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
F : J ⥤ C
c : Cone F
hc : IsLimit c
X : J
hX : IsInitial X
⊢ IsIso (c.π.app X)

Tactic:
by

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)
c : Cone F
⊢ lift F c ≫ pre F E = lift (E ⋙ F) (Cone.whisker E c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal X
hY : IsTerminal Y
f : X ⟶ Y
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsInitial X
hY : IsInitial Y
f : X ⟶ Y
⊢ IsIso f

Tactic:
by

Goal state after:
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_1 : C ⥤ D) (m : X_1 ⟶ (const C).obj X), m = { app := fun Z ↦ hX.from (X_1.obj Z), naturality := ⋯ }

Tactic:
by

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)
⊢ pre F E ≫ pre (E ⋙ F) D = pre F (D ⋙ E)

Tactic:
by

Goal state after:
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:
by

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)
s : LimitCone (E ⋙ F)
t : LimitCone F
⊢ pre F E = (isoLimitCone t).hom ≫ s.isLimit.lift (Cone.whisker E t.cone) ≫ (isoLimitCone s).inv

Tactic:
by

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
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
j : J
⊢ post F G ≫ π (F ⋙ G) j = G.map (π F j)

Tactic:
by

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
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:
by

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
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)
⊢ H.map (post F G) ≫ post (F ⋙ G) H = post F (G ⋙ H)

Tactic:
by

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
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)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E

Tactic:
by

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
e : K ≌ J
inst✝ : HasLimit (e.functor ⋙ F)
⊢ HasLimit F

Tactic:
by

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✝ : HasLimitsOfShape J C
F : J ⥤ C
⊢ limMap (𝟙 F) = 𝟙 (limit F)

Tactic:
by

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✝ : HasLimitsOfShape J C
X✝ Y✝ Z✝ : J ⥤ C
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
⊢ limMap (α ≫ β) = limMap α ≫ limMap β

Tactic:
by

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✝¹ : 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:
by

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
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
⊢ pre F E₂ = pre F E₁ ≫ lim.map (whiskerRight α F)

Tactic:
by

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
inst✝ : HasLimitsOfShape J C
F : J ⥤ C
⊢ pre F (𝟭 J) = lim.map F.leftUnitor.inv

Tactic:
by

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 : 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:
by

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✝ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : C
g : J ⥤ C
⊢ Function.LeftInverse (fun f ↦ { app := fun x ↦ f ≫ limit.π g x, naturality := ⋯ }) fun f ↦
    limit.lift g { pt := c, π := f }

Tactic:
by

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✝ : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
c : C
g : J ⥤ C
⊢ Function.RightInverse (fun f ↦ { app := fun x ↦ f ≫ limit.π g x, naturality := ⋯ }) fun f ↦
    limit.lift g { pt := c, π := f }

Tactic:
by

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✝ F G : J ⥤ C
inst✝² : HasLimit F
inst✝¹ : HasLimit G
α : F ⟶ G
inst✝ : ∀ (j : J), Mono (α.app j)
Z : C
u v : Z ⟶ limit F
h : u ≫ limMap α = v ≫ limMap α
j : J
⊢ (u ≫ limit.π F j) ≫ α.app j = (v ≫ limit.π F j) ≫ α.app j

Tactic:
by

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
⊢ (adj.homEquiv s.pt F) s.π ≫ (coneOfAdj adj F).π.app j = s.π.app j

Tactic:
by

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
m : s.pt ⟶ (coneOfAdj adj F).pt
hm : ∀ (j : J), m ≫ (coneOfAdj adj F).π.app j = s.π.app j
⊢ (adj.homEquiv s.pt F).symm m = (adj.homEquiv s.pt F).symm ((adj.homEquiv s.pt F) s.π)

Tactic:
by

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
J' : Type u₂
inst✝¹ : Category.{v₂, u₂} J'
e : J ≌ J'
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J' C

Tactic:
by

Goal state after:
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:
by

Goal state after:
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✝¹ : EssentiallySmall.{u₁, v₂, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
⊢ HasLimitsOfShape J C

Tactic:
by

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
G : K ⥤ C
inst✝ : HasColimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ colimit.ι F j ≫ (isoOfEquivalence e w).hom =
    F.map (e.unit.app j) ≫
      w.inv.app ((e.functor ⋙ e.inverse).obj j) ≫ colimit.ι G (e.functor.obj ((e.functor ⋙ e.inverse).obj j))

Tactic:
by

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
G : K ⥤ C
inst✝ : HasColimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
k : K
⊢ colimit.ι G k ≫ (isoOfEquivalence e w).inv =
    G.map (e.counitInv.app k) ≫ w.hom.app (e.inverse.obj k) ≫ colimit.ι F (e.inverse.obj k)

Tactic:
by

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)
k : K
⊢ ι (E ⋙ F) k ≫ pre F E = ι F (E.obj k)

Tactic:
by

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)
inst✝ : IsIso (pre F E)
k : K
⊢ ι F (E.obj k) ≫ inv (pre F E) = ι (E ⋙ F) k

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
X✝ Y✝ Z✝ : WidePullbackShape J
f : X✝.Hom Y✝
g : Y✝.Hom Z✝
⊢ X✝.Hom Z✝

Tactic:
by

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)
c : Cocone F
⊢ pre F E ≫ desc F c = desc (E ⋙ F) (Cocone.whisker E c)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

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

Tactic:
by

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)
⊢ pre (E ⋙ F) D ≫ pre F E = pre F (D ⋙ E)

Tactic:
by

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)
s : ColimitCocone (E ⋙ F)
t : ColimitCocone F
⊢ pre F E = (isoColimitCocone s).hom ≫ s.isColimit.desc (Cocone.whisker E t.cocone) ≫ (isoColimitCocone t).inv

Tactic:
by

Goal state after: