awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasCokernel g
inst_9 : HasCokernel (G.map g)
inst_10 : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ Eq (α := G.obj (cokernel f) ⟶ cokernel (G.map g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (cokernel g)) (G.map (cokernel.map f g p q hpq))
      (Iso.hom (PreservesCokernel.iso G g)))
have rw : Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
  (CategoryStruct.comp (Y := cokernel (G.map g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) sorry))
    (Iso.inv (PreservesCokernel.iso G g)))
  (G.map (cokernel.map f g p q hpq))
Tactic: rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
    cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasCokernel g
inst_9 : HasCokernel (G.map g)
inst_10 : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw :
  Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g))
      (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
        (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
      (Iso.inv (PreservesCokernel.iso G g)))
    (G.map (cokernel.map f g p q hpq))
⊢ Eq (α := G.obj (cokernel f) ⟶ cokernel (G.map g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (cokernel g)) (G.map (cokernel.map f g p q hpq))
      (Iso.hom (PreservesCokernel.iso G g)))
have rw₁ : Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
  (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
    (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) sorry)
      (Iso.inv (PreservesCokernel.iso G g))))
  (G.map (cokernel.map f g p q hpq))
Tactic: rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
    cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasCokernel g
inst_9 : HasCokernel (G.map g)
inst_10 : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw :
  Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g))
      (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
        (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
      (Iso.inv (PreservesCokernel.iso G g)))
    (G.map (cokernel.map f g p q hpq))
rw₁ :
  Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
        (Iso.inv (PreservesCokernel.iso G g))))
    (G.map (cokernel.map f g p q hpq))
⊢ Eq (α := G.obj (cokernel f) ⟶ cokernel (G.map g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (cokernel g)) (G.map (cokernel.map f g p q hpq))
      (Iso.hom (PreservesCokernel.iso G g)))
have rw₂ : Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
  (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) sorry)
    (Iso.inv (PreservesCokernel.iso G g)))
  (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
    (G.map (cokernel.map f g p q hpq)))
Tactic: rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
    cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasCokernel g
inst_9 : HasCokernel (G.map g)
inst_10 : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw :
  Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g))
      (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
        (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
      (Iso.inv (PreservesCokernel.iso G g)))
    (G.map (cokernel.map f g p q hpq))
rw₁ :
  Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
        (Iso.inv (PreservesCokernel.iso G g))))
    (G.map (cokernel.map f g p q hpq))
rw₂ :
  Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (Iso.inv (PreservesCokernel.iso G g)))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
      (G.map (cokernel.map f g p q hpq)))
⊢ Eq (α := G.obj (cokernel f) ⟶ cokernel (G.map g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (cokernel g)) (G.map (cokernel.map f g p q hpq))
      (Iso.hom (PreservesCokernel.iso G g)))
have rw₃ : Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
  (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) sorry)
    (cokernelComparison g G))
  (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
    (G.map (cokernel.map f g p q hpq)))
Tactic: rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
    cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasCokernel g
inst_9 : HasCokernel (G.map g)
inst_10 : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw :
  Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g))
      (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
        (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
      (Iso.inv (PreservesCokernel.iso G g)))
    (G.map (cokernel.map f g p q hpq))
rw₁ :
  Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
        (Iso.inv (PreservesCokernel.iso G g))))
    (G.map (cokernel.map f g p q hpq))
rw₂ :
  Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (Iso.inv (PreservesCokernel.iso G g)))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
      (G.map (cokernel.map f g p q hpq)))
rw₃ :
  Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (cokernelComparison g G))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
      (G.map (cokernel.map f g p q hpq)))
⊢ Eq (α := G.obj (cokernel f) ⟶ cokernel (G.map g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (cokernel g)) (G.map (cokernel.map f g p q hpq))
      (Iso.hom (PreservesCokernel.iso G g)))
have rw₄ : Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
  (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.map f g p q hpq)))
  (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
    (G.map (cokernel.map f g p q hpq)))
Tactic: rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
    cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst_8 : HasCokernel g
inst_9 : HasCokernel (G.map g)
inst_10 : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw :
  Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g))
      (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
        (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
      (Iso.inv (PreservesCokernel.iso G g)))
    (G.map (cokernel.map f g p q hpq))
rw₁ :
  Eq (α := G.obj (cokernel f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
        (Iso.inv (PreservesCokernel.iso G g))))
    (G.map (cokernel.map f g p q hpq))
rw₂ :
  Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (Iso.inv (PreservesCokernel.iso G g)))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
      (G.map (cokernel.map f g p q hpq)))
rw₃ :
  Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := cokernel (G.map g)) (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (cokernelComparison g G))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
      (G.map (cokernel.map f g p q hpq)))
rw₄ :
  Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.map f g p q hpq)))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
      (G.map (cokernel.map f g p q hpq)))
