awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : Type u₂
inst_1 : Category.{v₂, u₂} J_1
inst_2 : HasFiniteWidePushouts.{v₁, u₁} C
J : Type
h : Finite J
⊢ HasColimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J)ᵒᵖ C

Tactic:
hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePullbackShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : Type u₂
inst_1 : Category.{v₂, u₂} J_1
inst_2 : HasFiniteWidePushouts.{v₁, u₁} C
J : Type
h : Finite J
⊢ HasColimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J)ᵒᵖ C

Tactic:
exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePullbackShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ ↔ HasFiniteWidePushouts.{v₁, u₁} C

Tactic:
⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteWidePushouts.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
refine :
  ∀ (h : HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ) (J : Type),
    Finite J → HasColimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J) C
⊢ HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ ↔ HasFiniteWidePushouts.{v₁, u₁} C

Tactic:
refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ
J : Type
h_1 : Finite J
rw : HasLimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J)ᵒᵖ Cᵒᵖ
⊢ HasColimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J) C

Tactic:
rw [← hasLimitsOfShape_opposite_opposite_iff]

Premises used: CategoryTheory.Limits.hasLimitsOfShape_opposite_opposite_iff
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ
J : Type
h_1 : Finite J
⊢ HasLimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J)ᵒᵖ Cᵒᵖ

Tactic:
hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePushoutShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ
J : Type
h_1 : Finite J
⊢ HasLimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J)ᵒᵖ Cᵒᵖ

Tactic:
exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePushoutShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ ↔ HasFiniteWidePullbacks.{v₁, u₁} C

Tactic:
⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteWidePullbacks.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
refine :
  ∀ (h : HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ) (J : Type),
    Finite J → HasLimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J) C
⊢ HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ ↔ HasFiniteWidePullbacks.{v₁, u₁} C

Tactic:
refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ
J : Type
h_1 : Finite J
rw : HasColimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J)ᵒᵖ Cᵒᵖ
⊢ HasLimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J) C

Tactic:
rw [← hasColimitsOfShape_opposite_opposite_iff]

Premises used: CategoryTheory.Limits.hasColimitsOfShape_opposite_opposite_iff
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ
J : Type
h_1 : Finite J
⊢ HasColimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J)ᵒᵖ Cᵒᵖ

Tactic:
hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePullbackShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ
J : Type
h_1 : Finite J
⊢ HasColimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J)ᵒᵖ Cᵒᵖ

Tactic:
exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePullbackShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
X : C
F : J ⥤ Over.{v, u} X
i : HasColimit (F ⋙ forget X)
⊢ HasColimit F

Tactic:
CostructuredArrow.hasColimit (i₁ := i)

Premises used: CategoryTheory.Over, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.hasColimit
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
X : C
inst_2 : HasColimits.{v, u} C
⊢ HasColimits (Over.{v, u} X)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
X : C
inst_2 : HasColimits.{v, u} C
⊢ PreservesColimits (C := Over.{v, u} X) (forget X)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
X : C
⊢ ReflectsColimits (C := Over.{v, u} X) (forget X)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : HasPushouts.{v, u} C
f g : Over.{v, u} X
h : f ⟶ g
inst_2 : Epi h
⊢ Epi (Hom.left h)

Tactic:
CostructuredArrow.epi_left_of_epi _

Premises used: CategoryTheory.CostructuredArrow.epi_left_of_epi
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : HasPushouts.{v, u} C
f g : Over.{v, u} X
h : f ⟶ g
⊢ Epi h ↔ Epi (Hom.left h)

Tactic:
CostructuredArrow.epi_iff_epi_left _

