feat: positivity extension for the coercion ℝ → ℂ (#9528)

From LeanAPAP

Author: YaelDillies

Mathlib/Analysis/NormedSpace/Star/ContinuousFunctionalCalculus.lean

@@ -92,9 +92,7 @@ theorem spectrum_star_mul_self_of_isStarNormal :
     rintro - ⟨φ, rfl⟩
     rw [gelfandTransform_apply_apply ℂ _ (star a' * a') φ, map_mul φ, map_star φ]
     rw [Complex.eq_coe_norm_of_nonneg (star_mul_self_nonneg _), ← map_star, ← map_mul]
-    exact
-      ⟨Complex.zero_le_real.2 (norm_nonneg _),
-        Complex.real_le_real.2 (AlgHom.norm_apply_le_self φ (star a' * a'))⟩
+    exact ⟨by positivity, Complex.real_le_real.2 (AlgHom.norm_apply_le_self φ (star a' * a'))⟩
 #align spectrum_star_mul_self_of_is_star_normal spectrum_star_mul_self_of_isStarNormal
 
 variable {a}

Mathlib/Data/Complex/Order.lean

@@ -125,3 +125,39 @@ lemma monotone_ofReal : Monotone ofReal' := by
   simp only [ofReal_eq_coe, real_le_real, hxy]
 
 end Complex
+
+namespace Mathlib.Meta.Positivity
+open Lean Meta Qq Complex
+open scoped ComplexOrder
+
+private alias ⟨_, ofReal_pos⟩ := zero_lt_real
+private alias ⟨_, ofReal_nonneg⟩ := zero_le_real
+private alias ⟨_, ofReal_ne_zero_of_ne_zero⟩ := ofReal_ne_zero
+
+/-- Extension for the `positivity` tactic: `Complex.ofReal` is positive/nonnegative/nonzero if its
+input is. -/
+@[positivity Complex.ofReal' _, Complex.ofReal _]
+def evalComplexOfReal : PositivityExt where eval {u α} _ _ e := do
+  -- TODO: Can we avoid duplicating the code?
+  match u, α, e with
+  | 0, ~q(ℂ), ~q(Complex.ofReal' $a) =>
+    assumeInstancesCommute
+    match ← core q(inferInstance) q(inferInstance) a with
+    | .positive pa => return .positive q(ofReal_pos $pa)
+    | .nonnegative pa => return .nonnegative q(ofReal_nonneg $pa)
+    | .nonzero pa => return .nonzero q(ofReal_ne_zero_of_ne_zero $pa)
+    | _ => return .none
+  | 0, ~q(ℂ), ~q(Complex.ofReal $a) =>
+    assumeInstancesCommute
+    match ← core q(inferInstance) q(inferInstance) a with
+    | .positive pa => return .positive q(ofReal_pos $pa)
+    | .nonnegative pa => return .nonnegative q(ofReal_nonneg $pa)
+    | .nonzero pa => return .nonzero q(ofReal_ne_zero_of_ne_zero $pa)
+    | _ => return .none
+  | _, _ => throwError "not Complex.ofReal'"
+
+example (x : ℝ) (hx : 0 < x) : 0 < (x : ℂ) := by positivity
+example (x : ℝ) (hx : 0 ≤ x) : 0 ≤ (x : ℂ) := by positivity
+example (x : ℝ) (hx : x ≠ 0) : (x : ℂ) ≠ 0 := by positivity
+
+end Mathlib.Meta.Positivity