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

State before:
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
inst✝ : HasPullback f i
⊢ (fromExplicit f hi ≫ toExplicit f hi) ≫ pullback.fst f hi = 𝟙 (OpenEmbeddingCone f hi).pt ≫ pullback.fst f hi
Tactic:
simp [toExplicit, fromExplicit]
State after:
no goals