awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
⊢ Eq (α := s.pt ⟶ s.pt)
    (CategoryStruct.comp (Y := t.pt)
        (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) :
          ((Cone.equivalenceOfReindexing e.symm w').functor.obj s).pt ⟶ t.pt)
        (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) :
          ((Cone.equivalenceOfReindexing e w).functor.obj t).pt ⟶ s.pt) :
      s.pt ⟶ s.pt)
    (𝟙 s.pt : s.pt ⟶ s.pt)
have apply : ∀ (j : J),
  CategoryStruct.comp (Y := t.pt)
        (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) :
          ((Cone.equivalenceOfReindexing e.symm w').functor.obj s).pt ⟶ t.pt)
        (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) :
          ((Cone.equivalenceOfReindexing e w).functor.obj t).pt ⟶ s.pt) ≫
      s.π.app j =
    𝟙 s.pt ≫ s.π.app j
Tactic: apply hom_ext P
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ CategoryStruct.comp (Y := t.pt)
        (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) :
          ((Cone.equivalenceOfReindexing e.symm w').functor.obj s).pt ⟶ t.pt)
        (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) :
          ((Cone.equivalenceOfReindexing e w).functor.obj t).pt ⟶ s.pt) ≫
      s.π.app j =
    𝟙 s.pt ≫ s.π.app j
have dsimp : CategoryStruct.comp (Y := t.pt)
      (Q.lift
          ((Cone.postcompose (e.inverse.whiskerLeft w.inv ≫ (e.invFunIdAssoc G).hom)).obj (Cone.whisker e.inverse s)) :
        ((Cone.postcompose (e.inverse.whiskerLeft w.inv ≫ (e.invFunIdAssoc G).hom)).obj (Cone.whisker e.inverse s)).pt ⟶
          t.pt)
      (P.lift ((Cone.postcompose w.hom).obj (Cone.whisker e.functor t)) :
        ((Cone.postcompose w.hom).obj (Cone.whisker e.functor t)).pt ⟶ s.pt) ≫
    s.π.app j =
  𝟙 s.pt ≫ s.π.app j
Tactic: dsimp [w']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ CategoryStruct.comp (Y := t.pt)
        (Q.lift
            ((Cone.postcompose (e.inverse.whiskerLeft w.inv ≫ (e.invFunIdAssoc G).hom)).obj
              (Cone.whisker e.inverse s)) :
          ((Cone.postcompose (e.inverse.whiskerLeft w.inv ≫ (e.invFunIdAssoc G).hom)).obj
                (Cone.whisker e.inverse s)).pt ⟶
            t.pt)
        (P.lift ((Cone.postcompose w.hom).obj (Cone.whisker e.functor t)) :
          ((Cone.postcompose w.hom).obj (Cone.whisker e.functor t)).pt ⟶ s.pt) ≫
      s.π.app j =
    𝟙 s.pt ≫ s.π.app j
have simp : s.π.app (e.inverse.obj (e.functor.obj j)) ≫
    w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ G.map (e.counit.app (e.functor.obj j)) ≫ w.hom.app j =
  s.π.app j
Tactic: simp only [Limits.Cone.whisker_π, Limits.Cone.postcompose_obj_π, fac, whiskerLeft_app,
        assoc, id_comp, invFunIdAssoc_hom_app, fac_assoc, NatTrans.comp_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ s.π.app (e.inverse.obj (e.functor.obj j)) ≫
      w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ G.map (e.counit.app (e.functor.obj j)) ≫ w.hom.app j =
    s.π.app j
have rw : s.π.app (e.inverse.obj (e.functor.obj j)) ≫
    w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ (e.functor ⋙ G).map (e.unitInv.app j) ≫ w.hom.app j =
  s.π.app j
Tactic: rw [counit_app_functor, ← Functor.comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ s.π.app (e.inverse.obj (e.functor.obj j)) ≫
      w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ (e.functor ⋙ G).map (e.unitInv.app j) ≫ w.hom.app j =
    s.π.app j
have l : w.hom.app j = w.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 J) j)
Tactic: have l :
        NatTrans.app w.hom j = NatTrans.app w.hom ((𝟭 J).obj j) := by dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
l : w.hom.app j = w.hom.app (obj.{v₁, v₁, u₁, u₁} (𝟭 J) j)
⊢ s.π.app (e.inverse.obj (e.functor.obj j)) ≫
      w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ (e.functor ⋙ G).map (e.unitInv.app j) ≫ w.hom.app j =
    s.π.app j
have rw : s.π.app (e.inverse.obj (e.functor.obj j)) ≫
    w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ w.hom.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.unitInv.app j) =
  s.π.app j
Tactic: rw [l, w.hom.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
F : Functor.{v₁, v₃, u₁, u₃} J C
s : Cone F
G : Functor.{v₂, v₃, u₂, u₃} K C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : Equivalence.{v₁, v₂, u₁, u₂} J K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
⊢ Eq (α := t.pt ⟶ t.pt)
    (CategoryStruct.comp (Y := s.pt)
        (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) :
          ((Cone.equivalenceOfReindexing e w).functor.obj t).pt ⟶ s.pt)
        (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) :
          ((Cone.equivalenceOfReindexing e.symm w').functor.obj s).pt ⟶ t.pt) :
      t.pt ⟶ t.pt)
    (𝟙 t.pt : t.pt ⟶ t.pt)
have apply : ∀ (j : K),
  CategoryStruct.comp (Y := s.pt)
        (P.lift ((Cone.equivalenceOfReindexing e w).functor.obj t) :
          ((Cone.equivalenceOfReindexing e w).functor.obj t).pt ⟶ s.pt)
        (Q.lift ((Cone.equivalenceOfReindexing e.symm w').functor.obj s) :
          ((Cone.equivalenceOfReindexing e.symm w').functor.obj s).pt ⟶ t.pt) ≫
      t.π.app j =
    𝟙 t.pt ≫ t.π.app j
Tactic: apply hom_ext Q
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
π : obj (const J) W ⟶ F
j j' : J
f : j ⟶ j'
⊢ Eq (α := W ⟶ F.obj j') ((fun (j : J) ↦ π.app j) j ≫ F.map f) ((fun (j : J) ↦ π.app j) j')
have h₁ : (obj.{v₁, v₃, u₁, u₃} (obj (const J) W) j ⟶ F.obj j') = (W ⟶ F.obj j') →
  Functor.map (obj (const J) W) f ≫ π.app j' = (fun (j : J) ↦ π.app j) j'
Tactic: convert! ← (π.naturality f).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
p : { p : (j : J) → W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
⊢ Functor.map (obj (const J) W) f ≫ (↑p : (j : J) → W ⟶ F.obj j) j' = (↑p : (j : J) → W ⟶ F.obj j) j ≫ F.map f
have dsimp : 𝟙 W ≫ (↑p : (j : J) → W ⟶ F.obj j) j' = (↑p : (j : J) → W ⟶ F.obj j) j ≫ F.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
h : IsLimit t
W : C
p : { p : (j : J) → W ⟶ F.obj j // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
⊢ 𝟙 W ≫ (↑p : (j : J) → W ⟶ F.obj j) j' = (↑p : (j : J) → W ⟶ F.obj j) j ≫ F.map f
have rw : (↑p : (j : J) → W ⟶ F.obj j) j' = (↑p : (j : J) → W ⟶ F.obj j) j ≫ F.map f
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
⊢ lift s ≫ t.π.app j = s.π.app j
have a : G.map (lift s ≫ t.π.app j) = G.map (s.π.app j)
Tactic: apply G.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
⊢ G.map (lift s ≫ t.π.app j) = G.map (s.π.app j)
have a : ht.lift (G.mapCone s) ≫ G.map (t.π.app j) = G.map (s.π.app j)
Tactic: rw [G.map_comp, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ m = lift s
have a : G.map m = G.map (lift s)
Tactic: apply G.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ G.map m = G.map (lift s)
have a : G.map m = ht.lift (G.mapCone s)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ G.map m = ht.lift (G.mapCone s)
have a : ∀ (j : J), G.map m ≫ (G.mapCone t).π.app j = (G.mapCone s).π.app j
Tactic: refine ht.uniq (mapCone G s) _ fun j => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t_1 t : Cone F
D : Type u₄
inst_3 : Category.{v₄, u₄} D
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_4 : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
j : J
⊢ G.map m ≫ (G.mapCone t).π.app j = (G.mapCone s).π.app j
have h₁ : (G.obj s.pt ⟶ G.obj (F.obj j)) = ((G.mapCone s).pt ⟶ (F ⋙ G).obj j) →
  G.map (m ≫ t.π.app j) = G.map m ≫ (G.mapCone t).π.app j
Tactic: convert! ← congrArg (fun f => G.map f) (w j)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K_1 : Type u₂
inst_1 : Category.{v₂, u₂} K_1
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
t_1 : Cone F_1
D : Type u₄
inst_3 : Category.{v₄, u₄} D
K : Functor.{v₁, v₃, u₁, u₃} J C
F G : Functor.{v₃, v₄, u₃, u₄} C D
h : F ≅ G
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (G.mapCone c)
have apply : IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj (G.mapCone c))
Tactic: apply postcomposeInvEquiv (isoWhiskerLeft K h :) (mapCone G c) _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cones.RepresentableBy X
s : Cone F
⊢ coneOfHom h (homOfCone h s) = s
have dsimp : { pt := s.pt,
    π :=
      (h.homEquiv : (a : s.pt ⟶ X) → (const J).obj s.pt ⟶ F)
        ((Equiv.symm h.homEquiv : (a : (const J).obj s.pt ⟶ F) → s.pt ⟶ X) s.π) } =
  s
Tactic: dsimp [coneOfHom, homOfCone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cones.RepresentableBy X
s : Cone F
s_pt : C
s_π : obj (const J) s_pt ⟶ F
⊢ { pt := { pt := s_pt, π := s_π : Cone F }.pt,
      π :=
        (h.homEquiv : (a : { pt := s_pt, π := s_π }.pt ⟶ X) → (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F)
          ((Equiv.symm h.homEquiv :
              (a : (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F) → { pt := s_pt, π := s_π }.pt ⟶ X)
            { pt := s_pt, π := s_π }.π) } =
    { pt := s_pt, π := s_π : Cone F }
have e_π : (h.homEquiv : (a : { pt := s_pt, π := s_π }.pt ⟶ X) → (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F)
    ((Equiv.symm h.homEquiv : (a : (const J).obj { pt := s_pt, π := s_π }.pt ⟶ F) → { pt := s_pt, π := s_π }.pt ⟶ X)
      { pt := s_pt, π := s_π }.π) =
  s_π
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ coneOfHom h f = (limitCone h).extend (X := Y) f
have dsimp : Eq (α := Cone F) { pt := Y, π := (h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) f }
  { pt := Y, π := Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) }
Tactic: dsimp [coneOfHom, limitCone, Cone.extend]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ Eq (α := Cone F) { pt := Y, π := (h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) f }
    { pt := Y, π := Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) }
have e_π : Eq (α := obj (const J) Y ⟶ F) ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) f : obj (const J) Y ⟶ F)
  (Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) : obj (const J) Y ⟶ F)
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
| ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) f : obj (const J) Y ⟶ F)
have rw : ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) (f ≫ 𝟙 X) : obj (const J) Y ⟶ F)
Tactic: rw [← Category.comp_id f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ Eq (α := obj (const J) Y ⟶ F) ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) f : obj (const J) Y ⟶ F)
    (Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) : obj (const J) Y ⟶ F)
have e_π : Eq (α := obj (const J) Y ⟶ F) ((h.homEquiv : (a : Y ⟶ X) → (const J).obj Y ⟶ F) (f ≫ 𝟙 X) : obj (const J) Y ⟶ F)
  (Functor.map (const J) f ≫ (h.homEquiv : (a : X ⟶ X) → (const J).obj X ⟶ F) (𝟙 X) : obj (const J) Y ⟶ F)
Tactic: conv_lhs => rw [← Category.comp_id f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cones.RepresentableBy X
s : Cone F
⊢ (limitCone h).extend (X := s.pt) (homOfCone h s) = s
have rw : (limitCone h).extend (X := (coneOfHom h (homOfCone h s)).pt) (homOfCone h (coneOfHom h (homOfCone h s))) =
  coneOfHom h (homOfCone h s)
Tactic: rw [← coneOfHom_homOfCone h s]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cones.RepresentableBy X
s : Cone F
| (limitCone h).extend (X := (coneOfHom h (homOfCone h s)).pt) (homOfCone h (coneOfHom h (homOfCone h s)))
have simp : (limitCone h).extend (X := (coneOfHom h (homOfCone h s)).pt) (homOfCone h s)
Tactic: simp only [homOfCone_coneOfHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
X : C
h : F.cones.RepresentableBy X
s : Cone F
⊢ (limitCone h).extend (X := (coneOfHom h (homOfCone h s)).pt) (homOfCone h (coneOfHom h (homOfCone h s))) =
    coneOfHom h (homOfCone h s)
have conv_lhs : (limitCone h).extend (X := (coneOfHom h (homOfCone h s)).pt) (homOfCone h s) = coneOfHom h (homOfCone h s)
Tactic: conv_lhs => simp only [homOfCone_coneOfHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
X : C
h : F.cones.RepresentableBy X
s : Cone F
j : J
⊢ homOfCone h s ≫ (limitCone h).π.app j = s.π.app j
have h₁ : (limitCone h).extend (X := s.pt) (homOfCone h s) = s
Tactic: have h := cone_fac h s
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
X : C
h_1 : F.cones.RepresentableBy X
s : Cone F
j : J
h : (limitCone h_1).extend (X := s.pt) (homOfCone h_1 s) = s
⊢ homOfCone h_1 s ≫ (limitCone h_1).π.app j = s.π.app j
have mk : ∀ (pt : C) (π : obj (const J) pt ⟶ F)
  (h :
    (limitCone h_1).extend (X := { pt := pt, π := π : Cone F }.pt) (homOfCone h_1 { pt := pt, π := π : Cone F }) =
      { pt := pt, π := π }),
  homOfCone h_1 { pt := pt, π := π } ≫ (limitCone h_1).π.app j = { pt := pt, π := π : Cone F }.π.app j
Tactic: cases s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
X : C
h_1 : F.cones.RepresentableBy X
j : J
pt : C
π : obj (const J) pt ⟶ F
h :
  (limitCone h_1).extend (X := { pt := pt, π := π : Cone F }.pt) (homOfCone h_1 { pt := pt, π := π : Cone F }) =
    { pt := pt, π := π }
⊢ homOfCone h_1 { pt := pt, π := π } ≫ (limitCone h_1).π.app j = { pt := pt, π := π : Cone F }.π.app j
have h₁ : { pt := pt, π := π : Cone F }.pt = pt
Tactic: injection h with h₁ h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (hypothesis)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
X : C
h_1 : F.cones.RepresentableBy X
j : J
pt : C
π : obj (const J) pt ⟶ F
h :
  (limitCone h_1).extend (X := { pt := pt, π := π : Cone F }.pt) (homOfCone h_1 { pt := pt, π := π : Cone F }) =
    { pt := pt, π := π }
h₁ : { pt := pt, π := π : Cone F }.pt = pt
⊢ homOfCone h_1 { pt := pt, π := π } ≫ (limitCone h_1).π.app j = { pt := pt, π := π : Cone F }.π.app j
have h₂ : Functor.map (const J) (homOfCone h_1 { pt := pt, π := π }) ≫ (limitCone h_1).π = π
Tactic: injection h with h₁ h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
X : C
h : F.cones.RepresentableBy X
j : J
pt : C
π : obj (const J) pt ⟶ F
h₁ : { pt := pt, π := π : Cone F }.pt = pt
h₂ : Functor.map (const J) (homOfCone h { pt := pt, π := π }) ≫ (limitCone h).π = π
| { pt := pt, π := π : Cone F }.π.app j
have rw : NatTrans.app
  (Cone.π
    { pt := pt,
      π := (Functor.map (const J) (homOfCone h { pt := pt, π := π }) ≫ (limitCone h).π : obj (const J) pt ⟶ F) })
  j
Tactic: rw [← h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
X : C
h : F.cones.RepresentableBy X
j : J
pt : C
π : obj (const J) pt ⟶ F
h₁ : { pt := pt, π := π : Cone F }.pt = pt
h₂ : Functor.map (const J) (homOfCone h { pt := pt, π := π }) ≫ (limitCone h).π = π
⊢ homOfCone h { pt := pt, π := π } ≫ (limitCone h).π.app j = { pt := pt, π := π : Cone F }.π.app j
have mk : Eq (α := { pt := pt, π := π : Cone F }.pt ⟶ F.obj j) (homOfCone h { pt := pt, π := π } ≫ (limitCone h).π.app j)
  (NatTrans.app
    (Cone.π
      { pt := pt,
        π := (Functor.map (const J) (homOfCone h { pt := pt, π := π }) ≫ (limitCone h).π : obj (const J) pt ⟶ F) })
    j)
Tactic: conv_rhs => rw [← h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.IsLimit (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
K : Type u₂
inst_1 : Category.{v₂, u₂} K
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₃, u₁, u₃} J C
t : Cone F
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ m = homOfCone h s
have rw : homOfCone h (coneOfHom h m) = homOfCone h s
Tactic: rw [← homOfCone_coneOfHom h m]