awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
⊢ CategoryStruct.comp (Y := (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))
      (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)
      (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
        { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
          π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) }) =
    𝟙 (Cone F)
have h : ∀ (X : Cone F),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))
          (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)
          (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
            { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
              π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })))
      X =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Cone F))).toFun X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
X : Cone F
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))
          (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)
          (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
            { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
              π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })))
      X =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Cone F))).toFun X
have h : ∀ (pt : C) (π : obj (const J) pt ⟶ F),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))
          (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)
          (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
            { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
              π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })))
      { pt := pt, π := π : Cone F } =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Cone F))).toFun { pt := pt, π := π : Cone F }
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
⊢ CategoryStruct.comp (Y := Cone F)
      (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
        { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
          π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) })
      (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π) =
    𝟙 ((X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))
have h : ∀ (X : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)),
  Sigma.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Cone F)
            (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
              { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
                π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })
            (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)))
        X) =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)))).toFun X).fst (β :=
      fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
X : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)
⊢ Sigma.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Cone F)
            (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
              { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
                π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })
            (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)))
        X) =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)))).toFun X).fst (β :=
      fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)
have h : ∀ (fst : Cᵒᵖ) (snd : obj (const J) (unop fst) ⟶ F),
  Sigma.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)
      (TypeCat.Fun.toFun (X := (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F))
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Cone F)
            (↾fun (c : (X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)) ↦
              { pt := unop (c.fst (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)),
                π := c.snd (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) : Cone F })
            (↾fun (c : Cone F) ↦ Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) (op c.pt) c.π)))
        (Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) fst snd)) =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)))).toFun
          (Sigma.mk (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F) fst snd)).fst
      (β := fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F)
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
⊢ CategoryStruct.comp (Y := (X : C) × F.cocones.obj X)
      (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι)
      (↾fun (c : (X : C) × F.cocones.obj X) ↦
        { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) }) =
    𝟙 (Cocone F)
have h : ∀ (X : Cocone F),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (X : C) × F.cocones.obj X)
          (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι)
          (↾fun (c : (X : C) × F.cocones.obj X) ↦
            { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) :
              Cocone F })))
      X =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Cocone F))).toFun X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
X : Cocone F
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (X : C) × F.cocones.obj X)
          (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι)
          (↾fun (c : (X : C) × F.cocones.obj X) ↦
            { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) :
              Cocone F })))
      X =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Cocone F))).toFun X
have h : ∀ (pt : C) (ι : F ⟶ obj (const J) pt),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := (X : C) × F.cocones.obj X)
          (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι)
          (↾fun (c : (X : C) × F.cocones.obj X) ↦
            { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) :
              Cocone F })))
      { pt := pt, ι := ι : Cocone F } =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (Cocone F))).toFun { pt := pt, ι := ι : Cocone F }
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
⊢ CategoryStruct.comp (Y := Cocone F)
      (↾fun (c : (X : C) × F.cocones.obj X) ↦
        { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) })
      (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι) =
    𝟙 ((X : C) × F.cocones.obj X)
have h : ∀ (X : (X : C) × F.cocones.obj X),
  Sigma.fst (β := fun (X : C) ↦ F.cocones.obj X)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Cocone F)
            (↾fun (c : (X : C) × F.cocones.obj X) ↦
              { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) :
                Cocone F })
            (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι)))
        X) =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((X : C) × F.cocones.obj X))).toFun X).fst (β := fun (X : C) ↦
      F.cocones.obj X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
h :
  ∀ (X : (X : C) × F.cocones.obj X),
    Sigma.fst (β := fun (X : C) ↦ F.cocones.obj X)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := Cocone F)
              (↾fun (c : (X : C) × F.cocones.obj X) ↦
                { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) :
                  Cocone F })
              (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι)))
          X) =
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((X : C) × F.cocones.obj X))).toFun X).fst (β := fun (X : C) ↦
        F.cocones.obj X)
⊢ CategoryStruct.comp (Y := Cocone F)
      (↾fun (c : (X : C) × F.cocones.obj X) ↦
        { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) })
      (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι) =
    𝟙 ((X : C) × F.cocones.obj X)
have h₁ : ∀ (X : (X : C) × F.cocones.obj X),
  HEq (α :=
    F.cocones.obj
      (Sigma.fst (β := fun (X : C) ↦ F.cocones.obj X)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := Cocone F)
              (↾fun (c : (X : C) × F.cocones.obj X) ↦
                { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) :
                  Cocone F })
              (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι)))
          X)))
    (Sigma.snd (β := fun (X : C) ↦ F.cocones.obj X)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Cocone F)
            (↾fun (c : (X : C) × F.cocones.obj X) ↦
              { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) :
                Cocone F })
            (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι)))
        X))
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((X : C) × F.cocones.obj X))).toFun X).snd (β := fun (X : C) ↦
      F.cocones.obj X))
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 F : Functor.{v₁, v₃, u₁, u₃} J C
X : (X : C) × F.cocones.obj X
⊢ Sigma.fst (β := fun (X : C) ↦ F.cocones.obj X)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Cocone F)
            (↾fun (c : (X : C) × F.cocones.obj X) ↦
              { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) :
                Cocone F })
            (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι)))
        X) =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((X : C) × F.cocones.obj X))).toFun X).fst (β := fun (X : C) ↦
      F.cocones.obj X)
