awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Cones
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)
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)
⊢ 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:
cases X
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
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:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Cones
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)
⊢ HEq (α :=
    obj (const J)
        (unop
          (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))) ⟶
      F)
    (Sigma.snd (β := 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) :
      obj (const J)
          (unop
            (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))) ⟶
        F)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 ((X : Cᵒᵖ) × (obj (const J) (unop X) ⟶ F)))).toFun X).snd (β :=
      fun (X : Cᵒᵖ) ↦ obj (const J) (unop X) ⟶ F))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Cones
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 : 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
⊢ 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)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
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 }
⊢ 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:
cases X
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
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:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Cones
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)
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))
⊢ 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)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
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)
⊢ 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:
cases X
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
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:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
⊢ 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:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
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
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
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 }
⊢ { hom := hom, w := w_1 : ConeMorphism c c' } = g

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
hom : c.pt ⟶ c'.pt
w_1 : ∀ (j : J), hom ≫ c'.π.app j = c.π.app j
hom_1 : c.pt ⟶ c'.pt
w_2 : ∀ (j : J), hom_1 ≫ c'.π.app j = c.π.app j
w : { hom := hom, w := w_1 : ConeMorphism c c' }.hom = { hom := hom_1, w := w_2 }.hom
⊢ { hom := hom, w := w_1 : ConeMorphism c c' } = { hom := hom_1, w := w_2 }

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Limits.Cones
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 d : Cone F
f : c ≅ d
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 c.pt

Tactic:
simp [← Cone.category_comp_hom]

Premises used: CategoryTheory.Limits.Cone.category_comp_hom
-- Module: Mathlib.CategoryTheory.Limits.Cones
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 d : Cone F
f : c ≅ d
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 d.pt

Tactic:
simp [← Cone.category_comp_hom]

Premises used: CategoryTheory.Limits.Cone.category_comp_hom
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
c d : Cone F
f : c ≅ d
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 c.pt ∧ f.inv.hom ≫ f.hom.hom = 𝟙 d.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
c d : Cone F
f : c ≅ d
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 d.pt ∧ f.hom.hom ≫ f.inv.hom = 𝟙 c.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Cones
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₃
inst_1 : Category.{v₃, u₃} C
D : Type u₄
inst_2 : Category.{v₄, u₄} D
F : Functor.{v₁, v₃, u₁, u₃} J C
c c' : Cone F
f : c ⟶ c'
G : Functor.{v₃, v₄, u₃, u₄} C D
j : J
⊢ G.map f.hom ≫ G.map (c'.π.app j) = G.map (c.π.app j)

Tactic:
simp [← map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
e : Equivalence.{v₂, v₁, u₂, u₁} K J
s : Cone (e.functor ⋙ F)
k : K
⊢ (((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).π.app k =
    Iso.hom
        (Iso.refl (((whiskering e.inverse ⋙ postcompose (e.invFunIdAssoc F).hom) ⋙ whiskering e.functor).obj s).pt) ≫
      (obj (𝟭 (Cone (e.functor ⋙ F))) s).π.app k

Tactic:
simpa [e.counit_app_functor] using s.w (e.unitInv.app k)

Premises used: CategoryTheory.Limits.Cone.w, CategoryTheory.Equivalence.unitInv, CategoryTheory.NatTrans.app, CategoryTheory.Equivalence.counit_app_functor
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
G : Functor.{v₃, v₄, u₃, u₄} C D
A : Cone F
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y), map (obj (const J) (G.obj A.pt)) f ≫ G.map (A.π.app Y) = G.map (A.π.app X) ≫ (F ⋙ G).map f

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
G : Functor.{v₃, v₄, u₃, u₄} C D
inst_5 : G.Full
inst_6 : G.Faithful
X Y : Cone F
t : (functoriality F G).obj X ⟶ (functoriality F G).obj Y
j : J
⊢ G.map (G.preimage t.hom ≫ Y.π.app j) = G.map (X.π.app j)

Tactic:
simpa using t.w j

Premises used: CategoryTheory.Limits.ConeMorphism.w
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
reflects : ∀ {A B : Cone K} (f : A ⟶ B) [IsIso ((functoriality K F).map f)], IsIso f
⊢ (functoriality K F).ReflectsIsomorphisms

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Cones
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
reflects : ∀ [IsIso ((functoriality K F).map f)], IsIso f
⊢ ∀ [IsIso ((functoriality K F).map f)], IsIso f

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.Cones
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.map f.hom)

Tactic:
haveI : IsIso (F.map f.hom) :=
    (forget (K ⋙ F)).map_isIso ((functoriality K F).map f)
-- Module: Mathlib.CategoryTheory.Limits.Cones
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.hom

Tactic:
haveI := ReflectsIsomorphisms.reflects F f.hom
-- Module: Mathlib.CategoryTheory.Limits.Cones
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_1 : IsIso (F.map f.hom)
this : IsIso f.hom
⊢ IsIso f

Tactic:
apply cone_iso_of_hom_iso

Premises used: CategoryTheory.Limits.Cone.cone_iso_of_hom_iso