Theorem: ExtrDisc.isIso_of_bijective (ExtrDisc/ExplicitSheaves.lean)

State before:
X Y : ExtrDisc
f : X ⟶ Y
hf : Function.Bijective ↑f
⊢ IsIso (toCompHaus.map f)
Tactic:
exact CompHaus.isIso_of_bijective _ hf
State after:
no goals

State before:
X Y : ExtrDisc
f : X ⟶ Y
hf : Function.Bijective ↑f
this : IsIso (toCompHaus.map f)
⊢ IsIso f
Tactic:
apply isIso_of_fully_faithful toCompHaus
State after:
no goals