awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map (f ≫ coequalizer.π f 0)) 0
rw₁ : Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map 0) 0
rw₂ rw₃ : Eq.{v₂ + 1} (α := G.obj X ⟶ G.obj (cokernel f)) 0 0
⊢ Eq (α := G.obj X ⟶ G.obj (cokernel f)) (G.map f ≫ G.map (coequalizer.π f 0)) 0

Tactic:
rw [← G.map_comp, cokernel.condition, G.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.cokernel.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
rw : Eq (α := G.obj X' ⟶ G.obj (cokernel g)) (G.map (g ≫ coequalizer.π g 0)) 0
rw₁ : Eq (α := G.obj X' ⟶ G.obj (cokernel g)) (G.map 0) 0
rw₂ rw₃ : Eq.{v₂ + 1} (α := G.obj X' ⟶ G.obj (cokernel g)) 0 0
⊢ Eq (α := G.obj X' ⟶ G.obj (cokernel g)) (G.map g ≫ G.map (coequalizer.π g 0)) 0

Tactic:
rw [← G.map_comp, cokernel.condition, G.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.cokernel.condition, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
simp :
  Eq (α := G.obj Y ⟶ G.obj (cokernel g))
    (G.map (CategoryStruct.comp (Y := cokernel f) (coequalizer.π f 0) (cokernel.map f g p q hpq)))
    (G.map (q ≫ coequalizer.π g 0))
⊢ Eq (α := G.obj Y ⟶ G.obj (cokernel g))
    (CategoryStruct.comp (Y := G.obj (cokernel f)) (G.map (coequalizer.π f 0)) (G.map (cokernel.map f g p q hpq)))
    (G.map q ≫ G.map (coequalizer.π g 0))

Tactic:
simp only [← G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ Eq (α := G.obj Y ⟶ G.obj (cokernel g))
    (G.map (CategoryStruct.comp (Y := cokernel f) (coequalizer.π f 0) (cokernel.map f g p q hpq)))
    (G.map (q ≫ coequalizer.π g 0))

Tactic:
G.congr_map (cokernel.π_desc _ _ _)

Premises used: CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
X Y : C
f : X ⟶ Y
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
inst_5 : HasCokernel f
inst_6 : HasCokernel (G.map f)
g : X' ⟶ Y'
inst_7 : HasCokernel g
inst_8 : HasCokernel (G.map g)
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ Eq (α := G.obj Y ⟶ G.obj (cokernel g))
    (G.map (CategoryStruct.comp (Y := cokernel f) (coequalizer.π f 0) (cokernel.map f g p q hpq)))
    (G.map (q ≫ coequalizer.π g 0))

Tactic:
exact G.congr_map (cokernel.π_desc _ _ _)

Premises used: CategoryTheory.Limits.cokernel.π_desc, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasKernels.{v, u} C
f g : Arrow.{v, u} C
u : f ⟶ g
⊢ Eq (α := kernel f.hom ⟶ g.right) ((kernel.ι f.hom ≫ Arrow.Hom.left u) ≫ g.hom) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasCokernels.{v, u} C
f g : Arrow.{v, u} C
u : f ⟶ g
⊢ Eq (α := f.left ⟶ cokernel g.hom) (f.hom ≫ Arrow.Hom.right u ≫ cokernel.π g.hom) 0

Tactic:
simp [← Arrow.w_assoc u]

Premises used: CategoryTheory.Arrow.w_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
k : J.R
hk : k = J.fst default
⊢ I.right k = I.right (J.fst default)

Tactic:
simp [hk]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
⊢ Membership.mem (γ := Set J.R) {J.fst default, J.snd default} k

Tactic:
have := h.symm.le (Set.mem_univ k)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
this : Membership.mem (γ := Set J.R) {J.fst default, J.snd default} k
⊢ k = J.fst default ∨ k = J.snd default

Tactic:
push _ ∈ _ at this
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
this : k = J.fst default ∨ k = J.snd default
inl : ∀ (this : k = J.fst default), k = J.snd default
inr inr₁ inr₂ : ∀ (this : k = J.snd default), k = J.snd default
⊢ k = J.snd default

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
k : J.R
hk : ¬k = J.fst default
obtain : ∀ (hk : ¬J.snd default = J.fst default), I.right (J.snd default) = I.right (J.snd default)
⊢ I.right k = I.right (J.snd default)

Tactic:
obtain rfl : k = J.snd default := by
            have := h.symm.le (Set.mem_univ k)
            push _ ∈ _ at this
            tauto

Premises used: Inhabited.default, CategoryTheory.Limits.MultispanShape.snd, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
hk : ¬J.snd default = J.fst default
⊢ I.right (J.snd default) = I.right (J.snd default)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
rw :
  Eq (α := I.left default ⟶ s.pt)
    (I.fst default ≫
      (fun (k : J.R) ↦ (if hk : k = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr : I.right k ⟶ s.pt))
        (J.fst default))
    (I.snd default ≫
      (fun (k : J.R) ↦ (if hk : k = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr : I.right k ⟶ s.pt))
        (J.snd default))
⊢ ∀ (a : J.L),
    Eq (α := I.left a ⟶ s.pt)
      (I.fst a ≫
        (fun (k : J.R) ↦ (if hk : k = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr : I.right k ⟶ s.pt))
          (J.fst a))
      (I.snd a ≫
        (fun (k : J.R) ↦ (if hk : k = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr : I.right k ⟶ s.pt))
          (J.snd a))

Tactic:
rw [Unique.forall_iff]

Premises used: Unique.forall_iff
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
⊢ Eq (α := I.left default ⟶ s.pt)
    (I.fst default ≫
      (fun (k : J.R) ↦ (if hk : k = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr : I.right k ⟶ s.pt))
        (J.fst default))
    (I.snd default ≫
      (fun (k : J.R) ↦ (if hk : k = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr : I.right k ⟶ s.pt))
        (J.snd default))

Tactic:
simpa [h'.symm] using s.condition

Premises used: CategoryTheory.Limits.PushoutCocone.condition, Ne.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
dsimp : (if hk : J.fst default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inl
⊢ (multicofork h h' s).π (J.fst default) = s.inl

Tactic:
dsimp only [multicofork, ofπ, π]

Premises used: CategoryTheory.Limits.Multicofork.ofπ, CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork, CategoryTheory.Limits.Multicofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
rw : eqToHom ⋯ ≫ s.inl = s.inl
rw₁ : 𝟙 (I.right (J.fst default)) ≫ s.inl = s.inl
rw₂ rw₃ : s.inl = s.inl
⊢ (if hk : J.fst default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inl

Tactic:
rw [dif_pos rfl, eqToHom_refl, Category.id_comp]

Premises used: dif_pos, CategoryTheory.eqToHom_refl, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
dsimp : (if hk : J.snd default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inr
⊢ (multicofork h h' s).π (J.snd default) = s.inr

Tactic:
dsimp only [multicofork, ofπ, π]

Premises used: CategoryTheory.Limits.Multicofork.ofπ, CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork, CategoryTheory.Limits.Multicofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_2, u_3, v_1, u_1} J C
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
rw : eqToHom ⋯ ≫ s.inr = s.inr
rw₁ : 𝟙 (I.right (J.snd default)) ≫ s.inr = s.inr
rw₂ rw₃ : s.inr = s.inr
⊢ (if hk : J.snd default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inr

Tactic:
rw [dif_neg h'.symm, eqToHom_refl, Category.id_comp]

Premises used: Ne.symm, CategoryTheory.eqToHom_refl, dif_neg, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
⊢ c.π (J.fst default) ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s =
    s.inl

Tactic:
simpa using hc.fac (isPushout.multicofork h h' s) (.right (J.fst default))

Premises used: CategoryTheory.Limits.IsColimit.fac, Inhabited.default, CategoryTheory.Limits.MultispanShape.fst, CategoryTheory.Limits.WalkingMultispan.right, CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
⊢ c.π (J.snd default) ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s =
    s.inr

Tactic:
simpa using hc.fac (isPushout.multicofork h h' s) (.right (J.snd default))

Premises used: CategoryTheory.Limits.IsColimit.fac, Inhabited.default, CategoryTheory.Limits.WalkingMultispan.right, CategoryTheory.Limits.MultispanShape.snd, CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
apply :
  ∀ (a : J.R),
    c.π a ≫ m =
      c.π a ≫
        (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
            (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
          s
⊢ m =
    (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
        (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
      s

Tactic:
apply Multicofork.IsColimit.hom_ext hc

Premises used: CategoryTheory.Limits.Multicofork.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
k : J.R
⊢ Membership.mem (γ := Set J.R) {J.fst default, J.snd default} k

Tactic:
have := h.symm.le (Set.mem_univ k)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
k : J.R
this : Membership.mem (γ := Set J.R) {J.fst default, J.snd default} k
⊢ k = J.fst default ∨ k = J.snd default

Tactic:
push _ ∈ _ at this
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
k : J.R
this : k = J.fst default ∨ k = J.snd default
inl :
  Eq (α := I.right (J.fst default) ⟶ s.pt) (c.π (J.fst default) ≫ m)
    (c.π (J.fst default) ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s)
inr :
  Eq (α := I.right (J.snd default) ⟶ s.pt) (c.π (J.snd default) ≫ m)
    (c.π (J.snd default) ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s)
⊢ c.π k ≫ m =
    c.π k ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s

Tactic:
obtain rfl | rfl := this

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ Eq (α := I.right (J.fst default) ⟶ s.pt) (c.π (J.fst default) ≫ m)
    (c.π (J.fst default) ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s)

Tactic:
simpa [h₁] using (hc.fac (isPushout.multicofork h h' s) (.right (J.fst default))).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, Inhabited.default, CategoryTheory.Limits.MultispanShape.fst, CategoryTheory.Limits.WalkingMultispan.right, CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
J : MultispanShape
inst_1 : Unique J.L
I : MultispanIndex.{u_3, u_2, v_1, u_1} J C
c : Multicofork I
h : Eq (α := Set J.R) {J.fst default, J.snd default} Set.univ
h' : J.fst default ≠ J.snd default
hc : IsColimit c
s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)
m : c.pt ⟶ s.pt
h₁ : c.π (J.fst default) ≫ m = s.inl
h₂ : c.π (J.snd default) ≫ m = s.inr
⊢ Eq (α := I.right (J.snd default) ⟶ s.pt) (c.π (J.snd default) ≫ m)
    (c.π (J.snd default) ≫
      (fun (s : PushoutCocone (X := I.left default) (I.fst default) (I.snd default)) ↦
          (hc.desc (isPushout.multicofork h h' s) : c.pt ⟶ (isPushout.multicofork h h' s).pt))
        s)

Tactic:
simpa [h₂] using (hc.fac (isPushout.multicofork h h' s) (.right (J.snd default))).symm

Premises used: CategoryTheory.Limits.IsColimit.fac, Inhabited.default, CategoryTheory.Limits.WalkingMultispan.right, CategoryTheory.Limits.MultispanShape.snd, CategoryTheory.Limits.Multicofork.IsColimit.isPushout.multicofork, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₁, u₂} D
inst_3 : HasZeroMorphisms.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
inst_4 : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
W : D
h : @NormalMono.Z _ _ _ _ inst_3 (F.map f) _ ⟶ W
rw : (F.map f ≫ NormalMono.g) ≫ h = 0 ≫ h
rw₁ rw₂ : Eq (α := F.obj X ⟶ W) (0 ≫ h) (0 ≫ h)
⊢ F.map f ≫ NormalMono.g ≫ h = 0 ≫ h

Tactic:
rw [← Category.assoc, eq_whisker hf.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eq_whisker, CategoryTheory.NormalMono.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₁, u₂} D
inst_3 : HasZeroMorphisms.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
inst_4 : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ ∀ {W : D} (h : @NormalMono.Z _ _ _ _ inst_3 (F.map f) _ ⟶ W), F.map f ≫ NormalMono.g ≫ h = 0 ≫ h

Tactic:
have reassoc' {W : D} (h : hf.Z ⟶ W) : F.map f ≫ hf.g ≫ h = 0 ≫ h := by
      rw [← Category.assoc, eq_whisker hf.w]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₁, u₂} D
inst_3 : HasZeroMorphisms.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
inst_4 : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
reassoc' : ∀ {W : D} (h : @NormalMono.Z _ _ _ _ inst_3 (F.map f) _ ⟶ W), F.map f ≫ NormalMono.g ≫ h = 0 ≫ h
⊢ Eq (α := F.obj X ⟶ F.obj (F.objPreimage (@NormalMono.Z _ _ _ _ inst_3 (F.map f) _)))
    (F.map (f ≫ F.preimage (NormalMono.g ≫ Iso.inv (F.objObjPreimageIso (@NormalMono.Z _ _ _ _ inst_3 (F.map f) _)))))
    (F.map 0)

Tactic:
simp [reassoc']
-- Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 Y_1 : C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₁, u₂} D
inst_3 : HasZeroMorphisms.{v₁, u₂} D
F : Functor.{v₁, v₁, u₁, u₂} C D
inst_4 : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ Eq (α := F.obj Y ⟶ @NormalMono.Z _ _ _ _ inst_3 (F.map f) _)
    (CategoryStruct.comp (Y := F.obj (F.objPreimage (@NormalMono.Z _ _ _ _ inst_3 (F.map f) _)))
      (F.map (F.preimage (NormalMono.g ≫ Iso.inv (F.objObjPreimageIso (@NormalMono.Z _ _ _ _ inst_3 (F.map f) _)))))
      (Iso.hom (F.objObjPreimageIso (@NormalMono.Z _ _ _ _ inst_3 (F.map f) _))))
    NormalMono.g

Tactic:
simp only [Functor.map_preimage, Category.assoc, Iso.inv_hom_id, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_preimage