-- Mathlib/CategoryTheory/Limits/MorphismProperty.lean
lemma CostructuredArrow.closedUnderLimitsOfShape_discrete_empty [L.Faithful] [L.Full] {Y : A}
    [P.ContainsIdentities] [P.RespectsIso] :
    ClosedUnderLimitsOfShape (Discrete PEmpty.{1})
      (fun f : CostructuredArrow L (L.obj Y) ↦ P f.hom)

Proof state:
T : Type u_1
inst✝⁵ : Category.{u_4, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{u_3, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
c : Cone (Functor.empty (CostructuredArrow L (L.obj Y)))
hc : IsLimit c
e : c.pt ≅ mk (𝟙 (L.obj Y)) := hc.conePointUniqueUpToIso mkIdTerminal
⊢ P c.pt.hom

Tactic:
rw [P.costructuredArrow_iso_iff e]

Result:
T : Type u_1
inst✝⁵ : Category.{u_4, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{u_3, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
c : Cone (Functor.empty (CostructuredArrow L (L.obj Y)))
hc : IsLimit c
e : c.pt ≅ mk (𝟙 (L.obj Y)) := hc.conePointUniqueUpToIso mkIdTerminal
⊢ P (mk (𝟙 (L.obj Y))).hom

Proof state:
T : Type u_1
inst✝⁵ : Category.{u_4, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{u_3, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
D : Discrete PEmpty.{1} ⥤ CostructuredArrow L (L.obj Y)
c : Cone D
hc : IsLimit c
this : D = Functor.empty (CostructuredArrow L (L.obj Y))
⊢ P c.pt.hom

Tactic:
subst this

Result:
T : Type u_1
inst✝⁵ : Category.{u_4, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{u_3, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
c : Cone (Functor.empty (CostructuredArrow L (L.obj Y)))
hc : IsLimit c
⊢ P c.pt.hom

Proof state:
T : Type u_1
inst✝⁵ : Category.{u_4, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{u_3, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
c : Cone (Functor.empty (CostructuredArrow L (L.obj Y)))
hc : IsLimit c
e : c.pt ≅ mk (𝟙 (L.obj Y)) := hc.conePointUniqueUpToIso mkIdTerminal
⊢ P (mk (𝟙 (L.obj Y))).hom

Tactic:
simpa using P.id_mem (L.obj Y)

Result:
no goals

Proof state:
T : Type u_1
inst✝⁵ : Category.{u_4, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{u_3, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
D : Discrete PEmpty.{1} ⥤ CostructuredArrow L (L.obj Y)
c : Cone D
hc : IsLimit c
⊢ P c.pt.hom

Tactic:
have : D = Functor.empty _ := Functor.empty_ext' _ _

Result:
T : Type u_1
inst✝⁵ : Category.{u_4, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{u_3, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
D : Discrete PEmpty.{1} ⥤ CostructuredArrow L (L.obj Y)
c : Cone D
hc : IsLimit c
this : D = Functor.empty (CostructuredArrow L (L.obj Y))
⊢ P c.pt.hom

Proof state:
T : Type u_1
inst✝⁵ : Category.{u_4, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{u_3, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
⊢ ClosedUnderLimitsOfShape (Discrete PEmpty.{1}) fun f => P f.hom

Tactic:
rintro D c hc -

Result:
T : Type u_1
inst✝⁵ : Category.{u_4, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{u_3, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
D : Discrete PEmpty.{1} ⥤ CostructuredArrow L (L.obj Y)
c : Cone D
hc : IsLimit c
⊢ P c.pt.hom

Proof state:
T : Type u_1
inst✝⁵ : Category.{u_4, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{u_3, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
c : Cone (Functor.empty (CostructuredArrow L (L.obj Y)))
hc : IsLimit c
⊢ P c.pt.hom

Tactic:
let e : c.pt ≅ CostructuredArrow.mk (𝟙 (L.obj Y)) :=
  hc.conePointUniqueUpToIso CostructuredArrow.mkIdTerminal

Result:
T : Type u_1
inst✝⁵ : Category.{u_4, u_1} T
P : MorphismProperty T
A : Type u_2
inst✝⁴ : Category.{u_3, u_2} A
L : A ⥤ T
inst✝³ : L.Faithful
inst✝² : L.Full
Y : A
inst✝¹ : P.ContainsIdentities
inst✝ : P.RespectsIso
c : Cone (Functor.empty (CostructuredArrow L (L.obj Y)))
hc : IsLimit c
e : c.pt ≅ mk (𝟙 (L.obj Y)) := hc.conePointUniqueUpToIso mkIdTerminal
⊢ P c.pt.hom