awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasColimitsOfSize.{w, w', v₂, u₂} D
inst_3 : CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
⊢ HasColimitsOfSize.{w, w', v₁, u₁} C

Tactic:
⟨fun _ _ => hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape F⟩

Premises used: CategoryTheory.hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
⊢ (Cone.functoriality K F).map f = i.inv

Tactic:
have : (Cone.functoriality K F).map f = i.inv :=
          (hd.ofIsoLimit i.symm).uniq_cone_morphism
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this : (Cone.functoriality K F).map f = i.inv
rw : IsIso i.inv
⊢ IsIso ((Cone.functoriality K F).map f)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this : (Cone.functoriality K F).map f = i.inv
⊢ IsIso i.inv

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this : (Cone.functoriality K F).map f = i.inv
⊢ IsIso ((Cone.functoriality K F).map f)

Tactic:
haveI : IsIso ((Cone.functoriality K F).map f) := by
          rw [this]
          infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this_1 : (Cone.functoriality K F).map f = i.inv
this : IsIso ((Cone.functoriality K F).map f)
⊢ IsIso f

Tactic:
haveI : IsIso f := isIso_of_reflects_iso f (Cone.functoriality K F)
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cone (K ⋙ F)) → (t : IsLimit c) → LiftsToLimit K F c t
d : Cone K
hd : IsLimit (F.mapCone d)
d' : Cone K := (h (F.mapCone d) hd).liftedCone
i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).validLift
hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
f : d ⟶ d' := hd'.liftConeMorphism d
this_1 : (Cone.functoriality K F).map f = i.inv
this_2 : IsIso ((Cone.functoriality K F).map f)
this : IsIso f
⊢ IsLimit d

Tactic:
exact IsLimit.ofIsoLimit hd' (asIso f).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
l : Cone (K ⋙ F)
hl : IsLimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (map (obj (const J) X) f ≫ F.preimage (i.hom ≫ l.π.app Z)) = F.map (F.preimage (i.hom ≫ l.π.app Y) ≫ K.map f)

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

Premises used: CategoryTheory.Limits.Cone.w, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
l : Cone (K ⋙ F)
hl : IsLimit l
X : C
i : F.obj X ≅ l.pt
j : J
⊢ NatTrans.app
      (Cone.π (F.mapCone { pt := X, π := { app := fun (j : J) ↦ F.preimage (i.hom ≫ l.π.app j), naturality := ⋯ } }))
      j =
    i.hom ≫ l.π.app j

Tactic:
simp only [Functor.map_preimage, Functor.mapCone_π_app]

Premises used: CategoryTheory.Functor.mapCone_π_app, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
⊢ (Cocone.functoriality K F).map f = i.hom

Tactic:
have : (Cocone.functoriality K F).map f = i.hom :=
          (hd.ofIsoColimit i.symm).uniq_cocone_morphism
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this : (Cocone.functoriality K F).map f = i.hom
rw : IsIso i.hom
⊢ IsIso ((Cocone.functoriality K F).map f)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this : (Cocone.functoriality K F).map f = i.hom
⊢ IsIso i.hom

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this : (Cocone.functoriality K F).map f = i.hom
⊢ IsIso ((Cocone.functoriality K F).map f)

Tactic:
haveI : IsIso ((Cocone.functoriality K F).map f) := by
          rw [this]
          infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this_1 : (Cocone.functoriality K F).map f = i.hom
this : IsIso ((Cocone.functoriality K F).map f)
⊢ IsIso f

Tactic:
haveI := isIso_of_reflects_iso f (Cocone.functoriality K F)
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.ReflectsIsomorphisms
h : (c : Cocone (K ⋙ F)) → (t : IsColimit c) → LiftsToColimit K F c t
d : Cocone K
hd : IsColimit (F.mapCocone d)
d' : Cocone K := (h (F.mapCocone d) hd).liftedCocone
i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).validLift
hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
f : d' ⟶ d := hd'.descCoconeMorphism d
this_1 : (Cocone.functoriality K F).map f = i.hom
this_2 : IsIso ((Cocone.functoriality K F).map f)
this : IsIso f
⊢ IsColimit d

