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
allEq : ∀ (a b : ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
⊢ Subsingleton (ReflectsColimitsOfSize.{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], ReflectsColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J 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_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : ReflectsLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
⊢ ReflectsLimit K F

Tactic:
ReflectsLimitsOfShape.reflectsLimit

Premises used: CategoryTheory.Limits.ReflectsLimitsOfShape.reflectsLimit
-- 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
inst_3 : ReflectsColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
⊢ ReflectsColimit K F

Tactic:
ReflectsColimitsOfShape.reflectsColimit

Premises used: CategoryTheory.Limits.ReflectsColimitsOfShape.reflectsColimit
-- 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
inst_4 : ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
⊢ ReflectsLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F

Tactic:
ReflectsLimitsOfSize.reflectsLimitsOfShape

Premises used: CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsLimitsOfShape
-- 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
inst_4 : ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
⊢ ReflectsColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F

Tactic:
ReflectsColimitsOfSize.reflectsColimitsOfShape

Premises used: CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsColimitsOfShape
-- 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
J : Type w'
𝒥 : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cone K
h : IsLimit (F := K ⋙ 𝟭 C) (Functor.mapCone (𝟭 C) c)
mk :
  ∀ (obj : J → C) (map : {X Y : J} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : J), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    {c : Cone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }}
    (h :
      IsLimit (F :=
        { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙ 𝟭 C)
        (Functor.mapCone (𝟭 C) c))
    (s : Cone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C })
    (j : J),
    (fun (s : Cone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.pt.{w, v₁, w', u₁} (J := J) (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt)
                          ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                              Functor.{w, v₁, w', u₁} J C } ⋙
                            𝟭 C) } :
                    Cone
                      ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                          Functor.{w, v₁, w', u₁} J C } ⋙
                        𝟭 C) } ⟶
                Cone.pt (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  (Functor.mapCone (𝟭 C) c)))
          s ≫
        c.π.app j =
      s.π.app j
⊢ ∀ (s : Cone K) (j : J),
    (fun (s : Cone K) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.pt.{w, v₁, w', u₁} (J := J) (F := K ⋙ 𝟭 C)
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt) (K ⋙ 𝟭 C) } :
                    Cone (K ⋙ 𝟭 C) } ⟶
                Cone.pt (F := K ⋙ 𝟭 C) (Functor.mapCone (𝟭 C) c)))
          s ≫
        c.π.app j =
      s.π.app j

Tactic:
cases K
-- 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
J : Type w'
𝒥 : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cone K
h : IsLimit (F := K ⋙ 𝟭 C) (Functor.mapCone (𝟭 C) c)
mk :
  ∀ (obj : J → C) (map : {X Y : J} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : J), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    {c : Cone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }}
    (h :
      IsLimit (F :=
        { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙ 𝟭 C)
        (Functor.mapCone (𝟭 C) c))
    (s : Cone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C })
    (m : s.pt ⟶ c.pt),
    (∀ (j : J), m ≫ c.π.app j = s.π.app j) →
      m =
        (fun
              (s :
                Cone
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.pt.{w, v₁, w', u₁} (J := J) (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt)
                          ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                              Functor.{w, v₁, w', u₁} J C } ⋙
                            𝟭 C) } :
                    Cone
                      ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                          Functor.{w, v₁, w', u₁} J C } ⋙
                        𝟭 C) } ⟶
                Cone.pt (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  (Functor.mapCone (𝟭 C) c)))
          s
⊢ ∀ (s : Cone K) (m : s.pt ⟶ c.pt),
    (∀ (j : J), m ≫ c.π.app j = s.π.app j) →
      m =
        (fun (s : Cone K) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.pt.{w, v₁, w', u₁} (J := J) (F := K ⋙ 𝟭 C)
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt) (K ⋙ 𝟭 C) } :
                    Cone (K ⋙ 𝟭 C) } ⟶
                Cone.pt (F := K ⋙ 𝟭 C) (Functor.mapCone (𝟭 C) c)))
          s

