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

State before:
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
inst✝ : HasPullback f i
⊢ toExplicit f hi ≫ fromExplicit f hi = 𝟙 (pullback f i)
Tactic:
refine' Limits.pullback.hom_ext (k := (toExplicit f hi ≫ fromExplicit f hi)) _ _
State after:
case refine'_1
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
inst✝ : HasPullback f i
⊢ (toExplicit f hi ≫ fromExplicit f hi) ≫ Limits.pullback.fst = 𝟙 (pullback f i) ≫ Limits.pullback.fst

case refine'_2
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
inst✝ : HasPullback f i
⊢ (toExplicit f hi ≫ fromExplicit f hi) ≫ Limits.pullback.snd = 𝟙 (pullback f i) ≫ Limits.pullback.snd

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

State before:
case refine'_2
X Y Z : ExtrDisc
f : X ⟶ Z
i : Y ⟶ Z
hi : OpenEmbedding ↑i
inst✝ : HasPullback f i
⊢ (toExplicit f hi ≫ fromExplicit f hi) ≫ Limits.pullback.snd = 𝟙 (pullback f i) ≫ Limits.pullback.snd
Tactic:
rw [Category.id_comp, Category.assoc, fromExplicit, Limits.pullback.lift_snd,
  toExplicit, pullback.lift_snd]
State after:
no goals