Theorem: ExtrDisc.openEmbedding_of_sigma_desc_iso (ExtrDisc/ExplicitSheaves.lean)

State before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
⊢ ∀ (a : α), OpenEmbedding ↑(i a)
Tactic:
intro a
State after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
⊢ OpenEmbedding ↑(i a)

State before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
⊢ OpenEmbedding ↑(i a)
Tactic:
have h₁ : OpenEmbedding (Sigma.desc i) :=
  (ExtrDisc.homeoOfIso (asIso (Sigma.desc i))).openEmbedding
State after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
⊢ OpenEmbedding ↑(i a)

State before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
⊢ OpenEmbedding ↑(i a)
Tactic:
have h₂ : OpenEmbedding (Sigma.ι Z a) := openEmbedding_ι _ _
State after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
⊢ OpenEmbedding ↑(i a)

State before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
⊢ OpenEmbedding ↑(i a)
Tactic:
have := OpenEmbedding.comp h₁ h₂
State after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding (↑(Sigma.desc i) ∘ ↑(Sigma.ι Z a))
⊢ OpenEmbedding ↑(i a)

State before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding (↑(Sigma.desc i) ∘ ↑(Sigma.ι Z a))
⊢ OpenEmbedding ↑(i a)
Tactic:
erw [← CategoryTheory.coe_comp (Sigma.ι Z a) (Sigma.desc i)] at this
State after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding ↑(Sigma.ι Z a ≫ Sigma.desc i)
⊢ OpenEmbedding ↑(i a)

State before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding ↑(Sigma.ι Z a ≫ Sigma.desc i)
⊢ OpenEmbedding ↑(i a)
Tactic:
simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app] at this
State after:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding ↑(i a)
⊢ OpenEmbedding ↑(i a)

State before:
α : Type
inst✝ : Fintype α
X : ExtrDisc
Z : α → ExtrDisc
i : (a : α) → Z a ⟶ X
HIso : IsIso (Sigma.desc i)
a : α
h₁ : OpenEmbedding ↑(Sigma.desc i)
h₂ : OpenEmbedding ↑(Sigma.ι Z a)
this : OpenEmbedding ↑(i a)
⊢ OpenEmbedding ↑(i a)
Tactic:
assumption
State after:
no goals