[Merged by Bors] - chore: cleanup TODOs around leanprover/lean4#3060

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -148,26 +148,20 @@ open Lean Meta Qq
 /-- Extension for the `positivity` tactic: `UpperHalfPlane.im`. -/
 @[positivity UpperHalfPlane.im _]
 def evalUpperHalfPlaneIm : PositivityExt where eval {u α} _zα _pα e := do
-  -- TODO: can't merge the `match`es without lean4#3060
-  match u with
-  | 0 => match α, e with
-    | ~q(ℝ), ~q(UpperHalfPlane.im $a) =>
-      assertInstancesCommute
-      pure (.positive q(@UpperHalfPlane.im_pos $a))
-    | _, _ => throwError "not UpperHalfPlane.im"
-  | _ => throwError "not UpperHalfPlane.im"
+  match u, α, e with
+  | 0, ~q(ℝ), ~q(UpperHalfPlane.im $a) =>
+    assertInstancesCommute
+    pure (.positive q(@UpperHalfPlane.im_pos $a))
+  | _, _, _ => throwError "not UpperHalfPlane.im"
 
 /-- Extension for the `positivity` tactic: `UpperHalfPlane.coe`. -/
 @[positivity UpperHalfPlane.coe _]
 def evalUpperHalfPlaneCoe : PositivityExt where eval {u α} _zα _pα e := do
-  -- TODO: can't merge the `match`es without lean4#3060
-  match u with
-  | 0 => match α, e with
-    | ~q(ℂ), ~q(UpperHalfPlane.coe $a) =>
-      assertInstancesCommute
-      pure (.nonzero q(@UpperHalfPlane.ne_zero $a))
-    | _, _ => throwError "not UpperHalfPlane.coe"
-  | _ => throwError "not UpperHalfPlane.coe"
+  match u, α, e with
+  | 0, ~q(ℂ), ~q(UpperHalfPlane.coe $a) =>
+    assertInstancesCommute
+    pure (.nonzero q(@UpperHalfPlane.ne_zero $a))
+  | _, _, _ => throwError "not UpperHalfPlane.coe"
 
 end Mathlib.Meta.Positivity
 

Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean

@@ -1201,17 +1201,15 @@ is. -/
 def evalSinh : PositivityExt where eval {u α} _ _ e := do
   let zα : Q(Zero ℝ) := q(inferInstance)
   let pα : Q(PartialOrder ℝ) := q(inferInstance)
-  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
-    match α, e with
-    | ~q(ℝ), ~q(Real.sinh $a) =>
-      assumeInstancesCommute
-      match ← core zα pα a with
-      | .positive pa => return .positive q(sinh_pos_of_pos $pa)
-      | .nonnegative pa => return .nonnegative q(sinh_nonneg_of_nonneg $pa)
-      | .nonzero pa => return .nonzero q(sinh_ne_zero_of_ne_zero $pa)
-      | _ => return .none
-    | _, _ => throwError "not Real.sinh"
-  else throwError "not Real.sinh"
+  match u, α, e with
+  | 0, ~q(ℝ), ~q(Real.sinh $a) =>
+    assumeInstancesCommute
+    match ← core zα pα a with
+    | .positive pa => return .positive q(sinh_pos_of_pos $pa)
+    | .nonnegative pa => return .nonnegative q(sinh_nonneg_of_nonneg $pa)
+    | .nonzero pa => return .nonzero q(sinh_ne_zero_of_ne_zero $pa)
+    | _ => return .none
+  | _, _, _ => throwError "not Real.sinh"
 
 example (x : ℝ) (hx : 0 < x) : 0 < x.sinh := by positivity
 example (x : ℝ) (hx : 0 ≤ x) : 0 ≤ x.sinh := by positivity

Mathlib/Data/Nat/Factorial/DoubleFactorial.lean

@@ -95,13 +95,11 @@ open Lean Meta Qq
 /-- Extension for `Nat.doubleFactorial`. -/
 @[positivity Nat.doubleFactorial _]
 def evalDoubleFactorial : PositivityExt where eval {u α} _ _ e := do
-  if let 0 := u then -- lean4#3060 means we can't combine this with the match below
-    match α, e with
-    | ~q(ℕ), ~q(Nat.doubleFactorial $n) =>
-      assumeInstancesCommute
-      return .positive q(Nat.doubleFactorial_pos $n)
-    | _, _ => throwError "not Nat.doubleFactorial"
-  else throwError "not Nat.doubleFactorial"
+  match u, α, e with
+  | 0, ~q(ℕ), ~q(Nat.doubleFactorial $n) =>
+    assumeInstancesCommute
+    return .positive q(Nat.doubleFactorial_pos $n)
+  | _, _ => throwError "not Nat.doubleFactorial"
 
 example (n : ℕ) : 0 < n‼ := by positivity