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

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

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