Complex.CartanBound.intervalIntegrable_sqrt_two_div_abs_one_sub_Icc

lemma intervalIntegrable_sqrt_two_div_abs_one_sub_Icc :    IntervalIntegrable      (fun t : ℝ => Real.sqrt (2 / |1 - t|))      volume (1 / 4 : ℝ) (4 : ℝ) := by  let f : ℝ → ℝ := fun u => Real.sqrt (2 / |u|)  have hf0 : IntervalIntegrable f volume (0 : ℝ) (3 : ℝ) := by    have hpow :        IntervalIntegrable (fun u : ℝ => u ^ (- (2⁻¹ : ℝ))) volume (0 : ℝ) (3 : ℝ) := by      simpa using        (intervalIntegral.intervalIntegrable_rpow' (a := (0 : ℝ)) (b := (3 : ℝ))          (r := (- (2⁻¹ : ℝ))) (by linarith : (-1 : ℝ) < - (2⁻¹ : ℝ)))    have hpow2 :        IntervalIntegrable (fun u : ℝ => Real.sqrt 2 * u ^ (- (2⁻¹ : ℝ))) volume (0 : ℝ) (3 : ℝ) :=      hpow.const_mul (Real.sqrt 2)    have hEq :        Set.EqOn f (fun u : ℝ => Real.sqrt 2 * u ^ (- (2⁻¹ : ℝ))) (Set.uIoc (0 : ℝ) (3 : ℝ)) := by      intro u hu      have hu' : u ∈ Set.Ioc (0 : ℝ) (3 : ℝ) := by        simpa [Set.uIoc_of_le (show (0 : ℝ) ≤ 3 by norm_num)] using hu      have hu0 : 0 < u := hu'.1      have hu0' : 0 ≤ u := le_of_lt hu0      have habs : |u| = u := abs_of_nonneg hu0'      have : f u = Real.sqrt (2 / u) := by simp [f, habs]      calc        f u = Real.sqrt (2 / u) := this        _ = Real.sqrt 2 / Real.sqrt u := by simp        _ = Real.sqrt 2 * (Real.sqrt u)⁻¹ := by simp [div_eq_mul_inv]        _ = Real.sqrt 2 * (u ^ (2⁻¹ : ℝ))⁻¹ := by simp [Real.sqrt_eq_rpow]        _ = Real.sqrt 2 * u ^ (- (2⁻¹ : ℝ)) := by              have h : (u ^ (2⁻¹ : ℝ))⁻¹ = u ^ (- (2⁻¹ : ℝ)) := by                simpa using (Real.rpow_neg hu0' (2⁻¹ : ℝ)).symm              simp [h]    exact      (IntervalIntegrable.congr (a := (0 : ℝ)) (b := (3 : ℝ))          (μ := (volume : MeasureTheory.Measure ℝ))          (f := fun u : ℝ => Real.sqrt 2 * u ^ (- (2⁻¹ : ℝ))) (g := f) hEq.symm)        hpow2  have hf0' : IntervalIntegrable f volume (0 : ℝ) (3 / 4 : ℝ) :=    hf0.mono_set (by      intro u hu      have hsub : Set.uIcc (0 : ℝ) (3 / 4 : ℝ) ⊆ Set.uIcc (0 : ℝ) (3 : ℝ) := by        refine Set.uIcc_subset_uIcc ?_ ?_        · simp        · have h0 : (0 : ℝ) ≤ (3 / 4 : ℝ) := by nlinarith          have h1 : (3 / 4 : ℝ) ≤ (3 : ℝ) := by nlinarith          exact (Set.mem_uIcc).2 (Or.inl ⟨h0, h1⟩)      exact hsub hu)  have hleft :      IntervalIntegrable (fun t : ℝ => Real.sqrt (2 / |1 - t|)) volume (1 / 4 : ℝ) (1 : ℝ) := by    have htmp :        IntervalIntegrable (fun t : ℝ => f (1 - t)) volume (1 : ℝ) ((1 : ℝ) - (3 / 4 : ℝ)) := by      simpa using (hf0'.comp_sub_left (c := (1 : ℝ)))    have htmp' :        IntervalIntegrable (fun t : ℝ => f (1 - t)) volume ((1 : ℝ) - (3 / 4 : ℝ)) (1 : ℝ) :=      htmp.symm    have hsub : ((1 : ℝ) - (3 / 4 : ℝ)) = (1 / 4 : ℝ) := by norm_num    have htmp'' : IntervalIntegrable (fun t : ℝ => f (1 - t)) volume (1 / 4 : ℝ) (1 : ℝ) := by      simpa [hsub] using htmp'    simpa [f] using htmp''  have hright :      IntervalIntegrable (fun t : ℝ => Real.sqrt (2 / |1 - t|)) volume (1 : ℝ) (4 : ℝ) := by    have htmp :        IntervalIntegrable (fun t : ℝ => f (t - 1)) volume (1 : ℝ) ((3 : ℝ) + (1 : ℝ)) := by      simpa using (hf0.comp_sub_right (c := (1 : ℝ)))    have hsub : ((3 : ℝ) + (1 : ℝ)) = (4 : ℝ) := by norm_num    have htmp' : IntervalIntegrable (fun t : ℝ => f (t - 1)) volume (1 : ℝ) (4 : ℝ) := by      simpa [hsub] using htmp    have hcongr :        Set.EqOn (fun t : ℝ => f (t - 1)) (fun t : ℝ => Real.sqrt (2 / |1 - t|))          (Set.uIoc (1 : ℝ) (4 : ℝ)) := by      intro t _ht      simp [f, abs_sub_comm]    exact      (IntervalIntegrable.congr (a := (1 : ℝ)) (b := (4 : ℝ))          (μ := (volume : MeasureTheory.Measure ℝ))          (f := fun t : ℝ => f (t - 1)) (g := fun t : ℝ => Real.sqrt (2 / |1 - t|)) hcongr)        htmp'  exact hleft.trans hright