Theorem: CategoryTheory.ExtrDisc.HasPullbackOpenEmbedding (ExtrDisc/Pullback.lean)

State before:
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
⊢ HasPullback f i
Tactic:
constructor
State after:
case exists_limit
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
⊢ Nonempty (LimitCone (cospan f i))

State before:
case exists_limit
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
⊢ Nonempty (LimitCone (cospan f i))
Tactic:
use OpenEmbeddingCone f hi
State after:
case exists_limit
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
⊢ IsLimit (OpenEmbeddingCone f hi)

State before:
case exists_limit
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
⊢ IsLimit (OpenEmbeddingCone f hi)
Tactic:
exact ExtrDisc.OpenEmbeddingLimitCone f hi
State after:
no goals