awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F F' : Functor.{v_1, v_3, u_5, u_1} K J
e : F ≅ F'
h : ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C), preservesColimit F G ↔ preservesColimit F' G
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C)) (preservesColimit F) (preservesColimit F')

Tactic:
ext G
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F F' : Functor.{v_1, v_3, u_5, u_1} K J
e : F ≅ F'
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesColimit F G ↔ PreservesColimit F' G

Tactic:
⟨fun h ↦ preservesColimit_of_iso_diagram _ e,
    fun h ↦ preservesColimit_of_iso_diagram _ e.symm⟩

Premises used: CategoryTheory.Limits.preservesColimit_of_iso_diagram, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F F' : Functor.{v_1, v_3, u_5, u_1} K J
e : F ≅ F'
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesColimit F G ↔ PreservesColimit F' G

Tactic:
exact ⟨fun h ↦ preservesColimit_of_iso_diagram _ e,
    fun h ↦ preservesColimit_of_iso_diagram _ e.symm⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F : Functor.{v_3, v_5, u_1, u_3} J C
⊢ preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K F ↔ PreservesLimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K F

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
h :
  ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C),
    preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔
      (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesLimit F) G
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C)) (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K)
    (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesLimit F)

Tactic:
ext G
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
G : Functor.{v_3, v_5, u_1, u_3} J C
h :
  PreservesLimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔
    ∀ (i : Functor.{v_1, v_3, u_5, u_1} K J), PreservesLimit i G
⊢ preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔
    (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesLimit F) G

Tactic:
simp only [preservesLimitsOfShape_iff, iInf_apply, preservesLimit_iff, iInf_Prop_eq]

Premises used: iInf_apply, iInf_Prop_eq, CategoryTheory.ObjectProperty.preservesLimit_iff, CategoryTheory.ObjectProperty.preservesLimitsOfShape_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesLimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔
    ∀ (i : Functor.{v_1, v_3, u_5, u_1} K J), PreservesLimit i G

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ ⟨inferInstance⟩⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesLimitsOfShape.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesLimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔
    ∀ (i : Functor.{v_1, v_3, u_5, u_1} K J), PreservesLimit i G

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨inferInstance⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_5, u_3} C
e : Equivalence.{v_1, v_2, u_5, u_6} K K'
h :
  ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C),
    preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔
      preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_2, u_6} K' G
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C)) (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K)
    (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_2, u_6} K')

Tactic:
ext G
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_5, u_3} C
e : Equivalence.{v_1, v_2, u_5, u_6} K K'
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesLimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔ PreservesLimitsOfShape.{v_2, u_6, v_3, v_5, u_1, u_3} K' G

Tactic:
⟨fun _ ↦ preservesLimitsOfShape_of_equiv e _,
    fun _ ↦ preservesLimitsOfShape_of_equiv e.symm _⟩

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, Iff.intro, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_5, u_3} C
e : Equivalence.{v_1, v_2, u_5, u_6} K K'
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesLimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔ PreservesLimitsOfShape.{v_2, u_6, v_3, v_5, u_1, u_3} K' G

Tactic:
exact ⟨fun _ ↦ preservesLimitsOfShape_of_equiv e _,
    fun _ ↦ preservesLimitsOfShape_of_equiv e.symm _⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
F : Functor.{v_3, v_5, u_1, u_3} J C
⊢ preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K F ↔
    PreservesColimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K F

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
h :
  ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C),
    preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔
      (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesColimit F) G
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C))
    (preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K)
    (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesColimit F)

Tactic:
ext G
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
G : Functor.{v_3, v_5, u_1, u_3} J C
h :
  PreservesColimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔
    ∀ (i : Functor.{v_1, v_3, u_5, u_1} K J), PreservesColimit i G
⊢ preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔
    (⨅ (F : Functor.{v_1, v_3, u_5, u_1} K J), preservesColimit F) G

Tactic:
simp only [preservesColimitsOfShape_iff, iInf_apply, preservesColimit_iff, iInf_Prop_eq]

Premises used: iInf_apply, iInf_Prop_eq, CategoryTheory.ObjectProperty.preservesColimitsOfShape_iff, CategoryTheory.ObjectProperty.preservesColimit_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesColimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔
    ∀ (i : Functor.{v_1, v_3, u_5, u_1} K J), PreservesColimit i G

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ ⟨inferInstance⟩⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.Limits.PreservesColimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_3, u_1} J
inst_2 : Category.{v_5, u_3} C
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesColimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔
    ∀ (i : Functor.{v_1, v_3, u_5, u_1} K J), PreservesColimit i G

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨inferInstance⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_5, u_3} C
e : Equivalence.{v_1, v_2, u_5, u_6} K K'
h :
  ∀ (G : Functor.{v_3, v_5, u_1, u_3} J C),
    preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G ↔
      preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_2, u_6} K' G
