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 : Functor.{v₁, v₃, u₁, u₃} J C
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
a : Quiver.Hom.unop (f.hom.op ≫ X.op.π.app j) = (Y.op.π.app j).unop
⊢ f.hom.op ≫ X.op.π.app j = Y.op.π.app j

Tactic:
apply Quiver.Hom.unop_inj

Premises used: Quiver.Hom.unop_inj
-- 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
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
a : Eq (α := F.obj (unop j) ⟶ Y.pt) (X.ι.app (unop j) ≫ f.hom) (Y.ι.app (unop j))
⊢ Quiver.Hom.unop (f.hom.op ≫ X.op.π.app j) = (Y.op.π.app j).unop

Tactic:
dsimp
-- 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
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ Eq (α := F.obj (unop j) ⟶ Y.pt) (X.ι.app (unop j) ≫ f.hom) (Y.ι.app (unop j))

Tactic:
apply CoconeMorphism.w

Premises used: CategoryTheory.Limits.CoconeMorphism.w
-- 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
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
a : Eq (α := (unop Y).pt ⟶ op (F.obj j)) (f.unop.hom ≫ (unop X).π.app (op j)) ((unop Y).π.app (op j))
⊢ ((unop X).unop.ι.app j ≫ f.unop.hom.unop).op = ((unop Y).unop.ι.app j).op

Tactic:
dsimp
-- 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
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ Eq (α := (unop Y).pt ⟶ op (F.obj j)) (f.unop.hom ≫ (unop X).π.app (op j)) ((unop Y).π.app (op j))

Tactic:
apply ConeMorphism.w

Premises used: CategoryTheory.Limits.ConeMorphism.w
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
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
⊢ 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

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
rw : s.π.app (Classical.arbitrary J) = s.π.app 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

Tactic:
rw [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Connected
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 x x_1 : J
f : x ⟶ x_1
⊢ s.π.app x = s.π.app x_1

Tactic:
simpa using s.w f

Premises used: CategoryTheory.Limits.Cone.w
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
⊢ s.π.app (Classical.arbitrary J) = s.π.app j

Tactic:
exact constant_of_preserves_morphisms _
      (fun _ _ f ↦ by simpa using s.w f) _ _

Premises used: CategoryTheory.constant_of_preserves_morphisms
-- Module: Mathlib.CategoryTheory.Limits.Connected
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)
m : s.pt ⟶ Cone.pt.{v₁, v₂, u₁, u₂} (constCone J X)
hm : ∀ (j : J), m ≫ NatTrans.app (Cone.π (constCone J X)) j = s.π.app j
⊢ m = s.π.app (Classical.arbitrary J)

Tactic:
simpa using hm (Classical.arbitrary _)

Premises used: Classical.arbitrary
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
dsimp : 𝟙 X ≫ s.ι.app (Classical.arbitrary J) = s.ι.app 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

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
rw : s.ι.app (Classical.arbitrary J) = s.ι.app j
⊢ 𝟙 X ≫ s.ι.app (Classical.arbitrary J) = s.ι.app j

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Connected
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 x x_1 : J
f : x ⟶ x_1
⊢ s.ι.app x = s.ι.app x_1

Tactic:
simpa using (s.w f).symm

Premises used: CategoryTheory.Limits.Cocone.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
⊢ s.ι.app (Classical.arbitrary J) = s.ι.app j

Tactic:
exact constant_of_preserves_morphisms _
      (fun _ _ f ↦ by simpa using (s.w f).symm) _ _

Premises used: CategoryTheory.constant_of_preserves_morphisms
-- Module: Mathlib.CategoryTheory.Limits.Connected
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)
m : Cocone.pt.{v₁, v₂, u₁, u₂} (constCocone J X) ⟶ s.pt
hm : ∀ (j : J), NatTrans.app (Cocone.ι (constCocone J X)) j ≫ m = s.ι.app j
⊢ m = s.ι.app (Classical.arbitrary J)

Tactic:
simpa using hm (Classical.arbitrary _)

Premises used: Classical.arbitrary
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
⊢ HasLimit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) X)

Tactic:
⟨_, isLimitConstCone J X⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.isLimitConstCone, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
⊢ HasColimit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) X)

Tactic:
⟨_, isColimitConstCocone J X⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.isColimitConstCocone
-- Module: Mathlib.CategoryTheory.Limits.Connected
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.π)
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
⊢ IsLimit c

