Theorem: Set.Nonempty.continuousOn_invCoe (Ray/Misc/TotallyDisconnected.lean)

State before:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
⊢ ContinuousOn ne.invCoe s
Tactic:
rw [embedding_subtype_val.continuousOn_iff]
State after:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
⊢ ContinuousOn (Subtype.val ∘ ne.invCoe) s

State before:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
⊢ ContinuousOn (Subtype.val ∘ ne.invCoe) s
Tactic:
apply continuousOn_id.congr
State after:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
⊢ EqOn (Subtype.val ∘ ne.invCoe) id s

State before:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
⊢ EqOn (Subtype.val ∘ ne.invCoe) id s
Tactic:
intro x m
State after:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
x : X
m : x ∈ s
⊢ (Subtype.val ∘ ne.invCoe) x = id x

State before:
X : Type
s : Set X
ne : s.Nonempty
inst✝ : TopologicalSpace X
x : X
m : x ∈ s
⊢ (Subtype.val ∘ ne.invCoe) x = id x
Tactic:
simp only [Function.comp, ne.right_invCoe _ m, id]
State after:
no goals