awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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 : Functor.{v₁, v₂, u₁, u₂} C D
t : Cone K
h : IsLimit t
⊢ PreservesLimit K F ↔ Nonempty (IsLimit (F.mapCone t))

Tactic:
⟨fun _ ↦ ⟨isLimitOfPreserves _ h⟩, fun h' ↦ preservesLimit_of_preserves_limit_cone h h'.some⟩

Premises used: Nonempty.some, Nonempty.intro, Iff.intro, CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
apply : IsLimit ((Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c))
⊢ IsLimit (F.mapCone c)

Tactic:
apply IsLimit.postcomposeInvEquiv (Functor.isoWhiskerRight h F :) _ _

Premises used: CategoryTheory.Limits.IsLimit.postcomposeInvEquiv, CategoryTheory.Functor.isoWhiskerRight, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
have :
  (this : IsLimit ((Cone.postcompose h.inv).obj c)) →
    IsLimit ((Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c))
⊢ IsLimit ((Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c))

Tactic:
have := (IsLimit.postcomposeInvEquiv h c).symm t
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : IsLimit ((Cone.postcompose h.inv).obj c)
apply :
  F.mapCone ((Cone.postcompose h.inv).obj c) ≅ (Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c)
⊢ IsLimit ((Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c))

Tactic:
apply IsLimit.ofIsoLimit (isLimitOfPreserves F this)

Premises used: CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : IsLimit ((Cone.postcompose h.inv).obj c)
⊢ F.mapCone ((Cone.postcompose h.inv).obj c) ≅ (Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c)

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

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
⊢ PreservesLimit K₁ F ↔ PreservesLimit K₂ F

Tactic:
⟨fun _ ↦ preservesLimit_of_iso_diagram _ h, fun _ ↦ preservesLimit_of_iso_diagram _ h.symm⟩

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
⊢ PreservesLimit K F ↔ PreservesLimit K G

Tactic:
⟨fun _ ↦ preservesLimit_of_natIso _ h, fun _ ↦ preservesLimit_of_natIso _ h.symm⟩

Premises used: CategoryTheory.Limits.preservesLimit_of_natIso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
⊢ PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F ↔ PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G

Tactic:
⟨fun _ ↦ preservesLimitsOfShape_of_natIso h, fun _ ↦ preservesLimitsOfShape_of_natIso h.symm⟩

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_natIso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
⊢ PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F ↔ PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G

Tactic:
⟨fun _ ↦ preservesLimits_of_natIso h, fun _ ↦ preservesLimits_of_natIso h.symm⟩

Premises used: Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesLimits_of_natIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
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 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
have : (this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))) → IsLimit (F.mapCone c)
⊢ IsLimit (F.mapCone c)

Tactic:
have := (isLimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
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 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
apply :
  (Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c))) ≅ F.mapCone c
⊢ IsLimit (F.mapCone c)

Tactic:
apply ((IsLimit.postcomposeHomEquiv equ _).symm this).ofIsoLimit

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, Equiv.symm, CategoryTheory.Limits.IsLimit.ofIsoLimit, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
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 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
refine :
  ∀ (j : J'),
    ((Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).π.app j =
      Iso.hom
          (Iso.refl
            ((Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).pt) ≫
        (F.mapCone c).π.app j
⊢ (Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c))) ≅ F.mapCone c

Tactic:
refine Cone.ext (Iso.refl _) fun j => ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
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 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
j : J'
⊢ ((Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).π.app j =
    Iso.hom
        (Iso.refl
          ((Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).pt) ≫
      (F.mapCone c).π.app j

Tactic:
simp [equ, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F
⊢ PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

Tactic:
preservesLimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

Premises used: CategoryTheory.Limits.preservesLimitsOfSize_of_univLE
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesLimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F
⊢ PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Tactic:
preservesLimitsOfSize_shrink F

Premises used: CategoryTheory.Limits.preservesLimitsOfSize_shrink
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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 : Functor.{v₁, v₂, u₁, u₂} C D
t : Cocone K
h : IsColimit t
hF : IsColimit (F.mapCocone t)
⊢ PreservesColimit K F

Tactic:
⟨fun h' => ⟨IsColimit.ofIsoColimit hF (Functor.mapIso _ (IsColimit.uniqueUpToIso h h'))⟩⟩

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Limits.IsColimit.uniqueUpToIso, Nonempty.intro, CategoryTheory.Limits.Cocone.functoriality, CategoryTheory.Limits.PreservesColimit.mk, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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 : Functor.{v₁, v₂, u₁, u₂} C D
t : Cocone K
h : IsColimit t
⊢ PreservesColimit K F ↔ Nonempty (IsColimit (F.mapCocone t))

Tactic:
⟨fun _ ↦ ⟨isColimitOfPreserves _ h⟩,
    fun h' ↦ preservesColimit_of_preserves_colimit_cocone h h'.some⟩

Premises used: Nonempty.some, Nonempty.intro, Iff.intro, CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
apply : IsColimit ((Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c))
⊢ IsColimit (F.mapCocone c)

Tactic:
apply IsColimit.precomposeHomEquiv (Functor.isoWhiskerRight h F :) _ _

Premises used: CategoryTheory.Functor.isoWhiskerRight, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
have :
  (this : IsColimit ((Cocone.precompose h.hom).obj c)) →
    IsColimit ((Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c))
⊢ IsColimit ((Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c))

Tactic:
have := (IsColimit.precomposeHomEquiv h c).symm t
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : IsColimit ((Cocone.precompose h.hom).obj c)
apply :
  F.mapCocone ((Cocone.precompose h.hom).obj c) ≅
    (Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c)
⊢ IsColimit ((Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c))

Tactic:
apply IsColimit.ofIsoColimit (isColimitOfPreserves F this)

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : IsColimit ((Cocone.precompose h.hom).obj c)
⊢ F.mapCocone ((Cocone.precompose h.hom).obj c) ≅
    (Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c)

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

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
⊢ PreservesColimit K₁ F ↔ PreservesColimit K₂ F

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

Premises used: CategoryTheory.Limits.preservesColimit_of_iso_diagram, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
⊢ PreservesColimit K F ↔ PreservesColimit K G

Tactic:
⟨fun _ ↦ preservesColimit_of_natIso _ h, fun _ ↦ preservesColimit_of_natIso _ h.symm⟩

Premises used: Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesColimit_of_natIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
⊢ PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F ↔ PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G

Tactic:
⟨fun _ ↦ preservesColimitsOfShape_of_natIso h, fun _ ↦ preservesColimitsOfShape_of_natIso h.symm⟩

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_natIso, Iff.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
⊢ PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F ↔ PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} G

Tactic:
⟨fun _ ↦ preservesColimits_of_natIso h, fun _ ↦ preservesColimits_of_natIso h.symm⟩

Premises used: Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesColimits_of_natIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
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 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
have :
  (this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))) →
    IsColimit (F.mapCocone c)
