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

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