Tactic:
exact IsColimit.ofIsoColimit hd' (asIso f)

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
l : Cocone (K ⋙ F)
hl : IsColimit l
X : C
i : F.obj X ≅ l.pt
Y Z : J
f : Y ⟶ Z
⊢ F.map (K.map f ≫ F.preimage (l.ι.app Z ≫ i.inv)) = F.map (F.preimage (l.ι.app Y ≫ i.inv) ≫ map (obj (const J) X) f)

Tactic:
simpa [← cancel_mono i.hom] using l.w f

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Limits.Cocone.w, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
l : Cocone (K ⋙ F)
hl : IsColimit l
X : C
i : F.obj X ≅ l.pt
j : J
⊢ NatTrans.app
        (Cocone.ι
          (F.mapCocone { pt := X, ι := { app := fun (j : J) ↦ F.preimage (l.ι.app j ≫ i.inv), naturality := ⋯ } }))
        j ≫
      i.hom =
    l.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K K₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : CreatesLimit K₁ F
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c) :=
  ((IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm :
      (a : IsLimit c) → IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c))
    t
j : J
dsimp : (c.π.app j ≫ F.map (h.inv.app j)) ≫ F.map (h.hom.app j) = 𝟙 c.pt ≫ c.π.app j
⊢ ((Cone.postcompose (isoWhiskerRight h F).hom).obj ((Cone.postcompose (isoWhiskerRight h F).inv).obj c)).π.app j =
    Iso.hom
        (Iso.refl
          ((Cone.postcompose (isoWhiskerRight h F).hom).obj ((Cone.postcompose (isoWhiskerRight h F).inv).obj c)).pt) ≫
      c.π.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K K₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : CreatesLimit K₁ F
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c) :=
  ((IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm :
      (a : IsLimit c) → IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c))
    t
j : J
rw : c.π.app j ≫ F.map (h.inv.app j ≫ h.hom.app j) = 𝟙 c.pt ≫ c.π.app j
⊢ (c.π.app j ≫ F.map (h.inv.app j)) ≫ F.map (h.hom.app j) = 𝟙 c.pt ≫ c.π.app j

