chore(*): update to lean 3.36.0 (#11253)

The main breaking change is the change in elaboration of double membership binders into x hx y hy, from x y hx hy.




Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

archive/imo/imo1994_q1.lean

@@ -85,7 +85,7 @@ begin
     rcases hx with ⟨i, ⟨hi, rfl⟩⟩,
     have h1 : a i + a (fin.last m - k) ≤ n,
     { linarith only [h, a.monotone hi.2] },
-    have h2 : a i + a (fin.last m - k) ∈ A := hadd _ _ (ha _) (ha _) h1,
+    have h2 : a i + a (fin.last m - k) ∈ A := hadd _ (ha _) _ (ha _) h1,
     rw [←mem_coe, ←range_order_emb_of_fin A hm, set.mem_range] at h2,
     cases h2 with j hj,
     use j,

archive/imo/imo2021_q1.lean

@@ -143,7 +143,7 @@ begin
     { rw [finset.mem_insert, finset.mem_singleton, finset.mem_singleton],
       push_neg,
       exact ⟨⟨hab.ne, (hab.trans hbc).ne⟩, hbc.ne⟩ } },
-  { intros x y hx hy hxy,
+  { intros x hx y hy hxy,
     simp only [finset.mem_insert, finset.mem_singleton] at hx hy,
     rcases hx with rfl|rfl|rfl; rcases hy with rfl|rfl|rfl,
     all_goals { contradiction <|> assumption <|> simpa only [add_comm x y], } },
@@ -177,5 +177,5 @@ begin
   simp only [finset.subset_iff, finset.mem_inter] at hCA,
   -- Now we split into the two cases C ⊆ [n, 2n] \ A and C ⊆ A, which can be dealt with identically.
   cases hCA; [right, left];
-  exact ⟨a, b, (hCA ha).2, (hCA hb).2, hab, h₁ a b (hCA ha).1 (hCA hb).1 hab⟩,
+  exact ⟨a, (hCA ha).2, b, (hCA hb).2, hab, h₁ a (hCA ha).1 b (hCA hb).1 hab⟩,
 end

leanpkg.toml

@@ -1,7 +1,7 @@
 [package]
 name = "mathlib"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.35.1"
+lean_version = "leanprover-community/lean:3.36.0"
 path = "src"
 
 [dependencies]

src/algebra/lie/solvable.lean

@@ -261,19 +261,15 @@ instance radical_is_solvable [is_noetherian R L] : is_solvable R (radical R L) :
 begin
   have hwf := lie_submodule.well_founded_of_noetherian R L L,
   rw ← complete_lattice.is_sup_closed_compact_iff_well_founded at hwf,
-  refine hwf { I : lie_ideal R L | is_solvable R I } _ _,
-  { use ⊥, exact lie_algebra.is_solvable_bot R L, },
-  { intros I J hI hJ, apply lie_algebra.is_solvable_add R L; [exact hI, exact hJ], },
+  refine hwf { I : lie_ideal R L | is_solvable R I } ⟨⊥, _⟩ (λ I hI J hJ, _),
+  { exact lie_algebra.is_solvable_bot R L, },
+  { apply lie_algebra.is_solvable_add R L, exacts [hI, hJ] },
 end
 
 /-- The `→` direction of this lemma is actually true without the `is_noetherian` assumption. -/
 lemma lie_ideal.solvable_iff_le_radical [is_noetherian R L] (I : lie_ideal R L) :
   is_solvable R I ↔ I ≤ radical R L :=
-begin
-  split; intros h,
-  { exact le_Sup h, },
-  { apply le_solvable_ideal_solvable h, apply_instance, },
-end
+⟨λ h, le_Sup h, λ h, le_solvable_ideal_solvable h infer_instance⟩
 
 lemma center_le_radical : center R L ≤ radical R L :=
 have h : is_solvable R (center R L), { apply_instance, }, le_Sup h

src/algebraic_geometry/prime_spectrum/basic.lean

@@ -349,7 +349,7 @@ topological_space.of_closed (set.range prime_spectrum.zero_locus)
     simp only [hf],
     exact ⟨_, zero_locus_Union _⟩
   end
-  (by { rintro _ _ ⟨s, rfl⟩ ⟨t, rfl⟩, exact ⟨_, (union_zero_locus s t).symm⟩ })
+  (by { rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩, exact ⟨_, (union_zero_locus s t).symm⟩ })
 
 lemma is_open_iff (U : set (prime_spectrum R)) :
   is_open U ↔ ∃ s, Uᶜ = zero_locus s :=

src/algebraic_geometry/properties.lean

@@ -207,7 +207,9 @@ begin
       exact H } },
   { intros R hX s hs x,
     erw [basic_open_eq_of_affine', prime_spectrum.basic_open_eq_bot_iff] at hs,
-    replace hs := (hs.map (Spec_Γ_identity.app R).inv).eq_zero,
+    replace hs := (hs.map (Spec_Γ_identity.app R).inv),
+    -- what the hell?!
+    replace hs := @is_nilpotent.eq_zero _ _ _ _ (show _, from _) hs,
     rw coe_hom_inv_id at hs,
     rw [hs, map_zero],
     exact @@is_reduced.component_reduced hX ⊤ }

src/algebraic_geometry/structure_sheaf.lean

@@ -694,7 +694,7 @@ begin
   refine ⟨(λ i, a i * (h i) ^ N), (λ i, (h i) ^ (N + 1)),
     (λ i, eq_to_hom (basic_opens_eq i) ≫ iDh i), _, _, _⟩,
   { simpa only [basic_opens_eq] using h_cover },
-  { intros i j hi hj,
+  { intros i hi j hj,
     -- Here we need to show that our new fractions `a i / h i` satisfy the normalization condition
     -- Of course, the power `N` we used to expand the fractions might be bigger than the power
     -- `n (i, j)` which was originally chosen. We denote their difference by `k`
@@ -795,7 +795,7 @@ begin
   rw [← hb, finset.sum_mul, finset.mul_sum],
   apply finset.sum_congr rfl,
   intros j hj,
-  rw [mul_assoc, ah_ha j i hj hi],
+  rw [mul_assoc, ah_ha j hj i hi],
   ring
 end
 

src/analysis/ODE/gronwall.lean

@@ -165,9 +165,8 @@ begin
   assume t ht,
   have := dist_triangle4_right (f' t) (g' t) (v t (f t)) (v t (g t)),
   rw [dist_eq_norm] at this,
-  apply le_trans this,
-  apply le_trans (add_le_add (add_le_add (f_bound t ht) (g_bound t ht))
-    (hv t (f t) (g t) (hfs t ht) (hgs t ht))),
+  refine this.trans ((add_le_add (add_le_add (f_bound t ht) (g_bound t ht))
+    (hv t (f t) (hfs t ht) (g t) (hgs t ht))).trans _),
   rw [dist_eq_norm, add_comm]
 end
 
@@ -188,7 +187,7 @@ theorem dist_le_of_approx_trajectories_ODE {v : ℝ → E → E}
   (ha : dist (f a) (g a) ≤ δ) :
   ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwall_bound δ K (εf + εg) (t - a) :=
 have hfs : ∀ t ∈ Ico a b, f t ∈ (@univ E), from λ t ht, trivial,
-dist_le_of_approx_trajectories_ODE_of_mem_set (λ t x y hx hy, (hv t).dist_le_mul x y)
+dist_le_of_approx_trajectories_ODE_of_mem_set (λ t x hx y hy, (hv t).dist_le_mul x y)
   hf hf' f_bound hfs hg hg' g_bound (λ t ht, trivial) ha
 
 /-- If `f` and `g` are two exact solutions of the same ODE, then the distance between them
@@ -234,7 +233,7 @@ theorem dist_le_of_trajectories_ODE {v : ℝ → E → E}
   (ha : dist (f a) (g a) ≤ δ) :
   ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * exp (K * (t - a)) :=
 have hfs : ∀ t ∈ Ico a b, f t ∈ (@univ E), from λ t ht, trivial,
-dist_le_of_trajectories_ODE_of_mem_set (λ t x y hx hy, (hv t).dist_le_mul x y)
+dist_le_of_trajectories_ODE_of_mem_set (λ t x hx y hy, (hv t).dist_le_mul x y)
   hf hf' hfs hg hg' (λ t ht, trivial) ha
 
 /-- There exists only one solution of an ODE \(\dot x=v(t, x)\) in a set `s ⊆ ℝ × E` with
@@ -270,5 +269,5 @@ theorem ODE_solution_unique {v : ℝ → E → E}
   (ha : f a = g a) :
   ∀ t ∈ Icc a b, f t = g t :=
 have hfs : ∀ t ∈ Ico a b, f t ∈ (@univ E), from λ t ht, trivial,
-ODE_solution_unique_of_mem_set (λ t x y hx hy, (hv t).dist_le_mul x y)
+ODE_solution_unique_of_mem_set (λ t x hx y hy, (hv t).dist_le_mul x y)
   hf hf' hfs hg hg' (λ t ht, trivial) ha

src/analysis/analytic/basic.lean

@@ -565,7 +565,7 @@ lemma has_fpower_series_on_ball.image_sub_sub_deriv_le
   ∃ C, ∀ (y z ∈ emetric.ball x r'),
     ∥f y - f z - (p 1 (λ _, y - z))∥ ≤ C * (max ∥y - x∥ ∥z - x∥) * ∥y - z∥ :=
 by simpa only [is_O_principal, mul_assoc, normed_field.norm_mul, norm_norm, prod.forall,
-  emetric.mem_ball, prod.edist_eq, max_lt_iff, and_imp]
+  emetric.mem_ball, prod.edist_eq, max_lt_iff, and_imp, @forall_swap (_ < _) E]
   using hf.is_O_image_sub_image_sub_deriv_principal hr
 
 /-- If `f` has formal power series `∑ n, pₙ` at `x`, then

src/analysis/box_integral/basic.lean

@@ -658,7 +658,7 @@ begin
     have : 0 ≤ μ.to_box_additive J, from ennreal.to_real_nonneg,
     rw [norm_smul, real.norm_eq_abs, abs_of_nonneg this, ← dist_eq_norm],
     refine mul_le_mul_of_nonneg_left _ this,
-    refine Hδ _ _ (tagged_prepartition.tag_mem_Icc _ _) (tagged_prepartition.tag_mem_Icc _ _) _,
+    refine Hδ _ (tagged_prepartition.tag_mem_Icc _ _) _ (tagged_prepartition.tag_mem_Icc _ _) _,
     rw [← add_halves δ],
     refine (dist_triangle_left _ _ J.upper).trans (add_le_add (h₁.1 _ _ _) (h₂.1 _ _ _)),
     { exact prepartition.bUnion_index_mem _ hJ },

src/analysis/box_integral/divergence_theorem.lean

@@ -178,7 +178,7 @@ begin
       { rcases ((nhds_within_has_basis nhds_basis_closed_ball _).tendsto_iff
           nhds_basis_closed_ball).1 (Hs x hx.2) _ (half_pos $ half_pos ε0) with ⟨δ₁, δ₁0, hδ₁⟩,
         filter_upwards [Ioc_mem_nhds_within_Ioi ⟨le_rfl, δ₁0⟩],
-        rintro δ hδ y₁ y₂ hy₁ hy₂,
+        rintro δ hδ y₁ hy₁ y₂ hy₂,
         have : closed_ball x δ ∩ I.Icc ⊆ closed_ball x δ₁ ∩ I.Icc,
           from inter_subset_inter_left _ (closed_ball_subset_closed_ball hδ.2),
         rw ← dist_eq_norm,
@@ -217,7 +217,7 @@ begin
         prod_le_prod (λ _ _ , abs_nonneg _) (λ j hj, this j)
       ... = (2 * δ) ^ (n + 1) : by simp },
     { refine (norm_integral_le_of_le_const (λ y hy,
-        hdfδ _ _ (Hmaps _ Hu hy) (Hmaps _ Hl hy)) _).trans _,
+        hdfδ _ (Hmaps _ Hu hy) _ (Hmaps _ Hl hy)) _).trans _,
       refine (mul_le_mul_of_nonneg_right _ (half_pos ε0).le).trans_eq (one_mul _),
       rw [box.coe_eq_pi, real.volume_pi_Ioc_to_real (box.lower_le_upper _)],
       refine prod_le_one (λ _ _, sub_nonneg.2 $ box.lower_le_upper _ _) (λ j hj, _),

src/analysis/calculus/fderiv_measurable.lean

@@ -119,8 +119,8 @@ begin
   have : s ∈ Ioc (r/2) r := ⟨s_gt, le_of_lt (s_lt.trans_le r'_mem.2)⟩,
   refine ⟨r' - s, by linarith, λ x' hx', ⟨s, this, _⟩⟩,
   have B : ball x' s ⊆ ball x r' := ball_subset (le_of_lt hx'),
-  assume y z hy hz,
-  exact hr' y z (B hy) (B hz)
+  assume y hy z hz,
+  exact hr' y (B hy) z (B hz)
 end
 
 lemma is_open_B {K : set (E →L[𝕜] F)} {r s ε : ℝ} : is_open (B f K r s ε) :=
@@ -130,9 +130,7 @@ lemma A_mono (L : E →L[𝕜] F) (r : ℝ) {ε δ : ℝ} (h : ε ≤ δ) :
   A f L r ε ⊆ A f L r δ :=
 begin
   rintros x ⟨r', r'r, hr'⟩,
-  refine ⟨r', r'r, λ y z hy hz, _⟩,
-  apply le_trans (hr' y z hy hz),
-  apply mul_le_mul_of_nonneg_right h,
+  refine ⟨r', r'r, λ y hy z hz, (hr' y hy z hz).trans (mul_le_mul_of_nonneg_right h _)⟩,
   linarith [mem_ball.1 hy, r'r.2, @dist_nonneg _ _ y x],
 end
 
@@ -141,8 +139,7 @@ lemma le_of_mem_A {r ε : ℝ} {L : E →L[𝕜] F} {x : E} (hx : x ∈ A f L r
   ∥f z - f y - L (z-y)∥ ≤ ε * r :=
 begin
   rcases hx with ⟨r', r'mem, hr'⟩,
-  exact hr' _ _ (lt_of_le_of_lt (mem_closed_ball.1 hy) r'mem.1)
-    (lt_of_le_of_lt (mem_closed_ball.1 hz) r'mem.1)
+  exact hr' _ ((mem_closed_ball.1 hy).trans_lt r'mem.1) _ ((mem_closed_ball.1 hz).trans_lt r'mem.1)
 end
 
 lemma mem_A_of_differentiable {ε : ℝ} (hε : 0 < ε) {x : E} (hx : differentiable_at 𝕜 f x) :
@@ -153,7 +150,7 @@ begin
   rcases eventually_nhds_iff_ball.1 (this (half_pos hε)) with ⟨R, R_pos, hR⟩,
   refine ⟨R, R_pos, λ r hr, _⟩,
   have : r ∈ Ioc (r/2) r := ⟨half_lt_self hr.1, le_refl _⟩,
-  refine ⟨r, this, λ y z hy hz, _⟩,
+  refine ⟨r, this, λ y hy z hz, _⟩,
   calc  ∥f z - f y - (fderiv 𝕜 f x) (z - y)∥
       = ∥(f z - f x - (fderiv 𝕜 f x) (z - x)) - (f y - f x - (fderiv 𝕜 f x) (y - x))∥ :
     by { congr' 1, simp only [continuous_linear_map.map_sub], abel }

src/analysis/calculus/local_extr.lean

@@ -368,7 +368,7 @@ begin
   { rw eq_C_of_nat_degree_eq_zero (nat_degree_eq_zero_of_derivative_eq_zero hp'),
     simp_rw [root_set_C, set.empty_card', zero_le] },
   simp_rw [root_set_def, finset.coe_sort_coe, fintype.card_coe],
-  refine finset.card_le_of_interleaved (λ x y hx hy hxy, _),
+  refine finset.card_le_of_interleaved (λ x hx y hy hxy, _),
   rw [←finset.mem_coe, ←root_set_def, mem_root_set hp] at hx hy,
   obtain ⟨z, hz1, hz2⟩ := exists_deriv_eq_zero (λ x : ℝ, aeval x p) hxy
     p.continuous_aeval.continuous_on (hx.trans hy.symm),

src/analysis/calculus/mean_value.lean

@@ -822,7 +822,7 @@ theorem convex.mul_sub_lt_image_sub_of_lt_deriv {D : set ℝ} (hD : convex ℝ D
   {C} (hf'_gt : ∀ x ∈ interior D, C < deriv f x) :
   ∀ x y ∈ D, x < y → C * (y - x) < f y - f x :=
 begin
-  assume x y hx hy hxy,
+  assume x hx y hy hxy,
   have hxyD : Icc x y ⊆ D, from hD.ord_connected.out hx hy,
   have hxyD' : Ioo x y ⊆ interior D,
     from subset_sUnion_of_mem ⟨is_open_Ioo, subset.trans Ioo_subset_Icc_self hxyD⟩,
@@ -838,7 +838,7 @@ theorem mul_sub_lt_image_sub_of_lt_deriv {f : ℝ → ℝ} (hf : differentiable
   {C} (hf'_gt : ∀ x, C < deriv f x) ⦃x y⦄ (hxy : x < y) :
   C * (y - x) < f y - f x :=
 convex_univ.mul_sub_lt_image_sub_of_lt_deriv hf.continuous.continuous_on hf.differentiable_on
-  (λ x _, hf'_gt x) x y trivial trivial hxy
+  (λ x _, hf'_gt x) x trivial y trivial hxy
 
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `C ≤ f'`, then
@@ -849,7 +849,7 @@ theorem convex.mul_sub_le_image_sub_of_le_deriv {D : set ℝ} (hD : convex ℝ D
   {C} (hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x) :
   ∀ x y ∈ D, x ≤ y → C * (y - x) ≤ f y - f x :=
 begin
-  assume x y hx hy hxy,
+  assume x hx y hy hxy,
   cases eq_or_lt_of_le hxy with hxy' hxy', by rw [hxy', sub_self, sub_self, mul_zero],
   have hxyD : Icc x y ⊆ D, from hD.ord_connected.out hx hy,
   have hxyD' : Ioo x y ⊆ interior D,
@@ -866,7 +866,7 @@ theorem mul_sub_le_image_sub_of_le_deriv {f : ℝ → ℝ} (hf : differentiable
   {C} (hf'_ge : ∀ x, C ≤ deriv f x) ⦃x y⦄ (hxy : x ≤ y) :
   C * (y - x) ≤ f y - f x :=
 convex_univ.mul_sub_le_image_sub_of_le_deriv hf.continuous.continuous_on hf.differentiable_on
-  (λ x _, hf'_ge x) x y trivial trivial hxy
+  (λ x _, hf'_ge x) x trivial y trivial hxy
 
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `f' < C`, then
@@ -877,13 +877,13 @@ theorem convex.image_sub_lt_mul_sub_of_deriv_lt {D : set ℝ} (hD : convex ℝ D
   {C} (lt_hf' : ∀ x ∈ interior D, deriv f x < C) :
   ∀ x y ∈ D, x < y → f y - f x < C * (y - x) :=
 begin
-  assume x y hx hy hxy,
+  assume x hx y hy hxy,
   have hf'_gt : ∀ x ∈ interior D, -C < deriv (λ y, -f y) x,
   { assume x hx,
     rw [deriv.neg, neg_lt_neg_iff],
     exact lt_hf' x hx },
   simpa [-neg_lt_neg_iff]
-    using neg_lt_neg (hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x y hx hy hxy)
+    using neg_lt_neg (hD.mul_sub_lt_image_sub_of_lt_deriv hf.neg hf'.neg hf'_gt x hx y hy hxy)
 end
 
 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f' < C`, then `f` grows slower than
@@ -892,7 +892,7 @@ theorem image_sub_lt_mul_sub_of_deriv_lt {f : ℝ → ℝ} (hf : differentiable
   {C} (lt_hf' : ∀ x, deriv f x < C) ⦃x y⦄ (hxy : x < y) :
   f y - f x < C * (y - x) :=
 convex_univ.image_sub_lt_mul_sub_of_deriv_lt hf.continuous.continuous_on hf.differentiable_on
-  (λ x _, lt_hf' x) x y trivial trivial hxy
+  (λ x _, lt_hf' x) x trivial y trivial hxy
 
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `f' ≤ C`, then
@@ -903,13 +903,13 @@ theorem convex.image_sub_le_mul_sub_of_deriv_le {D : set ℝ} (hD : convex ℝ D
   {C} (le_hf' : ∀ x ∈ interior D, deriv f x ≤ C) :
   ∀ x y ∈ D, x ≤ y → f y - f x ≤ C * (y - x) :=
 begin
-  assume x y hx hy hxy,
+  assume x hx y hy hxy,
   have hf'_ge : ∀ x ∈ interior D, -C ≤ deriv (λ y, -f y) x,
   { assume x hx,
     rw [deriv.neg, neg_le_neg_iff],
     exact le_hf' x hx },
   simpa [-neg_le_neg_iff]
-    using neg_le_neg (hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x y hx hy hxy)
+    using neg_le_neg (hD.mul_sub_le_image_sub_of_le_deriv hf.neg hf'.neg hf'_ge x hx y hy hxy)
 end
 
 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f' ≤ C`, then `f` grows at most as fast
@@ -918,7 +918,7 @@ theorem image_sub_le_mul_sub_of_deriv_le {f : ℝ → ℝ} (hf : differentiable
   {C} (le_hf' : ∀ x, deriv f x ≤ C) ⦃x y⦄ (hxy : x ≤ y) :
   f y - f x ≤ C * (y - x) :=
 convex_univ.image_sub_le_mul_sub_of_deriv_le hf.continuous.continuous_on hf.differentiable_on
-  (λ x _, le_hf' x) x y trivial trivial hxy
+  (λ x _, le_hf' x) x trivial y trivial hxy
 
 /-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
 of the real line. If `f` is differentiable on the interior of `D` and `f'` is positive, then
@@ -930,7 +930,7 @@ theorem convex.strict_mono_on_of_deriv_pos {D : set ℝ} (hD : convex ℝ D) {f
   strict_mono_on f D :=
 begin
   rintro x hx y hy,
-  simpa only [zero_mul, sub_pos] using hD.mul_sub_lt_image_sub_of_lt_deriv hf _ hf' x y hx hy,
+  simpa only [zero_mul, sub_pos] using hD.mul_sub_lt_image_sub_of_lt_deriv hf _ hf' x hx y hy,
   exact λ z hz, (differentiable_at_of_deriv_ne_zero (hf' z hz).ne').differentiable_within_at,
 end
 
@@ -952,7 +952,7 @@ theorem convex.monotone_on_of_deriv_nonneg {D : set ℝ} (hD : convex ℝ D) {f
   (hf'_nonneg : ∀ x ∈ interior D, 0 ≤ deriv f x) :
   monotone_on f D :=
 λ x hx y hy hxy, by simpa only [zero_mul, sub_nonneg]
-  using hD.mul_sub_le_image_sub_of_le_deriv hf hf' hf'_nonneg x y hx hy hxy
+  using hD.mul_sub_le_image_sub_of_le_deriv hf hf' hf'_nonneg x hx y hy hxy
 
 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonnegative, then
 `f` is a monotone function. -/
@@ -969,7 +969,7 @@ theorem convex.strict_anti_on_of_deriv_neg {D : set ℝ} (hD : convex ℝ D) {f
   strict_anti_on f D :=
 λ x hx y, by simpa only [zero_mul, sub_lt_zero]
   using hD.image_sub_lt_mul_sub_of_deriv_lt hf
-  (λ z hz, (differentiable_at_of_deriv_ne_zero (hf' z hz).ne).differentiable_within_at) hf' x y hx
+  (λ z hz, (differentiable_at_of_deriv_ne_zero (hf' z hz).ne).differentiable_within_at) hf' x hx y
 
 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is negative, then
 `f` is a strictly antitone function.
@@ -990,7 +990,7 @@ theorem convex.antitone_on_of_deriv_nonpos {D : set ℝ} (hD : convex ℝ D) {f
   (hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0) :
   antitone_on f D :=
 λ x hx y hy hxy, by simpa only [zero_mul, sub_nonpos]
-  using hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos x y hx hy hxy
+  using hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos x hx y hy hxy
 
 /-- Let `f : ℝ → ℝ` be a differentiable function. If `f'` is nonpositive, then
 `f` is an antitone function. -/

src/analysis/convex/exposed.lean

@@ -167,7 +167,7 @@ end
 protected lemma is_extreme (hAB : is_exposed 𝕜 A B) :
   is_extreme 𝕜 A B :=
 begin
-  refine ⟨hAB.subset, λ x₁ x₂ hx₁A hx₂A x hxB hx, _⟩,
+  refine ⟨hAB.subset, λ x₁ hx₁A x₂ hx₂A x hxB hx, _⟩,
   obtain ⟨l, rfl⟩ := hAB ⟨x, hxB⟩,
   have hl : convex_on 𝕜 univ l := l.to_linear_map.convex_on convex_univ,
   have hlx₁ := hxB.2 x₁ hx₁A,