no goals
α : Type u_2
β : Type u_1
β₂ : Type ?u.162828
γ : Type ?u.162831
ι : Sort ?u.162834
ι' : Sort ?u.162837
κ : ι → Sort ?u.162842
κ' : ι' → Sort ?u.162847
inst✝ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
s : Set β
f : β → α
⊢ IsGLB (f '' s) (⨅ (x : β) (_ : x ∈ s), f x)
simpa only [range_comp, Subtype.range_coe, iInf_subtype'] using
  @isGLB_iInf α s _ (f ∘ fun x => (x : β))