awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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
⊢ Eq (α := G.obj Y ⟶ cokernel (G.map f))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (G.map (cokernel.π f)) (Iso.hom (iso G f))) (cokernel.π (G.map f))

Tactic:
IsColimit.comp_coconePointUniqueUpToIso_hom (isColimitOfHasCokernelOfPreservesColimit G f)
    (colimit.isColimit _) (WalkingParallelPair.one)

Premises used: CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.isColimitOfHasCokernelOfPreservesColimit, CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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
rw :
  Eq (α := G.obj Y ⟶ G.obj (cokernel f))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (cokernel.π (G.map f)) (Iso.inv (iso G f)))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (cokernel.π (G.map f)) (cokernelComparison f G))
⊢ Eq (α := cokernel (G.map f) ⟶ G.obj (cokernel f)) (Iso.inv (iso G f)) (cokernelComparison f G)

Tactic:
rw [← cancel_epi (cokernel.π _)]

Premises used: CategoryTheory.Limits.cokernel.π, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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
⊢ Eq (α := G.obj Y ⟶ G.obj (cokernel f))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (cokernel.π (G.map f)) (Iso.inv (iso G f)))
    (CategoryStruct.comp (Y := cokernel (G.map f)) (cokernel.π (G.map f)) (cokernelComparison f G))

Tactic:
simp [PreservesCokernel.iso]

Premises used: CategoryTheory.Limits.PreservesCokernel.iso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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 Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
rw : IsIso (X := cokernel (G.map f)) (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))
⊢ IsIso (X := cokernel (G.map f)) (Y := G.obj (cokernel f)) (cokernelComparison f G)

Tactic:
rw [← PreservesCokernel.iso_inv]

Premises used: CategoryTheory.Limits.PreservesCokernel.iso_inv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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 Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
inst_7 : PreservesColimit (parallelPair f 0) G
⊢ IsIso (X := cokernel (G.map f)) (Y := G.obj (cokernel f)) (Iso.inv (PreservesCokernel.iso G f))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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 Z : C
f : X ⟶ Y
h : Y ⟶ Z
w : f ≫ h = 0
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 : G.map (f ≫ q) = G.map p ≫ G.map g
rw₁ : G.map (p ≫ g) = G.map p ≫ G.map g
rw₂ rw₃ : G.map p ≫ G.map g = G.map p ≫ G.map g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
rw [← G.map_comp, hpq, G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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
⊢ IsIso (Fork.ι c)

Tactic:
have := KernelFork.IsLimit.isIso_ι c hc rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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)
refine : IsLimit (F := parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0) (KernelFork.map c G)
⊢ IsLimit (G.mapCone c)

Tactic:
refine (KernelFork.isLimitMapConeEquiv c G).symm ?_

Premises used: CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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)
refine :
  Iso (C := Cone (parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0)) (KernelFork.ofι (𝟙 (G.obj X)) ⋯)
    (KernelFork.map c G)
⊢ IsLimit (F := parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0) (KernelFork.map c G)

Tactic:
refine IsLimit.ofIsoLimit (KernelFork.IsLimit.ofId _ (G.map_zero _ _)) ?_

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.KernelFork.IsLimit.ofId, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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)
⊢ Eq (α :=
    Cone.pt.{0, v₂, 0, u₂} (F := parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0)
        (KernelFork.ofι (𝟙 (G.obj X)) ⋯) ⟶
      G.obj X)
    ((G.mapIso (asIso (Fork.ι c))).symm.hom ≫ Fork.ι (KernelFork.map c G)) (Fork.ι (KernelFork.ofι (𝟙 (G.obj X)) ⋯))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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)
⊢ Iso (C := Cone (parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0)) (KernelFork.ofι (𝟙 (G.obj X)) ⋯)
    (KernelFork.map c G)

Tactic:
exact (Fork.ext (G.mapIso (asIso (Fork.ι c))).symm (by simp))

Premises used: CategoryTheory.Limits.Fork.ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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
⊢ IsIso (Cofork.π c)

Tactic:
have := CokernelCofork.IsColimit.isIso_π c hc rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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)
refine : IsColimit (F := parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0) (CokernelCofork.map c G)
⊢ IsColimit (G.mapCocone c)

