refactor(analysis/convex/basic): rewrite a few proofs (#13658)

* prove that a closed segment is the union of the corresponding open segment and the endpoints;
* use this lemma to golf some proofs;
* make the "field" argument of `mem_open_segment_of_ne_left_right` implicit.
* use section variables.

src/analysis/convex/basic.lean

@@ -109,42 +109,42 @@ segment_symm 𝕜 y x ▸ left_mem_segment 𝕜 y x
 end mul_action_with_zero
 
 section module
-variables (𝕜) [module 𝕜 E]
+variables (𝕜) [module 𝕜 E] {x y z : E} {s : set E}
 
 @[simp] lemma segment_same (x : E) : [x -[𝕜] x] = {x} :=
 set.ext $ λ z, ⟨λ ⟨a, b, ha, hb, hab, hz⟩,
   by simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz,
   λ h, mem_singleton_iff.1 h ▸ left_mem_segment 𝕜 z z⟩
 
-lemma mem_open_segment_of_ne_left_right {x y z : E} (hx : x ≠ z) (hy : y ≠ z)
-  (hz : z ∈ [x -[𝕜] y]) :
-  z ∈ open_segment 𝕜 x y :=
+lemma insert_endpoints_open_segment (x y : E) :
+  insert x (insert y (open_segment 𝕜 x y)) = [x -[𝕜] y] :=
 begin
-  obtain ⟨a, b, ha, hb, hab, hz⟩ := hz,
-  by_cases ha' : a = 0,
-  { rw [ha', zero_add] at hab,
-    rw [ha', hab, zero_smul, one_smul, zero_add] at hz,
-    exact (hy hz).elim },
-  by_cases hb' : b = 0,
-  { rw [hb', add_zero] at hab,
-    rw [hb', hab, zero_smul, one_smul, add_zero] at hz,
-    exact (hx hz).elim },
-  exact ⟨a, b, ha.lt_of_ne (ne.symm ha'), hb.lt_of_ne (ne.symm hb'), hab, hz⟩,
+  simp only [subset_antisymm_iff, insert_subset, left_mem_segment, right_mem_segment,
+    open_segment_subset_segment, true_and],
+  rintro z ⟨a, b, ha, hb, hab, rfl⟩,
+  refine hb.eq_or_gt.imp _ (λ hb', ha.eq_or_gt.imp _ _),
+  { rintro rfl,
+    rw add_zero at hab,
+    rw [hab, one_smul, zero_smul, add_zero] },
+  { rintro rfl,
+    rw zero_add at hab,
+    rw [hab, one_smul, zero_smul, zero_add] },
+  { exact λ ha', ⟨a, b, ha', hb', hab, rfl⟩ }
 end
 
 variables {𝕜}
 
-lemma open_segment_subset_iff_segment_subset {x y : E} {s : set E} (hx : x ∈ s) (hy : y ∈ s) :
-  open_segment 𝕜 x y ⊆ s ↔ [x -[𝕜] y] ⊆ s :=
+lemma mem_open_segment_of_ne_left_right (hx : x ≠ z) (hy : y ≠ z) (hz : z ∈ [x -[𝕜] y]) :
+  z ∈ open_segment 𝕜 x y :=
 begin
-  refine ⟨λ h z hz, _, (open_segment_subset_segment 𝕜 x y).trans⟩,
-  obtain rfl | hxz := eq_or_ne x z,
-  { exact hx },
-  obtain rfl | hyz := eq_or_ne y z,
-  { exact hy },
-  exact h (mem_open_segment_of_ne_left_right 𝕜 hxz hyz hz),
+  rw [← insert_endpoints_open_segment] at hz,
+  exact ((hz.resolve_left hx.symm).resolve_left hy.symm)
 end
 
+lemma open_segment_subset_iff_segment_subset (hx : x ∈ s) (hy : y ∈ s) :
+  open_segment 𝕜 x y ⊆ s ↔ [x -[𝕜] y] ⊆ s :=
+by simp only [← insert_endpoints_open_segment, insert_subset, *, true_and]
+
 end module
 end ordered_semiring
 
@@ -299,10 +299,9 @@ section linear_ordered_field
 variables [linear_ordered_field 𝕜]
 
 section add_comm_group
-variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F]
+variables [add_comm_group E] [add_comm_group F] [module 𝕜 E] [module 𝕜 F] {x y z : E}
 
-lemma mem_segment_iff_same_ray {x y z : E} :
-  x ∈ [y -[𝕜] z] ↔ same_ray 𝕜 (x - y) (z - x) :=
+lemma mem_segment_iff_same_ray : x ∈ [y -[𝕜] z] ↔ same_ray 𝕜 (x - y) (z - x) :=
 begin
   refine ⟨same_ray_of_mem_segment, λ h, _⟩,
   rcases h.exists_eq_smul_add with ⟨a, b, ha, hb, hab, hxy, hzx⟩,
@@ -312,7 +311,7 @@ begin
   rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_self]
 end
 
-lemma mem_segment_iff_div {x y z : E} : x ∈ [y -[𝕜] z] ↔
+lemma mem_segment_iff_div : x ∈ [y -[𝕜] z] ↔
   ∃ a b : 𝕜, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x :=
 begin
   split,
@@ -324,7 +323,7 @@ begin
     rw [← add_div, div_self hab.ne'] }
 end
 
-lemma mem_open_segment_iff_div {x y z : E} : x ∈ open_segment 𝕜 y z ↔
+lemma mem_open_segment_iff_div : x ∈ open_segment 𝕜 y z ↔
   ∃ a b : 𝕜, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x :=
 begin
   split,
@@ -427,7 +426,7 @@ end
 (segment_subset_Icc h).antisymm Icc_subset_segment
 
 lemma Ioo_subset_open_segment {x y : 𝕜} : Ioo x y ⊆ open_segment 𝕜 x y :=
-λ z hz, mem_open_segment_of_ne_left_right _ hz.1.ne hz.2.ne'
+λ z hz, mem_open_segment_of_ne_left_right hz.1.ne hz.2.ne'
     (Icc_subset_segment $ Ioo_subset_Icc_self hz)
 
 @[simp] lemma open_segment_eq_Ioo {x y : 𝕜} (h : x < y) : open_segment 𝕜 x y = Ioo x y :=

src/analysis/convex/extreme.lean

@@ -194,18 +194,14 @@ that contain it are those with `x` as one of their endpoints. -/
 lemma mem_extreme_points_iff_forall_segment :
   x ∈ A.extreme_points 𝕜 ↔ x ∈ A ∧ ∀ (x₁ x₂ ∈ A), x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x :=
 begin
+  refine and_congr_right (λ hxA, forall₄_congr $ λ x₁ h₁ x₂ h₂, _),
   split,
-  { rintro ⟨hxA, hAx⟩,
-    use hxA,
-    rintro x₁ hx₁ x₂ hx₂ hx,
-    by_contra' h,
-    exact h.1 (hAx _ hx₁ _ hx₂ (mem_open_segment_of_ne_left_right 𝕜 h.1 h.2 hx)).1 },
-  rintro ⟨hxA, hAx⟩,
-  use hxA,
-  rintro x₁ x₂ hx₁ hx₂ hx,
-  obtain rfl | rfl := hAx x₁ x₂ hx₁ hx₂ (open_segment_subset_segment 𝕜 _ _ hx),
-  { exact ⟨rfl, (left_mem_open_segment_iff.1 hx).symm⟩ },
-  exact ⟨right_mem_open_segment_iff.1 hx, rfl⟩,
+  { rw ← insert_endpoints_open_segment,
+    rintro H (rfl|rfl|hx),
+    exacts [or.inl rfl, or.inr rfl, or.inl $ (H hx).1] },
+  { intros H hx,
+    rcases H (open_segment_subset_segment _ _ _ hx) with rfl | rfl,
+    exacts [⟨rfl, (left_mem_open_segment_iff.1 hx).symm⟩, ⟨right_mem_open_segment_iff.1 hx, rfl⟩] }
 end
 
 lemma convex.mem_extreme_points_iff_convex_diff (hA : convex 𝕜 A) :