Tactic:
refine IsLimit.ofIsoLimit (limit.isLimit _) (Cone.ext ((asIso (limMap c.π)).symm ≪≫
    (limit.isLimit _).conePointUniqueUpToIso (isLimitConstCone J c.pt)) ?_)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso, CategoryTheory.Limits.Cone.pt, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Iso.trans, CategoryTheory.Limits.isLimitConstCone, CategoryTheory.Iso.symm, CategoryTheory.Limits.limMap, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.asIso, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
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)
⊢ (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:
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_π]

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Category.assoc, CategoryTheory.Iso.symm_hom, CategoryTheory.IsIso.eq_inv_comp, CategoryTheory.asIso_inv, CategoryTheory.Limits.limit.cone_x, CategoryTheory.Limits.limit.cone_π, CategoryTheory.Iso.trans_hom, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
e_a :
  Eq.{v₂ + 1} (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ c.pt)
    (limit.π (Functor.obj (Functor.const J) c.pt) j)
    (Iso.hom
      (IsLimit.conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt)))
⊢ 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:
congr 1
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
⊢ Eq.{v₂ + 1} (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ c.pt)
    (limit.π (Functor.obj (Functor.const J) c.pt) j)
    (Iso.hom
      (IsLimit.conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt)))

Tactic:
simp [← Iso.inv_comp_eq_id]

Premises used: CategoryTheory.Iso.inv_comp_eq_id
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
this :
  Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ limit F) (limMap c.π)
    (Iso.hom
      (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
        hc.conePointUniqueUpToIso (limit.isLimit F)))
rw :
  IsIso (X := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Y := limit F)
    (Iso.hom
      (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
        hc.conePointUniqueUpToIso (limit.isLimit F)))
⊢ IsIso (X := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Y := limit F) (limMap c.π)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
this :
  Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ limit F) (limMap c.π)
    (Iso.hom
      (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
        hc.conePointUniqueUpToIso (limit.isLimit F)))
⊢ IsIso (X := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Y := limit F)
    (Iso.hom
      (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
        hc.conePointUniqueUpToIso (limit.isLimit F)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
suffices :
  Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ limit F) (limMap c.π)
    (Iso.hom
      (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
        hc.conePointUniqueUpToIso (limit.isLimit F)))
⊢ IsIso (X := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Y := limit F) (limMap c.π)

Tactic:
suffices limMap c.π = ((limit.isLimit _).conePointUniqueUpToIso (isLimitConstCone J c.pt) ≪≫
      hc.conePointUniqueUpToIso (limit.isLimit _)).hom by
    rw [this]; infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
w :
  ∀ (j : J),
    Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ F.obj j)
      (CategoryStruct.comp (Y := limit F) (limMap c.π) (limit.π F j))
      (CategoryStruct.comp (Y := limit F)
        (Iso.hom
          (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
            hc.conePointUniqueUpToIso (limit.isLimit F)))
        (limit.π F j))
⊢ Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ limit F) (limMap c.π)
    (Iso.hom
      (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
        hc.conePointUniqueUpToIso (limit.isLimit F)))

Tactic:
ext j
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
j : J
w :
  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 (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt)) ≫
      c.π.app j)
⊢ Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ F.obj j)
    (CategoryStruct.comp (Y := limit F) (limMap c.π) (limit.π F j))
    (CategoryStruct.comp (Y := limit F)
      (Iso.hom
        (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
          hc.conePointUniqueUpToIso (limit.isLimit F)))
      (limit.π F j))

Tactic:
simp only [limMap_π, Functor.const_obj_obj, limit.cone_x, constCone_pt, Iso.trans_hom, assoc,
    limit.conePointUniqueUpToIso_hom_comp]

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Category.assoc, CategoryTheory.Limits.constCone_pt, CategoryTheory.Limits.limit.cone_x, CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Iso.trans_hom, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
j : J
w :
  Eq.{v₂ + 1} (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ c.pt)
    (limit.π (Functor.obj (Functor.const J) c.pt) j)
    (Iso.hom (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt)))
⊢ 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 (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt)) ≫
      c.π.app j)

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
j : J
⊢ Eq.{v₂ + 1} (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ c.pt)
    (limit.π (Functor.obj (Functor.const J) c.pt) j)
    (Iso.hom (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt)))

