Mathlib Real.exp/log/sqrt/rpow: which lemmas are iffs, and where hypotheses go

Checked with #check on Mathlib v4.35.0. Real.exp_le_exp/exp_lt_exp are hypothesis-free iffs, so Real.exp_le_exp h fails with 'Function expected'; write Real.exp_le_exp.2 h or Real.exp_monotone h. Real.log_le_log hx h / log_lt_log hx h are implications (0 < x → x ≤ y → log x ≤ log y); the iff is log_le_log_iff hx hy, and the old (Real.log_le_log hx hy).2 h fails with 'Invalid projection'. Square roots: sqrt_le_sqrt h needs no sign hypothesis, sqrt_lt_sqrt needs 0 ≤ x; sqrt_le_iff : √x ≤ y ↔ 0 ≤ y ∧ x ≤ y ^ 2 is hypothesis-free, sqrt_le_left (hy : 0 ≤ y) drops the conjunct; sqrt_mul hx y puts the hypothesis on the left factor, sqrt_mul' x hy on the right; Real.sqrt_eq_iff does not exist, use sqrt_eq_iff_eq_sq hx hy, sqrt_eq_iff_mul_self_eq hx hy or the hypothesis-free sqrt_eq_cases. Real.rpow_add needs 0 < x but Real.rpow_mul only 0 ≤ x. Finally, x ^ (2 : ℝ) prints as x ^ 2: ring on x ^ (2 : ℝ) = x * x fails showing ⊢ x ^ 2 = x ^ 2; rw [Real.rpow_two] or norm_cast before ring fixes it, and set_option pp.numericTypes true shows the difference.