awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesLimit F G
inst_4 : HasLimit F
inst_5 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasLimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasLimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
j : J
⊢ Eq (α := G.obj (limit X) ⟶ G.obj (Y.obj j))
    (CategoryStruct.comp (Y := limit (Y ⋙ G))
      (CategoryStruct.comp (Y := G.obj (limit Y)) (G.map (limMap f)) (Iso.hom (preservesLimitIso G Y)) :
        G.obj (limit X) ⟶ limit (Y ⋙ G))
      (limit.π (Y ⋙ G) j : limit (Y ⋙ G) ⟶ (Y ⋙ G).obj j))
    (CategoryStruct.comp (Y := limit (Y ⋙ G))
      (CategoryStruct.comp (Y := limit (X ⋙ G)) (Iso.hom (preservesLimitIso G X) : G.obj (limit X) ⟶ limit (X ⋙ G))
        (limMap (Functor.whiskerRight f G) : limit (X ⋙ G) ⟶ limit (Y ⋙ G)))
      (limit.π (Y ⋙ G) j))

Tactic:
simp only [preservesLimitIso_hom_π, Functor.whiskerRight_app, limMap_π, Category.assoc,
        preservesLimitIso_hom_π_assoc, ← G.map_comp]

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Category.assoc, CategoryTheory.preservesLimitIso_hom_π_assoc, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.preservesLimitIso_hom_π, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : HasLimit F
inst_4 : HasLimit (F ⋙ G)
inst_5 : IsIso (X := G.obj (limit F)) (Y := limit (F ⋙ G)) (limit.post F G)
convert_2 :
  IsIso (X := (G.mapCone (limit.cone F)).pt) (Y := (limit.cone (F ⋙ G)).pt)
    (IsLimit.lift (limit.isLimit (F ⋙ G)) (G.mapCone (limit.cone F)))
⊢ IsLimit (G.mapCone (limit.cone F))

Tactic:
convert! IsLimit.ofPointIso (limit.isLimit (F ⋙ G))
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : HasLimit F
inst_4 : HasLimit (F ⋙ G)
inst_5 : IsIso (X := G.obj (limit F)) (Y := limit (F ⋙ G)) (limit.post F G)
⊢ IsIso (X := (G.mapCone (limit.cone F)).pt) (Y := (limit.cone (F ⋙ G)).pt)
    (IsLimit.lift (limit.isLimit (F ⋙ G)) (G.mapCone (limit.cone F)))

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
c₁ c₂ : Cocone F
t : IsColimit c₁
⊢ ∀ (j : J), (G.mapCocone c₁).ι.app j ≫ G.map (t.desc c₂) = (G.mapCocone c₂).ι.app j

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
j : J
⊢ Eq (α := (F ⋙ G).obj j ⟶ G.obj (colimit F))
    (CategoryStruct.comp (Y := colimit (F ⋙ G)) (colimit.ι (F ⋙ G) j : (F ⋙ G).obj j ⟶ colimit (F ⋙ G))
      (Iso.inv (preservesColimitIso G F) : colimit (F ⋙ G) ⟶ G.obj (colimit F)))
    (G.map (colimit.ι F j))

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_inv _ (colimit.isColimit (F ⋙ G)) j

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
j : J
⊢ Eq (α := G.obj (F.obj j) ⟶ colimit (F ⋙ G))
    (CategoryStruct.comp (Y := G.obj (colimit F)) (G.map (colimit.ι F j)) (Iso.hom (preservesColimitIso G F)) :
      G.obj (F.obj j) ⟶ colimit (F ⋙ G))
    (colimit.ι (F ⋙ G) j : (F ⋙ G).obj j ⟶ colimit (F ⋙ G))

