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

State before:
⊢ coherentTopology ExtrDisc = CoverDense.inducedTopology coverDense
Tactic:
ext X S
State after:
case h.h.h
X : ExtrDisc
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X ↔
    S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X

State before:
case h.h.h
X : ExtrDisc
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X ↔
    S ∈ GrothendieckTopology.sieves (CoverDense.inducedTopology coverDense) X
Tactic:
rw [← coverDense.inducedTopology_Sieve_iff_EffectiveEpiFamily X]
State after:
case h.h.h
X : ExtrDisc
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X ↔
    ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

State before:
case h.h.h
X : ExtrDisc
S : Sieve X
⊢ S ∈ GrothendieckTopology.sieves (coherentTopology ExtrDisc) X ↔
    ∃ α x Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Tactic:
rw [← coherentTopology.Sieve_iff_hasEffectiveEpiFamily S]
State after:
no goals