awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder (hypothesis)
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
inst_4 : HasIterationOfShape.{w, v, u} J C
K : Type u_1
inst_5 : Category.{v_1, u_1} K
X : K
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape (C := Functor.{v_1, v, u_1, u} K C) (↑(Set.Iio j) : Type w) (Functor.obj (evaluation K C) X)
have this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C
Tactic: have := hasColimitsOfShape_of_isSuccLimit C j hj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder (hypothesis)
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
inst_4 : HasIterationOfShape.{w, v, u} J C
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape (C := Arrow.{v, u} C) (↑(Set.Iio j) : Type w) Arrow.leftFunc
have this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C
Tactic: have := hasColimitsOfShape_of_isSuccLimit C j hj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder (hypothesis)
Goal:
C : Type u
D : Type u'
E : Type u''
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
inst_2 : Category.{v'', u''} E
J : Type w
inst_3 : LinearOrder J
inst_4 : HasIterationOfShape.{w, v, u} J C
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape (C := Arrow.{v, u} C) (↑(Set.Iio j) : Type w) Arrow.rightFunc
have this : HasColimitsOfShape.{w, w, v, u} (↑(Set.Iio j) : Type w) C
Tactic: have := hasColimitsOfShape_of_isSuccLimit C j hj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ IsLimit (G.mapCone (Fan.mk P g)) ≃
    IsLimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
      (Fan.mk (G.obj P) fun (j : J) ↦ G.map (g j))
have refine_1 : Discrete.functor f ⋙ G ≅ Discrete.functor fun (j : J) ↦ G.obj (f j)
Tactic: refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
P : C
g : (j : J) → P ⟶ f j
refine_1 : Discrete.functor f ⋙ G ≅ Discrete.functor fun (j : J) ↦ G.obj (f j)
⊢ IsLimit (G.mapCone (Fan.mk P g)) ≃
    IsLimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
      (Fan.mk (G.obj P) fun (j : J) ↦ G.map (g j))
