-- 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 : β
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.π
⊢ 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 neg : ∀ (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