⊢ Eq (α := ObjectProperty (Functor.{v_3, v_5, u_1, u_3} J C))
    (preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K)
    (preservesColimitsOfShape.{v_3, u_1, v_5, u_3, v_2, u_6} K')

Tactic:
ext G
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_5, u_3} C
e : Equivalence.{v_1, v_2, u_5, u_6} K K'
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesColimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔
    PreservesColimitsOfShape.{v_2, u_6, v_3, v_5, u_1, u_3} K' G

Tactic:
⟨fun _ ↦ preservesColimitsOfShape_of_equiv e _,
    fun _ ↦ preservesColimitsOfShape_of_equiv e.symm _⟩

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, Iff.intro, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_5, u_3} C
e : Equivalence.{v_1, v_2, u_5, u_6} K K'
G : Functor.{v_3, v_5, u_1, u_3} J C
⊢ PreservesColimitsOfShape.{v_1, u_5, v_3, v_5, u_1, u_3} K G ↔
    PreservesColimitsOfShape.{v_2, u_6, v_3, v_5, u_1, u_3} K' G

Tactic:
exact ⟨fun _ ↦ preservesColimitsOfShape_of_equiv e _,
    fun _ ↦ preservesColimitsOfShape_of_equiv e.symm _⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_3, u_1} J
