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
F : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasLimit F
inst_5 : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this :
  IsIso (Y := (Cone.functoriality F G).obj (limit.cone F))
    ((Cone.functoriality F G).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
⊢ IsIso (Y := limit.cone F) (IsLimit.liftConeMorphism (limit.isLimit F) c)

Tactic:
apply isIso_of_reflects_iso _ (Cone.functoriality F G)

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.Limits.Cone.functoriality
-- 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 : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasLimit F
inst_5 : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
suffices :
  IsIso (Y := (Cone.functoriality F G).obj (limit.cone F))
    ((Cone.functoriality F G).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
⊢ IsIso (Y := limit.cone F) (IsLimit.liftConeMorphism (limit.isLimit F) c)

Tactic:
suffices IsIso ((Cone.functoriality F G).map
      (IsLimit.liftConeMorphism (limit.isLimit F) c)) from by
        apply isIso_of_reflects_iso _ (Cone.functoriality F G)
-- 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 : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasLimit F
inst_5 : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso (Y := (Cone.functoriality F G).obj (limit.cone F))
    ((Cone.functoriality F G).map (IsLimit.liftConeMorphism (limit.isLimit F) c))

Tactic:
t.hom_isIso (isLimitOfPreserves G (limit.isLimit F)) _

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Functor.mapCone, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Limits.IsLimit.hom_isIso
-- 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 : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasLimit F
inst_5 : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
⊢ IsIso (Y := (Cone.functoriality F G).obj (limit.cone F))
    ((Cone.functoriality F G).map (IsLimit.liftConeMorphism (limit.isLimit F) c))

Tactic:
exact t.hom_isIso (isLimitOfPreserves G (limit.isLimit F)) _

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.isLimitOfPreserves, CategoryTheory.Limits.IsLimit.hom_isIso
-- 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
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : PreservesColimit K (F ⋙ G)
inst_4 : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
t : IsColimit (G.mapCocone (F.mapCocone c))
⊢ IsColimit (F.mapCocone c)

Tactic:
apply isColimitOfReflects G

Premises used: CategoryTheory.Limits.isColimitOfReflects
-- 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
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : PreservesColimit K (F ⋙ G)
inst_4 : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
⊢ IsColimit (G.mapCocone (F.mapCocone c))

Tactic:
apply isColimitOfPreserves (F ⋙ G) h

Premises used: CategoryTheory.Functor.comp, 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 : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
apply : IsColimit (F.mapCocone ((Cocone.precompose h.hom).obj c))
⊢ IsColimit c

Tactic:
apply IsColimit.precomposeHomEquiv h c (isColimitOfReflects F _)

Premises used: CategoryTheory.Limits.isColimitOfReflects, 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 : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
apply :
  (Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c) ≅
    F.mapCocone ((Cocone.precompose h.hom).obj c)
⊢ IsColimit (F.mapCocone ((Cocone.precompose h.hom).obj c))

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

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, Equiv.symm, 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 : ReflectsColimit K₁ F
c : Cocone K₂
t : IsColimit (F.mapCocone c)
⊢ (Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c) ≅
    F.mapCocone ((Cocone.precompose h.hom).obj 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
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 : ReflectsColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cocone K
t : IsColimit (F.mapCocone c)
apply : IsColimit (Cocone.whisker e.functor c)
⊢ IsColimit c

Tactic:
apply IsColimit.ofWhiskerEquivalence e

Premises used: CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence
-- 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 : ReflectsColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cocone K
t : IsColimit (F.mapCocone c)
t₁ : IsColimit (F.mapCocone (Cocone.whisker e.functor c))
⊢ IsColimit (Cocone.whisker e.functor c)

Tactic:
apply isColimitOfReflects F

Premises used: CategoryTheory.Limits.isColimitOfReflects
-- 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 : ReflectsColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cocone K
t : IsColimit (F.mapCocone c)
apply : IsColimit (Cocone.whisker e.functor (F.mapCocone c))
⊢ IsColimit (F.mapCocone (Cocone.whisker e.functor c))

Tactic:
apply IsColimit.ofIsoColimit _ (Functor.mapCoconeWhisker _).symm

Premises used: CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Functor.mapCoconeWhisker, 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
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 : ReflectsColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor (F.mapCocone c))

Tactic:
exact IsColimit.whiskerEquivalence t _

Premises used: CategoryTheory.Limits.IsColimit.whiskerEquivalence
-- 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 : ReflectsColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F
⊢ ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F

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

Premises used: CategoryTheory.Limits.reflectsColimitsOfSize_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 : ReflectsColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F
⊢ ReflectsColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F

Tactic:
reflectsColimitsOfSize_shrink F

Premises used: CategoryTheory.Limits.reflectsColimitsOfSize_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
F : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasColimit F
inst_5 : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso (X := (colimit.cocone F).pt) (IsColimit.desc (colimit.isColimit F) c)
⊢ IsColimit c

Tactic:
apply IsColimit.ofPointIso (colimit.isColimit F)

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.ofPointIso
-- 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 : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasColimit F
inst_5 : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
suffices : IsIso (X := (colimit.cocone F).pt) (IsColimit.desc (colimit.isColimit F) c)
⊢ Nonempty (IsColimit c)

Tactic:
suffices IsIso (IsColimit.desc (colimit.isColimit F) c) from ⟨by
      apply IsColimit.ofPointIso (colimit.isColimit F)⟩
-- 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 : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasColimit F
inst_5 : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
change :
  IsIso (X := (Cocone.forget F).obj (colimit.cocone F))
    ((Cocone.forget F).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
⊢ IsIso (X := (colimit.cocone F).pt) (IsColimit.desc (colimit.isColimit F) c)

Tactic:
change IsIso ((Cocone.forget _).map ((colimit.isColimit F).descCoconeMorphism c))

Premises used: CategoryTheory.IsIso, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Functor.map, CategoryTheory.Limits.Cocone.forget, CategoryTheory.Limits.IsColimit.descCoconeMorphism
-- 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 : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasColimit F
inst_5 : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso (X := colimit.cocone F) (IsColimit.descCoconeMorphism (colimit.isColimit F) c)
⊢ IsIso (X := (Cocone.forget F).obj (colimit.cocone F))
    ((Cocone.forget F).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))

Tactic:
apply (Cocone.forget F).map_isIso _

Premises used: CategoryTheory.Limits.Cocone.forget, CategoryTheory.Functor.map_isIso
-- 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 : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasColimit F
inst_5 : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
suffices : IsIso (X := colimit.cocone F) (IsColimit.descCoconeMorphism (colimit.isColimit F) c)
⊢ IsIso (X := (Cocone.forget F).obj (colimit.cocone F))
    ((Cocone.forget F).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))

Tactic:
suffices IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c) from by
      apply (Cocone.forget F).map_isIso _