Tactic:
cases K
-- 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
J : Type w'
𝒥 : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cocone K
h : IsColimit (F := K ⋙ 𝟭 C) (Functor.mapCocone (𝟭 C) c)
mk :
  ∀ (obj : J → C) (map : {X Y : J} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : J), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    {c : Cocone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }}
    (h :
      IsColimit (F :=
        { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙ 𝟭 C)
        (Functor.mapCocone (𝟭 C) c))
    (s : Cocone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C })
    (j : J),
    c.ι.app j ≫
        (fun
              (s :
                Cocone
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              Cocone.pt (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  (Functor.mapCocone (𝟭 C) c) ⟶
                Cocone.pt.{w, v₁, w', u₁} (J := J) (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } }))
          s =
      s.ι.app j
⊢ ∀ (s : Cocone K) (j : J),
    c.ι.app j ≫
        (fun (s : Cocone K) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              Cocone.pt (F := K ⋙ 𝟭 C) (Functor.mapCocone (𝟭 C) c) ⟶
                Cocone.pt.{w, v₁, w', u₁} (J := J) (F := K ⋙ 𝟭 C)
                  { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } }))
          s =
      s.ι.app j

Tactic:
cases K
-- 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
J : Type w'
𝒥 : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cocone K
h : IsColimit (F := K ⋙ 𝟭 C) (Functor.mapCocone (𝟭 C) c)
mk :
  ∀ (obj : J → C) (map : {X Y : J} → (X ⟶ Y) → (obj X ⟶ obj Y)) (map_id : ∀ (X : J), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    {c : Cocone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }}
    (h :
      IsColimit (F :=
        { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙ 𝟭 C)
        (Functor.mapCocone (𝟭 C) c))
    (s : Cocone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C })
    (m : c.pt ⟶ s.pt),
    (∀ (j : J), c.ι.app j ≫ m = s.ι.app j) →
      m =
        (fun
              (s :
                Cocone
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              Cocone.pt (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  (Functor.mapCocone (𝟭 C) c) ⟶
                Cocone.pt.{w, v₁, w', u₁} (J := J) (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } }))
          s
⊢ ∀ (s : Cocone K) (m : c.pt ⟶ s.pt),
    (∀ (j : J), c.ι.app j ≫ m = s.ι.app j) →
      m =
        (fun (s : Cocone K) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              Cocone.pt (F := K ⋙ 𝟭 C) (Functor.mapCocone (𝟭 C) c) ⟶
                Cocone.pt.{w, v₁, w', u₁} (J := J) (F := K ⋙ 𝟭 C)
                  { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } }))
          s

Tactic:
cases K
-- 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 : ReflectsLimit K F
inst_4 : ReflectsLimit (K ⋙ F) G
⊢ ReflectsLimit K (F ⋙ G)

Tactic:
⟨fun h => ReflectsLimit.reflects (isLimitOfReflects G h)⟩

Premises used: CategoryTheory.Limits.isLimitOfReflects, CategoryTheory.Limits.ReflectsLimit.reflects, CategoryTheory.Limits.ReflectsLimit.mk
-- 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 : ReflectsColimit K F
inst_4 : ReflectsColimit (K ⋙ F) G
⊢ ReflectsColimit K (F ⋙ G)

Tactic:
⟨fun h => ReflectsColimit.reflects (isColimitOfReflects G h)⟩

Premises used: CategoryTheory.Limits.ReflectsColimit.mk, CategoryTheory.Limits.isColimitOfReflects, CategoryTheory.Limits.ReflectsColimit.reflects
-- 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 : PreservesLimit K (F ⋙ G)
inst_4 : ReflectsLimit (K ⋙ F) G
c : Cone K
h : IsLimit c
t : IsLimit (G.mapCone (F.mapCone c))
⊢ IsLimit (F.mapCone c)

Tactic:
apply isLimitOfReflects G

Premises used: CategoryTheory.Limits.isLimitOfReflects
-- 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 : PreservesLimit K (F ⋙ G)
inst_4 : ReflectsLimit (K ⋙ F) G
c : Cone K
h : IsLimit c
⊢ IsLimit (G.mapCone (F.mapCone c))

Tactic:
apply isLimitOfPreserves (F ⋙ G) h

Premises used: CategoryTheory.Functor.comp, 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 : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
apply : IsLimit (F.mapCone ((Cone.postcompose h.inv).obj c))
⊢ IsLimit c

Tactic:
apply IsLimit.postcomposeInvEquiv h c (isLimitOfReflects F _)

Premises used: CategoryTheory.Limits.IsLimit.postcomposeInvEquiv, CategoryTheory.Limits.isLimitOfReflects, 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 : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
apply :
  (Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c) ≅ F.mapCone ((Cone.postcompose h.inv).obj c)
⊢ IsLimit (F.mapCone ((Cone.postcompose h.inv).obj c))

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

Premises used: CategoryTheory.Limits.IsLimit.postcomposeInvEquiv, Equiv.symm, CategoryTheory.Functor.isoWhiskerRight, 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
K₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ (Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c) ≅ F.mapCone ((Cone.postcompose h.inv).obj 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
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 : ReflectsLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cone K
t : IsLimit (F.mapCone c)
apply : IsLimit (Cone.whisker e.functor c)
⊢ IsLimit c

Tactic:
apply IsLimit.ofWhiskerEquivalence e

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

Tactic:
apply isLimitOfReflects F

Premises used: CategoryTheory.Limits.isLimitOfReflects
-- 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 : ReflectsLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cone K
t : IsLimit (F.mapCone c)
apply : IsLimit (Cone.whisker e.functor (F.mapCone c))
⊢ IsLimit (F.mapCone (Cone.whisker e.functor c))

Tactic:
apply IsLimit.ofIsoLimit _ (Functor.mapConeWhisker _).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Limits.IsLimit.ofIsoLimit, CategoryTheory.Functor.mapConeWhisker
-- 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 : ReflectsLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (Cone.whisker e.functor (F.mapCone c))

Tactic:
exact IsLimit.whiskerEquivalence t _

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

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

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

Tactic:
reflectsLimitsOfSize_shrink F

Premises used: CategoryTheory.Limits.reflectsLimitsOfSize_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 : HasLimit F
inst_5 : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso (Y := (limit.cone F).pt) (IsLimit.lift (limit.isLimit F) c)
⊢ IsLimit c

Tactic:
apply IsLimit.ofPointIso (limit.isLimit F)

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.IsLimit.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 : HasLimit F
inst_5 : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
suffices : IsIso (Y := (limit.cone F).pt) (IsLimit.lift (limit.isLimit F) c)
⊢ Nonempty (IsLimit c)

Tactic:
suffices IsIso (IsLimit.lift (limit.isLimit F) c) from ⟨by
      apply IsLimit.ofPointIso (limit.isLimit 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 : HasLimit F
inst_5 : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
change :
  IsIso (Y := (Cone.forget F).obj (limit.cone F)) ((Cone.forget F).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
⊢ IsIso (Y := (limit.cone F).pt) (IsLimit.lift (limit.isLimit F) c)

Tactic:
change IsIso ((Cone.forget _).map ((limit.isLimit F).liftConeMorphism c))

Premises used: CategoryTheory.IsIso, CategoryTheory.Functor.map, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.IsLimit.liftConeMorphism, CategoryTheory.Limits.Cone.forget
-- 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 := limit.cone F) (IsLimit.liftConeMorphism (limit.isLimit F) c)
⊢ IsIso (Y := (Cone.forget F).obj (limit.cone F)) ((Cone.forget F).map (IsLimit.liftConeMorphism (limit.isLimit F) c))

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

Premises used: CategoryTheory.Functor.map_isIso, CategoryTheory.Limits.Cone.forget
-- 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 := limit.cone F) (IsLimit.liftConeMorphism (limit.isLimit F) c)
⊢ IsIso (Y := (Cone.forget F).obj (limit.cone F)) ((Cone.forget F).map (IsLimit.liftConeMorphism (limit.isLimit F) c))

Tactic:
suffices IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c) from by
      apply (Cone.forget F).map_isIso _