Tactic:
(isColimitOfPreserves G (colimit.isColimit _)).comp_coconePointUniqueUpToIso_hom _ j

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
t : Cocone F
w :
  ∀ (j : J),
    CategoryStruct.comp (Y := colimit (F ⋙ G)) (colimit.ι (F ⋙ G) j : (F ⋙ G).obj j ⟶ colimit (F ⋙ G))
        (CategoryStruct.comp (Y := G.obj (colimit F)) (Iso.inv (preservesColimitIso G F)) (G.map (colimit.desc F t)) :
          colimit (F ⋙ G) ⟶ G.obj t.pt) =
      CategoryStruct.comp (Y := colimit (F ⋙ G)) (colimit.ι (F ⋙ G) j) (colimit.desc (F ⋙ G) (G.mapCocone t))
⊢ Eq (α := colimit (F ⋙ G) ⟶ G.obj t.pt)
    (CategoryStruct.comp (Y := G.obj (colimit F)) (Iso.inv (preservesColimitIso G F)) (G.map (colimit.desc F t)) :
      colimit (F ⋙ G) ⟶ G.obj t.pt)
    (colimit.desc (F ⋙ G) (G.mapCocone t) : colimit (F ⋙ G) ⟶ (G.mapCocone t).pt)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
t : Cocone F
j : J
⊢ CategoryStruct.comp (Y := colimit (F ⋙ G)) (colimit.ι (F ⋙ G) j : (F ⋙ G).obj j ⟶ colimit (F ⋙ G))
      (CategoryStruct.comp (Y := G.obj (colimit F)) (Iso.inv (preservesColimitIso G F)) (G.map (colimit.desc F t)) :
        colimit (F ⋙ G) ⟶ G.obj t.pt) =
    CategoryStruct.comp (Y := colimit (F ⋙ G)) (colimit.ι (F ⋙ G) j) (colimit.desc (F ⋙ G) (G.mapCocone t))

Tactic:
simp [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
⊢ IsIso (X := colimit (F ⋙ G)) (Y := G.obj (colimit F)) (colimit.post F G)

Tactic:
show IsIso (preservesColimitIso G F).inv from inferInstance

Premises used: inferInstance, CategoryTheory.Limits.colimit.desc, CategoryTheory.Limits.colimit.post
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X : Functor.{w', v₁, w, u₁} J C
_ :
  ∀ {Y : Functor.{w', v₁, w, u₁} J C} (f : X ⟶ Y),
    Eq (α := Functor.obj (colim ⋙ G) X ⟶ Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) Y)
      (Functor.map (colim ⋙ G) f ≫
        Iso.hom
          ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) Y))
      (Iso.hom
          ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G)))
            X) ≫
        Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f)
⊢ ∀ {Y : Functor.{w', v₁, w, u₁} J C} (f : X ⟶ Y),
    Eq (α := Functor.obj (colim ⋙ G) X ⟶ Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) Y)
      (Functor.map (colim ⋙ G) f ≫
        Iso.hom
          ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) Y))
      (Iso.hom
          ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G)))
            X) ≫
        Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
rw :
  Eq (α := Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) X ⟶ Functor.obj (colim ⋙ G) Y)
    (Iso.inv
        ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) X) ≫
      Functor.map (colim ⋙ G) f)
    (Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f ≫
      Iso.inv
        ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) Y))
⊢ Eq (α := Functor.obj (colim ⋙ G) X ⟶ Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) Y)
    (Functor.map (colim ⋙ G) f ≫
      Iso.hom
        ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) Y))
    (Iso.hom
        ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) X) ≫
      Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f)

Tactic:
rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
w :
  ∀ (j : J),
    Eq (α := (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X).obj j ⟶ Functor.obj (colim ⋙ G) Y)
      (CategoryStruct.comp (Y := colimit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X))
        (colimit.ι (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X) j)
        (Iso.inv
            ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G)))
              X) ≫
          Functor.map (colim ⋙ G) f))
      (CategoryStruct.comp (Y := colimit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X))
        (colimit.ι (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X) j)
        (Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f ≫
          Iso.inv
            ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G)))
              Y)))
⊢ Eq (α := Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) X ⟶ Functor.obj (colim ⋙ G) Y)
    (Iso.inv
        ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) X) ≫
      Functor.map (colim ⋙ G) f)
    (Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f ≫
      Iso.inv
        ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G))) Y))

