Theorem: ExtrDisc.finiteCoproduct.ιOpenEmbedding (Sieves/OpenEmbedding.lean)

State before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ OpenEmbedding ↑(ι Z a)
Tactic:
exact openEmbedding_sigmaMk (σ := fun a => (Z a))
State after:
no goals