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

State before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g 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✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g 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