style

leanprover-community · Jan 6, 2025 · ad2ba3a · ad2ba3a
1 parent a9a7dce
commit ad2ba3a
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Algebra/Ring/SumsOfSquares.lean b/Mathlib/Algebra/Ring/SumsOfSquares.lean
@@ -204,7 +204,7 @@ sums of squares are non-negative.
 theorem IsSumSq.nonneg {R : Type*} [LinearOrderedSemiring R] [ExistsAddOfLE R] {s : R}
     (hs : IsSumSq s) : 0 ≤ s := by
   induction ps using IsSumSq.rec'
-  case zero => aesop
-  case sq_add x s hx hs h_sum => exact add_nonneg (IsSquare.nonneg hx) h_sum
+  | zero                   => aesop
+  | sq_add x s hx hs h_sum => exact add_nonneg (IsSquare.nonneg hx) h_sum
 
 @[deprecated (since := "2024-08-09")] alias isSumSq.nonneg := IsSumSq.nonneg