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

State before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ pullback.fst f i = fromExplicit f i ≫ Limits.pullback.fst
Tactic:
dsimp [fromExplicit]
State after:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ pullback.fst f i =
    Limits.pullback.lift (pullback.fst f i) (pullback.snd f i) (_ : pullback.fst f i ≫ f = pullback.snd f i ≫ i) ≫
      Limits.pullback.fst

State before:
α : Type
inst✝ : Fintype α
Z✝ : α → Profinite
X Y Z : Profinite
f : X ⟶ Z
g i : Y ⟶ Z
⊢ pullback.fst f i =
    Limits.pullback.lift (pullback.fst f i) (pullback.snd f i) (_ : pullback.fst f i ≫ f = pullback.snd f i ≫ i) ≫
      Limits.pullback.fst
Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
State after:
no goals