Theorem: CategoryTheory.EffectiveEpiFamily.toCompHaus (ExtrDisc/Coherent.lean)

State before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
⊢ EffectiveEpiFamily (fun a => ExtrDisc.toCompHaus.obj (X a)) fun a => ExtrDisc.toCompHaus.map (π a)
Tactic:
refine' ((CompHaus.effectiveEpiFamily_tfae _ _).out 0 2).2 (fun b => _)
State after:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
b : ↑(ExtrDisc.toCompHaus.obj B).toTop
⊢ ∃ a x, ↑(ExtrDisc.toCompHaus.map (π a)) x = b

State before:
α : Type
inst✝ : Fintype α
B : ExtrDisc
X : α → ExtrDisc
π : (a : α) → X a ⟶ B
H : EffectiveEpiFamily X π
b : ↑(ExtrDisc.toCompHaus.obj B).toTop
⊢ ∃ a x, ↑(ExtrDisc.toCompHaus.map (π a)) x = b
Tactic:
exact (((effectiveEpiFamily_tfae _ _).out 0 2).1 H : ∀ _, ∃ _, _) _
State after:
no goals