Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: case e'_2
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
j : Discrete α
hj : j ∈ unop t
e_1✝ : (s.pt ⟶ (Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ }) = (s.pt ⟶ F.obj j)
⊢ (m ≫
        limit.π
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          t) ≫
      limit.π (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } =
    m ≫
      { pt := limit (liftToFinsetObj F),
              π :=
                Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
        j

pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
j : Discrete α
hj : j ∈ unop t
e_1✝ : (s.pt ⟶ (Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ }) = (s.pt ⟶ F.obj j)
⊢ (limit.lift
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } } ≫
        limit.π
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          t) ≫
      limit.π (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } =
    s.π.app j

Tactic:
· simp [← limit.w (liftToFinsetObj F) ⟨⟨⟨Finset.singleton_subset_iff.2 hj⟩⟩⟩]
          rfl

Goal state after:
case e'_3
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
j : Discrete α
hj : j ∈ unop t
e_1✝ : (s.pt ⟶ (Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ }) = (s.pt ⟶ F.obj j)
⊢ (limit.lift
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } } ≫
        limit.π
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          t) ≫
      limit.π (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } =
    s.π.app j