Tactic:
rw [Category.assoc, ← F.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K K₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : CreatesLimit K₁ F
c : Cone (K₂ ⋙ F)
t : IsLimit c
t' : IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c) :=
  ((IsLimit.postcomposeInvEquiv (isoWhiskerRight h F) c).symm :
      (a : IsLimit c) → IsLimit ((Cone.postcompose (isoWhiskerRight h F).inv).obj c))
    t
j : J
⊢ c.π.app j ≫ F.map (h.inv.app j ≫ h.hom.app j) = 𝟙 c.pt ≫ c.π.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
inst_3 : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
refine :
  IsLimit.{w', v₂, w, u₂} (J := J) (F := K ⋙ F)
    (F.mapCone
      (liftLimit.{w', w, v₁, v₂, u₁, u₂} (D := D) (F := F) (c := (Cone.postcompose (K.isoWhiskerLeft h).inv).obj c)
        (((IsLimit.postcomposeInvEquiv (K.isoWhiskerLeft h) c).symm :
            (a : IsLimit c) → IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj c))
          t)))
⊢ G.mapCone
      (liftLimit.{w', w, v₁, v₂, u₁, u₂} (D := D) (F := F) (c := (Cone.postcompose (K.isoWhiskerLeft h).inv).obj c)
        (((IsLimit.postcomposeInvEquiv (K.isoWhiskerLeft h) c).symm :
            (a : IsLimit c) → IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj c))
          t)) ≅
    c

Tactic:
refine (IsLimit.mapConeEquiv h ?_).uniqueUpToIso t

Premises used: CategoryTheory.Limits.IsLimit.mapConeEquiv, CategoryTheory.Limits.IsLimit.uniqueUpToIso
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
inst_3 : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
apply : IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj c)
⊢ IsLimit.{w', v₂, w, u₂} (J := J) (F := K ⋙ F)
    (F.mapCone
      (liftLimit.{w', w, v₁, v₂, u₁, u₂} (D := D) (F := F) (c := (Cone.postcompose (K.isoWhiskerLeft h).inv).obj c)
        (((IsLimit.postcomposeInvEquiv (K.isoWhiskerLeft h) c).symm :
            (a : IsLimit c) → IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj c))
          t)))

Tactic:
apply IsLimit.ofIsoLimit _ (liftedLimitMapsToOriginal _).symm

Premises used: CategoryTheory.liftedLimitMapsToOriginal, CategoryTheory.Iso.symm, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K : Functor.{w', v₁, w, u₁} J C
F G : Functor.{v₁, v₂, u₁, u₂} C D
h : F ≅ G
inst_3 : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ IsLimit ((Cone.postcompose (K.isoWhiskerLeft h).inv).obj c)

Tactic:
apply (IsLimit.postcomposeInvEquiv _ _).symm t

Premises used: CategoryTheory.Limits.IsLimit.postcomposeInvEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 : Functor.{w', v₁, w, u₁} J C
J' : Type w₁
inst_3 : Category.{w'₁, w₁} J'
e : Equivalence.{w', w'₁, w, w₁} J J'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : CreatesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w'₁, v₁, w₁, u₁} J' C
c : Cone (K ⋙ F)
hc : IsLimit c
refine : F.mapCone (obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (liftLimit (hc.whiskerEquivalence e))) ≅ c
⊢ LiftableCone K F c

Tactic:
refine ⟨(Cone.whiskeringEquivalence e).inverse.obj
          (liftLimit (hc.whiskerEquivalence e)), ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K_1 : Functor.{w', v₁, w, u₁} J C
J' : Type w₁
inst_3 : Category.{w'₁, w₁} J'
e : Equivalence.{w', w'₁, w, w₁} J J'
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : CreatesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w'₁, v₁, w₁, u₁} J' C
c : Cone (K ⋙ F)
hc : IsLimit c
inner : obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (F.mapCone (liftLimit (hc.whiskerEquivalence e))) ≅
  obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (Cone.whisker e.functor c) :=
  mapIso (Equivalence.inverse (Cone.whiskeringEquivalence e)) (liftedLimitMapsToOriginal (hc.whiskerEquivalence e))
refine :
  F.mapCone (obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (liftLimit (hc.whiskerEquivalence e))) ≅
    obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (F.mapCone (liftLimit (hc.whiskerEquivalence e)))
⊢ F.mapCone (obj (Equivalence.inverse (Cone.whiskeringEquivalence e)) (liftLimit (hc.whiskerEquivalence e))) ≅ c

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

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

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

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K K₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : CreatesColimit K₁ F
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c) :=
  ((IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm :
      (a : IsColimit c) → IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c))
    t
j : J
dsimp : (F.map (h.inv.app j) ≫ F.map (h.hom.app j) ≫ c.ι.app j) ≫ 𝟙 c.pt = c.ι.app j
⊢ ((Cocone.precompose (isoWhiskerRight h F).inv).obj ((Cocone.precompose (isoWhiskerRight h F).hom).obj c)).ι.app j ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (isoWhiskerRight h F).inv).obj
              ((Cocone.precompose (isoWhiskerRight h F).hom).obj c)).pt) =
    c.ι.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K K₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : CreatesColimit K₁ F
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c) :=
  ((IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm :
      (a : IsColimit c) → IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c))
    t
j : J
rw : (F.map (h.inv.app j ≫ h.hom.app j) ≫ c.ι.app j) ≫ 𝟙 c.pt = c.ι.app j
⊢ (F.map (h.inv.app j) ≫ F.map (h.hom.app j) ≫ c.ι.app j) ≫ 𝟙 c.pt = c.ι.app j

Tactic:
rw [← F.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Limits.Creates
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type w
inst_2 : Category.{w', w} J
K K₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : CreatesColimit K₁ F
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c) :=
  ((IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm :
      (a : IsColimit c) → IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c))
    t
j : J
⊢ (F.map (h.inv.app j ≫ h.hom.app j) ≫ c.ι.app j) ≫ 𝟙 c.pt = c.ι.app j

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

Tactic:
refine (IsColimit.mapCoconeEquiv h ?_).uniqueUpToIso t

Premises used: CategoryTheory.Limits.IsColimit.mapCoconeEquiv, CategoryTheory.Limits.IsColimit.uniqueUpToIso