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) →
    ((Functor.const J).obj pt✝¹).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝¹).map f ≫ app✝¹ Y =
      app✝¹ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } }
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶
      ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C).map f
m :
  { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt ⟶
    ((𝟭 C).mapCone { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } }).pt
w :
  ∀ (j : J),
    m ≫ ((𝟭 C).mapCone { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } }).π.app j =
      { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j
⊢ m =
    h.lift
      { 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) →
    ((Functor.const J).obj pt✝¹).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝¹).map f ≫ app✝¹ Y =
      app✝¹ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } }
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶
      ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C).map f
m :
  { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt ⟶
    ((𝟭 C).mapCone { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } }).pt
w :
  ∀ (j : J),
    m ≫ ((𝟭 C).mapCone { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } }).π.app j =
      { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j
⊢ m =
    h.lift
      { pt := { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt,
        π :=
          { app := fun j ↦ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j, naturality := ⋯ } }