Tactic:
refine (CokernelCofork.isColimitMapCoconeEquiv c G).symm ?_

Premises used: CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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)
refine :
  Iso (C := Cocone (parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0)) (CokernelCofork.ofπ (𝟙 (G.obj Y)) ⋯)
    (CokernelCofork.map c G)
⊢ IsColimit (F := parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0) (CokernelCofork.map c G)

Tactic:
refine IsColimit.ofIsoColimit (CokernelCofork.IsColimit.ofId _ (G.map_zero _ _)) ?_

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Limits.CokernelCofork.IsColimit.ofId
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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)
⊢ Cofork.π (CokernelCofork.ofπ (𝟙 (G.obj Y)) ⋯) ≫ (G.mapIso (asIso (Cofork.π c))).hom =
    Cofork.π (CokernelCofork.map c G)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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)
⊢ Iso (C := Cocone (parallelPair (X := G.obj X) (Y := G.obj Y) (G.map 0) 0)) (CokernelCofork.ofπ (𝟙 (G.obj Y)) ⋯)
    (CokernelCofork.map c G)

Tactic:
exact (Cofork.ext (G.mapIso (asIso (Cofork.π c))) (by simp))

Premises used: CategoryTheory.Limits.Cofork.ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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
rw : PreservesLimit (parallelPair (X := X) (Y := Y) 0 0) G
⊢ PreservesLimit (parallelPair f 0) G

Tactic:
rw [hf]
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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 (X := X) (Y := Y) 0 0) G

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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
rw : PreservesColimit (parallelPair (X := X) (Y := Y) 0 0) G
⊢ PreservesColimit (parallelPair f 0) G

Tactic:
rw [hf]
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
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 (X := X) (Y := Y) 0 0) G

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
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
X : WalkingMultispan J
⊢ (d.map F).multispan.map (WalkingMultispan.Hom.id X) ≫
      Iso.hom
        ((fun (i : WalkingMultispan J) ↦
            (match (motive := (i : WalkingMultispan J) → (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i) i with
              | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a)) :
              (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i))
          X) =
    Iso.hom
        ((fun (i : WalkingMultispan J) ↦
            (match (motive := (i : WalkingMultispan J) → (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i) i with
              | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a)) :
              (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i))
          X) ≫
      (d.multispan ⋙ F).map (WalkingMultispan.Hom.id X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
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
a : J.L
⊢ (d.map F).multispan.map (WalkingMultispan.Hom.fst a) ≫
      Iso.hom
        ((fun (i : WalkingMultispan J) ↦
            (match (motive := (i : WalkingMultispan J) → (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i) i with
              | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a)) :
              (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i))
          (WalkingMultispan.right (J.fst a))) =
    Iso.hom
        ((fun (i : WalkingMultispan J) ↦
            (match (motive := (i : WalkingMultispan J) → (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i) i with
              | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a)) :
              (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i))
          (WalkingMultispan.left a)) ≫
      (d.multispan ⋙ F).map (WalkingMultispan.Hom.fst a)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
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
a : J.L
⊢ (d.map F).multispan.map (WalkingMultispan.Hom.snd a) ≫
      Iso.hom
        ((fun (i : WalkingMultispan J) ↦
            (match (motive := (i : WalkingMultispan J) → (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i) i with
              | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a)) :
              (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i))
          (WalkingMultispan.right (J.snd a))) =
    Iso.hom
        ((fun (i : WalkingMultispan J) ↦
            (match (motive := (i : WalkingMultispan J) → (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i) i with
              | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a)) :
              (d.map F).multispan.obj i ≅ (d.multispan ⋙ F).obj i))
          (WalkingMultispan.left a)) ≫
      (d.multispan ⋙ F).map (WalkingMultispan.Hom.snd a)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
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
dsimp : F.map (d.fst j) ≫ F.map (c.π (J.fst j)) = F.map (d.snd j) ≫ F.map (c.π (J.snd j))
⊢ 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))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
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))
rw₂ rw₃ : F.map (d.snd j ≫ c.π (J.snd 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))