Tactic:
simp [← Iso.inv_comp_eq_id]

Premises used: CategoryTheory.Iso.inv_comp_eq_id
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
⊢ Nonempty (IsLimit c) ↔
    IsIso (X := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Y := limit F) (limMap c.π)

Tactic:
⟨fun ⟨h⟩ => IsLimit.isIso_limMap_π h, fun _ => ⟨c.isLimitOfIsIsoLimMapπ⟩⟩

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.IsIso, _private.0.CategoryTheory.Limits.Cone.isLimit_iff_isIso_limMap_π.match_1, Nonempty.intro, CategoryTheory.Limits.IsLimit.isIso_limMap_π, Iff.intro, CategoryTheory.Limits.limMap, CategoryTheory.Limits.Cone.isLimitOfIsIsoLimMapπ
-- Module: Mathlib.CategoryTheory.Limits.Connected
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 : HasColimit F
c : Cocone F
inst_4 : IsIso (X := colimit F) (Y := colimit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (colimMap c.ι)
⊢ ∀ (j : J),
    (colimit.cocone F).ι.app j ≫
        Iso.hom
          (Iso.trans (Y := colimit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (asIso (colimMap c.ι))
            (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (Functor.obj (Functor.const J) c.pt))
              (isColimitConstCocone J c.pt))) =
      c.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasColimit F
c : Cocone F
⊢ Nonempty (IsColimit c) ↔
    IsIso (X := colimit F) (Y := colimit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (colimMap c.ι)

Tactic:
⟨fun ⟨h⟩ => IsColimit.isIso_colimMap_ι h, fun _ => ⟨c.isColimitOfIsIsoColimMapι⟩⟩

Premises used: _private.0.CategoryTheory.Limits.Cocone.isColimit_iff_isIso_colimMap_ι.match_1, CategoryTheory.IsIso, CategoryTheory.Limits.IsColimit.isIso_colimMap_ι, Nonempty.intro, CategoryTheory.Limits.Cocone.isColimitOfIsIsoColimMapι, CategoryTheory.Limits.Cocone.ι, Iff.intro, CategoryTheory.Limits.colimMap
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type v₁
h :
  ∀ (p : Set (WidePullbackShape J)),
    none ∈ p → (∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : WidePullbackShape J), j ∈ p
j₀ : WidePullbackShape J
⊢ IsConnected.{v₁, v₁} (WidePullbackShape J)

Tactic:
apply IsConnected.of_induct

Premises used: CategoryTheory.IsConnected.of_induct
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type v₁
p : Set (WidePullbackShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : WidePullbackShape J
h : none ∈ p
h₁ : ∀ (val : J), some val ∈ p
⊢ j ∈ p

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type v₁
p : Set (WidePullbackShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ none ∈ p

Tactic:
hp
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type v₁
p : Set (WidePullbackShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ none ∈ p

Tactic:
exact hp
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type v₁
p : Set (WidePullbackShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
val : J
h h₁ h₂ h₃ : none ∈ p
⊢ some val ∈ p

Tactic:
rwa [t (WidePullbackShape.Hom.term _)]

Premises used: CategoryTheory.Limits.WidePullbackShape.Hom.term
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type v₁
h :
  ∀ (p : Set (WidePushoutShape J)),
    none ∈ p → (∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : WidePushoutShape J), j ∈ p
j₀ : WidePushoutShape J
⊢ IsConnected.{v₁, v₁} (WidePushoutShape J)

Tactic:
apply IsConnected.of_induct

Premises used: CategoryTheory.IsConnected.of_induct
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type v₁
p : Set (WidePushoutShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : WidePushoutShape J
h : none ∈ p
h₁ : ∀ (val : J), some val ∈ p
⊢ j ∈ p

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type v₁
p : Set (WidePushoutShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ none ∈ p

Tactic:
hp
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type v₁
p : Set (WidePushoutShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ none ∈ p

Tactic:
exact hp
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
J : Type v₁
p : Set (WidePushoutShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
val : J
h h₁ h₂ h₃ : none ∈ p
⊢ some val ∈ p

Tactic:
rwa [← t (WidePushoutShape.Hom.init _)]

Premises used: CategoryTheory.Limits.WidePushoutShape.Hom.init