diff --git a/Convex/Algorithm/GradientDescent.lean b/Convex/Algorithm/GradientDescent.lean
index 578e021..9f4c66c 100644
--- a/Convex/Algorithm/GradientDescent.lean
+++ b/Convex/Algorithm/GradientDescent.lean
@@ -111,7 +111,7 @@ open InnerProductSpace Set
 
 variable {f : E → ℝ} {f' : E → E}
 
-variable {l : NNReal} {xm x₀ : E}{a : ℝ}
+variable {l : NNReal} {xm x₀ : E} {a : ℝ}
 
 variable {alg : Gradient_Descent_fix_stepsize f f' x₀}
 
@@ -142,7 +142,7 @@ lemma convex_lipschitz (h₁ : ∀ x₁ : E, HasGradientAt f (f' x₁) x₁)
         · simp;
           calc l / 2 * a * a = (l * a) * (a / 2) := by ring_nf
                 _  ≤ 1 * (a / 2) := by
-                  apply mul_le_mul_of_le_of_le _ (by linarith) (by positivity) (by linarith)
+                  apply mul_le_mul_of_nonneg _ (by linarith) (by positivity) (by linarith)
                   · exact (le_div_iff ha₂).mp ha₁
                 _  = - a / 2 + a := by ring_nf
         · exact sq_nonneg ‖f' x‖
@@ -153,15 +153,13 @@ lemma point_descent_for_convex (hfun : ConvexOn ℝ Set.univ f) (step₂ : alg.a
     ∀ k : ℕ, f (alg.x (k + 1)) ≤ f xm + 1 / ((2 : ℝ) * alg.a)
       * (‖alg.x k - xm‖ ^ 2 - ‖alg.x (k + 1) - xm‖ ^ 2) := by
   have step₂ : alg.l ≤ 1 / alg.a := by
-    rw [le_one_div alg.step₁] at step₂; exact step₂; linarith [alg.hl]
+    rw [le_one_div alg.step₁] at step₂; exact step₂; exact alg.hl
   intro k
-  have : LipschitzWith alg.l f' := alg.smooth
-  have : alg.l > 0 := alg.hl
   have descent: ∀ x : E, f (x - alg.a • (f' x)) ≤
       f xm + 1 / ((2 : ℝ) * alg.a) * (‖x - xm‖ ^ 2 - ‖x - alg.a • (f' x) - xm‖ ^ 2) := by
     intro x
     have t1 : 1 / ((2 : ℝ) * alg.a) * ((2 : ℝ) * alg.a) = 1 := by
-      field_simp; ring_nf; apply mul_inv_cancel; linarith [alg.step₁]
+      ring_nf; field_simp [ne_of_gt alg.step₁]
     have t2 : inner (f' x) (x - xm) - alg.a / 2 * ‖f' x‖ ^ 2 =
         1 / ((2 : ℝ) * alg.a) * (‖x - xm‖ ^ 2 - ‖x - alg.a • (f' x) - xm‖ ^ 2) := by
       symm
@@ -179,7 +177,7 @@ lemma point_descent_for_convex (hfun : ConvexOn ℝ Set.univ f) (step₂ : alg.a
           _ = inner (f' x) (x - xm) - alg.a / (2 : ℝ)
               * ‖f' x‖ ^ 2 := by ring_nf; simp; left; rw [pow_two,mul_self_mul_inv alg.a]
     calc f (x - alg.a • (f' x)) ≤ f x - alg.a / 2 * ‖f' x‖ ^ 2 := by
-              exact convex_lipschitz alg.diff this step₂ alg.step₁ alg.smooth x
+              exact convex_lipschitz alg.diff alg.hl step₂ alg.step₁ alg.smooth x
             _   ≤ f xm + inner (f' x) (x - xm) - alg.a / 2 * ‖f' x‖ ^ 2 := by
               linarith [convex_function alg.diff hfun x xm]
             _   = f xm + 1 / ((2 : ℝ) * alg.a) * (‖x - xm‖ ^ 2 - ‖x - alg.a • (f' x) - xm‖ ^ 2) := by
@@ -194,7 +192,7 @@ lemma gradient_method (hfun: ConvexOn ℝ Set.univ f) (step₂ : alg.a ≤ 1 / a
     ∀ k : ℕ, f (alg.x (k + 1)) - f xm ≤ 1 / (2 * (k + 1) * alg.a) * ‖x₀ - xm‖ ^ 2 := by
   intro k
   have step1₂ : alg.l ≤ 1 / alg.a := by
-    rw [le_one_div alg.step₁] at step₂; exact step₂; linarith [alg.hl]
+    rw [le_one_div alg.step₁] at step₂; exact step₂; exact alg.hl
   have : LipschitzWith alg.l f' := alg.smooth
   have : alg.l > 0 := alg.hl
   have tα : 1 / ((2 : ℝ) * (k + 1) * alg.a) > 0 := by
@@ -219,7 +217,7 @@ lemma gradient_method (hfun: ConvexOn ℝ Set.univ f) (step₂ : alg.a ≤ 1 / a
         _ ≤ f xm + 1 / (2 * alg.a) * (‖alg.x 0 - xm‖ ^ 2 - ‖alg.x (0 + 1) - xm‖ ^ 2) :=
             xdescent
         _ = alg.a⁻¹ * 2⁻¹ * (‖x₀ - xm‖^ 2 - ‖alg.x 1 - xm‖ ^ 2) + f xm := by
-            rw [alg.initial]; simp; ring_nf
+            rw [alg.initial, one_div, mul_inv_rev, zero_add]; ring_nf
     · specialize xdescent (j + 1)
       calc
         _ = (Finset.range (j + 1)).sum (fun (k : ℕ) ↦ f (alg.x (k + 1)) - f xm)
@@ -238,7 +236,7 @@ lemma gradient_method (hfun: ConvexOn ℝ Set.univ f) (step₂ : alg.a ≤ 1 / a
   specialize sum_prop k
   have h : f (alg.x (k + 1)) - f xm ≤ 1 / (2 * (k + 1) * alg.a) *
      (‖x₀ - xm‖ ^ 2 - ‖alg.x (k + 1) - xm‖ ^ 2) := by
-    have tt1 : 0 ≤ k + (1 : ℝ) := by exact add_nonneg (Nat.cast_nonneg k) zero_le_one
+    have tt1 : 0 ≤ k + (1 : ℝ) := add_nonneg (Nat.cast_nonneg k) zero_le_one
     calc
       _ ≤ (Finset.range (k + 1)).sum (fun (k : ℕ) ↦ f (alg.x (k + 1)) - f xm) / (k + 1) :=
         sum_prop_1
diff --git a/Convex/Algorithm/GradientDescentStronglyConvex.lean b/Convex/Algorithm/GradientDescentStronglyConvex.lean
index 9149432..1566bff 100644
--- a/Convex/Algorithm/GradientDescentStronglyConvex.lean
+++ b/Convex/Algorithm/GradientDescentStronglyConvex.lean
@@ -38,7 +38,7 @@ theorem Strong_convex_Lipschitz_smooth (hsc: StrongConvexOn univ m f) (mp : m >
   let phi : E → ℝ := fun x ↦ l / 2 * ‖x‖ ^ 2 - f x
   have convphi : ConvexOn ℝ univ phi := by
     apply lipschitz_to_lnorm_sub_convex
-    apply cov; simp; apply hf; rw [← lipschitzOn_univ] at h₂; apply h₂; apply hl
+    apply cov; simp; apply hf; rw [← lipschitzOnWith_univ] at h₂; apply h₂; apply hl
   let g : E → ℝ := fun x ↦ f x - m / 2 * ‖x‖ ^ 2
   let g' : E → E := fun x ↦ f' x - m • x
   let h : E → ℝ := fun x ↦ (l - m) / 2 * ‖x‖ ^ 2 - g x
@@ -135,10 +135,9 @@ lemma lipschitz_derivxm_eq_zero (h₁ : ∀ x : E, HasGradientAt f (f' x) x)
   have eq4 : ‖f' xm‖ ^ 2 / (2 * l) = 0 := by linarith
   field_simp at eq4; exact eq4
 
-variable (hsc: StrongConvexOn univ m f) {alg : Gradient_Descent_fix_stepsize f f' x₀}
+variable {alg : Gradient_Descent_fix_stepsize f f' x₀}
 
-lemma gradient_method_strong_convex (hm : m > 0) (min : IsMinOn f univ xm)
-    (step₂ : alg.a ≤ 2 / (m + alg.l)) : ∀ k : ℕ , ‖alg.x k - xm‖ ^ 2 ≤ (1 - alg.a *
+lemma gradient_method_strong_convex (hm : m > 0) (min : IsMinOn f univ xm) (step₂ : alg.a ≤ 2 / (m + alg.l)) (hsc: StrongConvexOn univ m f) : ∀ k : ℕ , ‖alg.x k - xm‖ ^ 2 ≤ (1 - alg.a *
     (2 * m * alg.l / (m + alg.l))) ^ k * ‖x₀ - xm‖ ^ 2 := by
   have : LipschitzWith alg.l f' := alg.smooth
   have : alg.l > (0 : ℝ) := alg.hl
diff --git a/Convex/Algorithm/LASSO.lean b/Convex/Algorithm/LASSO.lean
index 28ead33..956a719 100644
--- a/Convex/Algorithm/LASSO.lean
+++ b/Convex/Algorithm/LASSO.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Yuxuan Wu, Chenyi Li. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yuxuan Wu, Chenyi Li
 -/
-import Mathlib.Analysis.NormedSpace.Star.Matrix
+import Mathlib.Analysis.CStarAlgebra.Matrix
 import Mathlib.LinearAlgebra.Matrix.DotProduct
 import Convex.Algorithm.ProximalGradient
 
@@ -148,8 +148,7 @@ theorem affine_sq_gradient :  ∀ x : (EuclideanSpace ℝ (Fin n)),
   have φeq : φ = fun x : (EuclideanSpace ℝ (Fin n)) => f x - h x + (1 / 2) * b ⬝ᵥ b := by
     ext z; simp [φ]; rw [norm2eq_dot]; simp [f, h]
     rw [← sub_add, dotProduct_comm _ b, sub_sub, ← two_mul, mul_add, mul_sub, ← mul_assoc]
-    rw [inv_mul_cancel, one_mul]
-    simp
+    field_simp
   have φ'eq : φ' = fun x : (EuclideanSpace ℝ (Fin n)) => f' x - h' x := by
     ext y z; simp [φ', f', h']
     rw [Matrix.mulVec_sub Aᵀ]; simp
@@ -211,8 +210,7 @@ theorem norm_one_proximal
     ext z; rw [Pi.smul_apply]; simp [g]; rw [lasso]; simp; rw [mul_assoc]
   rw [← geqth]
   show prox_prop ((t * μ) • (fun (x : EuclideanSpace ℝ (Fin n)) => ‖x‖₁)) x xm
-  have tμpos : 0 < t * μ := by
-    apply mul_pos; linarith [tpos]; linarith [μpos]
+  have tμpos : 0 < t * μ := mul_pos tpos μpos;
   rw [prox_iff_subderiv_smul (fun x : (EuclideanSpace ℝ (Fin n)) => ‖x‖₁) norm_one_convex tμpos]
   rw [← mem_SubderivAt, HasSubgradientAt]
   intro y
@@ -237,9 +235,7 @@ theorem norm_one_proximal
         exact aux; apply mul_nonneg; apply mul_nonneg
         apply abs_nonneg; simp; linarith [μpos]; simp; linarith [tpos]
       _ = |y i| := by
-        rw [mul_assoc _ (t⁻¹) t, inv_mul_cancel, mul_one]
-        rw [mul_assoc _ (μ⁻¹) μ, inv_mul_cancel, mul_one]
-        linarith [μpos]; linarith [tpos]
+        field_simp; linarith [μpos];
   · rw [eq_ite_iff, or_iff_right] at abs_subg
     rcases abs_subg with ⟨_, abs_subg⟩
     let sgnxm := sign (xm i)
@@ -256,7 +252,7 @@ theorem norm_one_proximal
       rw [eq1]; simp; nth_rw 3 [mul_sub]
       rw [← sub_add, real_sign_mul_abs]; simp
       nth_rw 2 [mul_comm (sign (x i))]
-      rw [← mul_assoc _ (t * μ), ← mul_inv, mul_comm μ t, inv_mul_cancel, one_mul]
+      rw [← mul_assoc _ (t * μ), ← mul_inv, mul_comm μ t, inv_mul_cancel₀ (ne_of_gt tμpos), one_mul];
       by_cases hx : 0 < x i
       · have eq2 : sign (sign (x i) * (|x i| - t * μ)) = 1 := by
           apply Real.sign_of_pos; apply mul_pos
@@ -276,7 +272,6 @@ theorem norm_one_proximal
             _ < 0 := by linarith
           linarith [ieq]
         rw [eq2]; symm; apply Real.sign_of_neg xneg
-      linarith [μpos, tpos]
     rw [aux2] at aux; linarith [aux]
     push_neg; intro hxm'; contrapose! hxm'; exact hxm
 
diff --git a/Convex/Algorithm/NesterovAccelerationFirst.lean b/Convex/Algorithm/NesterovAccelerationFirst.lean
index 52278e1..8ed814b 100644
--- a/Convex/Algorithm/NesterovAccelerationFirst.lean
+++ b/Convex/Algorithm/NesterovAccelerationFirst.lean
@@ -37,9 +37,9 @@ class Nesterov_first (f h: E → ℝ) (f' : E → E) (x0 : E) :=
   (update2 : ∀ k : ℕ, prox_prop (t k • h) (y k - t k • f' (y k)) (x (k + 1)))
 
 variable {alg : Nesterov_first f h f' x0}
-variable {xm : E} (minφ : IsMinOn (f + h) univ xm)
+variable {xm : E}
 
-theorem Nesterov_first_converge : ∀ k, f (alg.x (k + 1)) + h (alg.x (k + 1)) -
+theorem Nesterov_first_converge (minφ : IsMinOn (f + h) univ xm) : ∀ k, f (alg.x (k + 1)) + h (alg.x (k + 1)) -
     f xm - h xm ≤ (alg.γ k) ^ 2 / (2 * alg.t k) * ‖x0 - xm‖ ^ 2 := by
   have h1 : ∀ k : ℕ, alg.y k - alg.x (k + 1) - (alg.t k) • (f' (alg.y k))
       ∈ (SubderivAt ((alg.t k) • h) (alg.x (k + 1))) := by
@@ -277,9 +277,9 @@ theorem Nesterov_first_converge : ∀ k, f (alg.x (k + 1)) + h (alg.x (k + 1)) -
           linarith [alg.tbound 0]
         _ = ‖alg.x 0 - xm‖ ^ 2 := by
           rw [← add_sub, sub_self, add_zero, mul_add, ← mul_assoc]; ring_nf
-          rw [mul_inv_cancel, one_mul, one_mul, alg.oriy, norm_sub_rev (alg.x 1) xm]
+          rw [mul_inv_cancel₀ (by linarith [alg.tbound 0]), one_mul, one_mul, alg.oriy, norm_sub_rev (alg.x 1) xm]
           rw [add_comm (⟪alg.x 1 - alg.x 0, xm - alg.x 1⟫ * 2), mul_comm, ← norm_add_sq_real]
-          simp; rw [norm_sub_rev]; linarith [alg.tbound 0]
+          simp; rw [norm_sub_rev];
       rw [alg.initial]; apply div_pos; rw [sq_pos_iff]
       linarith [(alg.γbound k).1]; linarith [alg.tbound k]
 
@@ -329,9 +329,9 @@ instance {f h: E → ℝ} {f' : E → E} {x0 : E} [p : Nesterov_first_fix_stepsi
 
 variable {alg : Nesterov_first_fix_stepsize f h f' x0}
 
-variable {xm : E} (minφ : IsMinOn (f + h) univ xm)
+variable {xm : E}
 
-theorem Nesterov_first_fix_stepsize_converge:
+theorem Nesterov_first_fix_stepsize_converge (minφ : IsMinOn (f + h) univ xm):
     ∀ (k : ℕ), f (alg.x (k + 1)) + h (alg.x (k + 1)) - f xm - h xm ≤
     2 * alg.l / (k + 2) ^ 2 * ‖x0 - xm‖ ^ 2 := by
   intro k
diff --git a/Convex/Algorithm/NesterovAccelerationSecond.lean b/Convex/Algorithm/NesterovAccelerationSecond.lean
index 1506ffb..1b065ec 100644
--- a/Convex/Algorithm/NesterovAccelerationSecond.lean
+++ b/Convex/Algorithm/NesterovAccelerationSecond.lean
@@ -41,9 +41,9 @@ class Nesterov_second (f h : E → ℝ) (f' : E → E) (x0 : E) :=
 
 variable {alg : Nesterov_second f h f' x0}
 
-variable {xm : E} (minφ : IsMinOn (f + h) Set.univ xm)
+variable {xm : E}
 
-theorem Nesterov_second_convergence :
+theorem Nesterov_second_convergence (minφ : IsMinOn (f + h) Set.univ xm):
     ∀ (k : ℕ), f (alg.x (k + 1)) + h (alg.x (k + 1)) - f xm - h xm ≤
       (alg.γ (k + 1)) ^ 2 / (2 * alg.t (k + 1)) * ‖x0 - xm‖ ^ 2 := by
   let φ := fun z : E ↦ f z + h z
@@ -52,13 +52,13 @@ theorem Nesterov_second_convergence :
       ∈ (SubderivAt (alg.t k • h) (alg.y k)) := by
     intro k; obtain h1 := alg.update2 k
     rw [prox_iff_subderiv] at h1
-    have upd2 := @SubderivAt.pos_smul _ _ _ ((alg.t k / alg.γ k) • h) (alg.y k) (alg.γ k) (alg.γbound k).1
+    have upd2 := @SubderivAt.pos_smul _ _ _ _ ((alg.t k / alg.γ k) • h) (alg.y k) (alg.γ k) (alg.γbound k).1
     rw [← smul_assoc, smul_eq_mul, mul_div, mul_comm, ← mul_div, div_self, mul_one] at upd2
     rw [upd2]
     use (alg.y (↑k - 1) - (alg.t ↑k / alg.γ ↑k) • f' (alg.z k) - alg.y ↑k)
     constructor
-    . exact h1
-    . simp
+    · exact h1
+    · simp
       rw [sub_right_comm, smul_sub, ← smul_assoc, smul_eq_mul]
       rw [mul_div, mul_comm, ← mul_div, div_self, mul_one]
       linarith [(alg.γbound k).1]
@@ -81,16 +81,16 @@ theorem Nesterov_second_convergence :
     have mem1 : (alg.x (k - 1)) ∈ univ := by simp
     have mem2 : alg.y k ∈ univ := by simp
     by_cases eq1 : alg.γ k = 1
-    . simp [eq1]
+    · simp [eq1]
       obtain update3 := alg.update3 k
       simp [eq1] at update3
       rw [update3]
-    . push_neg at eq1
+    · push_neg at eq1
       have pos : 1 - alg.γ k > 0 := by
         apply lt_iff_le_and_ne.mpr
         constructor
-        . linarith [(alg.γbound k).2]
-        . contrapose eq1
+        · linarith [(alg.γbound k).2]
+        · contrapose eq1
           push_neg at *
           linarith [eq1]
       specialize fall mem1 mem2 pos ((alg.γbound k).1) (by linarith)
@@ -132,9 +132,9 @@ theorem Nesterov_second_convergence :
     apply le_trans (hieq4 k)
     simp only [add_le_add_iff_left]
     by_cases nm0 : ‖alg.x ↑k - alg.z k‖ ^ 2 = 0
-    . rw [nm0]
+    · rw [nm0]
       simp
-    . push_neg at nm0
+    · push_neg at nm0
       have ax : ‖alg.x ↑k - alg.z k‖ ^ 2 > 0 := by
         apply lt_of_le_of_ne
         simp
@@ -186,13 +186,13 @@ theorem Nesterov_second_convergence :
           + ((alg.γ k) ^ 2 / (2 * alg.t k)) * ‖alg.y k - alg.y (k - 1)‖ ^ 2 := by
         simp only [add_le_add_iff_right]
         by_cases eq1 : alg.γ k = 1
-        . simp [eq1]
-        . push_neg at eq1
+        · simp [eq1]
+        · push_neg at eq1
           have pos : 1 - alg.γ k > 0 := by
             apply lt_iff_le_and_ne.mpr
             constructor
-            . linarith [(alg.γbound k).2]
-            . contrapose eq1
+            · linarith [(alg.γbound k).2]
+            · contrapose eq1
               push_neg at *
               linarith [eq1]
           apply (mul_le_mul_left pos).mpr
@@ -228,7 +228,7 @@ theorem Nesterov_second_convergence :
           + alg.γ ↑k * (f (alg.z k) + ⟪f' (alg.z k), alg.y ↑k - alg.z k⟫_ℝ)
           + alg.γ ↑k ^ 2 / (2 * alg.t ↑k) * ‖alg.y ↑k - alg.y (↑k - 1)‖ ^ 2 := by
         simp
-        have gpos : alg.γ k > 0 := by exact (alg.γbound k).1
+        have gpos : alg.γ k > 0 := (alg.γbound k).1
         apply (mul_le_mul_left gpos).mpr
         apply Convex_first_order_condition' (alg.h₁ (alg.z k)) alg.convf
         simp
@@ -315,7 +315,7 @@ theorem Nesterov_second_convergence :
       + 1 / 2 * ‖alg.y (k + 1) - xm‖ ^ 2 ≤
       alg.t 1 / (alg.γ 1 ^ 2) * (φ (alg.x 1) - φ xm) + 1 / 2 * ‖alg.y 1 - xm‖ ^ 2 := by
     induction' k with k ik
-    . simp
+    · simp
     have ine := decrease (Nat.toPNat' (k + 1))
     simp only [Nat.toPNat'_coe, add_pos_iff, zero_lt_one, or_true, ↓reduceIte] at ine
     apply le_trans ine
@@ -422,9 +422,9 @@ instance {f h : E → ℝ} {f' : E → E} {x0 : E} [p : Nesterov_second_fix_step
 
 variable {alg : Nesterov_second_fix_stepsize f h f' x0}
 
-variable {xm : E} (minφ : IsMinOn (f + h) univ xm)
+variable {xm : E}
 
-theorem Nesterov_second_fix_stepsize_converge:
+theorem Nesterov_second_fix_stepsize_converge (minφ : IsMinOn (f + h) univ xm):
     ∀ (k : ℕ), f (alg.x (k + 1)) + h (alg.x (k + 1)) - f xm - h xm ≤
     2 * alg.l / (k + 2) ^ 2 * ‖x0 - xm‖ ^ 2 := by
   intro k
@@ -442,7 +442,7 @@ theorem Nesterov_second_fix_stepsize_converge:
         ‖x0 - xm‖ ^ 2 =
         Nesterov_second.γ f h f' x0 (k + 1) ^ 2 / (2 * Nesterov_second.t f h f' x0 (k + 1)) *
         ‖x0 - xm‖ ^ 2 := rfl
-      rw [h1, h2]; apply Nesterov_second_convergence minφ
+      rw [h1, h2]; apply Nesterov_second_convergence minφ _
     _ ≤ 2 * alg.l / (k + 2) ^ 2 * ‖x0 - xm‖ ^ 2 := by
       apply mul_le_mul_of_nonneg_right _ (sq_nonneg _)
       rw [alg.γeq (k + 1), alg.teq (k + 1)]; field_simp
diff --git a/Convex/Algorithm/NesterovSmooth.lean b/Convex/Algorithm/NesterovSmooth.lean
index a803cf3..604e201 100644
--- a/Convex/Algorithm/NesterovSmooth.lean
+++ b/Convex/Algorithm/NesterovSmooth.lean
@@ -131,7 +131,7 @@ lemma one_iter (hfun : ConvexOn ℝ Set.univ f) (hg : ∀ (k : ℕ+), γ k = 2 /
         _ = alg.l / 2 * (‖alg.y k - (1 - γ k) • (alg.x (k - 1)) - γ k • xm‖ ^ 2 -
                 ‖alg.x k - (1 - γ k) • alg.x (k - 1) - γ k • xm‖ ^ 2) := by
             rw [smul_add, smul_smul]; simp
-            left; rw [mul_inv_cancel (by linarith), one_smul, sub_smul, one_smul, add_comm, sub_add]
+            left; rw [mul_inv_cancel₀ (ne_of_gt hzs), one_smul, sub_smul, one_smul, add_comm, sub_add]
   have this2 : alg.l / 2 * (‖alg.y k - (1 - γ k) • (alg.x (k - 1)) - γ k • xm‖ ^ 2 -
       ‖alg.x k - (1 - γ k) • alg.x (k - 1) - γ k • xm‖ ^ 2) = alg.l *
       (inner (alg.x k - alg.y k) ((1 - γ k) • (alg.x (k - 1)) + ((γ k) • xm)- alg.x k))
@@ -199,7 +199,7 @@ theorem nesterov_algorithm_smooth (hfun: ConvexOn ℝ Set.univ f)
     · specialize IH j (le_refl _)
       specialize h5 (j + 1)
       have y1: ↑(j + 1) - (1 : ℕ) = j := by simp
-      have y2: j + 1 - 1 = j := by exact Iff.mp PNat.natPred_inj rfl
+      have y2: j + 1 - 1 = j := Iff.mp PNat.natPred_inj rfl
       apply le_trans h5 _
       rw [y1, y2]
       exact IH
diff --git a/Convex/Algorithm/ProximalGradient.lean b/Convex/Algorithm/ProximalGradient.lean
index 6ea846e..c017c59 100644
--- a/Convex/Algorithm/ProximalGradient.lean
+++ b/Convex/Algorithm/ProximalGradient.lean
@@ -44,19 +44,19 @@ theorem proximal_gradient_method_converge : ∀ (k : ℕ+),
   have th : ContinuousOn (alg.t • h) univ := by
     apply ContinuousOn.const_smul alg.h₃ alg.t
   have th' : ConvexOn ℝ univ (alg.t • h) := by
-    apply ConvexOn.smul; linarith [alg.tpos]; apply alg.hconv
+    apply ConvexOn.smul; apply le_of_lt; exact alg.tpos; apply alg.hconv
   let Gt := fun x ↦ (1 / alg.t) • (x - prox_point_c'  (alg.t • h)  (x - alg.t • f' x) th th')
   let φ := fun x ↦ f x + h x
   have hG : ∀ z : E, Gt z - f' z ∈ (SubderivAt h (z - alg.t • Gt z)) := by
     intro z
     have eq1 : z - alg.t • Gt z = prox_point_c' (alg.t • h) (z - alg.t • f' z) th th' := by
-      simp [Gt]; rw [smul_inv_smul₀, ← sub_add]; simp; linarith [alg.tpos]
+      simp [Gt]; rw [smul_inv_smul₀ (ne_of_gt alg.tpos), ← sub_add, sub_self, zero_add]
     have eq2 : prox_prop (alg.t • h) (z - alg.t • f' z) (z - alg.t • Gt z) := by
       rw [prox_point_c'] at eq1; rw [eq1]; apply Classical.choose_spec
     rw [prox_iff_subderiv_smul, sub_sub_sub_comm, sub_sub_eq_add_sub] at eq2;
     rw [sub_self, zero_add, ← smul_sub, ← smul_assoc, smul_eq_mul] at eq2;
-    rw [one_div_mul_cancel, one_smul] at eq2
-    exact eq2; linarith [alg.tpos]; exact alg.hconv; linarith [alg.tpos]
+    rw [one_div_mul_cancel (ne_of_gt alg.tpos), one_smul] at eq2
+    exact eq2; exact alg.hconv; exact alg.tpos
   have fieq1 : ∀ x : E, f (x - alg.t • Gt x) ≤
       f x - alg.t * inner (f' x) (Gt x) + alg.t ^ 2 * alg.L / 2 * ‖Gt x‖ ^ 2 := by
     intro x
@@ -66,7 +66,7 @@ theorem proximal_gradient_method_converge : ∀ (k : ℕ+),
     have eq3 : y - x = - alg.t • Gt x := by simp [Gt, y]
     rw [eq3] at ieq1; rw [inner_smul_right, norm_smul, mul_pow] at ieq1
     rw [← mul_assoc, mul_comm ] at ieq1
-    simp at ieq1; rw [← sub_eq_add_neg] at ieq1; simp; linarith [alg.tpos]
+    simp at ieq1; rw [← sub_eq_add_neg] at ieq1; linarith [alg.tpos]
   have fieq2 : ∀ x : E,
       f (x - alg.t • Gt x) ≤ f x - alg.t * inner (f' x) (Gt x) + alg.t / 2 * ‖Gt x‖ ^ 2 := by
     intro x
@@ -129,15 +129,14 @@ theorem proximal_gradient_method_converge : ∀ (k : ℕ+),
           rw [norm_sub_sq_real]; field_simp; ring_nf
           rw [inner_smul_right, real_inner_comm];
           nth_rw 2 [mul_comm _ (alg.t)⁻¹]; rw [norm_smul, mul_pow, pow_two ‖alg.t‖]
-          simp; rw [mul_comm _ ⟪q, p⟫_ℝ, mul_assoc _ alg.t, mul_inv_cancel, ← mul_assoc]
-          rw [← mul_assoc, inv_mul_cancel]; simp
-          repeat linarith [alg.tpos]
+          simp; rw [mul_comm _ ⟪q, p⟫_ℝ, mul_assoc _ alg.t, mul_inv_cancel₀ (ne_of_gt alg.tpos), ← mul_assoc]
+          rw [← mul_assoc, inv_mul_cancel₀ (ne_of_gt alg.tpos), mul_one, one_mul]
         rw [sub_right_comm]; apply aux
   have iter : ∀ i : ℕ, alg.x (i + 1) = alg.x i - alg.t • Gt (alg.x i) := by
     intro i
     apply prox_unique_of_convex
     apply th'; apply alg.update i; simp [Gt]; rw [smul_inv_smul₀, ← sub_add]; simp
-    rw [prox_point_c']; apply Classical.choose_spec; linarith [alg.tpos]
+    rw [prox_point_c']; apply Classical.choose_spec; exact ne_of_gt alg.tpos;
   have φdecrease : ∀ i : ℕ, φ (alg.x (i + 1)) ≤ φ (alg.x i) := by
     intro i
     specialize φieq1 (alg.x i)
@@ -200,6 +199,6 @@ theorem proximal_gradient_method_converge : ∀ (k : ℕ+),
     _ = ‖(alg.x 0) - alg.xm‖ ^ 2 - ‖(alg.x k) - alg.xm‖ ^ 2 := by
       rw [← mul_sub, ← mul_assoc, mul_one_div_cancel]; simp; linarith [alg.tpos]
     _ ≤ ‖x₀ - alg.xm‖ ^ 2 := by rw [alg.ori]; simp
-  field_simp; linarith [alg.tpos]
+  field_simp; exact alg.tpos
 
 end method
diff --git a/Convex/Algorithm/SubgradientMethod.lean b/Convex/Algorithm/SubgradientMethod.lean
index 790ec1a..919fa1c 100644
--- a/Convex/Algorithm/SubgradientMethod.lean
+++ b/Convex/Algorithm/SubgradientMethod.lean
@@ -29,10 +29,10 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteS
 
 variable {S :Set E} {f : E → ℝ} {g : E} {x : E}
 
-variable {G : NNReal} (hf : ConvexOn ℝ univ f) (hc : ContinuousOn f univ)
+variable {G : NNReal}
 
 theorem bounded_subgradient_to_Lipschitz
-    (h : ∀ ⦃x : E⦄ , ∀ ⦃g⦄ , g ∈ SubderivAt f x → ‖g‖ ≤ G) :
+    (h : ∀ ⦃x : E⦄ , ∀ ⦃g⦄ , g ∈ SubderivAt f x → ‖g‖ ≤ G) (hf : ConvexOn ℝ univ f) (hc : ContinuousOn f univ) :
     LipschitzWith G f := by
   intro x y
   have hx₂' : Nonempty (SubderivAt f x) := SubderivAt.nonempty hf hc x
@@ -118,9 +118,9 @@ theorem Lipschitz_to_bounded_subgradient (h : LipschitzWith G f ) :
   linarith
 
 /- Subgradient of `f` is bounded if and only if `f` is Lipschitz -/
-theorem bounded_subgradient_iff_Lipschitz :
-    (∀ ⦃x : E⦄ , ∀ ⦃g⦄ , g ∈ SubderivAt f x → ‖g‖ ≤ G)  ↔ LipschitzWith G f :=
-  ⟨bounded_subgradient_to_Lipschitz hf hc, Lipschitz_to_bounded_subgradient⟩
+theorem bounded_subgradient_iff_Lipschitz (hf : ConvexOn ℝ univ f) (hc : ContinuousOn f Set.univ) :
+    (∀ ⦃x : E⦄ , ∀ ⦃g⦄ , g ∈ SubderivAt f x → ‖g‖ ≤ G) ↔ LipschitzWith G f :=
+    ⟨fun h ↦ bounded_subgradient_to_Lipschitz h hf hc, Lipschitz_to_bounded_subgradient⟩
 
 end
 
@@ -142,7 +142,7 @@ class subgradient_method (f : E → ℝ) (x₀ : E) :=
   (update : ∀ k, (x (k + 1)) = x k - a k • (g k))
   (hg : ∀ n, g n ∈ SubderivAt f (x n))
 
-variable (xm x₀ : E) (hm : IsMinOn f univ xm) {alg : subgradient_method f x₀}
+variable (xm x₀ : E) {alg : subgradient_method f x₀}
 
 /- Convergence of general subgradient method -/
 theorem subgradient_method_converge:
@@ -257,7 +257,7 @@ theorem subgradient_method_fix_step_size {t : ℝ}
 
 /-- convergence with fixed $‖x^{i+1}-x^{i}‖$ --/
 theorem subgradient_method_fixed_distance {s : ℝ}
-   (ha' : ∀ (n : ℕ), alg.a n * ‖alg.g n‖ = s) (hs : s > 0):
+   (ha' : ∀ (n : ℕ), alg.a n * ‖alg.g n‖ = s) (hs : s > 0) (hm : IsMinOn f univ xm):
     ∀ (k : ℕ) ,(sInf {x | ∃ i ∈ Finset.range (k + 1), f (alg.x i) = x}) - (f xm)
       ≤ alg.G * ‖x₀ - xm‖ ^ 2 / (2 * (k + 1) * s) + alg.G * s / 2 := by
   intro k
@@ -374,7 +374,8 @@ theorem subgradient_method_fixed_distance {s : ℝ}
 /-- convergence with diminishing step size --/
 theorem subgradient_method_diminishing_step_size
     (ha' : Tendsto alg.a atTop (𝓝 0))
-    (ha'' : Tendsto (fun (k : ℕ) => (Finset.range (k + 1)).sum alg.a) atTop atTop) :
+    (ha'' : Tendsto (fun (k : ℕ) => (Finset.range (k + 1)).sum alg.a) atTop atTop)
+    (hm : IsMinOn f univ xm) :
     Tendsto (fun k => sInf {f (alg.x i) | i ∈ Finset.range (k + 1)}) atTop (𝓝 (f xm)) := by
   have h₁ : Tendsto (fun k => sInf {f (alg.x i) | i ∈ Finset.range (k + 1)} - f xm)
       atTop (𝓝 0) := by
diff --git a/Convex/Analysis/GradientDiv.lean b/Convex/Analysis/GradientDiv.lean
index fe92dd4..76d1ce1 100644
--- a/Convex/Analysis/GradientDiv.lean
+++ b/Convex/Analysis/GradientDiv.lean
@@ -151,7 +151,7 @@ theorem HasGradientAt.one_div (hf : HasGradientAt f grad x)(h₁: ¬ f x = (0 :
     apply mul_pos
     linarith
     have h' : (0 : ℝ)  < 1 := by linarith
-    have h'' : 0 ≤ ‖grad‖ := by exact norm_nonneg (grad)
+    have h'' : 0 ≤ ‖grad‖ := norm_nonneg (grad)
     exact add_pos_of_nonneg_of_pos h'' h'
   have h₃ : ∃ δ₃ > (0 : ℝ), ∀ (x' : E),
       ‖x - x'‖ ≤ δ₃ → ‖f x' - f x‖ ≤ ε * ‖f x‖ * ‖f x‖ * ‖f x‖ /(4 * (‖grad‖ + 1 )) := by
@@ -167,10 +167,10 @@ theorem HasGradientAt.one_div (hf : HasGradientAt f grad x)(h₁: ¬ f x = (0 :
     exact lt_min δ₀pos δ₃pos
     intro x' h'
     have hp₁ : ‖x - x'‖ ≤ δ₀ := by
-      have h₂ : min δ₀ δ₃ ≤ δ₀ := by exact min_le_left δ₀ δ₃
+      have h₂ : min δ₀ δ₃ ≤ δ₀ := min_le_left δ₀ δ₃
       apply le_trans h' h₂
     have hp₂ : ‖x - x'‖ ≤ δ₃ := by
-      have h₂ : min δ₀ δ₃ ≤ δ₃ := by exact min_le_right δ₀ δ₃
+      have h₂ : min δ₀ δ₃ ≤ δ₃ := min_le_right δ₀ δ₃
       apply le_trans h' h₂
     have l0 : 0 < ‖f x'‖ := by
       have h' : ‖f x‖/2 ≤ ‖f x'‖ := hδ₀ x' hp₁
@@ -191,7 +191,7 @@ theorem HasGradientAt.one_div (hf : HasGradientAt f grad x)(h₁: ¬ f x = (0 :
       have h' : ‖f x' - f x‖ * ‖grad‖ * ‖x' - x‖ = ‖f x' - f x‖ * (‖grad‖ * ‖x' - x‖) := by
         apply mul_assoc
       rw [h']
-      have h'' : 0 ≤ ‖f x' - f x‖ := by apply norm_nonneg (f x' - f x)
+      have h'' : 0 ≤ ‖f x' - f x‖ := norm_nonneg (f x' - f x)
       have h''' : ‖⟪grad, (x' - x)⟫‖ ≤ ‖grad‖ * ‖x' - x‖ := by
         exact norm_inner_le_norm grad (x' - x)
       exact mul_le_mul_of_nonneg_left h''' h''
@@ -245,10 +245,10 @@ theorem HasGradientAt.one_div (hf : HasGradientAt f grad x)(h₁: ¬ f x = (0 :
     exact lt_min δ₀pos δ₂pos
     intro x' h'
     have hp₁ : ‖x - x'‖ ≤ δ₀ := by
-      have h₂ : min δ₀ δ₂ ≤ δ₀ := by exact min_le_left δ₀ δ₂
+      have h₂ : min δ₀ δ₂ ≤ δ₀ := min_le_left δ₀ δ₂
       apply le_trans h' h₂
     have hp₂ : ‖x - x'‖ ≤ δ₂ := by
-      have h₂ : min δ₀ δ₂ ≤ δ₂ := by exact min_le_right δ₀ δ₂
+      have h₂ : min δ₀ δ₂ ≤ δ₂ := min_le_right δ₀ δ₂
       apply le_trans h' h₂
 
     have zp1 :‖f x * (f x - f x' + inner grad (x' - x)) / (f x * f x * f x')‖ =
@@ -339,14 +339,14 @@ theorem HasGradientAt.one_div (hf : HasGradientAt f grad x)(h₁: ¬ f x = (0 :
   have hp₁ : ‖x - x'‖ ≤ δ₄ := by
     have h₀ : min δ₀ (min δ₄ δ₅) ≤ (min δ₄ δ₅) := by
       exact min_le_right δ₀ (min δ₄ δ₅)
-    have h₂ : min δ₄ δ₅ ≤ δ₄ := by exact min_le_left δ₄ δ₅
+    have h₂ : min δ₄ δ₅ ≤ δ₄ := min_le_left δ₄ δ₅
     have h₃ : ‖x - x'‖ ≤ (min δ₄ δ₅) := by
       apply le_trans h' h₀
     apply le_trans h₃ h₂
   have hp₂ : ‖x - x'‖ ≤ δ₅ := by
     have h₀ : min δ₀ (min δ₄ δ₅) ≤ (min δ₄ δ₅) := by
       exact min_le_right δ₀ (min δ₄ δ₅)
-    have h₂ : min δ₄ δ₅ ≤ δ₅ := by exact min_le_right δ₄ δ₅
+    have h₂ : min δ₄ δ₅ ≤ δ₅ := min_le_right δ₄ δ₅
     have h₃ : ‖x - x'‖ ≤ (min δ₄ δ₅) := by
       apply le_trans h' h₀
     apply le_trans h₃ h₂
@@ -421,7 +421,7 @@ theorem HasGradientAt.one_div (hf : HasGradientAt f grad x)(h₁: ¬ f x = (0 :
         apply norm_add_le ((f x) * (f x - f x' + inner grad (x' - x))/
       (f x * f x * f x')) ((f x' * inner grad (x' - x) - f x * inner grad (x' - x))/
       (f x * f x * f x'))
-      _ ≤ (ε/2) * ‖x' - x‖ + (ε/2) * ‖x' - x‖ := by exact add_le_add (hδ₅ x' hp₂) (hδ₄ x' hp₁)
+      _ ≤ (ε/2) * ‖x' - x‖ + (ε/2) * ‖x' - x‖ := add_le_add (hδ₅ x' hp₂) (hδ₄ x' hp₁)
       _ = ε * ‖x' - x‖ := by linarith
   have j₁ : ‖1 / f x' - 1 / f x - (- (⟪grad, (x' - x)⟫))/((f x) * (f x))‖ = ‖1 / f x' - 1 / f x -
       inner ((-(1 / f x ^ ↑2) • grad)) (x' - x)‖ := by
diff --git a/Convex/Analysis/Lemmas.lean b/Convex/Analysis/Lemmas.lean
index 4c1a92e..a759a95 100644
--- a/Convex/Analysis/Lemmas.lean
+++ b/Convex/Analysis/Lemmas.lean
@@ -210,8 +210,8 @@ lemma gradient_norm_sq_eq_two_self (x : E) :
   intro e ep
   use e
   constructor
-  . linarith
-  . intro x' dles
+  · linarith
+  · intro x' dles
     rw [← norm_neg (x - x'), neg_sub] at dles
     rw [← real_inner_self_eq_norm_sq, ← real_inner_self_eq_norm_sq, inner_sub_right]
     rw [real_inner_smul_left, real_inner_smul_left]; ring_nf
@@ -280,8 +280,8 @@ lemma sub_normsquare_gradient (hf : ∀ x ∈ s, HasGradientAt f (f' x) x) (m :
     ∀ x ∈ s, HasGradientAt (fun x ↦ f x - m / 2 * ‖x‖ ^ 2) (f' x - m • x) x := by
   intro x xs
   apply HasGradientAt.sub
-  . apply hf x xs
-  . have u := HasGradientAt.const_smul (gradient_norm_sq_eq_two_self x) (m / 2)
+  · apply hf x xs
+  · have u := HasGradientAt.const_smul (gradient_norm_sq_eq_two_self x) (m / 2)
     simp at u
     rw [smul_smul, div_mul_cancel_of_invertible] at u
     apply u
diff --git a/Convex/Function/BanachSubgradient.lean b/Convex/Function/BanachSubgradient.lean
index 07416cd..af85082 100644
--- a/Convex/Function/BanachSubgradient.lean
+++ b/Convex/Function/BanachSubgradient.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Wanyi He. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Wanyi He, Chenyi Li, Zichen Wang
 -/
-import Mathlib.Analysis.NormedSpace.Dual
+import Mathlib.Analysis.Normed.Module.Dual
 import Mathlib.Analysis.NormedSpace.HahnBanach.Separation
 import Mathlib.LinearAlgebra.Dual
 
@@ -32,8 +32,6 @@ def Banach_SubderivWithinAt (f : E → ℝ) (s : Set E) (x : E) : Set (E →L[
 def Epi (f : E → ℝ) (s : Set E) : Set (E × ℝ) :=
   {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2}
 
-variable (hf : ConvexOn ℝ s f)
-
 lemma EpigraphInterior_existence (hc : ContinuousOn f (interior s)) (hx : x ∈ interior s) :
     ∀ t > f x, (x, t) ∈ interior {p : E × ℝ| p.1 ∈ s ∧ f p.1 ≤ p.2} := by
   intro _ _
@@ -70,7 +68,7 @@ lemma mem_epi_frontier : ∀ y ∈ interior s, (y, f y) ∈
   obtain ⟨_, h2⟩ := st this
   simp at h2; linarith
 
-theorem Banach_SubderivWithinAt.Nonempty (hc : ContinuousOn f (interior s)) (hx : x ∈ interior s) :
+theorem Banach_SubderivWithinAt.Nonempty (hc : ContinuousOn f (interior s)) (hx : x ∈ interior s) (hf : ConvexOn ℝ s f) :
     Set.Nonempty (Banach_SubderivWithinAt f s x) := by
   have hepi_f₁ : Convex ℝ (interior (Epi f s)) := Convex.interior (ConvexOn.convex_epigraph hf)
   have disj : (x , f x) ∉ interior (Epi f s) := by
diff --git a/Convex/Function/ConvexFunction.lean b/Convex/Function/ConvexFunction.lean
index 2e43a7a..09b6114 100644
--- a/Convex/Function/ConvexFunction.lean
+++ b/Convex/Function/ConvexFunction.lean
@@ -412,7 +412,7 @@ theorem monotone_gradient_strict_convex (hs : Convex ℝ s)
     calc
       c * b < b := by rw [mul_lt_iff_lt_one_left]; apply cl1; linarith
       _ < b + d * a := by
-        have : 0 < d * a := by apply mul_pos dpos apos
+        have : 0 < d * a := mul_pos dpos apos
         linarith
   have neq0 : inner (f' u - f' v) (u - v) > (0 : ℝ) := by
     have uin : u ∈ s := by
@@ -437,7 +437,7 @@ theorem strict_convex_monotone_gradient (hf : ∀ x ∈ s, HasGradientAt f (f' x
     (h₁ : StrictConvexOn ℝ s f ) :
     ∀ x ∈ s, ∀ y ∈ s, x ≠ y → inner (f' x - f' y) (x - y) > (0 : ℝ) := by
   intro x xin y yin xney
-  have convf : ConvexOn ℝ s f := by apply StrictConvexOn.convexOn h₁
+  have convf : ConvexOn ℝ s f := StrictConvexOn.convexOn h₁
   rw [StrictConvexOn] at h₁
   rcases h₁ with ⟨hs, fsconv⟩
   have : inner (f' x - f' y) (x - y) ≥ (0 : ℝ) := by
diff --git a/Convex/Function/Lsmooth.lean b/Convex/Function/Lsmooth.lean
index 10c8719..b2355f1 100644
--- a/Convex/Function/Lsmooth.lean
+++ b/Convex/Function/Lsmooth.lean
@@ -55,18 +55,17 @@ theorem lipschitz_continuous_upper_bound
   let g' := fun t : ℝ ↦ (f' (x + t • (y - x)) (y - x))
   let LL := l * ‖y - x‖ ^ 2
   have H₁ : ∀ t₀ : ℝ , HasDerivAt g (g' t₀) t₀ := deriv_function_comp_segment x y h₁
-  have L₁ : LL = l * ‖y - x‖ ^ 2 := by exact rfl
+  have L₁ : LL = l * ‖y - x‖ ^ 2 := rfl
   have H₂ : ∀ u v : ℝ, ‖g' u - g' v‖  ≤ l * ‖y - x‖ ^ 2 * ‖u - v‖ := by
     intro u v
     specialize h₂ (x + u • (y - x)) (x + v • (y - x))
     have : x + u • (y - x) - (x + v • (y - x)) = (u - v) • (y - x) := by
       rw [← sub_sub, add_sub_right_comm, sub_self, zero_add, ← sub_smul]
-    calc ‖g' u - g' v‖ = ‖(f' (x + u • (y - x))) (y - x) - (f' (x + v • (y - x))) (y - x)‖ := rfl
-      _ = ‖(f' (x + u • (y - x)) - f' (x + v • (y - x))) (y - x)‖ := by congr
+    calc ‖g' u - g' v‖ = ‖(f' (x + u • (y - x)) - f' (x + v • (y - x))) (y - x)‖ := by congr
       _ ≤ ‖f' (x + u • (y - x)) - f' (x + v • (y - x))‖ * ‖y - x‖ :=
          ContinuousLinearMap.le_opNorm (f' (x + u • (y - x)) - f' (x + v • (y - x))) (y - x)
       _ ≤ l * ‖x + u • (y - x) - (x + v • (y - x))‖ * ‖y - x‖ :=
-         mul_le_mul_of_le_of_le h₂ (le_refl ‖y - x‖) (norm_nonneg _) (norm_nonneg _)
+         mul_le_mul_of_nonneg h₂ (le_refl ‖y - x‖) (norm_nonneg _) (norm_nonneg _)
       _ = l * ‖(u - v) • (y - x)‖ * ‖y - x‖  := by rw [this]
       _ = l * ‖y - x‖ ^ 2 * ‖u - v‖ := by rw [norm_smul]; ring_nf
   let upperf := fun t₀ : ℝ ↦ g 0 + t₀ * (g' 0) +  t₀ ^ 2 * (LL / 2)
@@ -77,8 +76,8 @@ theorem lipschitz_continuous_upper_bound
     rw [sub_zero] at H₂
     have abs_pos : LL * |t| = LL * t := congrArg (HMul.hMul LL) (abs_of_nonneg (by linarith))
     have HH₆ : g' t - g' 0 ≤ LL * t :=
-      calc  (g' t - g' 0) ≤ |g' t - g' 0| := by exact le_abs_self (g' t - g' 0)
-            _   ≤ l * ‖y - x‖ ^ 2 * |t| := by exact H₂
+      calc  (g' t - g' 0) ≤ |g' t - g' 0| := le_abs_self (g' t - g' 0)
+            _   ≤ l * ‖y - x‖ ^ 2 * |t| := H₂
             _   = LL * |t| := by simp
             _   = LL * t := abs_pos
     exact tsub_le_iff_left.mp HH₆
@@ -298,7 +297,7 @@ theorem convex_to_lower {l : ℝ} (h₁ : ∀ x : E, HasGradientAt f (f' x) x)
     simp only [] at t₁₁; rw [← sub_add (l / 2 * ‖z₁‖ ^ 2) _ _] at t₁₁
     calc
       _ ≤ l / 2 * ‖z₂‖ ^ 2 - (l / 2 * ‖z₁‖ ^ 2 - f z₁ +
-          inner (f' s) z₁ + inner (l • z₁ - fs' s z₁) (z₂ - z₁)) := by apply t₁₁
+          inner (f' s) z₁ + inner (l • z₁ - fs' s z₁) (z₂ - z₁)) := t₁₁
       _ = l / 2 * ‖z₂‖ ^ 2 -(l / 2 * ‖z₁‖ ^ 2 - f z₁ + inner (f' s) z₁ +
         (l * (inner z₁ z₂ - ‖z₁‖ ^ 2) - inner (f' z₁ - f' s) (z₂ - z₁))) := by
         rw [inner_sub_left, inner_smul_left]
@@ -323,7 +322,7 @@ theorem convex_to_lower {l : ℝ} (h₁ : ∀ x : E, HasGradientAt f (f' x) x)
     rcases hfx₂ x y (y - (1 / l) • fs' x y) with hfx₂'
     calc
       _ ≤ fs x y + inner (fs' x y) (y - (1 / l) • fs' x y - y)
-          + l / 2 * ‖y - (1 / l) • fs' x y - y‖ ^ 2 := by apply hfx₂'
+          + l / 2 * ‖y - (1 / l) • fs' x y - y‖ ^ 2 := hfx₂'
       _ = fs x y - 1 / (2 * l) * ‖fs' x y‖ ^ 2 := by
         have : y - (1 / l) • fs' x y - y = - (1 / l) • fs' x y := by simp
         rw [this, real_inner_smul_right]
@@ -339,7 +338,7 @@ theorem convex_to_lower {l : ℝ} (h₁ : ∀ x : E, HasGradientAt f (f' x) x)
     rcases hfx₂ y x (x - (1 / l) • fs' y x) with hfy₂'
     calc
       _ ≤ fs y x + inner (fs' y x) (x - (1 / l) • fs' y x - x)
-          + l / 2 * ‖x - (1 / l) • fs' y x - x‖ ^ 2 := by apply hfy₂'
+          + l / 2 * ‖x - (1 / l) • fs' y x - x‖ ^ 2 := hfy₂'
       _ = fs y x - 1 / (2 * l) * ‖fs' y x‖ ^ 2 := by
         have : x - (1 / l) • fs' y x - x = - (1 / l) • fs' y x := by simp
         rw [this, real_inner_smul_right]
@@ -388,7 +387,7 @@ theorem lipschitz_to_lower (h₁ : ∀ x, HasGradientAt f (f' x) x) (h₂ : Lips
     (hfun : ConvexOn ℝ Set.univ f) (hl : l > 0) :
     ∀ x y, inner (f' x - f' y) (x - y) ≥ 1 / l * ‖f' x - f' y‖ ^ 2 := by
   obtain convex : ConvexOn ℝ Set.univ (fun x ↦ l / 2 * ‖x‖ ^ 2 - f x) :=
-    lipschitz_to_lnorm_sub_convex convex_univ (fun x _ => h₁ x) (lipschitzOn_univ.mpr h₂) hl
+    lipschitz_to_lnorm_sub_convex convex_univ (fun x _ => h₁ x) (lipschitzOnWith_univ.mpr h₂) hl
   exact convex_to_lower h₁ convex hl hfun
 
 theorem lower_to_lipschitz (h₂ : ∀ x y, inner (f' x - f' y) (x - y) ≥ 1 / l * ‖f' x - f' y‖ ^ 2)
diff --git a/Convex/Function/MinimaClosedFunction.lean b/Convex/Function/MinimaClosedFunction.lean
index 9fdf4d1..b968db3 100644
--- a/Convex/Function/MinimaClosedFunction.lean
+++ b/Convex/Function/MinimaClosedFunction.lean
@@ -32,9 +32,6 @@ variable [FirstCountableTopology E] [FirstCountableTopology F]
 
 section
 
-/- Suppose `f` is LowerSemicontinuous -/
-variable (hf : LowerSemicontinuous f)
-
 private lemma l0 (y : F) (h : (f ⁻¹' Set.Iic y).Nonempty) :
     sInf {f x | x ∈ f ⁻¹' Set.Iic y} = sInf {f x | x : E}:= by
   have h₀ : {f x | x : E} = {f x | x ∈ f ⁻¹' Set.Iic y} ∪ {f x | x ∈ (f ⁻¹' Set.Iic y)ᶜ} := by
@@ -67,7 +64,7 @@ private lemma l0 (y : F) (h : (f ⁻¹' Set.Iic y).Nonempty) :
 /- If a premiage of `f` is nonempty and compact,
   then its minimum point set `{x | IsMinOn f univ x}` is nonempty -/
 theorem IsMinOn.of_isCompact_preimage {y : F}
-    (h1 : (f ⁻¹' Set.Iic y).Nonempty) (h2 : IsCompact (f ⁻¹' Set.Iic y)) :
+    (h1 : (f ⁻¹' Set.Iic y).Nonempty) (h2 : IsCompact (f ⁻¹' Set.Iic y)) (hf : LowerSemicontinuous f) :
     ∃ x, IsMinOn f univ x := by
   have hs : Set.Nonempty {f x | x ∈ (f ⁻¹' Set.Iic y)} := by
     rcases h1 with ⟨x, xsub⟩
@@ -95,9 +92,9 @@ variable [PseudoMetricSpace E] [ProperSpace E]
   then its minimum point set `{x | IsMinOn f univ x}` is compact -/
 
 theorem IsCompact_isMinOn_of_isCompact_preimage {y : F}
-    (h1 : (f ⁻¹' Set.Iic y).Nonempty) (h2 : IsCompact (f ⁻¹' Set.Iic y)) :
+    (h1 : (f ⁻¹' Set.Iic y).Nonempty) (h2 : IsCompact (f ⁻¹' Set.Iic y)) (hf : LowerSemicontinuous f) :
     IsCompact {x | IsMinOn f univ x} := by
-  obtain ⟨x', hx'⟩ := IsMinOn.of_isCompact_preimage hf h1 h2
+  obtain ⟨x', hx'⟩ := IsMinOn.of_isCompact_preimage h1 h2 hf
   have seq : {x | IsMinOn f univ x} = (f ⁻¹' Set.Iic (f x')) :=
       Set.ext fun xx =>
         { mp := fun hxx => isMinOn_iff.mp hxx x' trivial,
@@ -123,10 +120,8 @@ def strong_quasi : Prop :=
   ∀ ⦃x⦄, ∀ ⦃y⦄, x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1
     → f ((a • x : E) + (b • y : E)) < max (f x) (f y)
 
-variable ( hf' : @strong_quasi E F _ _ f 𝕜 _ _)
-
 /- the Minimum of strongly quasi function is unique -/
-theorem isMinOn_unique {x y : E} (hx : IsMinOn f univ x) (hy : IsMinOn f univ y) : x = y := by
+theorem isMinOn_unique {x y : E} (hx : IsMinOn f univ x) (hy : IsMinOn f univ y) (hf' : @strong_quasi E F _ _ f 𝕜 _ _) : x = y := by
   by_contra neq
   have : (0 : 𝕜) < (1 : 𝕜) := one_pos
   obtain ⟨a, lta, alt⟩ := exists_between this
diff --git a/Convex/Function/Proximal.lean b/Convex/Function/Proximal.lean
index 9a8269d..b7e4d54 100644
--- a/Convex/Function/Proximal.lean
+++ b/Convex/Function/Proximal.lean
@@ -497,7 +497,7 @@ lemma convex_of_norm_sq {s : Set E} (x : E) (conv: Convex ℝ s) :
         · rw [mul_le_mul_left]
           apply two_mul_le_add_pow_two
           linarith
-        · have ieq2 : 0 ≤ a * b := by apply mul_nonneg anneg bnneg
+        · have ieq2 : 0 ≤ a * b := mul_nonneg anneg bnneg
           have ieq3 : 0 = a * b := by linarith
           rw [← ieq3]; simp
       _ = b * ‖v‖ ^ 2 * a + b * a * ‖u‖ ^ 2 := by ring
@@ -526,7 +526,7 @@ theorem prox_iff_subderiv (f : E → ℝ) (hfun : ConvexOn ℝ univ f) :
     ∀ u : E, prox_prop f x u ↔ x - u ∈ SubderivAt f u := by
   intro u; rw [prox_prop, ← HasSubgradientAt_zero_iff_isMinOn, mem_SubderivAt]
   let g := fun u ↦ ‖u - x‖ ^ 2 / 2
-  have hg : ConvexOn ℝ Set.univ g := by apply convex_of_norm_sq x (convex_univ)
+  have hg : ConvexOn ℝ Set.univ g := convex_of_norm_sq x (convex_univ)
   have hcg : ContinuousOn g univ := by
     simp [g]; apply ContinuousOn.div
     apply ContinuousOn.pow _
@@ -582,8 +582,7 @@ theorem prox_iff_grad_smul (f : E → ℝ) {f' : E → E} (t : ℝ) (hfun : Conv
   intro u
   let g := fun u ↦ (t • f) u
   let g' := fun u ↦ t • f' u
-  have gconv : ConvexOn ℝ univ g := by
-    apply ConvexOn.smul tnonneg hfun
+  have gconv : ConvexOn ℝ univ g := ConvexOn.smul tnonneg hfun
   have gderiv : ∀ x, HasGradientAt g (g' x) x := by
     intro x
     simp only [Pi.smul_apply, g, g']
@@ -604,9 +603,8 @@ theorem prox_iff_subderiv_smul (f : E → ℝ) {t : ℝ} (hfun : ConvexOn ℝ un
     ∀ u : E, prox_prop (t • f) x u ↔ (1 / t) • (x - u) ∈ (SubderivAt f u) := by
   intro u
   let g := fun u ↦ (t • f) u
-  have tnonneg : 0 ≤ t := by linarith
   have gconv : ConvexOn ℝ univ g := by
-    apply ConvexOn.smul tnonneg hfun
+    apply ConvexOn.smul (le_of_lt ht) hfun
   rw [prox_iff_subderiv, ← mem_SubderivAt, ← mem_SubderivAt]
   rw [HasSubgradientAt, HasSubgradientAt]
   constructor
@@ -617,9 +615,9 @@ theorem prox_iff_subderiv_smul (f : E → ℝ) {t : ℝ} (hfun : ConvexOn ℝ un
     exact cond
   · intro cond y
     specialize cond y; rw [inner_smul_left] at cond; field_simp at cond
-    simp
+    rw [Pi.smul_apply, smul_eq_mul, ge_iff_le]
     have hrect : 0 < t⁻¹ := by
-      simp; linarith
+      rw [inv_pos]; exact ht
     rw [← mul_le_mul_left hrect]; ring_nf; field_simp
     exact cond
   exact gconv
@@ -636,7 +634,7 @@ theorem proximal_shift (a : E) {t : ℝ} (tnz : t ≠ 0) (f : E → ℝ):
   constructor
   · intro cond y
     specialize cond (t⁻¹ • (y - a))
-    rw [← smul_assoc, smul_eq_mul, mul_inv_cancel] at cond
+    rw [← smul_assoc, smul_eq_mul, mul_inv_cancel₀ tnz] at cond
     simp at cond
     calc
       t ^ 2 * f (t • z + a) + ‖t • z - t • x‖ ^ 2 / 2 =
@@ -647,59 +645,56 @@ theorem proximal_shift (a : E) {t : ℝ} (tnz : t ≠ 0) (f : E → ℝ):
       _ = t ^ 2 * f y + ‖t • ((1 / t) • (y - a) - x)‖ ^ 2 / 2 := by
         rw [mul_add, norm_smul, mul_pow]; field_simp
       _ = t ^ 2 * f y + ‖y - (t • x + a)‖ ^ 2 / 2 := by
-        rw [smul_sub, ← smul_assoc, smul_eq_mul, ← sub_sub, sub_right_comm]; field_simp
-    use tnz
+        rw [smul_sub, ← smul_assoc, smul_eq_mul, ← sub_sub, sub_right_comm];
+        field_simp
   · intro cond y
     specialize cond (t • y + a)
-    rw [← smul_sub, norm_smul, mul_pow] at cond; simp at cond
-    rw [← smul_sub, norm_smul, mul_pow] at cond; simp at cond
+    repeat rw [← smul_sub, norm_smul, mul_pow] at cond; simp at cond
     rw [mul_div_assoc, ← mul_add, mul_div_assoc, ← mul_add] at cond
     rw [mul_le_mul_left] at cond; use cond; rw [sq_pos_iff]; use tnz
 
 /-
   relation of proximal between a function and its scale
 -/
-theorem proximal_scale {t : ℝ} (tpos : 0 < t) (f : E → ℝ):
+theorem proximal_scale {t : ℝ} (tnz : t ≠ 0) (f : E → ℝ):
     ∀ z : E, prox_prop (fun x ↦ t • f (t⁻¹ • x)) x z ↔
       prox_prop (t⁻¹ • f) (t⁻¹ • x) (t⁻¹ • z) := by
   intro z
   rw [prox_prop, prox_prop, isMinOn_univ_iff, isMinOn_univ_iff]
   simp
+  have tsq : 0 < t ^ 2 := by rw [sq_pos_iff]; exact tnz;
   constructor
   · intro cond y
     specialize cond (t • y)
-    have tsq : 0 < t ^ 2 := by field_simp
     rw [← mul_le_mul_left tsq]
     calc
       t ^ 2 * (t⁻¹ * f (t⁻¹ • z) + ‖t⁻¹ • z - t⁻¹ • x‖ ^ 2 / 2) =
           t * f (t⁻¹ • z) + ‖z - x‖ ^ 2 / 2 := by
         rw [← smul_sub, norm_smul, mul_pow, mul_add, pow_two, ← mul_assoc, mul_assoc _ _ (t⁻¹)]
-        rw [mul_inv_cancel, mul_div_assoc, ← mul_assoc]; simp
-        rw [← pow_two, mul_inv_cancel]; repeat simp; repeat linarith
+        rw [mul_inv_cancel₀ tnz, mul_one, mul_div_assoc, ← mul_assoc]; simp
+        rw [← pow_two, mul_inv_cancel₀ (ne_of_gt tsq), one_mul];
       _ ≤ t * f (t⁻¹ • t • y) + ‖t • y - x‖ ^ 2 / 2 := cond
       _ = t ^ 2 * (t⁻¹ * f y) + ‖t • (y - t⁻¹ • x)‖ ^ 2 / 2 := by
-        rw [pow_two t, ← mul_assoc, mul_assoc _ _ (t⁻¹), mul_inv_cancel]
-        rw [← smul_assoc, smul_eq_mul, inv_mul_cancel]; simp
-        rw [smul_sub, ← smul_assoc, smul_eq_mul, mul_inv_cancel]; simp; repeat linarith
+        rw [pow_two t, ← mul_assoc, mul_inv_cancel_right₀ tnz]
+        rw [← smul_assoc, smul_eq_mul, inv_mul_cancel₀ tnz]; rw [one_smul, add_right_inj];
+        rw [smul_sub, ← smul_assoc, smul_eq_mul]; field_simp;
       _ = t ^ 2 * (t⁻¹ * f y + ‖y - t⁻¹ • x‖ ^ 2 / 2) := by
         rw [mul_add, norm_smul, mul_pow]; field_simp
   · intro cond y
     specialize cond (t⁻¹ • y)
-    have tsq : 0 < t ^ 2 := by field_simp
     rw [← mul_le_mul_left tsq] at cond
     calc
       t * f (t⁻¹ • z) + ‖z - x‖ ^ 2 / 2 =
           t ^ 2 * (t⁻¹ * f (t⁻¹ • z) + ‖t⁻¹ • z - t⁻¹ • x‖ ^ 2 / 2) := by
         rw [← smul_sub, norm_smul, mul_pow, mul_add, pow_two t, ← mul_assoc, mul_assoc _ _ (t⁻¹)]
-        rw [mul_inv_cancel, mul_div_assoc, ← mul_assoc]; simp
-        rw [← pow_two, mul_inv_cancel]; repeat simp; repeat linarith
+        rw [mul_inv_cancel₀ tnz]; ring_nf; field_simp
       _ ≤ t ^ 2 * (t⁻¹ * f (t⁻¹ • y) + ‖t⁻¹ • y - t⁻¹ • x‖ ^ 2 / 2) := cond
       _ = t ^ 2 * (t⁻¹ * f (t⁻¹ • y)) + ‖t • (t⁻¹ • y - t⁻¹ • x)‖ ^ 2 / 2 := by
         rw [mul_add, norm_smul, mul_pow]; field_simp
       _ = t * f (t⁻¹ • y) + ‖y - x‖ ^ 2 / 2 := by
-        rw [pow_two t, ← mul_assoc, mul_assoc _ _ (t⁻¹), mul_inv_cancel]
-        rw [smul_sub, ← smul_assoc, smul_eq_mul, mul_inv_cancel]; simp
-        rw [← smul_assoc, smul_eq_mul, mul_inv_cancel]; simp; repeat linarith
+        rw [pow_two t, ← mul_assoc, mul_assoc _ _ (t⁻¹), mul_inv_cancel₀ tnz]
+        rw [smul_sub, ← smul_assoc, smul_eq_mul, mul_inv_cancel₀ tnz, mul_one, one_smul, add_right_inj]
+        rw [← smul_assoc, smul_eq_mul, mul_inv_cancel₀ tnz, one_smul]
 
 /-
   change of proximal when added a linear components
diff --git a/Convex/Function/StronglyConvex.lean b/Convex/Function/StronglyConvex.lean
index 4517219..da95b12 100644
--- a/Convex/Function/StronglyConvex.lean
+++ b/Convex/Function/StronglyConvex.lean
@@ -15,7 +15,7 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteS
 
 section Strongly_Convex
 
-variable {s : Set E} {f : E → ℝ} {m : ℝ} {xm xm': E} {f' : E → E} {mp : m > 0}
+variable {s : Set E} {f : E → ℝ} {m : ℝ} {xm xm': E} {f' : E → E}
 
 open Set InnerProductSpace
 
@@ -47,13 +47,13 @@ theorem stronglyConvexOn_def (hs : Convex ℝ s)
   rw [← this]; exact hfun
 
 theorem Strongly_Convex_Unique_Minima (hsc: StrongConvexOn s m f)
-    (min: IsMinOn f s xm) (min' : IsMinOn f s xm') (hxm : xm ∈ s) (hxm' : xm' ∈ s): xm = xm' := by
+    (min: IsMinOn f s xm) (min' : IsMinOn f s xm') (hxm : xm ∈ s) (hxm' : xm' ∈ s) (mp : m > 0): xm = xm' := by
   by_contra neq
   push_neg at neq
   have eq : f xm = f xm' := by
     apply le_antisymm
-    . apply min hxm'
-    . apply min' hxm
+    · apply min hxm'
+    · apply min' hxm
   let x := (2 : ℝ)⁻¹ • xm + (2 : ℝ)⁻¹ • xm'
   have xeq : x = (2 : ℝ)⁻¹ • xm + (2 : ℝ)⁻¹ • xm' := by rfl
   rcases hsc with ⟨cr, sc⟩
@@ -67,19 +67,19 @@ theorem Strongly_Convex_Unique_Minima (hsc: StrongConvexOn s m f)
   specialize sc hxm hxm' this this (by norm_num)
   simp at sc
   rw [← xeq,← eq] at sc
-  rw [← two_mul,← mul_assoc, mul_inv_cancel (by norm_num), one_mul] at sc
+  rw [← two_mul,← mul_assoc, mul_inv_cancel₀ (by norm_num), one_mul] at sc
   have normp : ‖xm - xm'‖ > 0 := by
     apply norm_sub_pos_iff.mpr
     apply neq
   have nng : m / 2 * ‖xm - xm'‖ ^ 2 > 0 := by
     apply mul_pos
-    . linarith
-    . apply pow_pos; linarith
+    · linarith
+    · apply pow_pos; linarith
   apply absurd (min xs)
   simp [← xeq]
   calc
-    f x ≤ f xm - 2⁻¹ * 2⁻¹ * (m / 2 * ‖xm - xm'‖ ^ 2) := by apply sc
-    _ < f xm := by apply lt_of_sub_pos; simp; apply nng
+    f x ≤ f xm - 2⁻¹ * 2⁻¹ * (m / 2 * ‖xm - xm'‖ ^ 2) := sc
+    _ < f xm := by apply lt_of_sub_pos; simp; exact nng
 
 theorem Strong_Convex_lower (hsc : StrongConvexOn s m f) (hf : ∀ x ∈ s, HasGradientAt f (f' x) x) :
     ∀ x ∈ s, ∀ y ∈ s, inner (f' x - f' y) (x - y) ≥ m * ‖x - y‖ ^ 2 := by
diff --git a/Convex/Function/Subgradient.lean b/Convex/Function/Subgradient.lean
index a9d521e..a2f7140 100644
--- a/Convex/Function/Subgradient.lean
+++ b/Convex/Function/Subgradient.lean
@@ -165,9 +165,9 @@ variable (hf : ConvexOn ℝ s f) (hc : ContinuousOn f (interior s))
 open Bornology
 
 /- The subderiv of `f` at interior point `x` is a nonempty set -/
-theorem SubderivWithinAt.Nonempty : ∀ x ∈ interior s, (SubderivWithinAt f s x).Nonempty := by
+theorem SubderivWithinAt.Nonempty (hf : ConvexOn ℝ s f) (hc : ContinuousOn f (interior s)) : ∀ x ∈ interior s, (SubderivWithinAt f s x).Nonempty := by
   intro x hx
-  obtain h := Banach_SubderivWithinAt.Nonempty hf hc hx
+  obtain h := Banach_SubderivWithinAt.Nonempty hc hx hf
   unfold Set.Nonempty at h ⊢
   rcases h with ⟨g, hg⟩; unfold Banach_SubderivWithinAt at hg
   simp at hg
@@ -288,7 +288,7 @@ theorem SubderivWithinAt_eq_gradient {f'x : E} (hx : x ∈ interior s)
     have : dist (x + t • v) x < δ := by
       rw [dist_eq_norm, add_sub_cancel_left, norm_smul, ← (sub_zero t)]
       apply lt_of_lt_of_eq ((mul_lt_mul_right (norm_sub_pos_iff.mpr neq)).mpr ht)
-      rw [mul_assoc, inv_mul_cancel (norm_ne_zero_iff.mpr vneq), mul_one]
+      rw [mul_assoc, inv_mul_cancel₀ (norm_ne_zero_iff.mpr vneq), mul_one]
     specialize hδ this; rw [dist_eq_norm] at hδ
     have eq1 : ‖‖x + t • v - x‖⁻¹‖ = ‖t • v‖⁻¹ := by
       rw [add_sub_cancel_left, norm_inv, norm_norm]
@@ -316,7 +316,8 @@ theorem SubderivWithinAt_eq_gradient {f'x : E} (hx : x ∈ interior s)
     rw [mem_ball_iff_norm, add_sub_cancel_left, norm_smul]
     have : ‖t‖ * ‖v‖ < ε * ‖v‖⁻¹ * ‖v‖ := by
       apply (mul_lt_mul_right (norm_sub_pos_iff.mpr neq)).mpr tball
-    rwa [mul_assoc, inv_mul_cancel (norm_ne_zero_iff.mpr vneq), mul_one] at this
+    field_simp [norm_ne_zero_iff.mpr vneq] at this
+    exact this
   obtain ineq1 := hg' (x + t • v); rw [add_sub_cancel_left] at ineq1
   have eq1 : ‖v‖ = (⟪g', t • v⟫ - ⟪g, t • v⟫) * ‖t • v‖⁻¹ := by
     have eq2 : ‖v‖ = ⟪v, v⟫ * ‖v‖⁻¹ := by
@@ -518,7 +519,7 @@ theorem SubderivAt.add {f₁ f₂ : E → ℝ} (h₁ : ConvexOn ℝ univ f₁) (
     specialize hg (x + x₀); rw [← add_sub, sub_self, add_zero] at hg
     apply not_le_of_gt ?_ hg
     obtain ineq := add_lt_add_of_le_of_lt hp2 (neg_lt_neg hp1)
-    simp only [add_neg_self, neg_sub] at ineq
+    simp only [add_neg_cancel, neg_sub] at ineq
     have hh : ∀ x : E, (f₁ + f₂) x = f₁ x + f₂ x := fun x => rfl
     apply lt_of_sub_pos
     have eq : f₂ x₀ - f₂ (x + x₀) + (⟪g, x⟫_ℝ - (f₁ (x + x₀) - f₁ x₀)) =
@@ -576,9 +577,8 @@ theorem SubderivAt.add {f₁ f₂ : E → ℝ} (h₁ : ConvexOn ℝ univ f₁) (
     rw [eq] at htp; linarith
   have bleq0 : b < 0 := by
     rw [ceq0] at htp
-    specialize htp 1 (by linarith); rw [mul_one] at htp; linarith
+    specialize htp 1 (by linarith); linarith
   let hata := - (1 / b) • a
-
   have g1 : g + hata ∈ {g | HasSubgradientAt f₁ g x₀} := by
     rw [Set.mem_setOf]; unfold HasSubgradientAt; intro x
     simp [hata]
@@ -591,7 +591,7 @@ theorem SubderivAt.add {f₁ f₂ : E → ℝ} (h₁ : ConvexOn ℝ univ f₁) (
       rw [ceq0, hab (x - x₀, f₁ x - f₁ x₀ - ⟪g, x - x₀⟫_ℝ + t)] at hsl; simp at hsl
       obtain ineq := (mul_lt_mul_left_of_neg (inv_lt_zero.mpr bleq0)).mpr hsl
       simp at ineq
-      rw [mul_add, ← mul_assoc, inv_mul_cancel (ne_of_lt bleq0), one_mul] at ineq
+      rw [mul_add, ← mul_assoc, inv_mul_cancel₀ (ne_of_lt bleq0), one_mul] at ineq
       rw [← add_assoc, add_sub, add_sub] at ineq; exact ineq
     rw [inner_add_left, inner_neg_left, real_inner_smul_left]
     rw [← add_assoc]; simp
@@ -605,10 +605,10 @@ theorem SubderivAt.add {f₁ f₂ : E → ℝ} (h₁ : ConvexOn ℝ univ f₁) (
     rw [ceq0, hab (x - x₀, f₂ x₀ - f₂ x)] at hsr; simp at hsr
     obtain ineq := (mul_le_mul_left_of_neg (inv_lt_zero.mpr bleq0)).mpr hsr
     rw [mul_add, ← real_inner_smul_left, mul_zero, ← mul_assoc,
-        inv_mul_cancel (ne_of_lt bleq0), one_mul] at ineq
+        inv_mul_cancel₀ (ne_of_lt bleq0), one_mul] at ineq
     linarith
   use (g + hata); constructor; exact g1
-  use (- hata); constructor; exact g2; simp
+  use (-hata); constructor; exact g2; simp
 
 end computation
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 3417a6e..ac3a424 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dc4a6b1ac3cd502988e283d5c9c5fdf261125a07",
+   "rev": "ad26fe1ebccc9d5b7ca9111d5daf9b4488374415",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73",
+   "rev": "776a5a8f9c789395796e442d78a9d4cb9c4c9d03",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.39",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,41 +65,11 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f58ec1568bec05ff5045e4d697956089386f7c13",
+   "rev": "173d2e189fd79bd332fb19bffac0dce43ec8acb8",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
    "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "c74a052aebee847780e165611099854de050adf7",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4.git",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "d1be57c7fbd80ac20584ed0a86a2165c62cd993b",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "d1be57c7fbd80ac20584ed0a86a2165c62cd993b",
-   "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "convex",
  "lakeDir": ".lake"}
diff --git a/lean-toolchain b/lean-toolchain
index d69d1ed..e7a4f40 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc1
+leanprover/lean4:v4.11.0-rc2