Tactic:
rw [← F.map_comp, ← F.map_comp, condition]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Limits.Multicofork.condition
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
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
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))
⊢ π ((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

Tactic:
dsimp only [Multicofork.π]

Premises used: CategoryTheory.Limits.Multicofork.π
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
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
⊢ 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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
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
X : C
F : Functor.{v₁, v₂, u₁, u₂} C D
J : Type u_1
inst_3 : PreservesLimitsOfShape.{u_1, u_1, v₁, v₂, u₁, u₂} (WidePullbackShape J) F
⊢ PreservesLimitsOfShape.{u_1, u_1, v₁, v₂, u₁, u₂} (WithTerminal (Discrete J)) F

Tactic:
preservesLimitsOfShape_of_equiv WithTerminal.widePullbackShapeEquiv F

Premises used: CategoryTheory.Limits.preservesLimitsOfShape_of_equiv, CategoryTheory.WithTerminal.widePullbackShapeEquiv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
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
X : C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} (WithTerminal J) F
K : J ⥤ Over.{v₁, u₁} X
coneK : Cone K
isLimitConeK : IsLimit coneK
isLimitConeD :
  IsLimit
    (Functor.obj (Cone.postcompose (Iso.hom (Iso.symm liftFromOverComp)))
      (F.mapCone (Functor.obj (Equivalence.functor coneEquiv) coneK)))
⊢ Eq (α :=
    Functor.obj.{w', v₂, w, u₂} (C := WithTerminal J)
        (Functor.obj (Functor.const (WithTerminal J))
          (Functor.obj (Cone.postcompose (Iso.hom (Iso.symm liftFromOverComp)))
              (F.mapCone (Functor.obj (Equivalence.functor coneEquiv) coneK))).pt)
        WithTerminal.star ⟶
      (Functor.obj liftFromOver (K ⋙ Over.post F)).obj WithTerminal.star)
    ((Functor.obj (Cone.postcompose (Iso.hom (Iso.symm liftFromOverComp)))
            (F.mapCone (Functor.obj (Equivalence.functor coneEquiv) coneK))).π.app
      WithTerminal.star)
    (Iso.hom
        (Iso.refl
          (Functor.obj (Cone.postcompose (Iso.hom (Iso.symm liftFromOverComp)))
              (F.mapCone (Functor.obj (Equivalence.functor coneEquiv) coneK))).pt) ≫
      NatTrans.app (Cone.π (Functor.obj (Equivalence.functor coneEquiv) (Functor.mapCone (Over.post F) coneK)))
        WithTerminal.star)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
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
X : C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : PreservesLimitsOfShape.{w', w, v₁, v₂, u₁, u₂} (WithTerminal J) F
K : J ⥤ Over.{v₁, u₁} X
coneK : Cone K
isLimitConeK : IsLimit coneK
isLimitConeD :
  IsLimit
    (Functor.obj (Cone.postcompose (Iso.hom (Iso.symm liftFromOverComp)))
      (F.mapCone (Functor.obj (Equivalence.functor coneEquiv) coneK)))
a : J
⊢ Eq (α :=
    Functor.obj.{w', v₂, w, u₂}
        (Functor.obj (Functor.const (WithTerminal J))
          (Functor.obj (Cone.postcompose (Iso.hom (Iso.symm liftFromOverComp)))
              (F.mapCone (Functor.obj (Equivalence.functor coneEquiv) coneK))).pt)
        (of a) ⟶
      (Functor.obj liftFromOver (K ⋙ Over.post F)).obj (of a))
    ((Functor.obj (Cone.postcompose (Iso.hom (Iso.symm liftFromOverComp)))
            (F.mapCone (Functor.obj (Equivalence.functor coneEquiv) coneK))).π.app
      (of a))
    (Iso.hom
        (Iso.refl
          (Functor.obj (Cone.postcompose (Iso.hom (Iso.symm liftFromOverComp)))
              (F.mapCone (Functor.obj (Equivalence.functor coneEquiv) coneK))).pt) ≫
      NatTrans.app (Cone.π (Functor.obj (Equivalence.functor coneEquiv) (Functor.mapCone (Over.post F) coneK))) (of a))

Tactic:
aesop