refactor(analysis/convex): simplify proofs, use implicit args and dot notation

src/algebra/big_operators.lean

@@ -51,6 +51,11 @@ lemma prod_insert [decidable_eq α] : a ∉ s → (insert a s).prod f = f a * s.
 lemma prod_singleton : (singleton a).prod f = f a :=
 eq.trans fold_singleton $ mul_one _
 
+@[to_additive]
+lemma prod_pair [decidable_eq α] {a b : α} (h : a ≠ b) :
+  ({a, b} : finset α).prod f = f a * f b :=
+by simp [prod_insert (not_mem_singleton.2 h.symm), mul_comm]
+
 @[simp] lemma prod_const_one : s.prod (λx, (1 : β)) = 1 :=
 by simp only [finset.prod, multiset.map_const, multiset.prod_repeat, one_pow]
 @[simp] lemma sum_const_zero {β} {s : finset α} [add_comm_monoid β] : s.sum (λx, (0 : β)) = 0 :=

src/analysis/calculus/mean_value.lean

@@ -111,7 +111,7 @@ begin
     differentiable.add (differentiable_const _)
       (differentiable.smul' differentiable_id (differentiable_const _)),
   have segm : (λ (t : ℝ), x + t • (y - x)) '' Icc 0 1 ⊆ s,
-    by { rw image_Icc_zero_one_eq_segment, apply (convex_segment_iff _).1 hs x y xs ys },
+    by { rw [← segment_eq_image_Icc_zero_one], apply convex_segment_iff.1 hs x y xs ys },
   have : f x = g 0, by { simp only [g], rw [zero_smul, add_zero] },
   rw this,
   have : f y = g 1, by { simp only [g], rw one_smul, congr' 1, abel },

src/analysis/calculus/tangent_cone.lean

@@ -400,8 +400,8 @@ begin
         exact ⟨δ, δpos, this⟩ } },
     rcases this with ⟨δ, δpos, hδ⟩,
     refine ⟨y-x, _, (y + δ • v) - x, _, δ, δpos, by abel⟩,
-    exact mem_tangent_cone_of_segment_subset ((convex_segment_iff _).1 conv x y xs ys),
-    exact mem_tangent_cone_of_segment_subset ((convex_segment_iff _).1 conv x _ xs hδ) },
+    exact mem_tangent_cone_of_segment_subset (convex_segment_iff.1 conv x y xs ys),
+    exact mem_tangent_cone_of_segment_subset (convex_segment_iff.1 conv x _ xs hδ) },
   have B : ∀v:G, v ∈ submodule.span ℝ (tangent_cone_at ℝ s x),
   { assume v,
     rcases A v with ⟨a, ha, b, hb, δ, hδ, h⟩,