Segment' eq segment

theorem segment'_eq_segment (hm : StrictMono f) :    segment' f = segment f := by  classical  ext k; unfold segment'  rcases (show k < f 0 ∨ k ≥ f 0 by omega) with h_k | h_k  · grind  unfold segment; congr 1  simp only [count_eq_card_filter_range]  suffices h : ∃ g, BijOn g      ({x ∈ Finset.range (k - f 0 + 1) | x ∈ range fun x => f x - f 0})      ({x ∈ Finset.range (k + 1) | x ∈ range f}) by    grind [BijOn.finsetCard_eq, Finset.coe_filter]  refine ⟨fun n ↦ n + f 0, ?_, ?_, ?_⟩  · intro n; simp only [mem_range, Finset.mem_range]    rintro ⟨h_n, i, rfl⟩    have := StrictMono.monotone hm <| zero_le i    refine ⟨?_, i, ?_⟩ <;> omega  · grind [injOn_of_injective, Injective]  · intro n; simp only [mem_range, Finset.mem_range, mem_ofPred_eq, mem_image]    rintro ⟨h_n, i, rfl⟩    have := StrictMono.monotone hm <| zero_le i    grind