awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
coconeTypes : (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) → Functor.CoconeTypes.{v, w, v', u'} K :=
  fun (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) ↦
    { pt := R ⟶ s.pt, ι := fun (j : J) (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j,
      ι_naturality := ⋯ }
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
m : Cocone.pt.{v', v, u', u} (F := K ⋙ Functor.obj sigmaConst R) (Functor.mapCocone (Functor.obj sigmaConst R) c) ⟶ s.pt
hm : ∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj sigmaConst R) c)) j ≫ m = s.ι.app j
h :
  ∀ (x_1 : c.pt),
    Sigma.ι.{w, v, u} (C := C) (fun (x : c.pt) ↦ R) x_1 ≫ m =
      CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : c.pt) ↦ R)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : c.pt) ↦ R) x_1) (Sigma.desc (hc.desc (coconeTypes s)))
⊢ m = Sigma.desc (hc.desc (coconeTypes s))

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x_1 : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
coconeTypes : (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) → Functor.CoconeTypes.{v, w, v', u'} K :=
  fun (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) ↦
    { pt := R ⟶ s.pt, ι := fun (j : J) (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j,
      ι_naturality := ⋯ }
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
m : Cocone.pt.{v', v, u', u} (F := K ⋙ Functor.obj sigmaConst R) (Functor.mapCocone (Functor.obj sigmaConst R) c) ⟶ s.pt
hm : ∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj sigmaConst R) c)) j ≫ m = s.ι.app j
x : c.pt
h :
  ∀ (j : J) (k : K.obj j),
    Eq.{v + 1} (α := R ⟶ s.pt)
      (Sigma.ι.{w, v, u} (β := c.pt) (C := C) (fun (x : c.pt) ↦ R)
            (Functor.CoconeTypes.ι ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c) j k :
              Functor.CoconeTypes.pt.{w, w, v', u'} (J := J) (F := K)
                ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)) ≫
          m :
        R ⟶ s.pt)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : c.pt) ↦ R)
          (Sigma.ι.{w, v, u} (β := c.pt) (C := C) (fun (x : c.pt) ↦ R)
            (Functor.CoconeTypes.ι ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c) j k :
              Functor.CoconeTypes.pt.{w, w, v', u'} (J := J) (F := K)
                ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)))
          (Sigma.desc (hc.desc (coconeTypes s))) :
        R ⟶ s.pt)
⊢ Sigma.ι.{w, v, u} (C := C) (fun (x : c.pt) ↦ R) x ≫ m =
    CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : c.pt) ↦ R) (Sigma.ι.{w, v, u} (C := C) (fun (x : c.pt) ↦ R) x)
      (Sigma.desc (hc.desc (coconeTypes s)))

Tactic:
obtain ⟨j, k, rfl⟩ := Functor.CoconeTypes.IsColimit.ι_jointly_surjective hc x

Premises used: CategoryTheory.Functor.CoconeTypes.IsColimit.ι_jointly_surjective, rfl
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
coconeTypes : (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) → Functor.CoconeTypes.{v, w, v', u'} K :=
  fun (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) ↦
    { pt := R ⟶ s.pt, ι := fun (j : J) (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j,
      ι_naturality := ⋯ }
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
m : Cocone.pt.{v', v, u', u} (F := K ⋙ Functor.obj sigmaConst R) (Functor.mapCocone (Functor.obj sigmaConst R) c) ⟶ s.pt
hm : ∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj sigmaConst R) c)) j ≫ m = s.ι.app j
j : J
k : K.obj j
⊢ Eq.{v + 1} (α := R ⟶ s.pt)
    (Sigma.ι.{w, v, u} (β := c.pt) (C := C) (fun (x : c.pt) ↦ R)
          (Functor.CoconeTypes.ι ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c) j k :
            Functor.CoconeTypes.pt.{w, w, v', u'} (J := J) (F := K)
              ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)) ≫
        m :
      R ⟶ s.pt)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : c.pt) ↦ R)
        (Sigma.ι.{w, v, u} (β := c.pt) (C := C) (fun (x : c.pt) ↦ R)
          (Functor.CoconeTypes.ι ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c) j k :
            Functor.CoconeTypes.pt.{w, w, v', u'} (J := J) (F := K)
              ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)))
        (Sigma.desc (hc.desc (coconeTypes s))) :
      R ⟶ s.pt)

Tactic:
simp [coconeTypes, ← hm, dsimp% hc.fac_apply,
          dsimp% Sigma.ι_desc (hc.desc (coconeTypes s))]

Premises used: CategoryTheory.Limits.Sigma.ι_desc, CategoryTheory.Functor.CoconeTypes.IsColimit.fac_apply, CategoryTheory.Functor.CoconeTypes.IsColimit.desc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
coconeTypes : (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) → Functor.CoconeTypes.{v, w, v', u'} K :=
  fun (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) ↦
    { pt := R ⟶ s.pt, ι := fun (j : J) (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j,
      ι_naturality := ⋯ }
⊢ IsColimit.{v', v, u', u} (F := K ⋙ Functor.obj sigmaConst R) (Functor.mapCocone (Functor.obj sigmaConst R) c)

Tactic:
exact {
      desc s := Sigma.desc (hc.desc (coconeTypes s))
      fac s j := by
        dsimp
        ext k
        simp [dsimp% hc.fac_apply, dsimp% Sigma.ι_desc (hc.desc (coconeTypes s)), coconeTypes]
      uniq s m hm := by
        dsimp
        ext x
        obtain ⟨j, k, rfl⟩ := Functor.CoconeTypes.IsColimit.ι_jointly_surjective hc x
        simp [coconeTypes, ← hm, dsimp% hc.fac_apply,
          dsimp% Sigma.ι_desc (hc.desc (coconeTypes s))] }
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
h :
  ∀ (b : α),
    Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
      (CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} fun (x : α) ↦ R)
          (Sigma.ι.{u_1, v, u} (C := C) (fun (x : α) ↦ R) b)
          (CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.map' f fun (x : α) ↦ 𝟙 R)
            (Sigma.desc fun (b : β) ↦
              if hb : b ∈ (Set.range f)ᶜ then
                Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
                  (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb)
              else 0)) :
        R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
      (CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} fun (x : α) ↦ R)
          (Sigma.ι.{u_1, v, u} (C := C) (fun (x : α) ↦ R) b) 0 :
        R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
