style: make style chack pass

Author: ramonfmir

CvxLean/Examples/FittingSphere.lean

@@ -127,7 +127,7 @@ equivalence* eqv/fittingSphereT (n m : ℕ) (x : Fin m → Fin n → ℝ) : fitt
     apply ChangeOfVariablesBij.toEquivalence
       (fun (ct : (Fin n → ℝ) × ℝ) => (ct.1, sqrt (ct.2 + ‖ct.1‖ ^ 2))) covBij
     · rintro cr h; exact h
-    . rintro ct _; simp [covBij, sq_nonneg]
+    · rintro ct _; simp [covBij, sq_nonneg]
   rename_vars [c, t]
   rename_constrs [h₁, h₂]
   conv_constr h₁ => dsimp

CvxLean/Lib/Math/SchurComplement.lean

@@ -55,9 +55,9 @@ lemma IsHermitian.fromBlocks₁₁ [Fintype m] [DecidableEq m] {A : Matrix m m 
     apply hA.inv
   rw [isHermitian_fromBlocks_iff]
   constructor
-  . intro h
+  · intro h
     apply IsHermitian.sub h.2.2.2 hBAB
-  . intro h
+  · intro h
     refine' ⟨hA, rfl, conjTranspose_conjTranspose B, _⟩
     rw [← sub_add_cancel D]
     apply IsHermitian.add h hBAB

CvxLean/Tactic/DCP/AtomLibrary/Fns/Log.lean

@@ -20,8 +20,7 @@ solutionEqualsAtom by
   rfl;
 feasibility (c_exp : by
   unfold expCone
-  simp
-  rw [Real.exp_log cond])
+  simp [Real.exp_log cond])
 optimality by
   intros y hy
   unfold expCone at c_exp

CvxLean/Tactic/DCP/AtomLibrary/Fns/Sqrt.lean

@@ -26,8 +26,7 @@ feasibility
     dsimp
     unfold rotatedSoCone
     refine ⟨?_, cond, by norm_num⟩
-    simp
-    rw [sq_sqrt cond])
+    simp [sq_sqrt cond])
 optimality by
   intros y hy
   unfold rotatedSoCone at c1