arcosh_arg_ge_one

proof body

Tactic-mode proof.

  29  have hsin : 0 ≤ Real.sin ϑ := by
  30    have hmem : ϑ ∈ Set.Icc (0 : ℝ) Real.pi := by
  31      constructor
  32      · exact hϑ.1
  33      · have hpi2_le_pi : (Real.pi / 2 : ℝ) ≤ Real.pi := by nlinarith [Real.pi_pos]
  34        exact le_trans hϑ.2 hpi2_le_pi
  35    simpa using Real.sin_nonneg_of_mem_Icc hmem
  36  have hcos : 0 ≤ Real.cos ϑ := by
  37    have hmem : ϑ ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2) := by
  38      constructor
  39      · have hneg : (-(Real.pi / 2) : ℝ) ≤ 0 := by nlinarith [Real.pi_pos]
  40        exact le_trans hneg hϑ.1
  41      · exact hϑ.2
  42    simpa using Real.cos_nonneg_of_mem_Icc hmem
  43  have hcot : 0 ≤ Real.cot ϑ := by
  44    -- Rewrite `cot` as `cos / sin` on reals.
  45    simpa [Real.cot_eq_cos_div_sin] using (div_nonneg hcos hsin)
  46  have hprod : 0 ≤ 2 * Real.cot ϑ := by
  47    have htwo : 0 ≤ (2 : ℝ) := by norm_num
  48    exact mul_nonneg htwo hcot
  49  simpa using add_le_add_left hprod 1
  50
  51/-- Recognition profile is positive -/