awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
refine_1 : q.1 ⟶ c₁.pt
⊢ q.pt ⟶ (buildLimit s t hs ht i).pt
have refine_2 : Eq (α := q.1 ⟶ c₂.pt) (t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ s : q.1 ⟶ c₂.pt)
  (t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ t : q.1 ⟶ c₂.pt)
Tactic: refine hi.lift (Fork.ofι ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
⊢ q.1 ⟶ c₁.pt
have refine_1 : (j : J) → q.1 ⟶ F.obj j
Tactic: refine t₁.lift (Fan.mk _ fun j => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
F : Functor.{w, v, w, u} J C
c₁ : Fan.{w, v, u} F.obj
c₂ : Fan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    s ≫ c₂.π.app { as := f } =
      c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 : Discrete J } ≫
        F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      c₁.pt ⟶
        Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      (t ≫ c₂.π.app { as := f }) (c₁.π.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
i : Fork s t
t₁ : IsLimit c₁
t₂ : IsLimit c₂
hi : IsLimit i
q : Cone F
⊢ Eq (α := q.1 ⟶ c₂.pt) (t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ s : q.1 ⟶ c₂.pt)
    (t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ t : q.1 ⟶ c₂.pt)
have refine_2 : ∀ (j : Discrete ((p : J × J) × (p.1 ⟶ p.2))),
  Eq (α :=
    Quiver.Hom.{v, u} (V := C) q.1
      (Functor.obj.{w, v, w, u}
        (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) j))
    ((t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ s) ≫ c₂.π.app j :
      Quiver.Hom.{v, u} (V := C) q.1
        (Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) j))
    ((t₁.lift (Fan.mk q.1 fun (j : J) ↦ q.π.app j) ≫ t) ≫ c₂.π.app j :
      Quiver.Hom.{v, u} (V := C) q.1
        (Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) j))
Tactic: apply t₂.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ PreservesLimit K G
have apply : IsLimit (G.mapCone (buildLimit s t sorry sorry (limit.cone (parallelPair s t))))
Tactic: apply preservesLimit_of_preserves_limit_cone
        (buildIsLimit s t (by simp [P, s]) (by simp [P, t]) (limit.isLimit _)
          (limit.isLimit _) (limit.isLimit _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
⊢ IsLimit (G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t))))
have apply : Fan.{w, v₂, u₂} (K ⋙ G).obj
Tactic: apply IsLimit.ofIsoLimit (buildIsLimit _ _ _ _ _ _ _) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
apply : Fan.{w, v₂, u₂} (K ⋙ G).obj
⊢ IsLimit (G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t))))
have apply₁ : Fan.{w, v₂, u₂} (C := D) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
Tactic: apply IsLimit.ofIsoLimit (buildIsLimit _ _ _ _ _ _ _) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
apply : Fan.{w, v₂, u₂} (K ⋙ G).obj
apply₁ :
  Fan.{w, v₂, u₂} (C := D) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
⊢ IsLimit (G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t))))
have apply₂ : Cone.pt.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
    (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) ⟶
  Cone.pt.{w, v₂, w, u₂} (J := Discrete ((p : J × J) × (p.1 ⟶ p.2))) (F :=
    Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
    (Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
      G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f))
Tactic: apply IsLimit.ofIsoLimit (buildIsLimit _ _ _ _ _ _ _) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
apply : Fan.{w, v₂, u₂} (K ⋙ G).obj
apply₁ :
  Fan.{w, v₂, u₂} (C := D) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
apply₂ apply₃ :
  Cone.pt.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
      (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) ⟶
    Cone.pt.{w, v₂, w, u₂} (J := Discrete ((p : J × J) × (p.1 ⟶ p.2))) (F :=
      Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
      (Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
        G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f))
⊢ IsLimit (G.mapCone (buildLimit s t ⋯ ⋯ (limit.cone (parallelPair s t))))
have apply₄ : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
  Eq (α :=
    Cone.pt.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
        (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) ⟶
      Functor.obj.{w, v₂, w, u₂}
        (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
        { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
    (G.map s ≫
      NatTrans.app
        (Cone.π
          (Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f)))
        { as := f })
    (NatTrans.app (Cone.π (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)))
        { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      (K ⋙ G).map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)))
Tactic: apply IsLimit.ofIsoLimit (buildIsLimit _ _ _ _ _ _ _) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ Eq (α :=
    Cone.pt.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
        (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) ⟶
      Functor.obj.{w, v₂, w, u₂}
        (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
        { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
    (G.map s ≫
      NatTrans.app
        (Cone.π
          (Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f)))
        { as := f })
    (NatTrans.app (Cone.π (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)))
        { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      (K ⋙ G).map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)))
have dsimp : Eq (α := G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
  (CategoryStruct.comp (Y :=
      G.obj (piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
      (G.map
        (Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
          limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
            K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))))
      (G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f)) :
    G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
  (G.map (Pi.π K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ≫
      G.map (K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))) :
    G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
Tactic: dsimp [P, Q, s, Fan.mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ Eq (α := G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (CategoryStruct.comp (Y :=
        G.obj (piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
        (G.map
          (Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
              K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))))
        (G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f)) :
      G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
    (G.map (Pi.π K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) ≫
        G.map (K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))) :
      G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
have simp : Eq (α := G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
  (G.map
      (NatTrans.app
        (Cone.π
          (Fan.mk (piObj.{w, v, u} K.obj) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
              K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))))
        { as := f }) :
    G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
  (G.map (Pi.π K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 ≫ K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))) :
    G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
Tactic: simp only [← G.map_comp, limit.lift_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasLimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasLimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasEqualizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesLimitsOfShape WalkingParallelPair G
inst_7 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesLimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := piObj.{w, v, u} K.obj
Q : C := piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2
s : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫
      K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2))
t : P ⟶ Q :=
  Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
I : C := equalizer s t
i : I ⟶ P := equalizer.ι s t
f : (p : J × J) × (p.1 ⟶ p.2)
⊢ Eq (α :=
    Cone.pt.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor (K ⋙ G).obj)
        (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)) ⟶
      Functor.obj.{w, v₂, w, u₂}
        (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ (K ⋙ G).obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2)
        { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
    (G.map t ≫
      NatTrans.app
        (Cone.π
          (Fan.mk (G.obj Q) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
            G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f)))
        { as := f })
    (NatTrans.app (Cone.π (Fan.mk (G.obj (piObj.{w, v, u} K.obj)) fun (j : J) ↦ G.map (Pi.π K.obj j)))
      { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 })
have dsimp : Eq (α := G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
  (CategoryStruct.comp (Y :=
      G.obj (piObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
      (G.map
        (Pi.lift fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
          limit.π (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }))
      (G.map (Pi.π (fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) f)) :
    G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
  (G.map (Pi.π K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2) :
    G.obj (piObj.{w, v, u} K.obj) ⟶ G.obj (K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2))
Tactic: dsimp [P, Q, t, Fan.mk]