Theorem: CompHaus.finiteCoproduct.ι_jointly_surjective (CompHaus/ExplicitLimits.lean)

State before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → CompHaus
α : Type
inst✝ : Fintype α
Z : α → CompHaus
R : ↑(finiteCoproduct Z).toTop
⊢ ∃ a r, R = ↑(ι Z a) r
Tactic:
exact ⟨R.fst, R.snd, rfl⟩
State after:
no goals