awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
inst_3 : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
apply : IsColimit ((Cocone.precompose (K.isoWhiskerLeft h).hom).obj c)
⊢ IsColimit.{w', v₂, w, u₂} (J := J) (F := K ⋙ F)
    (F.mapCocone
      (liftColimit.{w', w, v₁, v₂, u₁, u₂} (D := D) (F := F) (c := (Cocone.precompose (K.isoWhiskerLeft h).hom).obj c)
        (((IsColimit.precomposeHomEquiv (K.isoWhiskerLeft h) c).symm :
            (a : IsColimit c) → IsColimit ((Cocone.precompose (K.isoWhiskerLeft h).hom).obj c))
          t)))

Tactic:
apply IsColimit.ofIsoColimit _ (liftedColimitMapsToOriginal _).symm

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Iso.symm, CategoryTheory.liftedColimitMapsToOriginal
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
inst_3 : CreatesColimit K F
c : Cocone (K ⋙ G)
t : IsColimit c
⊢ IsColimit ((Cocone.precompose (K.isoWhiskerLeft h).hom).obj c)

Tactic:
apply (IsColimit.precomposeHomEquiv _ _).symm t

Premises used: Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 : Functor.{w', v₁, w, u₁} J C
J' : Type w₁
inst_3 : Category.{w'₁, w₁} J'
e : Equivalence.{w', w'₁, w, w₁} J J'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : CreatesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w'₁, v₁, w₁, u₁} J' C
c : Cocone (K ⋙ F)
hc : IsColimit c
inner : obj (Equivalence.inverse (Cocone.whiskeringEquivalence e))
    (F.mapCocone (liftColimit (hc.whiskerEquivalence e))) ≅
  obj (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (Cocone.whisker e.functor c) :=
  mapIso (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (liftedColimitMapsToOriginal (hc.whiskerEquivalence e))
refine :
  F.mapCocone (obj (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (liftColimit (hc.whiskerEquivalence e))) ≅
    obj (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (F.mapCocone (liftColimit (hc.whiskerEquivalence e)))
⊢ F.mapCocone (obj (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (liftColimit (hc.whiskerEquivalence e))) ≅ c

Tactic:
refine ?_ ≪≫ inner ≪≫ ((Cocone.whiskeringEquivalence e).unitIso.app c).symm

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.Limits.Cocone.whiskeringEquivalence, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 : Functor.{w', v₁, w, u₁} J C
J' : Type w₁
inst_3 : Category.{w'₁, w₁} J'
e : Equivalence.{w', w'₁, w, w₁} J J'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : CreatesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w'₁, v₁, w₁, u₁} J' C
c : Cocone (K ⋙ F)
hc : IsColimit c
inner : obj (Equivalence.inverse (Cocone.whiskeringEquivalence e))
    (F.mapCocone (liftColimit (hc.whiskerEquivalence e))) ≅
  obj (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (Cocone.whisker e.functor c) :=
  mapIso (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (liftedColimitMapsToOriginal (hc.whiskerEquivalence e))
⊢ F.mapCocone (obj (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (liftColimit (hc.whiskerEquivalence e))) ≅
    obj (Equivalence.inverse (Cocone.whiskeringEquivalence e)) (F.mapCocone (liftColimit (hc.whiskerEquivalence e)))

Tactic:
exact Cocone.ext (Iso.refl _)

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : CreatesLimit K F
inst_4 : CreatesLimit (K ⋙ F) G
c : Cone (K ⋙ F ⋙ G)
t : IsLimit c
c' : Cone ((K ⋙ F) ⋙ G) := c
t' : IsLimit c' := t
⊢ LiftableCone K (F ⋙ G) c

Tactic:
exact
      { liftedCone := liftLimit (liftedLimitIsLimit t')
        validLift := (Cone.functoriality (K ⋙ F) G).mapIso
            (liftedLimitMapsToOriginal (liftedLimitIsLimit t')) ≪≫
          liftedLimitMapsToOriginal t' }
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
⊢ ∀ (j j' : I) (f : j ⟶ j'),
    Eq (α := (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj j'))
      ((hom (FC := TypeCat.Fun) (((F ⋙ π A) ⋙ A).map f) :
            (a : (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj j)) → (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj j'))
          ((fun (i : I) ↦ (F.obj i).snd (β := fun (c : C) ↦ A.obj c)) j) :
        (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj j'))
      ((fun (i : I) ↦ (F.obj i).snd (β := fun (c : C) ↦ A.obj c)) j' :
        A.obj ((F.obj j').fst (β := fun (c : C) ↦ A.obj c)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
i : I
⊢ (hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) : (a : limit ((F ⋙ π A) ⋙ A)) → A.obj (F.obj i).fst)
      (liftedConeElement' F : limit ((F ⋙ π A) ⋙ A)) =
    (F.obj i).snd (β := fun (c : C) ↦ A.obj c)

Tactic:
Types.Limit.π_mk _ _ _ _

Premises used: CategoryTheory.Limits.Types.Limit.π_mk, CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement'
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
c : Cone F
a :
  Eq (α := limit ((F ⋙ π A) ⋙ A))
    (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
          (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
        ((@hom _ types TypeCat.Fun _ _ _ _ _ (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
              (a : A.obj c.pt.fst) → A.obj (limit (F ⋙ π A)))
            (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
          A.obj (limit (F ⋙ π A))) :
      limit ((F ⋙ π A) ⋙ A))
    (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
          (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
        (liftedConeElement F : A.obj (limit (F ⋙ π A))) :
      limit ((F ⋙ π A) ⋙ A))
⊢ Eq (α := A.obj (limit (F ⋙ π A)))
    ((@hom _ types TypeCat.Fun _ _ _ _ _ (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
          (a : A.obj c.pt.fst) → A.obj (limit (F ⋙ π A)))
        (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
      A.obj (limit (F ⋙ π A)))
    (liftedConeElement F : A.obj (limit (F ⋙ π A)))

Tactic:
apply (preservesLimitIso A (F ⋙ π A)).toEquiv.injective

Premises used: CategoryTheory.Iso.toEquiv, CategoryTheory.Functor.comp, CategoryTheory.CategoryOfElements.π, CategoryTheory.preservesLimitIso, Equiv.injective
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
c : Cone F
a :
  ∀ (i : I),
    Eq (α := (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
      ((hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) :
            (a : (fun (X : Type w) ↦ X) (limit ((F ⋙ π A) ⋙ A))) → (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
          (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
                (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
              ((@hom _ types TypeCat.Fun _ _ _ _ _ (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
                    (a : A.obj c.pt.fst) → A.obj (limit (F ⋙ π A)))
                  (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
                A.obj (limit (F ⋙ π A))) :
            limit ((F ⋙ π A) ⋙ A)) :
        (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
      ((hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) :
            (a : (fun (X : Type w) ↦ X) (limit ((F ⋙ π A) ⋙ A))) → (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
          (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
                (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
              (liftedConeElement F : A.obj (limit (F ⋙ π A))) :
            limit ((F ⋙ π A) ⋙ A)) :
        (fun (X : Type w) ↦ X) (((F ⋙ π A) ⋙ A).obj i))
⊢ Eq (α := limit ((F ⋙ π A) ⋙ A))
    (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
          (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
        ((@hom _ types TypeCat.Fun _ _ _ _ _ (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
              (a : A.obj c.pt.fst) → A.obj (limit (F ⋙ π A)))
            (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
          A.obj (limit (F ⋙ π A))) :
      limit ((F ⋙ π A) ⋙ A))
    (((Iso.toEquiv (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ≃ limit ((F ⋙ π A) ⋙ A)) :
          (a : A.obj (limit (F ⋙ π A))) → limit ((F ⋙ π A) ⋙ A))
        (liftedConeElement F : A.obj (limit (F ⋙ π A))) :
      limit ((F ⋙ π A) ⋙ A))

Tactic:
ext i
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
c : Cone F
i : I
⊢ Eq (α := ((F ⋙ π A) ⋙ A).obj i)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := limit ((F ⋙ π A) ⋙ A))
              (Iso.hom (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ⟶ limit ((F ⋙ π A) ⋙ A))
              (limit.π ((F ⋙ π A) ⋙ A) i : limit ((F ⋙ π A) ⋙ A) ⟶ ((F ⋙ π A) ⋙ A).obj i)) :
          (a : A.obj (limit (F ⋙ π A))) → ((F ⋙ π A) ⋙ A).obj i)
        ((hom (FC := TypeCat.Fun) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
              (a : (fun (X : Type w) ↦ X) (A.obj ((π A).mapCone c).pt)) →
                (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A))))
            (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
          (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A)))) :
      ((F ⋙ π A) ⋙ A).obj i)
    ((hom (FC := TypeCat.Fun) (A.map (limit.π (F ⋙ π A) i)) : (a : A.obj (limit (F ⋙ π A))) → ((F ⋙ π A) ⋙ A).obj i)
        ((hom (FC := TypeCat.Fun) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
              (a : (fun (X : Type w) ↦ X) (A.obj ((π A).mapCone c).pt)) →
                (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A))))
            (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
          (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A)))) :
      ((F ⋙ π A) ⋙ A).obj i)

Tactic:
have h₁ := congr_hom (preservesLimitIso_hom_π A (F ⋙ π A) i)
    (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
c : Cone F
i : I
h₁ :
  Eq (α := ((F ⋙ π A) ⋙ A).obj i)
    ((hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := limit ((F ⋙ π A) ⋙ A))
              (Iso.hom (preservesLimitIso A (F ⋙ π A)) : A.obj (limit (F ⋙ π A)) ⟶ limit ((F ⋙ π A) ⋙ A))
              (limit.π ((F ⋙ π A) ⋙ A) i : limit ((F ⋙ π A) ⋙ A) ⟶ ((F ⋙ π A) ⋙ A).obj i)) :
          (a : A.obj (limit (F ⋙ π A))) → ((F ⋙ π A) ⋙ A).obj i)
        ((hom (FC := TypeCat.Fun) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
              (a : (fun (X : Type w) ↦ X) (A.obj ((π A).mapCone c).pt)) →
                (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A))))
            (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
          (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A)))) :
      ((F ⋙ π A) ⋙ A).obj i)
    ((hom (FC := TypeCat.Fun) (A.map (limit.π (F ⋙ π A) i)) : (a : A.obj (limit (F ⋙ π A))) → ((F ⋙ π A) ⋙ A).obj i)
        ((hom (FC := TypeCat.Fun) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c))) :
              (a : (fun (X : Type w) ↦ X) (A.obj ((π A).mapCone c).pt)) →
                (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A))))
            (c.pt.snd (β := fun (c : C) ↦ A.obj c)) :
          (fun (X : Type w) ↦ X) (A.obj (limit (F ⋙ π A)))) :
      ((F ⋙ π A) ⋙ A).obj i)
⊢ (hom (FC := TypeCat.Fun) (A.map (↑(c.π.app i) : (((Functor.const I).obj c.pt).obj i).fst ⟶ (F.obj i).fst)) :
        (a : (fun (X : Type w) ↦ X) (A.obj (((Functor.const I).obj c.pt).obj i).fst)) →
          (fun (X : Type w) ↦ X) (A.obj (F.obj i).fst))
      ((Functor.obj (Functor.obj (Functor.const I) c.pt) i).snd (β := fun (c : C) ↦ A.obj c)) =
    (F.obj i).snd (β := fun (c : C) ↦ A.obj c)

Tactic:
have h₂ := (c.π.app i).property
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
i : I
⊢ Eq (α := A.obj ((F ⋙ π A).obj i))
    (((hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := A.obj (limit (F ⋙ π A))) (Iso.inv (preservesLimitIso A (F ⋙ π A)))
                (A.map (limit.π (F ⋙ π A) i))) :
            TypeCat.Fun (limit ((F ⋙ π A) ⋙ A)) (A.obj ((F ⋙ π A).obj i))) :
          (a : limit ((F ⋙ π A) ⋙ A)) → A.obj ((F ⋙ π A).obj i))
        (liftedConeElement' F : limit ((F ⋙ π A) ⋙ A)) :
      A.obj ((F ⋙ π A).obj i))
    ((hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) : (a : limit ((F ⋙ π A) ⋙ A)) → A.obj ((F ⋙ π A).obj i))
        (liftedConeElement' F : limit ((F ⋙ π A) ⋙ A)) :
      A.obj ((F ⋙ π A).obj i))

Tactic:
have := congr_hom
    (preservesLimitIso_inv_π A (F ⋙ π A) i) (liftedConeElement' F)
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
i : I
this :
  Eq (α := A.obj ((F ⋙ π A).obj i))
    (((hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := A.obj (limit (F ⋙ π A))) (Iso.inv (preservesLimitIso A (F ⋙ π A)))
                (A.map (limit.π (F ⋙ π A) i))) :
            TypeCat.Fun (limit ((F ⋙ π A) ⋙ A)) (A.obj ((F ⋙ π A).obj i))) :
          (a : limit ((F ⋙ π A) ⋙ A)) → A.obj ((F ⋙ π A).obj i))
        (liftedConeElement' F : limit ((F ⋙ π A) ⋙ A)) :
      A.obj ((F ⋙ π A).obj i))
    ((hom (FC := TypeCat.Fun) (limit.π ((F ⋙ π A) ⋙ A) i) : (a : limit ((F ⋙ π A) ⋙ A)) → A.obj ((F ⋙ π A).obj i))
        (liftedConeElement' F : limit ((F ⋙ π A) ⋙ A)) :
      A.obj ((F ⋙ π A).obj i))
⊢ (hom (FC := TypeCat.Fun) (A.map (limit.π (F ⋙ π A) i)) : (a : A.obj (limit (F ⋙ π A))) → A.obj (F.obj i).fst)
      (liftedConeElement F : A.obj (limit (F ⋙ π A))) =
    (F.obj i).snd (β := fun (c : C) ↦ A.obj c)

Tactic:
simp [liftedConeElement, ← comp_apply]

Premises used: CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement, CategoryTheory.comp_apply
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
i : I
⊢ (hom (FC := TypeCat.Fun) (A.map (limit.π (F ⋙ π A) i)) :
        (a :
            (fun (X : Type w) ↦ X) (A.obj (((Functor.const I).obj ⟨limit (F ⋙ π A), liftedConeElement F⟩).obj i).fst)) →
          (fun (X : Type w) ↦ X) (A.obj (F.obj i).fst))
      ((Functor.obj
            (Functor.obj (Functor.const I)
              (Sigma.mk (β := fun (c : C) ↦ A.obj c) (limit (F ⋙ π A)) (liftedConeElement F : A.obj (limit (F ⋙ π A)))))
            i).snd
        (β := fun (c : C) ↦ A.obj c)) =
    (F.obj i).snd (β := fun (c : C) ↦ A.obj c)

Tactic:
simpa using map_π_liftedConeElement _ _

Premises used: CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_π_liftedConeElement
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
s : Cone F
⊢ ((@hom _ types TypeCat.Fun _ _ _ _ _ (A.map (limit.lift (F ⋙ π A) ((π A).mapCone s))) :
          TypeCat.Fun (A.obj (s.pt.fst (β := fun (c : C) ↦ A.obj c)))
            (A.obj ((liftedCone F).pt.fst (β := fun (c : C) ↦ A.obj c)))) :
        (a : (fun (X : Type w) ↦ X) (A.obj s.pt.fst)) → (fun (X : Type w) ↦ X) (A.obj (liftedCone F).pt.fst))
      (s.pt.snd (β := fun (c : C) ↦ A.obj c)) =
    (liftedCone F).pt.snd (β := fun (c : C) ↦ A.obj c)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
F : I ⥤ A.Elements
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
s : Cone F
m : s.pt ⟶ (liftedCone F).pt
h : ∀ (j : I), m ≫ (liftedCone F).π.app j = s.π.app j
i : I
⊢ (↑m : s.pt.fst ⟶ (liftedCone F).pt.fst) ≫ limit.π (F ⋙ π A) i =
    CategoryStruct.comp (Y := limit (F ⋙ π A))
      (↑(Subtype.mk (p :=
            fun (f : s.pt.fst (β := fun (c : C) ↦ A.obj c) ⟶ (liftedCone F).pt.fst (β := fun (c : C) ↦ A.obj c)) ↦
            (hom (FC := TypeCat.Fun) (A.map f) :
                  (a : (fun (X : Type w) ↦ X) (A.obj s.pt.fst)) → (fun (X : Type w) ↦ X) (A.obj (liftedCone F).pt.fst))
                (s.pt.snd (β := fun (c : C) ↦ A.obj c)) =
              (liftedCone F).pt.snd (β := fun (c : C) ↦ A.obj c))
            (limit.lift (F ⋙ π A) ((π A).mapCone s)) ⋯) :
        s.pt.fst ⟶ (liftedCone F).pt.fst)
      (limit.π (F ⋙ π A) i)

Tactic:
simpa using congrArg Subtype.val (h i)

Premises used: congrArg, Subtype.val
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
⊢ HasLimitsOfShape I A.Elements

Tactic:
hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape (π A)

Premises used: CategoryTheory.CategoryOfElements.π, CategoryTheory.hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
F : Functor.{v, u_1, u, u_1 + 1} Cᵒᵖ (Type u_1)
inst_5 : F.IsRepresentable
⊢ HasInitial F.Elements

Tactic:
(Functor.Elements.isInitialOfRepresentableBy F.representableBy).hasInitial

Premises used: CategoryTheory.Limits.IsInitial.hasInitial, CategoryTheory.Functor.Elements.isInitialOfRepresentableBy, CategoryTheory.Functor.representableBy
-- Module: Mathlib.CategoryTheory.Limits.Elements
Goal:
C : Type u
inst : Category.{v, u} C
A : Functor.{v, w, u, w + 1} C (Type w)
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : Small.{w, u₁} I
inst_3 : HasLimitsOfShape.{v₁, u₁, v, u} I C
inst_4 : PreservesLimitsOfShape.{v₁, u₁, v, w, u, w + 1} I A
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
inst_5 : F.IsCorepresentable
⊢ HasInitial F.Elements

Tactic:
(Functor.Elements.isInitialOfCorepresentableBy F.corepresentableBy).hasInitial

Premises used: CategoryTheory.Functor.Elements.isInitialOfCorepresentableBy, CategoryTheory.Limits.IsInitial.hasInitial, CategoryTheory.Functor.corepresentableBy
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
mp : Mono f → c.fst = c.snd
mpr : c.fst = c.snd → Mono f
⊢ Mono f ↔ c.fst = c.snd

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : Mono f
⊢ c.fst = c.snd

Tactic:
simpa only [← cancel_mono f] using c.condition

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
mpr : ∀ {Z : C} (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h
⊢ Mono f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
g g' : Z ⟶ X
h : g ≫ f = g' ≫ f
mpr : ∀ (φ : Z ⟶ c.pt) (h : (φ ≫ c.fst) ≫ f = (φ ≫ c.snd) ≫ f), φ ≫ c.fst = φ ≫ c.snd
⊢ g = g'

Tactic:
obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' hc g g' h

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.lift', rfl
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
hf : c.fst = c.snd
Z : C
φ : Z ⟶ c.pt
h : (φ ≫ c.fst) ≫ f = (φ ≫ c.snd) ≫ f
mpr mpr₁ : φ ≫ c.snd = φ ≫ c.snd
⊢ φ ≫ c.fst = φ ≫ c.snd

Tactic:
rw [hf]
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
rw : c.fst = c.snd ↔ IsIso c.fst
⊢ Mono f ↔ IsIso c.fst

Tactic:
rw [mono_iff_fst_eq_snd hc]

Premises used: CategoryTheory.mono_iff_fst_eq_snd
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
mp : c.fst = c.snd → IsIso c.fst
mpr : IsIso c.fst → c.fst = c.snd
⊢ c.fst = c.snd ↔ IsIso c.fst

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
⊢ 𝟙 X ≫ f = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
mp : ∀ (φ : X ⟶ c.pt) (hφ₁ : φ ≫ c.fst = 𝟙 X) (hφ₂ : φ ≫ c.snd = 𝟙 X), IsIso c.fst
⊢ IsIso c.fst

Tactic:
obtain ⟨φ, hφ₁, hφ₂⟩ := PullbackCone.IsLimit.lift' hc (𝟙 X) (𝟙 X) (by simp)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.PullbackCone.IsLimit.lift'
-- Module: Mathlib.CategoryTheory.Limits.EpiMono
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h : c.fst = c.snd
φ : X ⟶ c.pt
hφ₁ : φ ≫ c.fst = 𝟙 X
hφ₂ : φ ≫ c.snd = 𝟙 X
⊢ IsIso c.fst

Tactic:
⟨φ, PullbackCone.IsLimit.hom_ext hc ?_ ?_, hφ₁⟩

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext, And.intro, Exists.intro, CategoryTheory.IsIso.mk