have refine_2 : Iso (C := Cone.{w, v₂, w, u₂} (J := Discrete J) (C := D) (Discrete.functor fun (j : J) ↦ G.obj (f j)))
  (Functor.obj (Cone.postcompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
    (G.mapCone (Fan.mk P g)))
  (Fan.mk (G.obj P) fun (j : J) ↦ G.map (g j))
Tactic: refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
P : C
g : (j : J) → P ⟶ f j
j : Discrete J
⊢ NatTrans.app
      (Cone.π
        (Functor.obj (Cone.postcompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
          (G.mapCone (Fan.mk P g))))
      j =
    Iso.hom
        (Iso.refl
          (Cone.pt (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
            (Functor.obj (Cone.postcompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
              (G.mapCone (Fan.mk P g))))) ≫
      NatTrans.app (Cone.π (Fan.mk (G.obj P) fun (j : J) ↦ G.map (g j))) j
have dsimp : G.map (g j.as) ≫ 𝟙 (G.obj (f j.as)) = 𝟙 (G.obj P) ≫ G.map (g j.as)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
P : C
g : (j : J) → P ⟶ f j
j : Discrete J
⊢ G.map (g j.as) ≫ 𝟙 (G.obj (f j.as)) = 𝟙 (G.obj P) ≫ G.map (g j.as)
have mk : ∀ (as : J),
  G.map (g { as := as : Discrete J }.as) ≫ 𝟙 (G.obj (f { as := as : Discrete J }.as)) =
    𝟙 (G.obj P) ≫ G.map (g { as := as }.as)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
inst_2 : HasProduct.{w, v₁, u₁} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
i : IsIso (X := G.obj (piObj.{w, v₁, u₁} f)) (Y := piObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (piComparison G f)
⊢ PreservesLimit (Discrete.functor f) G
have apply : IsLimit (G.mapCone (Fan.mk (piObj.{w, v₁, u₁} f) (Pi.π f)))
Tactic: apply preservesLimit_of_preserves_limit_cone (productIsProduct f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
inst_2 : HasProduct.{w, v₁, u₁} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
i : IsIso (X := G.obj (piObj.{w, v₁, u₁} f)) (Y := piObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (piComparison G f)
⊢ IsLimit (G.mapCone (Fan.mk (piObj.{w, v₁, u₁} f) (Pi.π f)))
have apply : IsLimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
  (Fan.mk (G.obj (piObj.{w, v₁, u₁} f)) fun (j : J) ↦ G.map (Pi.π f j))
Tactic: apply (isLimitMapConeFanMkEquiv _ _ _).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
P : C
g : (j : J) → f j ⟶ P
⊢ IsColimit (G.mapCocone (Cofan.mk P g)) ≃
    IsColimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
      (Cofan.mk (G.obj P) fun (j : J) ↦ G.map (g j))
have refine_1 : (Discrete.functor fun (j : J) ↦ G.obj (f j)) ≅ Discrete.functor f ⋙ G
Tactic: refine (IsColimit.precomposeHomEquiv ?_ _).symm.trans (IsColimit.equivIsoColimit ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
P : C
g : (j : J) → f j ⟶ P
refine_1 : (Discrete.functor fun (j : J) ↦ G.obj (f j)) ≅ Discrete.functor f ⋙ G
⊢ IsColimit (G.mapCocone (Cofan.mk P g)) ≃
    IsColimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
      (Cofan.mk (G.obj P) fun (j : J) ↦ G.map (g j))
have refine_2 : Iso (C := Cocone.{w, v₂, w, u₂} (J := Discrete J) (C := D) (Discrete.functor fun (j : J) ↦ G.obj (f j)))
  (Functor.obj (Cocone.precompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
    (G.mapCocone (Cofan.mk P g)))
  (Cofan.mk (G.obj P) fun (j : J) ↦ G.map (g j))
Tactic: refine (IsColimit.precomposeHomEquiv ?_ _).symm.trans (IsColimit.equivIsoColimit ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
P : C
g : (j : J) → f j ⟶ P
j : Discrete J
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
        (Functor.obj (Cocone.precompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
          (G.mapCocone (Cofan.mk P g))))
      (NatTrans.app
          (Cocone.ι
            (Functor.obj
              (Cocone.precompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
              (G.mapCocone (Cofan.mk P g))))
          j :
        Functor.obj.{w, v₂, w, u₂} (Discrete.functor fun (j : J) ↦ G.obj (f j)) j ⟶
          Functor.obj.{w, v₂, w, u₂}
            (Functor.obj (Functor.const (Discrete J))
              (Cocone.pt (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
                (Functor.obj
                  (Cocone.precompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
                  (G.mapCocone (Cofan.mk P g)))))
            j)
      (Iso.hom
        (Iso.refl
          (Cocone.pt (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
            (Functor.obj
              (Cocone.precompose (Iso.hom (Discrete.natIso fun (j : Discrete J) ↦ Iso.refl (G.obj (f j.as)))))
              (G.mapCocone (Cofan.mk P g)))))) =
    NatTrans.app (Cocone.ι (Cofan.mk (G.obj P) fun (j : J) ↦ G.map (g j))) j
have dsimp : (𝟙 (G.obj (f j.as)) ≫ G.map (g j.as)) ≫ 𝟙 (G.obj P) = G.map (g j.as)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
P : C
g : (j : J) → f j ⟶ P
j : Discrete J
⊢ (𝟙 (G.obj (f j.as)) ≫ G.map (g j.as)) ≫ 𝟙 (G.obj P) = G.map (g j.as)
have mk : ∀ (as : J),
  (𝟙 (G.obj (f { as := as : Discrete J }.as)) ≫ G.map (g { as := as : Discrete J }.as)) ≫ 𝟙 (G.obj P) =
    G.map (g { as := as }.as)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
inst_2 : HasCoproduct.{w, v₁, u₁} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
i :
  IsIso (X := sigmaObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (Y := G.obj (sigmaObj.{w, v₁, u₁} f))
    (sigmaComparison G f)
⊢ PreservesColimit (Discrete.functor f) G
have apply : IsColimit (G.mapCocone (Cofan.mk (sigmaObj.{w, v₁, u₁} f) (Sigma.ι f)))
Tactic: apply preservesColimit_of_preserves_colimit_cocone (coproductIsCoproduct f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products (goal)
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
f : J → C
inst_2 : HasCoproduct.{w, v₁, u₁} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (j : J) ↦ G.obj (f j)
i :
  IsIso (X := sigmaObj.{w, v₂, u₂} fun (b : J) ↦ G.obj (f b)) (Y := G.obj (sigmaObj.{w, v₁, u₁} f))
    (sigmaComparison G f)
⊢ IsColimit (G.mapCocone (Cofan.mk (sigmaObj.{w, v₁, u₁} f) (Sigma.ι f)))
have apply : IsColimit.{w, v₂, w, u₂} (J := Discrete J) (F := Discrete.functor fun (j : J) ↦ G.obj (f j))
  (Cofan.mk (G.obj (sigmaObj.{w, v₁, u₁} f)) fun (j : J) ↦ G.map (Sigma.ι f j))
Tactic: apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ (Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c) ≅ c.map G
have refine_1 : fst ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
  Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫ (c.map G).fst
Tactic: refine PullbackCone.ext (Iso.refl _) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
refine_1 :
  fst ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫ (c.map G).fst
⊢ (Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c) ≅ c.map G
have refine_2 : snd ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
  Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫ (c.map G).snd
Tactic: refine PullbackCone.ext (Iso.refl _) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ fst ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫ (c.map G).fst
have refine_1 : ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).π.app WalkingCospan.left =
  Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫
    (c.map G).π.app WalkingCospan.left
Tactic: dsimp only [fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ snd ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)) =
    Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫ (c.map G).snd
have refine_2 : ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).π.app WalkingCospan.right =
  Iso.hom (Iso.refl ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ G)).hom).obj (G.mapCone c)).pt) ≫
    (c.map G).π.app WalkingCospan.right
Tactic: dsimp only [snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst_2 : PreservesLimit (cospan f g) G
l : IsLimit (PullbackCone.mk h k comm)
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g
have rw : G.map (h ≫ f) = G.map k ≫ G.map g
Tactic: rw [← G.map_comp, ← G.map_comp, comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst_2 : PreservesLimit (cospan f g) G
l : IsLimit (PullbackCone.mk h k comm)
rw : G.map (h ≫ f) = G.map k ≫ G.map g
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g
have rw₁ : G.map (h ≫ f) = G.map (k ≫ g)
Tactic: rw [← G.map_comp, ← G.map_comp, comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ X
k : W ⟶ Y
comm : h ≫ f = k ≫ g
inst_2 : PreservesLimit (cospan f g) G
l : IsLimit (PullbackCone.mk h k comm)
rw : G.map (h ≫ f) = G.map k ≫ G.map g
rw₁ : G.map (h ≫ f) = G.map (k ≫ g)
⊢ G.map h ≫ G.map f = G.map k ≫ G.map g
have rw₂ : G.map (k ≫ g) = G.map (k ≫ g)
Tactic: rw [← G.map_comp, ← G.map_comp, comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (G.mapCone c)
have apply : IsLimit ((Cone.postcompose (diagramIsoCospan (cospan g f ⋙ G)).hom).obj (G.mapCone c))
Tactic: apply (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₂} _) _).toFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit ((Cone.postcompose (diagramIsoCospan (cospan g f ⋙ G)).hom).obj (G.mapCone c))
have apply : IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) sorry)
Tactic: apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) ⋯)
have ht : IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) sorry).flip
Tactic: apply PullbackCone.isLimitOfFlip
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) ⋯).flip
have ht : IsLimit (G.mapCone (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) sorry))
Tactic: apply (isLimitMapConePullbackConeEquiv _ _).toFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
ht : IsLimit (G.mapCone (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯))
⊢ IsLimit (PullbackCone.mk ((G.mapCone c).π.app WalkingCospan.left) ((G.mapCone c).π.app WalkingCospan.right) ⋯).flip
have apply : c.π.app WalkingCospan.right ≫ (cospan g f).map WalkingCospan.Hom.inr =
  c.π.app WalkingCospan.left ≫ (cospan g f).map WalkingCospan.Hom.inl
Tactic: apply (isLimitMapConePullbackConeEquiv _ _).toFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (G.mapCone (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯))
have ht : IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) sorry)
Tactic: refine @isLimitOfPreserves _ _ _ _ _ _ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
ht : IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯)
⊢ IsLimit (G.mapCone (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯))
have ht₁ : PreservesLimit (cospan ((cospan g f).map WalkingCospan.Hom.inr) ((cospan g f).map WalkingCospan.Hom.inl)) G
Tactic: refine @isLimitOfPreserves _ _ _ _ _ _ _ _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯)
have ht : IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) sorry).flip
Tactic: apply PullbackCone.isLimitOfFlip
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ⋯).flip
have apply : IsLimit ((Cone.postcompose (diagramIsoCospan (cospan g f)).hom).obj c)
Tactic: apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ (Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c) ≅ c.map G
have refine_1 : inl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
    Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
  (c.map G).inl
Tactic: refine PushoutCocone.ext (Iso.refl _) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
refine_1 :
  inl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
    (c.map G).inl
⊢ (Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c) ≅ c.map G
have refine_2 : inr ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
    Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
  (c.map G).inr
Tactic: refine PushoutCocone.ext (Iso.refl _) ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ inl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
    (c.map G).inl
have refine_1 : ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).ι.app WalkingSpan.left ≫
    Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
  (c.map G).ι.app WalkingSpan.left
Tactic: dsimp only [inl]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
c : PushoutCocone f g
G : Functor.{v₁, v₂, u₁, u₂} C D
⊢ inr ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)) ≫
      Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
    (c.map G).inr
have refine_2 : ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).ι.app WalkingSpan.right ≫
    Iso.hom (Iso.refl ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone c)).pt) =
  (c.map G).ι.app WalkingSpan.right
Tactic: dsimp only [inr]