∀ {ι₁ : Type u_3} {ι₂ : Type u_4} {α : Type u_5} [inst : Preorder ι₂] [inst_1 : CompleteLattice α] {l : Filter ι₁}
  [l.NeBot] {f : ι₂ → α} {φ : ι₁ → ι₂}, Monotone f → Filter.Tendsto φ l Filter.atBot → ⨅ i, f i = ⨅ i, f (φ i)