Complex.Hadamard.cartan_rpow_mul_le

lemma cartan_rpow_mul_le    {τ R r : ℝ} (hRpos : 0 < R) (hrpos : 0 < r) (hR_le_r : R ≤ r) (hτ_nonneg : 0 ≤ τ) :    (4 * R) ^ τ ≤ (4 : ℝ) ^ τ * (1 + r) ^ τ := by  have hR_le_1r : R ≤ 1 + r := by linarith [hR_le_r, le_of_lt hrpos]  have hbase0 : 0 ≤ (4 * R : ℝ) := by nlinarith [le_of_lt hRpos]  have : (4 * R) ^ τ ≤ (4 * (1 + r)) ^ τ := by    refine Real.rpow_le_rpow hbase0 ?_ hτ_nonneg    nlinarith [hR_le_1r]  have hmul : (4 * (1 + r)) ^ τ = (4 : ℝ) ^ τ * (1 + r) ^ τ := by    have h4 : 0 ≤ (4 : ℝ) := by norm_num    have h1 : 0 ≤ (1 + r : ℝ) := by positivity    simpa [mul_assoc] using      (Real.mul_rpow (x := (4 : ℝ)) (y := (1 + r : ℝ)) (z := τ) h4 h1)  simpa [hmul] using this