Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝¹ : C
app✝¹ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝¹ Y =
      app✝¹ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } })
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
m :
  { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } }.pt ⟶
    { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt
w :
  ∀ (j : J),
    { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } }.ι.app j ≫ m =
      { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j
⊢ m =
    h.desc
      { pt := { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt,
        ι :=
          { app := fun j ↦ { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j, naturality := ⋯ } }

Tactic:
;

Goal state after:
case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝¹ : C
app✝¹ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝¹ Y =
      app✝¹ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } })
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
m :
  { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } }.pt ⟶
    { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt
w :
  ∀ (j : J),
    { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } }.ι.app j ≫ m =
      { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j
⊢ m =
    h.desc
      { pt := { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt,
        ι :=
          { app := fun j ↦ { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j, naturality := ⋯ } }