⊢ IsColimit (F.mapCocone c)

Tactic:
have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
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 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
apply :
  (Cocone.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c))) ≅
    F.mapCocone c
⊢ IsColimit (F.mapCocone c)

Tactic:
apply ((IsColimit.precomposeInvEquiv equ _).symm this).ofIsoColimit

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeInvEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
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 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
refine :
  ∀ (j : J'),
    ((Cocone.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).ι.app
          j ≫
        Iso.hom
          (Iso.refl
            ((Cocone.precompose equ.inv).obj
                (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).pt) =
      (F.mapCocone c).ι.app j
⊢ (Cocone.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c))) ≅
    F.mapCocone c

Tactic:
refine Cocone.ext (Iso.refl _) fun j => ?_

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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
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 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
j : J'
⊢ ((Cocone.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).ι.app j ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose equ.inv).obj
              (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).pt) =
    (F.mapCocone c).ι.app j

Tactic:
simp [equ, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F
⊢ PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

Tactic:
preservesColimitsOfSize_of_univLE.{max w w₂, max w' w₂'} F

Premises used: CategoryTheory.Limits.preservesColimitsOfSize_of_univLE
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : PreservesColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F
⊢ PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Tactic:
preservesColimitsOfSize_shrink F

Premises used: CategoryTheory.Limits.preservesColimitsOfSize_shrink
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
allEq : ∀ (a b : ReflectsLimit K F), a = b
⊢ Subsingleton (ReflectsLimit K F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : ∀ {c : Cone K} (hc : IsLimit (F.mapCone c)), Nonempty (IsLimit c)
⊢ ⋯ = ⋯

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
allEq : ∀ (a b : ReflectsColimit K F), a = b
⊢ Subsingleton (ReflectsColimit K F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : ∀ {c : Cocone K} (hc : IsColimit (F.mapCocone c)), Nonempty (IsColimit c)
⊢ ⋯ = ⋯

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
allEq : ∀ (a b : ReflectsLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F), a = b
⊢ Subsingleton (ReflectsLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : ∀ {K : Functor.{w', v₁, w, u₁} J C}, ReflectsLimit K F
⊢ ⋯ = ⋯

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
allEq : ∀ (a b : ReflectsColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F), a = b
⊢ Subsingleton (ReflectsColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K : Functor.{w', v₁, w, u₁} J_1 C
J : Type w
inst_3 : Category.{w', w} J
F : Functor.{v₁, v₂, u₁, u₂} C D
a b : ∀ {K : Functor.{w', v₁, w, u₁} J C}, ReflectsColimit K F
⊢ ⋯ = ⋯

Tactic:
congr!
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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 : Functor.{v₁, v₂, u₁, u₂} C D
allEq : ∀ (a b : ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
⊢ Subsingleton (ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
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 : Functor.{v₁, v₂, u₁, u₂} C D
a b : ∀ {J : Type w} [inst_3 : Category.{w', w} J], ReflectsLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
⊢ ⋯ = ⋯

Tactic:
congr!