Theorem: CompHaus.lift_lifts (ExtrDisc/Basic.lean)

State before:
X Y : CompHaus
Z : ExtrDisc
e : Z.compHaus ⟶ Y
f : X ⟶ Y
inst✝ : Epi f
⊢ lift e f ≫ f = e
Tactic:
simp [lift]
State after:
no goals