Theorem: Set.Nonempty.left_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, m⟩ = ⟨x, m⟩

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