-- 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 : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasColimit F
inst_5 : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this :
  IsIso (X := (Cocone.functoriality F G).obj (colimit.cocone F))
    ((Cocone.functoriality F G).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
⊢ IsIso (X := colimit.cocone F) (IsColimit.descCoconeMorphism (colimit.isColimit F) c)

Tactic:
apply isIso_of_reflects_iso _ (Cocone.functoriality F G)

Premises used: CategoryTheory.isIso_of_reflects_iso, CategoryTheory.Limits.Cocone.functoriality
-- 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 : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasColimit F
inst_5 : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
suffices :
  IsIso (X := (Cocone.functoriality F G).obj (colimit.cocone F))
    ((Cocone.functoriality F G).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
⊢ IsIso (X := colimit.cocone F) (IsColimit.descCoconeMorphism (colimit.isColimit F) c)

Tactic:
suffices IsIso ((Cocone.functoriality F G).map
      (IsColimit.descCoconeMorphism (colimit.isColimit F) c)) from by
        apply isIso_of_reflects_iso _ (Cocone.functoriality F G)
-- 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 : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasColimit F
inst_5 : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso (X := (Cocone.functoriality F G).obj (colimit.cocone F))
    ((Cocone.functoriality F G).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))

Tactic:
(isColimitOfPreserves G (colimit.isColimit F)).hom_isIso t _

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.hom_isIso, 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
F : Functor.{w', v₁, w, u₁} J C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : G.ReflectsIsomorphisms
inst_4 : HasColimit F
inst_5 : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ IsIso (X := (Cocone.functoriality F G).obj (colimit.cocone F))
    ((Cocone.functoriality F G).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))

Tactic:
exact (isColimitOfPreserves G (colimit.isColimit F)).hom_isIso t _

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.hom_isIso, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u_1
D : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} J
K : Functor.{v_3, v_1, u_3, u_1} J C
L L' : Functor.{v_1, v_2, u_1, u_2} C D
α : L ⟶ L'
inst_3 : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst_4 : PreservesColimit K L
inst_5 : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
⊢ IsIso e.hom

Tactic:
(inferInstance : IsIso e.hom)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u_1
D : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} J
K : Functor.{v_3, v_1, u_3, u_1} J C
L L' : Functor.{v_1, v_2, u_1, u_2} C D
α : L ⟶ L'
inst_3 : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst_4 : PreservesColimit K L
inst_5 : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
h : L.obj c.pt = (L.mapCocone c).pt → L'.obj c.pt = (L'.mapCocone c).pt → α.app c.pt = e.hom
⊢ IsIso (X := L.obj c.pt) (α.app c.pt)

Tactic:
convert! (inferInstance : IsIso e.hom)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u_1
D : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} J
K : Functor.{v_3, v_1, u_3, u_1} J C
L L' : Functor.{v_1, v_2, u_1, u_2} C D
α : L ⟶ L'
inst_3 : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst_4 : PreservesColimit K L
inst_5 : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
e_3 : L.obj c.pt = (L.mapCocone c).pt
e_4 : L'.obj c.pt = (L'.mapCocone c).pt
apply : ∀ (j : J), (L.mapCocone c).ι.app j ≫ α.app c.pt = (L.mapCocone c).ι.app j ≫ e.hom
⊢ α.app c.pt = e.hom

