case mk
α : Type u_1
s t u : Set α
hst : s ⊆ t
htu : t ⊆ u
val✝ : α
property✝ : val✝ ∈ s
⊢ inclusion htu (inclusion hst { val := val✝, property := property✝ }) =
    inclusion (_ : s ⊆ u) { val := val✝, property := property✝ }
α : Type u_1
s t u : Set α
hst : s ⊆ t
htu : t ⊆ u
x : ↑s
⊢ inclusion htu (inclusion hst x) = inclusion (_ : s ⊆ u) x
cases x
no goals
case mk
α : Type u_1
s t u : Set α
hst : s ⊆ t
htu : t ⊆ u
val✝ : α
property✝ : val✝ ∈ s
⊢ inclusion htu (inclusion hst { val := val✝, property := property✝ }) =
    inclusion (_ : s ⊆ u) { val := val✝, property := property✝ }
rfl