α : Type u_1
β : Type ?u.112631
γ : Type ?u.112634
δ : Type ?u.112637
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
⊢ {x | x ∈ s.carrier} = ↑s
α : Type u_1
β : Type ?u.112631
γ : Type ?u.112634
δ : Type ?u.112637
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
⊢ (localHomeomorphSubtypeCoe s).toLocalEquiv.target = ↑s
simp only [localHomeomorphSubtypeCoe, Subtype.range_coe_subtype, mfld_simps]
no goals
α : Type u_1
β : Type ?u.112631
γ : Type ?u.112634
δ : Type ?u.112637
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
s : Opens α
inst✝ : Nonempty { x // x ∈ s }
⊢ {x | x ∈ s.carrier} = ↑s
rfl