Tactic:
apply (isColimitOfPreserves L hc).hom_ext fun j ↦ ?_

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u_1
D : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} J
K : Functor.{v_3, v_1, u_3, u_1} J C
L L' : Functor.{v_1, v_2, u_1, u_2} C D
α : L ⟶ L'
inst_3 : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst_4 : PreservesColimit K L
inst_5 : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
e_3 : L.obj c.pt = (L.mapCocone c).pt
e_4 : L'.obj c.pt = (L'.mapCocone c).pt
j : J
simp :
  α.app (K.obj j) ≫ L'.map (c.ι.app j) =
    L.map (c.ι.app j) ≫ (isColimitOfPreserves L hc).map (L'.mapCocone c) (K.whiskerLeft α)
⊢ (L.mapCocone c).ι.app j ≫ α.app c.pt = (L.mapCocone c).ι.app j ≫ e.hom

Tactic:
simp only [Functor.comp_obj, Functor.mapCocone_pt, Functor.const_obj_obj, Functor.mapCocone_ι_app,
    NatTrans.naturality, IsColimit.coconePointsIsoOfNatIso_hom, asIso_hom, e]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.mapCocone_ι_app, CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_hom, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.const_obj_obj, CategoryTheory.asIso_hom, CategoryTheory.Functor.mapCocone_pt
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u_1
D : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} J
K : Functor.{v_3, v_1, u_3, u_1} J C
L L' : Functor.{v_1, v_2, u_1, u_2} C D
α : L ⟶ L'
inst_3 : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst_4 : PreservesColimit K L
inst_5 : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
e_3 : L.obj c.pt = (L.mapCocone c).pt
e_4 : L'.obj c.pt = (L'.mapCocone c).pt
j : J
⊢ α.app (K.obj j) ≫ L'.map (c.ι.app j) =
    L.map (c.ι.app j) ≫ (isColimitOfPreserves L hc).map (L'.mapCocone c) (K.whiskerLeft α)

Tactic:
(((isColimitOfPreserves L hc).ι_map (L'.mapCocone c) (whiskerLeft K α) j).trans ?_).symm

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.ι_map, CategoryTheory.Functor.whiskerLeft, Eq.symm, CategoryTheory.Limits.isColimitOfPreserves, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u_1
D : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} J
K : Functor.{v_3, v_1, u_3, u_1} J C
L L' : Functor.{v_1, v_2, u_1, u_2} C D
α : L ⟶ L'
inst_3 : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst_4 : PreservesColimit K L
inst_5 : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
e_3 : L.obj c.pt = (L.mapCocone c).pt
e_4 : L'.obj c.pt = (L'.mapCocone c).pt
j : J
refine : (K.whiskerLeft α).app j ≫ (L'.mapCocone c).ι.app j = α.app (K.obj j) ≫ L'.map (c.ι.app j)
⊢ α.app (K.obj j) ≫ L'.map (c.ι.app j) =
    L.map (c.ι.app j) ≫ (isColimitOfPreserves L hc).map (L'.mapCocone c) (K.whiskerLeft α)

Tactic:
refine (((isColimitOfPreserves L hc).ι_map (L'.mapCocone c) (whiskerLeft K α) j).trans ?_).symm

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.Limits.IsColimit.ι_map, CategoryTheory.Functor.whiskerLeft, Eq.symm, CategoryTheory.Limits.isColimitOfPreserves, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u_1
D : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} J
K : Functor.{v_3, v_1, u_3, u_1} J C
L L' : Functor.{v_1, v_2, u_1, u_2} C D
α : L ⟶ L'
inst_3 : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst_4 : PreservesColimit K L
inst_5 : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
e_3 : L.obj c.pt = (L.mapCocone c).pt
e_4 : L'.obj c.pt = (L'.mapCocone c).pt
j : J
⊢ (K.whiskerLeft α).app j ≫ (L'.mapCocone c).ι.app j = α.app (K.obj j) ≫ L'.map (c.ι.app j)

Tactic:
simp
-- 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_1 : Functor.{w', v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cone K
t : IsLimit (F.mapCone c)
apply :
  ∀ (s : Cone K) (m : s ⟶ c),
    (Cone.functoriality K F).map m =
      (Cone.functoriality K F).map
        ((Cone.functoriality K F).preimage (t.liftConeMorphism ((Cone.functoriality K F).obj s)))
⊢ ∀ (s : Cone K) (m : s ⟶ c),
    m = (Cone.functoriality K F).preimage (t.liftConeMorphism ((Cone.functoriality K F).obj s))

Tactic:
apply fun s m => (Cone.functoriality K F).map_injective _

Premises used: CategoryTheory.Functor.map_injective, CategoryTheory.Limits.Cone.functoriality