Is Locally Bounded of is Cadlag

lemma isLocallyBounded_of_isCadlag {E : Type*} [LinearOrder ι] [PseudoMetricSpace E]    {f : ι → E} (hf : IsCadlag f) (x : ι) : ∃ t ∈ 𝓝 x, IsBounded (f '' t) := by  obtain ⟨l, hl⟩ := hf.2 x  obtain ⟨U, ⟨⟨A, ⟨hp, ⟨W, hW⟩⟩⟩, hU⟩⟩ := Metric.exists_isBounded_image_of_tendsto hl  obtain ⟨V, ⟨⟨B, ⟨hq, ⟨R, hR⟩⟩⟩, hV⟩⟩ := Metric.exists_isBounded_image_of_tendsto (hf.1 x).tendsto  refine ⟨A ∩ B, inter_mem hp hq, ?_⟩  apply IsBounded.subset ((hU.union hV).union (isBounded_singleton : Bornology.IsBounded ({f x})))  rintro _ ⟨y, ⟨hyL, hyR⟩ , rfl⟩  rcases lt_trichotomy y x with (hlt | heq | hgt)  · have : y ∈ U := hW.2 ▸ ⟨hyL, hW.1 hlt⟩    grind  · grind  · have : y ∈ V := hR.2 ▸ ⟨hyR, hR.1 hgt⟩    grind