α β : Type u
ι : Sort u_1
f : ι → Cardinal
⊢ lift (sInf (range f)) = sInf (range fun i => lift (f i))
α β : Type u
ι : Sort u_1
f : ι → Cardinal
⊢ lift (iInf f) = ⨅ (i : ι), lift (f i)
unfold iInf
case h.e'_3.h.e'_3
α β : Type u
ι : Sort u_1
f : ι → Cardinal
⊢ (range fun i => lift (f i)) = lift '' range f
α β : Type u
ι : Sort u_1
f : ι → Cardinal
⊢ lift (sInf (range f)) = sInf (range fun i => lift (f i))
convert lift_sInf (range f)
no goals
case h.e'_3.h.e'_3
α β : Type u
ι : Sort u_1
f : ι → Cardinal
⊢ (range fun i => lift (f i)) = lift '' range f
simp_rw [←comp_apply (f := lift), range_comp]