inst_1 : Category.{v_5, u_3} C
F : Functor.{v_3, v_5, u_1, u_3} J C
⊢ preservesFiniteLimits F ↔ PreservesFiniteLimits F

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
C : Type u_3
inst : Category.{v_3, u_1} J
inst_1 : Category.{v_5, u_3} C
F : Functor.{v_3, v_5, u_1, u_3} J C
⊢ preservesFiniteColimits F ↔ PreservesFiniteColimits F

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_4, u_2} J'
inst_4 : Category.{v_5, u_3} C
inst_5 : Category.{v_6, u_4} D
inst_6 : HasColimitsOfShape.{v_2, u_6, v_5, u_3} K' C
inst_7 : PreservesLimitsOfShape (C := Functor.{v_2, v_5, u_6, u_3} K' C) K colim
G : Functor.{v_3, v_5, u_1, u_3} J C
h : ColimitOfShape (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K) K' G
⊢ ∀ (j : K'),
    preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K
      (h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.obj j)

Tactic:
have := h.prop_diag_obj
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_4, u_2} J'
inst_4 : Category.{v_5, u_3} C
inst_5 : Category.{v_6, u_4} D
inst_6 : HasColimitsOfShape.{v_2, u_6, v_5, u_3} K' C
inst_7 : PreservesLimitsOfShape (C := Functor.{v_2, v_5, u_6, u_3} K' C) K colim
G : Functor.{v_3, v_5, u_1, u_3} J C
h : ColimitOfShape (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K) K' G
this :
  ∀ (j : K'),
    preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K
      (h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.obj j)
⊢ PreservesLimitsOfShape K
    h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.flip

Tactic:
have : PreservesLimitsOfShape K h.diag.flip := ⟨fun {F} ↦ ⟨fun {c} hc ↦
      ⟨evaluationJointlyReflectsLimits _
        (fun k' ↦ isLimitOfPreserves (h.diag.obj k') hc)⟩⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_4, u_2} J'
inst_4 : Category.{v_5, u_3} C
inst_5 : Category.{v_6, u_4} D
inst_6 : HasColimitsOfShape.{v_2, u_6, v_5, u_3} K' C
inst_7 : PreservesLimitsOfShape (C := Functor.{v_2, v_5, u_6, u_3} K' C) K colim
G : Functor.{v_3, v_5, u_1, u_3} J C
h : ColimitOfShape (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K) K' G
this_1 :
  ∀ (j : K'),
    preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K
      (h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.obj j)
this :
  PreservesLimitsOfShape K
    h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.flip
e : h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.flip ⋙ colim ≅ G :=
  NatIso.ofComponents
    (fun (j : J) ↦
      IsColimit.coconePointUniqueUpToIso
        (colimit.isColimit
          (h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.flip.obj j))
        (isColimitOfPreserves (Functor.obj (evaluation J C) j)
          h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).isColimit))
    ⋯
⊢ preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G

Tactic:
preservesLimitsOfShape_of_natIso e

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_natIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_4, u_2} J'
inst_4 : Category.{v_5, u_3} C
inst_5 : Category.{v_6, u_4} D
inst_6 : HasColimitsOfShape.{v_2, u_6, v_5, u_3} K' C
inst_7 : PreservesLimitsOfShape (C := Functor.{v_2, v_5, u_6, u_3} K' C) K colim
G : Functor.{v_3, v_5, u_1, u_3} J C
h : ColimitOfShape (preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K) K' G
this_1 :
  ∀ (j : K'),
    preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K
      (h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.obj j)
this :
  PreservesLimitsOfShape K
    h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.flip
e : h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.flip ⋙ colim ≅ G :=
  NatIso.ofComponents
    (fun (j : J) ↦
      IsColimit.coconePointUniqueUpToIso
        (colimit.isColimit
          (h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).diag.flip.obj j))
        (isColimitOfPreserves (Functor.obj (evaluation J C) j)
          h.toColimitPresentation (P := preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K).isColimit))
    ⋯
⊢ preservesLimitsOfShape.{v_3, u_1, v_5, u_3, v_1, u_5} K G

Tactic:
exact preservesLimitsOfShape_of_natIso e

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_natIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_4, u_2} J'
inst_4 : Category.{v_5, u_3} C
inst_5 : Category.{v_6, u_4} D
inst_6 : HasColimitsOfShape.{v_2, u_6, v_5, u_3} K' C
inst_7 : HasExactColimitsOfShape.{v_5, v_2, u_3, u_6} K' C
G : Functor.{v_3, v_5, u_1, u_3} J C
h : ColimitOfShape preservesFiniteLimits K' G
⊢ ∀ (j : K'), preservesFiniteLimits (h.toColimitPresentation (P := preservesFiniteLimits).diag.obj j)

Tactic:
have := h.prop_diag_obj
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_4, u_2} J'
inst_4 : Category.{v_5, u_3} C
inst_5 : Category.{v_6, u_4} D
inst_6 : HasColimitsOfShape.{v_2, u_6, v_5, u_3} K' C
inst_7 : HasExactColimitsOfShape.{v_5, v_2, u_3, u_6} K' C
G : Functor.{v_3, v_5, u_1, u_3} J C
h : ColimitOfShape preservesFiniteLimits K' G
this : ∀ (j : K'), preservesFiniteLimits (h.toColimitPresentation (P := preservesFiniteLimits).diag.obj j)
⊢ preservesFiniteLimits G

Tactic:
⟨fun K _ _ ↦ (preservesLimitsOfShape K).prop_of_isColimit h.isColimit inferInstance⟩

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, inferInstance, CategoryTheory.Limits.PreservesFiniteLimits.mk, CategoryTheory.ObjectProperty.preservesLimitsOfShape, CategoryTheory.ObjectProperty.prop_of_isColimit, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
Goal:
J : Type u_1
J' : Type u_2
C : Type u_3
D : Type u_4
K : Type u_5
K' : Type u_6
inst : Category.{v_1, u_5} K
inst_1 : Category.{v_2, u_6} K'
inst_2 : Category.{v_3, u_1} J
inst_3 : Category.{v_4, u_2} J'
inst_4 : Category.{v_5, u_3} C
inst_5 : Category.{v_6, u_4} D
inst_6 : HasColimitsOfShape.{v_2, u_6, v_5, u_3} K' C
inst_7 : HasExactColimitsOfShape.{v_5, v_2, u_3, u_6} K' C
G : Functor.{v_3, v_5, u_1, u_3} J C
h : ColimitOfShape preservesFiniteLimits K' G
this : ∀ (j : K'), preservesFiniteLimits (h.toColimitPresentation (P := preservesFiniteLimits).diag.obj j)
⊢ preservesFiniteLimits G

Tactic:
exact ⟨fun K _ _ ↦ (preservesLimitsOfShape K).prop_of_isColimit h.isColimit inferInstance⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
κ : Cardinal.{w}
h : HasCardinalLT ι κ
i : ι
⊢ ofObj.{v, u, u_1} X (X i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
κ : Cardinal.{w}
h : HasCardinalLT ι κ
i : ι
⊢ ∃ (a : ι),
    Eq (α := Subtype (ofObj X)) ((fun (i : ι) ↦ (Subtype.mk (p := ofObj X) (X i) ⋯ : Subtype (ofObj X))) a)
      (Subtype.mk (p := ofObj X) (X i) ⋯)

Tactic:
⟨i, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
X : ι → C
κ : Cardinal.{w}
h : HasCardinalLT ι κ
i : ι
⊢ ∃ (a : ι),
    Eq (α := Subtype (ofObj X)) ((fun (i : ι) ↦ (Subtype.mk (p := ofObj X) (X i) ⋯ : Subtype (ofObj X))) a)
      (Subtype.mk (p := ofObj X) (X i) ⋯)

Tactic:
exact ⟨i, rfl⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
P : ι → ObjectProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
hP : ∀ (i : ι), (P i).HasCardinalLT κ
hι : HasCardinalLT ι κ
⊢ ObjectProperty.HasCardinalLT.{w, v, u} (C := C) (⨆ (i : ι), P i) κ

Tactic:
hasCardinalLT_subtype_iSup _ hι hP

Premises used: hasCardinalLT_subtype_iSup
-- Module: Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
Goal:
C : Type u
inst : Category.{v, u} C
P₁ P₂ : ObjectProperty.{v, u} C
κ : Cardinal.{w}
h₁ : P₁.HasCardinalLT κ
h₂ : P₂.HasCardinalLT κ
hκ : Cardinal.aleph0 ≤ κ
⊢ (P₁ ⊔ P₂).HasCardinalLT κ

Tactic:
hasCardinalLT_union hκ h₁ h₂

Premises used: Set.union, Set.Mem, setOf, hasCardinalLT_union
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : C
hX : P X
⊢ ∀ (i : PUnit.{w + 1}), P (Functor.obj.{w, v, w, u} (ColimitPresentation.diag (ColimitPresentation.self X)) i)

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
X : C
hX : P X
⊢ P.ind X

Tactic:
exact ⟨PUnit, inferInstance, inferInstance, .self X, by simpa⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : P.Nonempty
⊢ P.ind.Nonempty

Tactic:
.mono P.le_ind

Premises used: CategoryTheory.ObjectProperty.Nonempty.mono, CategoryTheory.ObjectProperty.le_ind
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
⊢ P.ind.ind = P.ind

Tactic:
le_antisymm (fun X h ↦ ?_) (le_ind P.ind)

Premises used: le_antisymm, CategoryTheory.ObjectProperty.le_ind, CategoryTheory.ObjectProperty.ind
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
refine : ∀ (X : C) (h : P.ind.ind X), P.ind X
⊢ P.ind.ind = P.ind

Tactic:
refine le_antisymm (fun X h ↦ ?_) (le_ind P.ind)

Premises used: le_antisymm, CategoryTheory.ObjectProperty.le_ind, CategoryTheory.ObjectProperty.ind
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h_1 : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
X : C
h : P.ind.ind X
choose :
  ∀ (J : Type w) (Jc : SmallCategory J) (Jf : IsFiltered J) (pres : ColimitPresentation.{w, w, v, u} J X)
    (K : (i : J) → Type w) (Kc : (i : J) → SmallCategory (K i)) (Kf : ∀ (i : J), IsFiltered.{w, w} (K i))
    (pres' : (i : J) → ColimitPresentation.{w, w, v, u} (K i) (pres.diag.obj i))
    (hp : ∀ (i : J) (i_1 : K i), P ((pres' i).diag.obj i_1)), P.ind X
⊢ P.ind X

Tactic:
choose J Jc Jf pres K Kc Kf pres' hp using h
-- Module: Mathlib.CategoryTheory.ObjectProperty.Ind
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h : P ≤ isFinitelyPresentable C
inst_1 : LocallySmall.{w, v, u} C
X : C
J : Type w
Jc : SmallCategory J
Jf : IsFiltered J
pres : ColimitPresentation.{w, w, v, u} J X
K : (i : J) → Type w
Kc : (i : J) → SmallCategory (K i)
Kf : ∀ (i : J), IsFiltered.{w, w} (K i)
pres' : (i : J) → ColimitPresentation.{w, w, v, u} (K i) (pres.diag.obj i)
hp : ∀ (i : J) (i_1 : K i), P ((pres' i).diag.obj i_1)
⊢ ∀ (j : J) (i : K j), IsFinitelyPresentable.{w, v, u} ((pres' j).diag.obj i)

Tactic:
have (j : J) (i : K j) : IsFinitelyPresentable ((pres' j).diag.obj i) := h _ (hp _ _)