awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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
⊢ Subsingleton (ReflectsColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F)
have allEq : ∀ (a b : ReflectsColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F), a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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
⊢ Subsingleton (ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
have allEq : ∀ (a b : ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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
⊢ Subsingleton (ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
have allEq : ∀ (a b : ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F), a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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)
⊢ ∀ (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
have 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 := sorry } } :
            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 := sorry :
                      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
Tactic: cases K
Cleared hypotheses: K, c, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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)
⊢ ∀ (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
have 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 := sorry } } :
            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 := sorry :
                      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
Tactic: cases K
Cleared hypotheses: K, c, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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)
⊢ ∀ (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
have 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 := sorry } } :
            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 := sorry } }))
        s =
    s.ι.app j
Tactic: cases K
Cleared hypotheses: K, c, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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)
⊢ ∀ (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
have 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 := sorry } } :
            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 := sorry } }))
        s
Tactic: cases K
Cleared hypotheses: K, c, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 (F.mapCone c)
have t : IsLimit (G.mapCone (F.mapCone c))
Tactic: apply isLimitOfReflects G
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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)
⊢ IsLimit c
have apply : IsLimit (F.mapCone ((Cone.postcompose h.inv).obj c))
Tactic: apply IsLimit.postcomposeInvEquiv h c (isLimitOfReflects F _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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)
⊢ IsLimit (F.mapCone ((Cone.postcompose h.inv).obj c))
have apply : (Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c) ≅ F.mapCone ((Cone.postcompose h.inv).obj c)
Tactic: apply ((IsLimit.postcomposeInvEquiv (Functor.isoWhiskerRight h F :) _).symm t).ofIsoLimit _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 c
have apply : IsLimit (Cone.whisker e.functor c)
Tactic: apply IsLimit.ofWhiskerEquivalence e
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 c)
have t₁ : IsLimit (F.mapCone (Cone.whisker e.functor c))
Tactic: apply isLimitOfReflects F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 (F.mapCone (Cone.whisker e.functor c))
have apply : IsLimit (Cone.whisker e.functor (F.mapCone c))
Tactic: apply IsLimit.ofIsoLimit _ (Functor.mapConeWhisker _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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)
⊢ Nonempty (IsLimit c)
have suffices : IsIso (Y := (limit.cone F).pt) (IsLimit.lift (limit.isLimit F) c)
Tactic: suffices IsIso (IsLimit.lift (limit.isLimit F) c) from ⟨by
      apply IsLimit.ofPointIso (limit.isLimit F)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 := (limit.cone F).pt) (IsLimit.lift (limit.isLimit F) c)
have change : IsIso (Y := (Cone.forget F).obj (limit.cone F)) ((Cone.forget F).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
Tactic: change IsIso ((Cone.forget _).map ((limit.isLimit F).liftConeMorphism c))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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.forget F).obj (limit.cone F)) ((Cone.forget F).map (IsLimit.liftConeMorphism (limit.isLimit F) c))
have suffices : IsIso (Y := limit.cone F) (IsLimit.liftConeMorphism (limit.isLimit F) c)
Tactic: suffices IsIso (IsLimit.liftConeMorphism (limit.isLimit F) c) from by
      apply (Cone.forget F).map_isIso _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 := limit.cone F) (IsLimit.liftConeMorphism (limit.isLimit F) c)
have suffices : IsIso (Y := (Cone.functoriality F G).obj (limit.cone F))
  ((Cone.functoriality F G).map (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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 (F.mapCocone c)
have t : IsColimit (G.mapCocone (F.mapCocone c))
Tactic: apply isColimitOfReflects G
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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)
⊢ IsColimit c
have apply : IsColimit (F.mapCocone ((Cocone.precompose h.hom).obj c))
Tactic: apply IsColimit.precomposeHomEquiv h c (isColimitOfReflects F _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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)
⊢ IsColimit (F.mapCocone ((Cocone.precompose h.hom).obj c))
have apply : (Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c) ≅
  F.mapCocone ((Cocone.precompose h.hom).obj c)
Tactic: apply ((IsColimit.precomposeHomEquiv (Functor.isoWhiskerRight h F :) _).symm t).ofIsoColimit _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 c
have apply : IsColimit (Cocone.whisker e.functor c)
Tactic: apply IsColimit.ofWhiskerEquivalence e
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 c)
have t₁ : IsColimit (F.mapCocone (Cocone.whisker e.functor c))
Tactic: apply isColimitOfReflects F
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 (F.mapCocone (Cocone.whisker e.functor c))
have apply : IsColimit (Cocone.whisker e.functor (F.mapCocone c))
Tactic: apply IsColimit.ofIsoColimit _ (Functor.mapCoconeWhisker _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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)
⊢ Nonempty (IsColimit c)
have suffices : IsIso (X := (colimit.cocone F).pt) (IsColimit.desc (colimit.isColimit F) c)
Tactic: suffices IsIso (IsColimit.desc (colimit.isColimit F) c) from ⟨by
      apply IsColimit.ofPointIso (colimit.isColimit F)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 := (colimit.cocone F).pt) (IsColimit.desc (colimit.isColimit F) c)
have change : IsIso (X := (Cocone.forget F).obj (colimit.cocone F))
  ((Cocone.forget F).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
Tactic: change IsIso ((Cocone.forget _).map ((colimit.isColimit F).descCoconeMorphism c))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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.forget F).obj (colimit.cocone F))
    ((Cocone.forget F).map (IsColimit.descCoconeMorphism (colimit.isColimit F) c))
have suffices : IsIso (X := colimit.cocone F) (IsColimit.descCoconeMorphism (colimit.isColimit F) c)
Tactic: suffices IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c) from by
      apply (Cocone.forget F).map_isIso _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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 := colimit.cocone F) (IsColimit.descCoconeMorphism (colimit.isColimit F) c)
have suffices : IsIso (X := (Cocone.functoriality F G).obj (colimit.cocone F))
  ((Cocone.functoriality F G).map (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)