α : Type u_2
β : Type ?u.4115
γ : Type ?u.4118
ι : Sort u_1
inst✝¹ : Nonempty ι
inst✝ : InfSet α
f : ι → α
⊢ sInf (range ((fun a => ↑a) ∘ f)) = sInf (range fun i => ↑(f i))
α : Type u_2
β : Type ?u.4115
γ : Type ?u.4118
ι : Sort u_1
inst✝¹ : Nonempty ι
inst✝ : InfSet α
f : ι → α
⊢ ↑(⨅ (i : ι), f i) = ⨅ (i : ι), ↑(f i)
rw [iInf, iInf, WithTop.coe_sInf' (range_nonempty f), ← range_comp]
no goals
α : Type u_2
β : Type ?u.4115
γ : Type ?u.4118
ι : Sort u_1
inst✝¹ : Nonempty ι
inst✝ : InfSet α
f : ι → α
⊢ sInf (range ((fun a => ↑a) ∘ f)) = sInf (range fun i => ↑(f i))
rfl