Theorem: Condensed.ExtrDiscCompHaus.coverPreserving (Condensed/Equivalence.lean)

State before:
⊢ CoverPreserving (coherentTopology ExtrDisc) (coherentTopology CompHaus) ExtrDisc.toCompHaus
Tactic:
rw [coherentTopology_is_induced]
State after:
⊢ CoverPreserving (CoverDense.inducedTopology coverDense) (coherentTopology CompHaus) ExtrDisc.toCompHaus

State before:
⊢ CoverPreserving (CoverDense.inducedTopology coverDense) (coherentTopology CompHaus) ExtrDisc.toCompHaus
Tactic:
exact LocallyCoverDense.inducedTopology_coverPreserving (CoverDense.locallyCoverDense coverDense)
State after:
no goals