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

State before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ OpenEmbedding ↑(Sigma.ι Z a)
Tactic:
refine' OpenEmbedding.of_comp _ (toFiniteCoproduct.OpenEmbedding Z) _
State after:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ OpenEmbedding (↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a))

State before:
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ OpenEmbedding (↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a))
Tactic:
convert finiteCoproduct.ιOpenEmbedding Z a
State after:
case h.e'_5
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ ↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a) = ↑(finiteCoproduct.ι Z a)

State before:
case h.e'_5
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
⊢ ↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a) = ↑(finiteCoproduct.ι Z a)
Tactic:
ext x
State after:
case h.e'_5.h
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
x : CoeSort.coe (Z a)
⊢ (↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a)) x = ↑(finiteCoproduct.ι Z a) x

State before:
case h.e'_5.h
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
x : CoeSort.coe (Z a)
⊢ (↑(toFiniteCoproductHomeo Z) ∘ ↑(Sigma.ι Z a)) x = ↑(finiteCoproduct.ι Z a) x
Tactic:
change ((Sigma.ι Z a) ≫ toFiniteCoproduct Z) x = _
State after:
case h.e'_5.h
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
x : CoeSort.coe (Z a)
⊢ ↑(Sigma.ι Z a ≫ toFiniteCoproduct Z) x = ↑(finiteCoproduct.ι Z a) x

State before:
case h.e'_5.h
α✝ : Type
inst✝¹ : Fintype α✝
Z✝ : α✝ → ExtrDisc
α : Type
inst✝ : Fintype α
Z : α → ExtrDisc
a : α
x : CoeSort.coe (Z a)
⊢ ↑(Sigma.ι Z a ≫ toFiniteCoproduct Z) x = ↑(finiteCoproduct.ι Z a) x
Tactic:
simp
State after:
no goals