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

State before:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
i : Y ⟶ Z
⊢ pullback.fst f i = fromExplicit f i ≫ Limits.pullback.fst
Tactic:
dsimp [fromExplicit]
State after:
α : Type
inst✝ : Fintype α
Z✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
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✝ : α → CompHaus
X Y Z : CompHaus
f : X ⟶ Z
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