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

State before:
X : Type
s : Set X
ne : s.Nonempty
⊢ ∀ x ∈ s, ↑(ne.invCoe x) = x
Tactic:
intro x m
State after:
X : Type
s : Set X
ne : s.Nonempty
x : X
m : x ∈ s
⊢ ↑(ne.invCoe x) = x

State before:
X : Type
s : Set X
ne : s.Nonempty
x : X
m : x ∈ s
⊢ ↑(ne.invCoe x) = x
Tactic:
simp only [Set.Nonempty.invCoe, m, dif_pos, Subtype.coe_mk]
State after:
no goals