solve conflicts

Author: CoolRmal

Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean

@@ -6,12 +6,10 @@ Authors: Bhavik Mehta, Yaël Dillies
 import Mathlib.Analysis.Convex.Cone.Extension
 import Mathlib.Analysis.Convex.Gauge
 import Mathlib.Analysis.Normed.Module.Convex
-import Mathlib.Analysis.NormedSpace.Extend
-import Mathlib.Topology.Algebra.Module.FiniteDimension
-import Mathlib.Topology.Instances.RealVectorSpace
 import Mathlib.Analysis.RCLike.Extend
 import Mathlib.Topology.Algebra.Module.FiniteDimension
 import Mathlib.Topology.Algebra.Module.LocallyConvex
+import Mathlib.Topology.Instances.RealVectorSpace
 
 /-!
 # Separation Hahn-Banach theorem
@@ -53,8 +51,7 @@ variable [IsTopologicalAddGroup E] [ContinuousSMul ℝ E]
 /-- Given a set `s` which is a convex neighbourhood of `0` and a point `x₀` outside of it, there is
 a continuous linear functional `f` separating `x₀` and `s`, in the sense that it sends `x₀` to 1 and
 all of `s` to values strictly below `1`. -/
-theorem separate_convex_open_set [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGroup E]
-    [Module ℝ E] [ContinuousSMul ℝ E] {s : Set E} (hs₀ : (0 : E) ∈ s) (hs₁ : Convex ℝ s)
+theorem separate_convex_open_set (hs₀ : (0 : E) ∈ s) (hs₁ : Convex ℝ s)
     (hs₂ : IsOpen s) {x₀ : E} (hx₀ : x₀ ∉ s) :
     ∃ f : StrongDual ℝ E, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1 := by
   let f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (ne_of_mem_of_not_mem hs₀ hx₀).symm

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean

@@ -271,7 +271,7 @@ theorem ConvexOn.iSup_affine_eq_of_separableSpace (hφ_cont : LowerSemicontinuou
             rw (config := {occs := .pos [1]}) [lem5 i]
             simp only [smul_eq_mul, ← ofReal_inv, ← ofReal_neg]
             rw [re_ofReal_mul, neg_mul, ← div_eq_inv_mul, ← neg_div]
-          _ = (- re (L i x) + c i) / re (T i 1) := by rw [div_add_div_same]
+          _ = (- re (L i x) + c i) / re (T i 1) := by rw [add_div]
           _ ≤ re (T i s) / re (T i 1) := by
             apply (div_le_div_iff_of_pos_right (lem4 i)).mpr; linarith
           _ = re s := by