Premises used: CategoryTheory.Over, CategoryTheory.Over.Hom, CategoryTheory.CostructuredArrow, CategoryTheory.CostructuredArrow.epi_iff_epi_left
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
X : C
inst_2 : HasColimitsOfSize.{w, w', v, u} C
Y : C
f : X ⟶ Y
⊢ PreservesColimitsOfSize.{w, w', v, v, max u v, max u v} (map f)

Tactic:
preservesColimits_of_reflects_of_preserves (map f) (forget Y)

Premises used: CategoryTheory.Over.map, CategoryTheory.Limits.preservesColimits_of_reflects_of_preserves, CategoryTheory.Over.forget
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
X : C
F : J ⥤ Under.{v, u} X
i : HasLimit (F ⋙ forget X)
⊢ HasLimit F

Tactic:
StructuredArrow.hasLimit (i₁ := i)

Premises used: CategoryTheory.StructuredArrow.hasLimit, CategoryTheory.StructuredArrow.Hom, CategoryTheory.Under, CategoryTheory.Under.Hom
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
X : C
inst_2 : HasLimits.{v, u} C
⊢ HasLimits (Under.{v, u} X)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasLimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : HasPullbacks.{v, u} C
f g : Under.{v, u} X
h : f ⟶ g
inst_2 : Mono h
⊢ Mono (Hom.right h)

Tactic:
StructuredArrow.mono_right_of_mono _

Premises used: CategoryTheory.StructuredArrow.mono_right_of_mono
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
inst_1 : HasPullbacks.{v, u} C
f g : Under.{v, u} X
h : f ⟶ g
⊢ Mono h ↔ Mono (Hom.right h)

Tactic:
StructuredArrow.mono_iff_mono_right _

Premises used: CategoryTheory.StructuredArrow.Hom, CategoryTheory.StructuredArrow.mono_iff_mono_right, CategoryTheory.Under, CategoryTheory.Under.Hom
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
X : C
inst_2 : HasLimits.{v, u} C
⊢ PreservesLimits (C := Under.{v, u} X) (forget X)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
X : C
⊢ ReflectsLimits (C := Under.{v, u} X) (forget X)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Over
Goal:
J : Type w
inst : Category.{w', w} J
C : Type u
inst_1 : Category.{v, u} C
X : C
inst_2 : HasLimitsOfSize.{w, w', v, u} C
Y : C
f : X ⟶ Y
⊢ PreservesLimitsOfSize.{w, w', v, v, max u v, max u v} (map f)

Tactic:
preservesLimits_of_reflects_of_preserves (map f) (forget X)

Premises used: CategoryTheory.Under.forget, CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves, CategoryTheory.Under.map
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
h :
  ∀ (i : I),
    Eq (α := Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)
      ((Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f ≫ fun (i : I) ↦ (c i).π.app j') i :
        Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)
      (((fun (i : I) ↦ (c i).π.app j) ≫ F.map f) i :
        Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j ⟶ F.obj j')
    (Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f ≫ fun (i : I) ↦ (c i).π.app j')
    ((fun (i : I) ↦ (c i).π.app j) ≫ F.map f)

Tactic:
funext i
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
i : I
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)
    ((Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f ≫ fun (i : I) ↦ (c i).π.app j') i :
      Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)
    (((fun (i : I) ↦ (c i).π.app j) ≫ F.map f) i :
      Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)

Tactic:
(c i).π.naturality f

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
i : I
⊢ Eq (α := Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)
    ((Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f ≫ fun (i : I) ↦ (c i).π.app j') i :
      Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)
    (((fun (i : I) ↦ (c i).π.app j) ≫ F.map f) i :
      Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j i ⟶ F.obj j' i)

Tactic:
exact (c i).π.naturality f

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
h :
  ∀ (i : I),
    Eq (α := F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)
      ((F.map f ≫ fun (i : I) ↦ (c i).ι.app j') i :
        F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)
      (((fun (i : I) ↦ (c i).ι.app j) ≫ Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f) i :
        F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)
⊢ Eq (α := F.obj j ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j')
    (F.map f ≫ fun (i : I) ↦ (c i).ι.app j')
    ((fun (i : I) ↦ (c i).ι.app j) ≫ Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f)

Tactic:
funext i
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
i : I
⊢ Eq (α := F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)
    ((F.map f ≫ fun (i : I) ↦ (c i).ι.app j') i :
      F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)
    (((fun (i : I) ↦ (c i).ι.app j) ≫ Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f) i :
      F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)

Tactic:
(c i).ι.naturality f

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
j j' : J
f : j ⟶ j'
i : I
⊢ Eq (α := F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)
    ((F.map f ≫ fun (i : I) ↦ (c i).ι.app j') i :
      F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)
    (((fun (i : I) ↦ (c i).ι.app j) ≫ Functor.map (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) f) i :
      F.obj j i ⟶ Functor.obj (Functor.obj (Functor.const J) fun (i : I) ↦ (c i).pt) j' i)

Tactic:
exact (c i).ι.naturality f

Premises used: CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
j : J
h :
  ∀ (i : I),
    ((fun (i : I) ↦ (P i).lift (coneCompEval (C := C) s i)) ≫ (coneOfConeCompEval (C := C) c).π.app j) i = s.π.app j i
⊢ (fun (i : I) ↦ (P i).lift (coneCompEval (C := C) s i)) ≫ (coneOfConeCompEval (C := C) c).π.app j = s.π.app j

Tactic:
funext i
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
j : J
i : I
⊢ ((fun (i : I) ↦ (P i).lift (coneCompEval (C := C) s i)) ≫ (coneOfConeCompEval (C := C) c).π.app j) i = s.π.app j i

Tactic:
(P i).fac (coneCompEval s i) j

Premises used: CategoryTheory.pi.coneCompEval, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
j : J
i : I
⊢ ((fun (i : I) ↦ (P i).lift (coneCompEval (C := C) s i)) ≫ (coneOfConeCompEval (C := C) c).π.app j) i = s.π.app j i

Tactic:
exact (P i).fac (coneCompEval s i) j

Premises used: CategoryTheory.pi.coneCompEval, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
m : s.pt ⟶ (coneOfConeCompEval (C := C) c).pt
w : ∀ (j : J), m ≫ (coneOfConeCompEval (C := C) c).π.app j = s.π.app j
h : ∀ (i : I), m i = (P i).lift (coneCompEval (C := C) s i)
⊢ m = fun (i : I) ↦ (P i).lift (coneCompEval (C := C) s i)

Tactic:
funext i
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
m : s.pt ⟶ (coneOfConeCompEval (C := C) c).pt
w : ∀ (j : J), m ≫ (coneOfConeCompEval (C := C) c).π.app j = s.π.app j
i : I
⊢ m i = (P i).lift (coneCompEval (C := C) s i)

Tactic:
(P i).uniq (coneCompEval s i) (m i) fun j => congr_fun (w j) i

Premises used: CategoryTheory.Limits.IsLimit.uniq, congr_fun, CategoryTheory.pi.coneCompEval
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cone (F ⋙ Pi.eval C i)
P : (i : I) → IsLimit (c i)
s : Cone F
m : s.pt ⟶ (coneOfConeCompEval (C := C) c).pt
w : ∀ (j : J), m ≫ (coneOfConeCompEval (C := C) c).π.app j = s.π.app j
i : I
⊢ m i = (P i).lift (coneCompEval (C := C) s i)

Tactic:
exact (P i).uniq (coneCompEval s i) (m i) fun j => congr_fun (w j) i

Premises used: CategoryTheory.Limits.IsLimit.uniq, congr_fun, CategoryTheory.pi.coneCompEval
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
j : J
h :
  ∀ (i : I),
    ((coconeOfCoconeCompEval (C := C) c).ι.app j ≫ fun (i : I) ↦ (P i).desc (coconeCompEval (C := C) s i)) i =
      s.ι.app j i
⊢ ((coconeOfCoconeCompEval (C := C) c).ι.app j ≫ fun (i : I) ↦ (P i).desc (coconeCompEval (C := C) s i)) = s.ι.app j

Tactic:
funext i
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
j : J
i : I
⊢ ((coconeOfCoconeCompEval (C := C) c).ι.app j ≫ fun (i : I) ↦ (P i).desc (coconeCompEval (C := C) s i)) i = s.ι.app j i

Tactic:
(P i).fac (coconeCompEval s i) j

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.pi.coconeCompEval
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
j : J
i : I
⊢ ((coconeOfCoconeCompEval (C := C) c).ι.app j ≫ fun (i : I) ↦ (P i).desc (coconeCompEval (C := C) s i)) i = s.ι.app j i

Tactic:
exact (P i).fac (coconeCompEval s i) j

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.pi.coconeCompEval
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
m : (coconeOfCoconeCompEval (C := C) c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeCompEval (C := C) c).ι.app j ≫ m = s.ι.app j
h : ∀ (i : I), m i = (P i).desc (coconeCompEval (C := C) s i)
⊢ m = fun (i : I) ↦ (P i).desc (coconeCompEval (C := C) s i)

Tactic:
funext i
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
m : (coconeOfCoconeCompEval (C := C) c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeCompEval (C := C) c).ι.app j ≫ m = s.ι.app j
i : I
⊢ m i = (P i).desc (coconeCompEval (C := C) s i)

Tactic:
(P i).uniq (coconeCompEval s i) (m i) fun j => congr_fun (w j) i

Premises used: CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.pi.coconeCompEval, congr_fun
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
c : (i : I) → Cocone (F ⋙ Pi.eval C i)
P : (i : I) → IsColimit (c i)
s : Cocone F
m : (coconeOfCoconeCompEval (C := C) c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeCompEval (C := C) c).ι.app j ≫ m = s.ι.app j
i : I
⊢ m i = (P i).desc (coconeCompEval (C := C) s i)

Tactic:
exact (P i).uniq (coconeCompEval s i) (m i) fun j => congr_fun (w j) i

Premises used: CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.pi.coconeCompEval, congr_fun
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
inst_2 : ∀ (i : I), HasLimit (F ⋙ Pi.eval C i)
⊢ HasLimit F

Tactic:
HasLimit.mk
    { cone := coneOfConeCompEval fun _ => limit.cone _
      isLimit := coneOfConeEvalIsLimit fun _ => limit.isLimit _ }

Premises used: CategoryTheory.Pi.eval, CategoryTheory.Functor.comp, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.pi.coneOfConeEvalIsLimit, CategoryTheory.pi.coneOfConeCompEval, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Pi
Goal:
I : Type v₁
C : I → Type u₁
inst : (i : I) → Category.{v₁, u₁} (C i)
J : Type v₁
inst_1 : SmallCategory J
F : J ⥤ ((i : I) → C i)
inst_2 : ∀ (i : I), HasColimit (F ⋙ Pi.eval C i)
⊢ HasColimit F

Tactic:
HasColimit.mk
    { cocone := coconeOfCoconeCompEval fun _ => colimit.cocone _
      isColimit := coconeOfCoconeEvalIsColimit fun _ => colimit.isColimit _ }

Premises used: CategoryTheory.pi.coconeOfCoconeCompEval, CategoryTheory.Pi.eval, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.colimit.cocone, CategoryTheory.pi.coconeOfCoconeEvalIsColimit
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cone F
x : C
this : ∀ (i : J) (p : F.obj i = x), c.pt ≤ x
⊢ x ∈ Set.range F.obj → c.pt ≤ x

Tactic:
⟨i, p⟩
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cone F
x : C
i : J
p : F.obj i = x
rw : c.pt ≤ F.obj i
⊢ c.pt ≤ x

Tactic:
rw [← p]
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cone F
x : C
i : J
p : F.obj i = x
⊢ c.pt ≤ F.obj i

Tactic:
(c.π.app i).le

Premises used: CategoryTheory.Limits.Cone.π, Quiver.Hom.le, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Preorder
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cone F
x : C
i : J
p : F.obj i = x
⊢ c.pt ≤ F.obj i

Tactic:
exact (c.π.app i).le

Premises used: CategoryTheory.Limits.Cone.π, Quiver.Hom.le, CategoryTheory.NatTrans.app