Theorem: CompHaus.fromExcplictComptoExplicit (CompHaus/ExplicitLimits.lean)

State before:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ (fromExplicit f i ≫ toExplicit f i) ≫ pullback.fst f i = 𝟙 (pullback f i) ≫ pullback.fst f i
Tactic:
simp [toExplicit, fromExplicit]
State after:
no goals

State before:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ (fromExplicit f i ≫ toExplicit f i) ≫ pullback.snd f i = 𝟙 (pullback f i) ≫ pullback.snd f i
Tactic:
simp [toExplicit, fromExplicit]
State after:
no goals