CH2.B_minus_mono

@[blueprint  "B-minus-mono"  (title := "$B^-$ is decreasing")  (statement := /--  For real $t$, $B^-(t)$ is decreasing.  -/)  (proof := /-- Similar to previous.. -/)  (latexEnv := "lemma")  (discussion := 1078)]theorem B_minus_mono : Antitone (fun t:ℝ ↦ (B (-1) t).re) := by  have hasDerivAt_div_exp (c : ℝ) (hne : rexp c - 1 ≠ 0) :      HasDerivAt (fun s => s / (rexp s - 1))        ((1 * (rexp c - 1) - c * rexp c) / (rexp c - 1) ^ 2) c :=    (hasDerivAt_id c).div (show HasDerivAt (fun s => rexp s - 1) (rexp c) c by      have := (Real.hasDerivAt_exp c).sub (hasDerivAt_const c (1 : ℝ))      simp only [sub_zero] at this; exact this) hne  have deriv_nonpos (c : ℝ) (hne : rexp c - 1 ≠ 0) :      (1 * (rexp c - 1) - c * rexp c) / (rexp c - 1) ^ 2 ≤ 0 :=    div_nonpos_of_nonpos_of_nonneg      (by nlinarith [Real.exp_pos c, Real.exp_neg c,        mul_inv_cancel₀ (ne_of_gt (Real.exp_pos c)),        Real.add_one_le_exp c, Real.add_one_le_exp (-c)])      (sq_nonneg _)  have mvt_anti (t1 t2 : ℝ) (hall : ∀ x, t1 ≤ x → x ≤ t2 → rexp x - 1 ≠ 0) (hlt : t1 < t2) :      t2 / (rexp t2 - 1) ≤ t1 / (rexp t1 - 1) := by    obtain ⟨c, hc, hc_eq⟩ : ∃ c ∈ Set.Ioo t1 t2,        deriv (fun s => s / (rexp s - 1)) c =          ((fun s => s / (rexp s - 1)) t2 - (fun s => s / (rexp s - 1)) t1) / (t2 - t1) := by      rw [show (fun s => s / (rexp s - 1)) = (_root_.id / fun x => rexp x - 1) from by        ext x; simp [_root_.id]]      exact exists_deriv_eq_slope _ hlt        (ContinuousOn.div continuousOn_id          (ContinuousOn.sub Real.continuous_exp.continuousOn continuousOn_const)          (fun x hx => hall x hx.1 hx.2))        (DifferentiableOn.div differentiableOn_id          (DifferentiableOn.sub Real.differentiable_exp.differentiableOn (differentiableOn_const _))          (fun x hx => hall x (le_of_lt hx.1) (le_of_lt hx.2)))    have hne := hall c (le_of_lt hc.1) (le_of_lt hc.2)    rw [(hasDerivAt_div_exp c hne).deriv] at hc_eq    have := deriv_nonpos c hne; rw [hc_eq] at this    cases div_nonpos_iff.mp this with    | inl h => linarith [h.1] | inr h => linarith [h.2]  have exp_sub_pos (x : ℝ) (hx : 0 < x) : rexp x - 1 > 0 := by linarith [Real.add_one_le_exp x]  have exp_sub_neg (x : ℝ) (hx : x < 0) : rexp x - 1 < 0 := by    nlinarith [Real.exp_pos x, Real.exp_neg x,      mul_inv_cancel₀ (ne_of_gt (Real.exp_pos x)), Real.add_one_le_exp (-x)]  have div_exp_le_one (t : ℝ) (ht : 0 < t) : t / (rexp t - 1) ≤ 1 := by    rw [div_le_iff₀ (exp_sub_pos t ht)]; linarith [Real.add_one_le_exp t]  have div_exp_ge_one (t : ℝ) (ht : t < 0) : 1 ≤ t / (rexp t - 1) := by    rw [le_div_iff_of_neg (exp_sub_neg t ht)]    nlinarith [Real.exp_pos t, Real.exp_neg t,      mul_inv_cancel₀ (ne_of_gt (Real.exp_pos t)),      Real.add_one_le_exp t, Real.add_one_le_exp (-t)]  suffices heq : (fun t:ℝ ↦ (B (-1) t).re) =      fun t : ℝ => if t = 0 then (1 : ℝ) else t / (rexp t - 1) by    rw [heq]; intro a b hab    rcases eq_or_lt_of_le hab with rfl | hlt; · rfl    simp only    by_cases ha0 : a = 0    · subst ha0; simp only [ite_true, show ¬b = 0 from by linarith, ite_false]      exact div_exp_le_one b (by linarith)    · by_cases hb0 : b = 0      · subst hb0; simp only [ite_true, ha0, ite_false]        exact div_exp_ge_one a (lt_of_le_of_ne (not_lt.mp (fun h => ha0 (by linarith))) ha0)      · simp only [ha0, hb0, ite_false]        by_cases! hpos : 0 < a        · exact mvt_anti a b (fun x hxa hxb => ne_of_gt (exp_sub_pos x (by linarith))) hlt        · have ha_neg : a < 0 := lt_of_le_of_ne hpos ha0          by_cases! hneg : b < 0          · exact mvt_anti a b (fun x hxa hxb => ne_of_lt (exp_sub_neg x (by linarith))) hlt          · have hb_pos : 0 < b := lt_of_le_of_ne hneg (Ne.symm hb0)            linarith [div_exp_le_one b hb_pos, div_exp_ge_one a ha_neg]  funext t; split  · next h => subst h; unfold B; simp  · next ht =>    unfold B coth    have ht' : (t : ℂ) ≠ 0 := by exact_mod_cast ht    simp only [ht', ↓reduceIte, one_div]    rw [show ((-1 : ℝ) : ℂ) = -1 from by push_cast; ring]    conv_lhs => rw [show (t : ℂ) / 2 = ((t / 2 : ℝ) : ℂ) from by push_cast; ring]    rw [show Complex.tanh ((t / 2 : ℝ) : ℂ) = ((Real.tanh (t / 2) : ℝ) : ℂ) from by        apply Complex.ext <;> simp,      show ((Real.tanh (t / 2) : ℝ) : ℂ)⁻¹ = ((Real.tanh (t / 2))⁻¹ : ℝ) from by push_cast; ring,      show (↑t * (↑(Real.tanh (t / 2))⁻¹ + (-1 : ℂ)) / 2 : ℂ) =        ((t * ((Real.tanh (t / 2))⁻¹ + (-1 : ℝ)) / 2 : ℝ) : ℂ) from by push_cast; ring]    simp only [Complex.ofReal_re]; rw [Real.tanh_eq]    have h2 : rexp (t / 2) - rexp (-(t / 2)) ≠ 0 := by      intro h; exact ht (by linarith [Real.exp_injective (show rexp (t/2) = rexp (-(t/2)) by linarith)])    have h3 : rexp t - 1 ≠ 0 := by      intro h; exact ht ((Real.exp_eq_one_iff t).mp (by linarith))    rw [inv_div]; field_simp    nlinarith [show rexp t = rexp (t / 2) * rexp (t / 2) by rw [← Real.exp_add]; ring_nf,      show rexp (t / 2) * rexp (-(t / 2)) = 1 by rw [← Real.exp_add]; simp,      Real.exp_pos (t/2), Real.exp_pos (-(t/2))]