awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preorder (goal)
Goal:
C : Type u
inst : Preorder C
J : Type u'
inst_1 : Category.{v, u'} J
F : CategoryTheory.Functor.{v, u, u', u} J C
c : Cocone F
x : C
i : J
p : F.obj i = x
⊢ x ≤ c.pt
have rw : F.obj i ≤ c.pt
Tactic: rw [← p]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preorder (hypothesis)
Goal:
C : Type u
inst : SemilatticeInf C
F : Discrete WalkingPair ⥤ C
⊢ HasLimit F
have this : HasLimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))
Tactic: have : HasLimit (pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)) :=
      ⟨⟨⟨_, isLimitBinaryFan (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preorder (hypothesis)
Goal:
C : Type u
inst : SemilatticeSup C
F : Discrete WalkingPair ⥤ C
⊢ HasColimit F
have this : HasColimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))
Tactic: have : HasColimit (pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)) :=
      ⟨⟨⟨_, isColimitBinaryCofan (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)⟩⟩⟩
-- 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_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ Subsingleton (PreservesLimit K F)
have allEq : ∀ (a b : PreservesLimit K 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_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ Subsingleton (PreservesColimit K F)
have allEq : ∀ (a b : PreservesColimit K 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 : 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 (PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F)
have allEq : ∀ (a b : PreservesLimitsOfShape.{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_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 (PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F)
have allEq : ∀ (a b : PreservesColimitsOfShape.{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 (PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
have allEq : ∀ (a b : PreservesLimitsOfSize.{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 (PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
have allEq : ∀ (a b : PreservesColimitsOfSize.{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 c
⊢ ∀ (s : Cone (K ⋙ 𝟭 C)) (j : J),
    CategoryStruct.comp (Y := Cone.pt (F := K ⋙ 𝟭 C) (Functor.mapCone (𝟭 C) c))
        ((fun (s : Cone (K ⋙ 𝟭 C)) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.pt.{w', v₁, w, u₁} (J := J) (F := K)
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt) K } :
                    Cone K } ⟶
                c.pt))
          s)
        (NatTrans.app (Cone.π (Functor.mapCone (𝟭 C) c)) 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 c)
  (s : Cone ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C))
  (j : J),
  CategoryStruct.comp (Y :=
      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))
      ((fun
            (s :
              Cone
                ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                  𝟭 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 })
                { 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 } } :
                  Cone
                    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                      Functor.{w', v₁, w, u₁} J C } } ⟶
              c.pt))
        s)
      (NatTrans.app (Cone.π (Functor.mapCone (𝟭 C) c)) 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 c
⊢ ∀ (s : Cone (K ⋙ 𝟭 C)) (m : s.pt ⟶ Cone.pt (F := K ⋙ 𝟭 C) (Functor.mapCone (𝟭 C) c)),
    (∀ (j : J), m ≫ NatTrans.app (Cone.π (Functor.mapCone (𝟭 C) c)) j = s.π.app j) →
      m =
        (fun (s : Cone (K ⋙ 𝟭 C)) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.pt.{w', v₁, w, u₁} (J := J) (F := K)
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt) K } :
                    Cone K } ⟶
                c.pt))
          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 c)
  (s : Cone ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C))
  (m :
    s.pt ⟶
      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)),
  (∀ (j : J), m ≫ NatTrans.app (Cone.π (Functor.mapCone (𝟭 C) c)) 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 } ⋙
                  𝟭 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 })
                { 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 } } :
                  Cone
                    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                      Functor.{w', v₁, w, u₁} J C } } ⟶
              c.pt))
        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 c
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (j : J),
    CategoryStruct.comp (Y :=
        Functor.obj.{w', v₁, w, u₁}
          (Functor.obj (Functor.const J) (Cocone.pt (F := K ⋙ 𝟭 C) (Functor.mapCocone (𝟭 C) c))) j)
        (NatTrans.app (Cocone.ι (Functor.mapCocone (𝟭 C) c)) j)
        ((fun (s : Cocone (K ⋙ 𝟭 C)) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              c.pt ⟶
                Cocone.pt.{w', v₁, w, u₁} (J := J) (F := K)
                  { 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 c)
  (s :
    Cocone ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C))
  (j : J),
  CategoryStruct.comp (Y :=
      Functor.obj.{w', v₁, w, u₁}
        (Functor.obj (Functor.const J)
          (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)))
        j)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (𝟭 C) c)) j)
      ((fun
            (s :
              Cocone
                ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                  𝟭 C)) ↦
          (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := sorry } } :
            c.pt ⟶
              Cocone.pt.{w', v₁, w, u₁} (J := J) (F :=
                { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp })
                { 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 c
⊢ ∀ (s : Cocone (K ⋙ 𝟭 C)) (m : Cocone.pt (F := K ⋙ 𝟭 C) (Functor.mapCocone (𝟭 C) c) ⟶ s.pt),
    (∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (𝟭 C) c)) j ≫ m = s.ι.app j) →
      m =
        (fun (s : Cocone (K ⋙ 𝟭 C)) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              c.pt ⟶
                Cocone.pt.{w', v₁, w, u₁} (J := J) (F := K)
                  { 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 c)
  (s :
    Cocone ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C))
  (m :
    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) ⟶
      s.pt),
  (∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (𝟭 C) c)) 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 } ⋙
                  𝟭 C)) ↦
          (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := sorry } } :
            c.pt ⟶
              Cocone.pt.{w', v₁, w, u₁} (J := J) (F :=
                { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp })
                { 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₁ K₂ : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
h : K₁ ≅ K₂
inst_3 : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
⊢ IsLimit (F.mapCone c)
have apply : IsLimit ((Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c))
Tactic: apply IsLimit.postcomposeInvEquiv (Functor.isoWhiskerRight h 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 : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
⊢ IsLimit ((Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c))
have have : (this : IsLimit ((Cone.postcompose h.inv).obj c)) →
  IsLimit ((Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c))
Tactic: have := (IsLimit.postcomposeInvEquiv h c).symm t
-- 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 : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : IsLimit ((Cone.postcompose h.inv).obj c)
⊢ IsLimit ((Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c))
have apply : F.mapCone ((Cone.postcompose h.inv).obj c) ≅ (Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c)
Tactic: apply IsLimit.ofIsoLimit (isLimitOfPreserves F this)
-- 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 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
⊢ IsLimit (F.mapCone c)
have have : (this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))) → IsLimit (F.mapCone c)
Tactic: have := (isLimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.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
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 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
⊢ IsLimit (F.mapCone c)
have apply : (Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c))) ≅ F.mapCone c
Tactic: apply ((IsLimit.postcomposeHomEquiv equ _).symm this).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 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
⊢ (Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c))) ≅ F.mapCone c
have refine : ∀ (j : J'),
  ((Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).π.app j =
    Iso.hom
        (Iso.refl
          ((Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).pt) ≫
      (F.mapCone c).π.app j
Tactic: refine Cone.ext (Iso.refl _) fun j => ?_
-- 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 : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
⊢ IsColimit (F.mapCocone c)
have apply : IsColimit ((Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c))
Tactic: apply IsColimit.precomposeHomEquiv (Functor.isoWhiskerRight h 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 : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
⊢ IsColimit ((Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c))
have have : (this : IsColimit ((Cocone.precompose h.hom).obj c)) →
  IsColimit ((Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c))
Tactic: have := (IsColimit.precomposeHomEquiv h c).symm t
-- 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 : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
this : IsColimit ((Cocone.precompose h.hom).obj c)
⊢ IsColimit ((Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c))
have apply : F.mapCocone ((Cocone.precompose h.hom).obj c) ≅
  (Cocone.precompose (Functor.isoWhiskerRight h F).hom).obj (F.mapCocone c)
Tactic: apply IsColimit.ofIsoColimit (isColimitOfPreserves F this)
-- 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 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
⊢ IsColimit (F.mapCocone c)
have have : (this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))) →
  IsColimit (F.mapCocone c)
Tactic: have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.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
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 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ IsColimit (F.mapCocone c)
have apply : (Cocone.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c))) ≅
  F.mapCocone c
Tactic: apply ((IsColimit.precomposeInvEquiv equ _).symm this).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 : PreservesColimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F
K : Functor.{w₂', v₁, w₂, u₁} J' C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ (Cocone.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c))) ≅
    F.mapCocone c
have refine : ∀ (j : J'),
  ((Cocone.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).ι.app j ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose equ.inv).obj
              (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).pt) =
    (F.mapCocone c).ι.app j
Tactic: refine Cocone.ext (Iso.refl _) fun j => ?_
-- 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_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ Subsingleton (ReflectsLimit K F)
have allEq : ∀ (a b : ReflectsLimit K 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_1 K : Functor.{w', v₁, w, u₁} J C
F : Functor.{v₁, v₂, u₁, u₂} C D
⊢ Subsingleton (ReflectsColimit K F)
have allEq : ∀ (a b : ReflectsColimit K 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 : 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 (ReflectsLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F)
have allEq : ∀ (a b : ReflectsLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} J F), a = b
Tactic: constructor