intro t ht
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
⊢ P.bind Qs ≤ P
α✝¹ : Type u_1
inst✝² : CompleteLattice α✝¹
s✝¹ x y z : α✝¹
α✝ : Type u_2
inst✝¹ : CompleteDistribLattice α✝
s✝ : α✝
α : Type u_3
inst✝ : CompleteDistribLattice α
s : α
P : Partition s
Qs : (a : α) → a ∈ P → Partition a
t : α
ht : t ∈ P.bind Qs
⊢ ∃ y ∈ P, t ≤ y