case mk
α : Type u_1
s t u : Set α
h : s ⊆ t
val✝ : α
property✝ : val✝ ∈ t
m : ↑{ val := val✝, property := property✝ } ∈ s
⊢ inclusion h { val := ↑{ val := val✝, property := property✝ }, property := m } = { val := val✝, property := property✝ }
α : Type u_1
s t u : Set α
h : s ⊆ t
x : ↑t
m : ↑x ∈ s
⊢ inclusion h { val := ↑x, property := m } = x
cases x
no goals
case mk
α : Type u_1
s t u : Set α
h : s ⊆ t
val✝ : α
property✝ : val✝ ∈ t
m : ↑{ val := val✝, property := property✝ } ∈ s
⊢ inclusion h { val := ↑{ val := val✝, property := property✝ }, property := m } = { val := val✝, property := property✝ }
rfl