awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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
⊢ m = Sigma.desc (hc.desc (coconeTypes s))
have 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)))
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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
⊢ 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)))
have 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)
Tactic: obtain ⟨j, k, rfl⟩ := Functor.CoconeTypes.IsColimit.ι_jointly_surjective hc x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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
⊢ 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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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)
    (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)
have 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)
Tactic: dsimp [sigmaConstCokernelCofork]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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)
    (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)
have 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)
Tactic: rw [Sigma.ι_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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)
    (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))
have 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))
Tactic: dsimp [sigmaConstCokernelCofork]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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)
    (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))
have 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
Tactic: rw [Sigma.ι_desc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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
⊢ 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.π
have 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.π
Tactic: ext b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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
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.π
have pos : ∀ (hb : b ∈ Set.range f),
  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.π
Tactic: by_cases hb : b ∈ Set.range f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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
b : β
hb : b ∈ Set.range f
⊢ 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.π
have pos : ∀ (a : α),
  CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R) (Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (f a))
      (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) (f a) ≫ s.π
Tactic: obtain ⟨a, rfl⟩ := hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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
m :
  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) ⟶
    s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
⊢ m =
    (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
have dsimp : m = Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑x : β) ≫ s.π
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
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
m :
  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) ⟶
    s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
⊢ m = Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑x : β) ≫ s.π
have h : ∀ (b : β) (hb : b ∈ (Set.range f)ᶜ),
  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) ≫
      m =
    CategoryStruct.comp (Y := 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))
      (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
        Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑x : β) ≫ s.π)
Tactic: ext ⟨b, hb⟩