have h : ∀ (fst : C) (snd : F.cocones.obj fst),
  Sigma.fst (β := fun (X : C) ↦ F.cocones.obj X)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := Cocone F)
            (↾fun (c : (X : C) × F.cocones.obj X) ↦
              { pt := c.fst (β := fun (X : C) ↦ F.cocones.obj X), ι := c.snd (β := fun (X : C) ↦ F.cocones.obj X) :
                Cocone F })
            (↾fun (c : Cocone F) ↦ Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) c.pt c.ι)))
        (Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) fst snd)) =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((X : C) × F.cocones.obj X))).toFun
          (Sigma.mk (β := fun (X : C) ↦ F.cocones.obj X) fst snd)).fst
      (β := fun (X : C) ↦ F.cocones.obj X)
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
c c' : Cone F
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g
have mk : ∀ (hom : c.pt ⟶ c'.pt) (w : ∀ (j : J), hom ≫ c'.π.app j = c.π.app j)
  (w_1 : { hom := hom, w := w : ConeMorphism c c' }.hom = g.hom), { hom := hom, w := w : ConeMorphism c c' } = g
Tactic: cases f
Cleared hypotheses: f, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
c c' : Cone F
g : c ⟶ c'
hom : c.pt ⟶ c'.pt
w_1 : ∀ (j : J), hom ≫ c'.π.app j = c.π.app j
w : { hom := hom, w := w_1 : ConeMorphism c c' }.hom = g.hom
⊢ { hom := hom, w := w_1 : ConeMorphism c c' } = g
have mk : ∀ (hom_1 : c.pt ⟶ c'.pt) (w : ∀ (j : J), hom_1 ≫ c'.π.app j = c.π.app j)
  (w_2 : { hom := hom, w := w_1 : ConeMorphism c c' }.hom = { hom := hom_1, w := w }.hom),
  { hom := hom, w := w_1 : ConeMorphism c c' } = { hom := hom_1, w := w }
Tactic: cases g
Cleared hypotheses: g, w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
G F : Functor.{v₃, v₄, u₃, u₄} C D
inst_5 : F.ReflectsIsomorphisms
K : Functor.{v₁, v₃, u₁, u₃} J C
⊢ (functoriality K F).ReflectsIsomorphisms
have reflects : ∀ {A B : Cone K} (f : A ⟶ B) [IsIso ((functoriality K F).map f)], IsIso f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (hypothesis)
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
G F : Functor.{v₃, v₄, u₃, u₄} C D
inst_5 : F.ReflectsIsomorphisms
K : Functor.{v₁, v₃, u₁, u₃} J C
A B : Cone K
f : A ⟶ B
inst_6 : IsIso ((functoriality K F).map f)
⊢ IsIso f
have this : IsIso (F.map f.hom)
Tactic: haveI : IsIso (F.map f.hom) :=
    (forget (K ⋙ F)).map_isIso ((functoriality K F).map f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (hypothesis)
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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F_1 : Functor.{v₁, v₃, u₁, u₃} J C
G F : Functor.{v₃, v₄, u₃, u₄} C D
inst_5 : F.ReflectsIsomorphisms
K : Functor.{v₁, v₃, u₁, u₃} J C
A B : Cone K
f : A ⟶ B
inst_6 : IsIso ((functoriality K F).map f)
this : IsIso (F.map f.hom)
⊢ IsIso f
have this₁ : IsIso f.hom
Tactic: haveI := ReflectsIsomorphisms.reflects F f.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : Functor.{v₁, v₃, u₁, u₃} J C
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ f.hom.op ≫ X.op.π.app j = Y.op.π.app j
have a : Quiver.Hom.unop (f.hom.op ≫ X.op.π.app j) = (Y.op.π.app j).unop
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : Functor.{v₁, v₃, u₁, u₃} J C
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ Quiver.Hom.unop (f.hom.op ≫ X.op.π.app j) = (Y.op.π.app j).unop
have a : Eq (α := F.obj (unop j) ⟶ Y.pt) (X.ι.app (unop j) ≫ f.hom) (Y.ι.app (unop j))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Cones (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
D : Type u₄
inst_3 : Category.{v₄, u₄} D
E : Type u₅
inst_4 : Category.{v₅, u₅} E
F : Functor.{v₁, v₃, u₁, u₃} J C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ ((unop X).unop.ι.app j ≫ f.unop.hom.unop).op = ((unop Y).unop.ι.app j).op
have a : Eq (α := (unop Y).pt ⟶ op (F.obj j)) (f.unop.hom ≫ (unop X).π.app (op j)) ((unop Y).π.app (op j))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
X : C
inst_2 : IsConnected.{v₁, u₁} J
s : Cone.{v₁, v₂, u₁, u₂} (Functor.obj (Functor.const J) X)
j : J
⊢ CategoryStruct.comp (Y := Cone.pt.{v₁, v₂, u₁, u₂} (constCone J X))
      (s.π.app (Classical.arbitrary J) :
        Functor.obj.{v₁, v₂, u₁, u₂} (Functor.obj (Functor.const J) s.pt) (Classical.arbitrary J) ⟶
          Functor.obj.{v₁, v₂, u₁, u₂} (Functor.obj (Functor.const J) X) (Classical.arbitrary J))
      (NatTrans.app (Cone.π (constCone J X)) j) =
    s.π.app j
have dsimp : CategoryStruct.comp (Y := X)
    (s.π.app (Classical.arbitrary J) :
      Functor.obj.{v₁, v₂, u₁, u₂} (Functor.obj (Functor.const J) s.pt) (Classical.arbitrary J) ⟶
        Functor.obj.{v₁, v₂, u₁, u₂} (Functor.obj (Functor.const J) X) (Classical.arbitrary J))
    (𝟙 X) =
  s.π.app j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
X : C
inst_2 : IsConnected.{v₁, u₁} J
s : Cone.{v₁, v₂, u₁, u₂} (Functor.obj (Functor.const J) X)
j : J
⊢ CategoryStruct.comp (Y := X)
      (s.π.app (Classical.arbitrary J) :
        Functor.obj.{v₁, v₂, u₁, u₂} (Functor.obj (Functor.const J) s.pt) (Classical.arbitrary J) ⟶
          Functor.obj.{v₁, v₂, u₁, u₂} (Functor.obj (Functor.const J) X) (Classical.arbitrary J))
      (𝟙 X) =
    s.π.app j
have rw : s.π.app (Classical.arbitrary J) = s.π.app j
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
X : C
inst_2 : IsConnected.{v₁, u₁} J
s : Cocone.{v₁, v₂, u₁, u₂} (Functor.obj (Functor.const J) X)
j : J
⊢ CategoryStruct.comp (Y :=
      Functor.obj.{v₁, v₂, u₁, u₂} (Functor.obj (Functor.const J) (Cocone.pt.{v₁, v₂, u₁, u₂} (constCocone J X))) j)
      (NatTrans.app (Cocone.ι (constCocone J X)) j) (s.ι.app (Classical.arbitrary J)) =
    s.ι.app j
have dsimp : 𝟙 X ≫ s.ι.app (Classical.arbitrary J) = s.ι.app j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
X : C
inst_2 : IsConnected.{v₁, u₁} J
s : Cocone.{v₁, v₂, u₁, u₂} (Functor.obj (Functor.const J) X)
j : J
⊢ 𝟙 X ≫ s.ι.app (Classical.arbitrary J) = s.ι.app j
have rw : s.ι.app (Classical.arbitrary J) = s.ι.app j
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
X : C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
inst_4 : IsIso (X := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Y := limit F) (limMap c.π)
⊢ IsLimit c
have refine : ∀ (j : J),
  (limit.cone F).π.app j =
    Iso.hom
        (Iso.trans (Y := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Iso.symm (asIso (limMap c.π)))
          (IsLimit.conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt))
            (isLimitConstCone J c.pt))) ≫
      c.π.app j
Tactic: refine IsLimit.ofIsoLimit (limit.isLimit _) (Cone.ext ((asIso (limMap c.π)).symm ≪≫
    (limit.isLimit _).conePointUniqueUpToIso (isLimitConstCone J c.pt)) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
X : C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
inst_4 : IsIso (X := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Y := limit F) (limMap c.π)
j : J
⊢ (limit.cone F).π.app j =
    Iso.hom
        (Iso.trans (Y := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Iso.symm (asIso (limMap c.π)))
          (IsLimit.conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt))
            (isLimitConstCone J c.pt))) ≫
      c.π.app j
have simp : Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ F.obj j)
  (limit.π (Functor.obj (Functor.const J) c.pt) j ≫ c.π.app j)
  (Iso.hom
      (IsLimit.conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt)) ≫
    c.π.app j)
Tactic: simp only [limit.cone_x, Functor.const_obj_obj, limit.cone_π, Iso.trans_hom, Iso.symm_hom,
    asIso_inv, assoc, IsIso.eq_inv_comp, limMap_π]