hpq₁ : f ≫ q = p ≫ g
⊢ Eq (α := G.obj (cokernel f) ⟶ cokernel (G.map g))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (Iso.hom (PreservesCokernel.iso G f))
      (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯))
    (CategoryStruct.comp (Y := G.obj (cokernel g)) (G.map (cokernel.map f g p q hpq))
      (Iso.hom (PreservesCokernel.iso G g)))
have rw₅ : Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel g))
  (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.map f g p q hpq)))
  (CategoryStruct.comp (Y := G.obj (cokernel f)) (cokernelComparison f G) (G.map (cokernel.map f g p q hpq)))
Tactic: rw [← Iso.comp_inv_eq, Category.assoc, ← Iso.eq_inv_comp, PreservesCokernel.iso_inv,
    cokernel_map_comp_cokernelComparison, PreservesCokernel.iso_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
c : Cone.{0, v₁, 0, u₁} (C := C) (parallelPair (X := X) (Y := Y) 0 0)
hc : IsLimit c
⊢ IsLimit (G.mapCone c)
have this : IsIso (Fork.ι c)
Tactic: have := KernelFork.IsLimit.isIso_ι c hc rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
c : Cone.{0, v₁, 0, u₁} (C := C) (parallelPair (X := X) (Y := Y) 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ IsLimit (G.mapCone c)
have refine : IsLimit (F := parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0) (KernelFork.map c G)
Tactic: refine (KernelFork.isLimitMapConeEquiv c G).symm ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
c : Cone.{0, v₁, 0, u₁} (C := C) (parallelPair (X := X) (Y := Y) 0 0)
hc : IsLimit c
this : IsIso (Fork.ι c)
⊢ IsLimit (F := parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0) (KernelFork.map c G)
have refine : Iso (C := Cone (parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0)) (KernelFork.ofι (𝟙 (G.obj X)) sorry)
  (KernelFork.map c G)
Tactic: refine IsLimit.ofIsoLimit (KernelFork.IsLimit.ofId _ (G.map_zero _ _)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
c : Cocone.{0, v₁, 0, u₁} (C := C) (parallelPair (X := X) (Y := Y) 0 0)
hc : IsColimit c
⊢ IsColimit (G.mapCocone c)
have this : IsIso (Cofork.π c)
Tactic: have := CokernelCofork.IsColimit.isIso_π c hc rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
c : Cocone.{0, v₁, 0, u₁} (C := C) (parallelPair (X := X) (Y := Y) 0 0)
hc : IsColimit c
this : IsIso (Cofork.π c)
⊢ IsColimit (G.mapCocone c)
have refine : IsColimit (F := parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0) (CokernelCofork.map c G)
Tactic: refine (CokernelCofork.isColimitMapCoconeEquiv c G).symm ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
c : Cocone.{0, v₁, 0, u₁} (C := C) (parallelPair (X := X) (Y := Y) 0 0)
hc : IsColimit c
this : IsIso (Cofork.π c)
⊢ IsColimit (F := parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0) (CokernelCofork.map c G)
have refine : Iso (C := Cocone (parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0)) (CokernelCofork.ofπ (𝟙 (G.obj Y)) sorry)
  (CokernelCofork.map c G)
Tactic: refine IsColimit.ofIsoColimit (CokernelCofork.IsColimit.ofId _ (G.map_zero _ _)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
f : X ⟶ Y
hf : f = 0
⊢ PreservesLimit (parallelPair f 0) G
have rw : PreservesLimit (parallelPair (X := X) (Y := Y) 0 0) G
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
X Y : C
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : G.PreservesZeroMorphisms
f : X ⟶ Y
hf : f = 0
⊢ PreservesColimit (parallelPair f 0) G
have rw : PreservesColimit (parallelPair (X := X) (Y := Y) 0 0) G
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex.{w, w', v_1, u_1} J C
c : Multicofork d
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J.L
⊢ Eq (α := (d.map F).left j ⟶ F.obj c.pt) ((d.map F).fst j ≫ (fun (i : J.R) ↦ F.map (c.π i)) (J.fst j))
    ((d.map F).snd j ≫ (fun (i : J.R) ↦ F.map (c.π i)) (J.snd j))
have dsimp : F.map (d.fst j) ≫ F.map (c.π (J.fst j)) = F.map (d.snd j) ≫ F.map (c.π (J.snd j))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex.{w, w', v_1, u_1} J C
c : Multicofork d
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J.L
⊢ F.map (d.fst j) ≫ F.map (c.π (J.fst j)) = F.map (d.snd j) ≫ F.map (c.π (J.snd j))
have rw : F.map (d.fst j ≫ c.π (J.fst j)) = F.map (d.snd j) ≫ F.map (c.π (J.snd j))
Tactic: rw [← F.map_comp, ← F.map_comp, condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex.{w, w', v_1, u_1} J C
c : Multicofork d
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J.L
rw : F.map (d.fst j ≫ c.π (J.fst j)) = F.map (d.snd j) ≫ F.map (c.π (J.snd j))
⊢ F.map (d.fst j) ≫ F.map (c.π (J.fst j)) = F.map (d.snd j) ≫ F.map (c.π (J.snd j))
have rw₁ : F.map (d.fst j ≫ c.π (J.fst j)) = F.map (d.snd j ≫ c.π (J.snd j))
Tactic: rw [← F.map_comp, ← F.map_comp, condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex.{w, w', v_1, u_1} J C
c : Multicofork d
F : Functor.{v_1, v_2, u_1, u_2} C D
j : J.L
rw : F.map (d.fst j ≫ c.π (J.fst j)) = F.map (d.snd j) ≫ F.map (c.π (J.snd j))
rw₁ : F.map (d.fst j ≫ c.π (J.fst j)) = F.map (d.snd j ≫ c.π (J.snd j))
⊢ F.map (d.fst j) ≫ F.map (c.π (J.fst j)) = F.map (d.snd j) ≫ F.map (c.π (J.snd j))
have rw₂ : F.map (d.snd j ≫ c.π (J.snd j)) = F.map (d.snd j ≫ c.π (J.snd j))
Tactic: rw [← F.map_comp, ← F.map_comp, condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex.{w, w', v_1, u_1} J C
c : Multicofork d
F : Functor.{v_1, v_2, u_1, u_2} C D
i : J.R
⊢ π ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)) i ≫
      Iso.hom (Iso.refl ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)).pt) =
    (c.map F).π i
have dsimp : Eq (α := (d.map F).right i ⟶ (c.map F).pt)
  (((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)).ι.app (WalkingMultispan.right i) ≫
      Iso.hom (Iso.refl ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)).pt) :
    (d.map F).right i ⟶ (c.map F).pt)
  ((c.map F).ι.app (WalkingMultispan.right i) :
    (d.map F).multispan.obj (WalkingMultispan.right i) ⟶
      Functor.obj (Functor.obj (Functor.const (WalkingMultispan J)) (c.map F).pt) (WalkingMultispan.right i))
Tactic: dsimp only [Multicofork.π]
-- 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
F : Functor.{w, v, w, u} J C
G : Functor.{v, v', u, u'} C D
inst_4 : F.IsWellOrderContinuous
inst_5 : PreservesWellOrderContinuousOfShape J G
j : J
hj : Order.IsSuccLimit j
⊢ IsColimit (J := (↑(Set.Iio j) : Type w)) (F :=
    Monotone.functor (f :=
        (⇑(PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Set.Iio j) : Type w)) ↦ x1 < x2) (s := fun (x1 x2 : J) ↦
              x1 < x2) (Set.principalSegIio j)) :
          (a : (↑(Set.Iio j) : Type w)) → J))
        ⋯ ⋙
      F ⋙ G)
    (PrincipalSeg.cocone (Set.principalSegIio j) (F ⋙ G))
have this : PreservesColimitsOfShape.{w, w, v, v', u, u'} (↑(Set.Iio j) : Type w) G
Tactic: have := preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape G 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
G₁ : Functor.{v, v', u, u'} C D
G₂ : Functor.{v', v'', u', u''} D E
inst_4 : PreservesWellOrderContinuousOfShape J G₁
inst_5 : PreservesWellOrderContinuousOfShape J G₂
j : J
hj : Order.IsSuccLimit j
⊢ PreservesColimitsOfShape.{w, w, v, v'', u, u''} (↑(Set.Iio j) : Type w) (G₁ ⋙ G₂)
have this : PreservesColimitsOfShape.{w, w, v, v', u, u'} (↑(Set.Iio j) : Type w) G₁
Tactic: have := preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape G₁ 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
G₁ : Functor.{v, v', u, u'} C D
G₂ : Functor.{v', v'', u', u''} D E
inst_4 : PreservesWellOrderContinuousOfShape J G₁
inst_5 : PreservesWellOrderContinuousOfShape J G₂
j : J
hj : Order.IsSuccLimit j
this : PreservesColimitsOfShape.{w, w, v, v', u, u'} (↑(Set.Iio j) : Type w) G₁
⊢ PreservesColimitsOfShape.{w, w, v, v'', u, u''} (↑(Set.Iio j) : Type w) (G₁ ⋙ G₂)
have this₁ : PreservesColimitsOfShape.{w, w, v', v'', u', u''} (↑(Set.Iio j) : Type w) G₂
Tactic: have := preservesColimitsOfShape_of_preservesWellOrderContinuousOfShape G₂ j hj