⊢ Eq.{v + 1} (α :=
    Quiver.Hom.{v, u} (V := C) (sigmaObj.{u_1, v, u} fun (x : α) ↦ R)
      (sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R))
    (CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.map' f fun (x : α) ↦ 𝟙 R)
      (Sigma.desc fun (b : β) ↦
        if hb : b ∈ (Set.range f)ᶜ then
          Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
            (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb)
        else 0))
    0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
b : α
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Sigma.ι.{u_1, v, u} (C := C) (fun (x : α) ↦ R) b)
        (CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.map' f fun (x : α) ↦ 𝟙 R)
          (Sigma.desc fun (b : β) ↦
            if hb : b ∈ (Set.range f)ᶜ then
              Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
                (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb)
            else 0)) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Sigma.ι.{u_1, v, u} (C := C) (fun (x : α) ↦ R) b)
        0 :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)

Tactic:
simp [Sigma.ι_desc]

Premises used: CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
b : β
hb : b ∉ Set.range f
dsimp :
  Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b)
        (Sigma.desc fun (b : β) ↦
          if hb : b ∈ (Set.range f)ᶜ then
            Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
              (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb)
          else 0) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b)
        (Cofork.π (sigmaConstCokernelCofork R f)) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)

Tactic:
dsimp [sigmaConstCokernelCofork]

Premises used: CategoryTheory.Limits.sigmaConstCokernelCofork
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
b : β
hb : b ∉ Set.range f
rw :
  Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (if hb : b ∈ (Set.range f)ᶜ then
        Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
          (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb)
      else 0 :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b)
        (Sigma.desc fun (b : β) ↦
          if hb : b ∈ (Set.range f)ᶜ then
            Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
              (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb)
          else 0) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)

Tactic:
rw [Sigma.ι_desc]

Premises used: CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
b : β
hb : b ∉ Set.range f
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (if hb : b ∈ (Set.range f)ᶜ then
        Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
          (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb)
      else 0 :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)

Tactic:
apply dif_pos

Premises used: dif_pos
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
a : α
dsimp :
  Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
        (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (f a))
        (Sigma.desc fun (b : β) ↦
          if hb : b ∈ (Set.range f)ᶜ then
            Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
              (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb)
          else 0) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (0 :
      R ⟶
        Cocone.pt.{0, v, 0, u} (F :=
          parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
            (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
          (sigmaConstCokernelCofork R f))
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
        (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (f a)) (Cofork.π (sigmaConstCokernelCofork R f)) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (0 :
      R ⟶
        Cocone.pt.{0, v, 0, u} (F :=
          parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
            (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
          (sigmaConstCokernelCofork R f))

Tactic:
dsimp [sigmaConstCokernelCofork]

Premises used: CategoryTheory.Limits.sigmaConstCokernelCofork
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
a : α
rw :
  Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (if hb : f a ∈ (Set.range f)ᶜ then
      Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) (f a) hb)
    else 0)
    0
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
        (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (f a))
        (Sigma.desc fun (b : β) ↦
          if hb : b ∈ (Set.range f)ᶜ then
            Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
              (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb)
          else 0) :
      R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (0 :
      R ⟶
        Cocone.pt.{0, v, 0, u} (F :=
          parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
            (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
          (sigmaConstCokernelCofork R f))

Tactic:
rw [Sigma.ι_desc]

Premises used: CategoryTheory.Limits.Sigma.ι_desc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
a : α
⊢ f a ∉ (Set.range f)ᶜ

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
a : α
⊢ Eq.{v + 1} (α := R ⟶ sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
    (if hb : f a ∈ (Set.range f)ᶜ then
      Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) (f a) hb)
    else 0)
    0

Tactic:
exact dif_neg (by simp)

Premises used: dif_neg
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
s :
  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0
h :
  ∀ (b : β),
    CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b)
        (CategoryStruct.comp (Y :=
          Cocone.pt.{0, v, 0, u} (F :=
            parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
              (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
            (sigmaConstCokernelCofork R f))
          (Cofork.π (sigmaConstCokernelCofork R f))
          ((fun
                (s :
                  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y :=
                    sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0) ↦
              (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
                  match (motive := (↑(Set.range f)ᶜ : Type u_2) → (R ⟶ s.pt)) x with
                  | ⟨b, property⟩ => Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b ≫ s.π :
                (sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R) ⟶ s.pt))
            s)) =
      Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b ≫ s.π
⊢ CategoryStruct.comp (Y :=
      Cocone.pt.{0, v, 0, u} (F :=
        parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
          (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
        (sigmaConstCokernelCofork R f))
      (Cofork.π (sigmaConstCokernelCofork R f))
      ((fun
            (s :
              Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y :=
                sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0) ↦
          (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
              match (motive := (↑(Set.range f)ᶜ : Type u_2) → (R ⟶ s.pt)) x with
              | ⟨b, property⟩ => Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) b ≫ s.π :
            (sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R) ⟶ s.pt))
        s) =
    s.π

Tactic:
ext b