-- 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
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f

Tactic:
have h := initialIsInitial (C := Discrete (PUnit.{w + 1}))

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})
⊢ 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₂
this : hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x => f) ≫ c₂.ι } = f
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f

Tactic:
rw [← this]

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₂
this : hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x => f) ≫ c₂.ι } = f
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) (hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x => f) ≫ c₂.ι })

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ W ≤ W.colimitsOfShape (Discrete PUnit.{w + 1})

Tactic:
intro X₁ X₂ f hf

Result:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
X₁ X₂ : C
f : X₁ ⟶ X₂
hf : W f
⊢ 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₂
x : Discrete PUnit.{w + 1}
⊢ x = ⊥_ Discrete PUnit.{w + 1}

Tactic:
ext

Result:
no goals

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}
⊢ (Discrete.functor fun x => X₁).obj x✝ ⟶ (Discrete.functor fun x => X₂).obj x✝

Tactic:
exact f

Result:
no goals

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₂
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f

Tactic:
have : hc₁.desc (Cocone.mk _ (Discrete.natTrans (fun _ ↦ by exact f) ≫ c₂.ι)) = f :=
  hc₁.hom_ext (fun x ↦ by
    obtain rfl : x = ⊥_ _ := by ext
    rw [IsColimit.fac]
    simp [c₁, c₂])

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₂
this : hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x => f) ≫ c₂.ι } = f
⊢ 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})
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f

Tactic:
let c₁ := coconeOfDiagramInitial (F := Discrete.functor (fun _ ↦ X₁)) 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₁)
⊢ 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₂
this : hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x => f) ≫ c₂.ι } = f
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) (hc₁.desc { pt := c₂.pt, ι := (Discrete.natTrans fun x => f) ≫ c₂.ι })

Tactic:
exact ⟨_, _, _, _, _, hc₂, _, fun _ ↦ hf⟩

Result:
no goals

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₂
⊢ { pt := c₂.pt, ι := (Discrete.natTrans fun x => f) ≫ c₂.ι }.ι.app (⊥_ Discrete PUnit.{w + 1}) =
    c₁.ι.app (⊥_ Discrete PUnit.{w + 1}) ≫ f

Tactic:
simp [c₁, c₂]

Result:
no goals

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₁
⊢ 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₁
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₁)
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f

Tactic:
let c₂ := coconeOfDiagramInitial (F := Discrete.functor (fun _ ↦ X₂)) 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₂)
⊢ W.colimitsOfShape (Discrete PUnit.{w + 1}) f