-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma le_colimitsOfShape_punit : W ≤ W.colimitsOfShape (Discrete PUnit.{w + 1})

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x => X₁) := coconeOfDiagramInitial h (Discrete.functor fun x => X₁)
c₂ : Cocone (Discrete.functor fun x => X₂) := coconeOfDiagramInitial h (Discrete.functor fun x => X₂)
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f

Tactic:
have hc₁ : IsColimit c₁ := colimitOfDiagramInitial h _

Result:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x => X₁) := coconeOfDiagramInitial h (Discrete.functor fun x => X₁)
c₂ : Cocone (Discrete.functor fun x => X₂) := coconeOfDiagramInitial h (Discrete.functor fun x => X₂)
hc₁ : IsColimit c₁
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x => X₁) := coconeOfDiagramInitial h (Discrete.functor fun x => X₁)
c₂ : Cocone (Discrete.functor fun x => X₂) := coconeOfDiagramInitial h (Discrete.functor fun x => X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x => f) ≫ c₂.ι } =
    c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f

Tactic:
rw [IsColimit.fac]

Result:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x => X₁) := coconeOfDiagramInitial h (Discrete.functor fun x => X₁)
c₂ : Cocone (Discrete.functor fun x => X₂) := coconeOfDiagramInitial h (Discrete.functor fun x => X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ { pt := c₂.pt, ι := (Discrete.natTrans fun x => f) ≫ c₂.ι }.ι.app (⊥_ Discrete PUnit.{w + 1}) =
    c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x => X₁) := coconeOfDiagramInitial h (Discrete.functor fun x => X₁)
c₂ : Cocone (Discrete.functor fun x => X₂) := coconeOfDiagramInitial h (Discrete.functor fun x => X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x : Discrete PUnit.{w + 1}
⊢ c₁.ι.app x ≫ hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x => f) ≫ c₂.ι } = c₁.ι.app x ≫ f

Tactic:
obtain rfl : x = ⊥_ _ := by ext

Result:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
h : IsInitial (⊥_ Discrete PUnit.{w + 1})
c₁ : Cocone (Discrete.functor fun x => X₁) := coconeOfDiagramInitial h (Discrete.functor fun x => X₁)
c₂ : Cocone (Discrete.functor fun x => X₂) := coconeOfDiagramInitial h (Discrete.functor fun x => X₂)
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x => f) ≫ c₂.ι } =
    c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f