Tactic:
apply colimit.hom_ext

Premises used: CategoryTheory.Limits.colimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
j : J
w :
  Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
    (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j : (X ⋙ G).obj j ⟶ colimit (X ⋙ G))
      (CategoryStruct.comp (Y := G.obj (colimit X)) (Iso.inv (preservesColimitIso G X)) (G.map (colimMap f)) :
        colimit (X ⋙ G) ⟶ G.obj (colimit Y)))
    (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j)
      (CategoryStruct.comp (Y := colimit (Y ⋙ G))
        (colimMap (Functor.whiskerRight f G) : colimit (X ⋙ G) ⟶ colimit (Y ⋙ G))
        (Iso.inv (preservesColimitIso G Y) : colimit (Y ⋙ G) ⟶ G.obj (colimit Y))))
⊢ Eq (α := (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X).obj j ⟶ Functor.obj (colim ⋙ G) Y)
    (CategoryStruct.comp (Y := colimit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X))
      (colimit.ι (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X) j)
      (Iso.inv
          ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G)))
            X) ≫
        Functor.map (colim ⋙ G) f))
    (CategoryStruct.comp (Y := colimit (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X))
      (colimit.ι (Functor.obj (Functor.obj (Functor.whiskeringRight J C D) G) X) j)
      (Functor.map (Functor.obj (Functor.whiskeringRight J C D) G ⋙ colim) f ≫
        Iso.inv
          ((fun (F : Functor.{w', v₁, w, u₁} J C) ↦ (preservesColimitIso G F : G.obj (colimit F) ≅ colimit (F ⋙ G)))
            Y)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
j : J
w :
  Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
    (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j : (X ⋙ G).obj j ⟶ colimit (X ⋙ G))
      (CategoryStruct.comp (Y := G.obj (colimit X)) (Iso.inv (preservesColimitIso G X)) (G.map (colimMap f)) :
        colimit (X ⋙ G) ⟶ G.obj (colimit Y)))
    ((Functor.whiskerRight f G).app j ≫
      CategoryStruct.comp (Y := colimit (Y ⋙ G)) (colimit.ι (Y ⋙ G) j : (Y ⋙ G).obj j ⟶ colimit (Y ⋙ G))
        (Iso.inv (preservesColimitIso G Y) : colimit (Y ⋙ G) ⟶ G.obj (colimit Y)))
⊢ Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
    (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j : (X ⋙ G).obj j ⟶ colimit (X ⋙ G))
      (CategoryStruct.comp (Y := G.obj (colimit X)) (Iso.inv (preservesColimitIso G X)) (G.map (colimMap f)) :
        colimit (X ⋙ G) ⟶ G.obj (colimit Y)))
    (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j)
      (CategoryStruct.comp (Y := colimit (Y ⋙ G))
        (colimMap (Functor.whiskerRight f G) : colimit (X ⋙ G) ⟶ colimit (Y ⋙ G))
        (Iso.inv (preservesColimitIso G Y) : colimit (Y ⋙ G) ⟶ G.obj (colimit Y))))

Tactic:
rw [ι_colimMap_assoc]

Premises used: CategoryTheory.Limits.ι_colimMap_assoc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
j : J
w :
  Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
    (G.map (CategoryStruct.comp (Y := colimit X) (colimit.ι X j) (colimMap f))) (G.map (f.app j ≫ colimit.ι Y j))
⊢ Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
    (CategoryStruct.comp (Y := colimit (X ⋙ G)) (colimit.ι (X ⋙ G) j : (X ⋙ G).obj j ⟶ colimit (X ⋙ G))
      (CategoryStruct.comp (Y := G.obj (colimit X)) (Iso.inv (preservesColimitIso G X)) (G.map (colimMap f)) :
        colimit (X ⋙ G) ⟶ G.obj (colimit Y)))
    ((Functor.whiskerRight f G).app j ≫
      CategoryStruct.comp (Y := colimit (Y ⋙ G)) (colimit.ι (Y ⋙ G) j : (Y ⋙ G).obj j ⟶ colimit (Y ⋙ G))
        (Iso.inv (preservesColimitIso G Y) : colimit (Y ⋙ G) ⟶ G.obj (colimit Y)))

Tactic:
simp only [ι_preservesColimitIso_inv, Functor.whiskerRight_app,
        ι_preservesColimitIso_inv_assoc, ← G.map_comp]

Premises used: CategoryTheory.ι_preservesColimitIso_inv_assoc, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Functor.map_comp, CategoryTheory.ι_preservesColimitIso_inv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : PreservesColimit F G
inst_4 : HasColimit F
inst_5 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J G
inst_6 : HasColimitsOfShape.{w', w, v₂, u₂} J D
inst_7 : HasColimitsOfShape.{w', w, v₁, u₁} J C
X Y : Functor.{w', v₁, w, u₁} J C
f : X ⟶ Y
j : J
w w₁ : Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y)) (G.map (f.app j ≫ colimit.ι Y j)) (G.map (f.app j ≫ colimit.ι Y j))
⊢ Eq (α := G.obj (X.obj j) ⟶ G.obj (colimit Y))
    (G.map (CategoryStruct.comp (Y := colimit X) (colimit.ι X j) (colimMap f))) (G.map (f.app j ≫ colimit.ι Y j))

Tactic:
rw [ι_colimMap]

Premises used: CategoryTheory.Limits.ι_colimMap
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : HasColimit F
inst_4 : HasColimit (F ⋙ G)
inst_5 : IsIso (X := colimit (F ⋙ G)) (Y := G.obj (colimit F)) (colimit.post F G)
convert_2 :
  IsIso (X := (colimit.cocone (F ⋙ G)).pt) (Y := (G.mapCocone (colimit.cocone F)).pt)
    (IsColimit.desc (colimit.isColimit (F ⋙ G)) (G.mapCocone (colimit.cocone F)))
⊢ IsColimit (G.mapCocone (colimit.cocone F))

Tactic:
convert! IsColimit.ofPointIso (colimit.isColimit (F ⋙ G))
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Limits
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
J : Type w
inst_2 : Category.{w', w} J
F : Functor.{w', v₁, w, u₁} J C
inst_3 : HasColimit F
inst_4 : HasColimit (F ⋙ G)
inst_5 : IsIso (X := colimit (F ⋙ G)) (Y := G.obj (colimit F)) (colimit.post F G)
⊢ IsIso (X := (colimit.cocone (F ⋙ G)).pt) (Y := (G.mapCocone (colimit.cocone F)).pt)
    (IsColimit.desc (colimit.isColimit (F ⋙ G)) (G.mapCocone (colimit.cocone F)))

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : PreservesFiniteCoproducts F
n : ℕ
inst : PreservesColimitsOfShape (Discrete (Fin n))ᵒᵖ F
⊢ PreservesLimitsOfShape (Discrete (Fin n)) F.op

Tactic:
apply +allowSynthFailures preservesLimitsOfShape_op

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_op
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteCoproducts F
n : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin n))ᵒᵖ F

Tactic:
preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteCoproducts F
n : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin n))ᵒᵖ F

Tactic:
exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C Dᵒᵖ
inst_3 : PreservesFiniteCoproducts F
x : ℕ
inst : PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ PreservesLimitsOfShape (Discrete (Fin x)) F.leftOp

Tactic:
apply +allowSynthFailures preservesLimitsOfShape_leftOp

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_leftOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteCoproducts F
x : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteCoproducts F
x : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
Goal:
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
inst_3 : PreservesFiniteCoproducts F
x : ℕ
inst : PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F
⊢ PreservesLimitsOfShape (Discrete (Fin x)) F.rightOp

Tactic:
apply +allowSynthFailures preservesLimitsOfShape_rightOp

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_rightOp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteCoproducts F
x : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites
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 : PreservesFiniteCoproducts F
x : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x))ᵒᵖ F

Tactic:
exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Discrete.opposite, CategoryTheory.Equivalence.symm