refactor(*): change definition of Set.image2 etc (#9275)

- Redefine `Set.image2` to use `∃ a ∈ s, ∃ b ∈ t, f a b = c` instead of `∃ a b, a ∈ s ∧ b ∈ t ∧ f a b = c`.
- Redefine `Set.seq` as `Set.image2`. The new definition is equal to the old one but `rw [Set.seq]` gives a different result.
- Redefine `Filter.map₂` to use `∃ u ∈ f, ∃ v ∈ g, image2 m u v ⊆ s` instead of `∃ u v, u ∈ f ∧ v ∈ g ∧ ...`
- Update lemmas like `Set.mem_image2`, `Finset.mem_image₂`, `Set.mem_mul`, `Finset.mem_div` etc

The two reasons to make the change are:

- `∃ a ∈ s, ∃ b ∈ t, _` is a `simp`-normal form, and
- it looks a bit nicer.

Mathlib/Algebra/Algebra/Tower.lean

@@ -299,7 +299,7 @@ open IsScalarTower
 
 theorem smul_mem_span_smul_of_mem {s : Set S} {t : Set A} {k : S} (hks : k ∈ span R s) {x : A}
     (hx : x ∈ t) : k • x ∈ span R (s • t) :=
-  span_induction hks (fun c hc => subset_span <| Set.mem_smul.2 ⟨c, x, hc, hx, rfl⟩)
+  span_induction hks (fun c hc => subset_span <| Set.smul_mem_smul hc hx)
     (by rw [zero_smul]; exact zero_mem _)
     (fun c₁ c₂ ih₁ ih₂ => by rw [add_smul]; exact add_mem ih₁ ih₂)
     fun b c hc => by rw [IsScalarTower.smul_assoc]; exact smul_mem _ _ hc
@@ -319,7 +319,7 @@ theorem smul_mem_span_smul' {s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S
     (hx : x ∈ span R (s • t)) : k • x ∈ span R (s • t) :=
   span_induction hx
     (fun x hx => by
-      let ⟨p, q, _hp, hq, hpq⟩ := Set.mem_smul.1 hx
+      let ⟨p, _hp, q, hq, hpq⟩ := Set.mem_smul.1 hx
       rw [← hpq, smul_smul]
       exact smul_mem_span_smul_of_mem (hs.symm ▸ mem_top) hq)
     (by rw [smul_zero]; exact zero_mem _)

Mathlib/Algebra/Group/UniqueProds.lean

@@ -375,8 +375,8 @@ open MulOpposite in
   uniqueMul_of_nonempty {A B} hA hB := by
     classical
     obtain ⟨g1, h1, g2, h2, hu⟩ := h (hB.mul hA)
-    obtain ⟨b1, a1, hb1, ha1, rfl⟩ := mem_mul.mp h1
-    obtain ⟨b2, a2, hb2, ha2, rfl⟩ := mem_mul.mp h2
+    obtain ⟨b1, hb1, a1, ha1, rfl⟩ := mem_mul.mp h1
+    obtain ⟨b2, hb2, a2, ha2, rfl⟩ := mem_mul.mp h2
     refine ⟨a1, ha1, b2, hb2, fun a b ha hb he => ?_⟩
     specialize hu (mul_mem_mul hb1 ha) (mul_mem_mul hb ha2) _
     · rw [mul_assoc b1, ← mul_assoc a, he, mul_assoc a1, ← mul_assoc b1]
@@ -414,26 +414,26 @@ open MulOpposite in
     · obtain ⟨e, he, f, hf, hu⟩ := this
       clear_value C D
       simp only [UniqueMul, mem_mul, mem_image] at he hf hu
-      obtain ⟨_, c1, ⟨d1, hd1, rfl⟩, hc1, rfl⟩ := he
-      obtain ⟨d2, _, hd2, ⟨c2, hc2, rfl⟩, rfl⟩ := hf
+      obtain ⟨_, ⟨d1, hd1, rfl⟩, c1, hc1, rfl⟩ := he
+      obtain ⟨d2, hd2, _, ⟨c2, hc2, rfl⟩, rfl⟩ := hf
       by_cases h12 : c1 ≠ 1 ∨ d2 ≠ 1
       · refine ⟨c1, hc1, d2, hd2, h12, fun c3 d3 hc3 hd3 he => ?_⟩
-        specialize hu ⟨_, _, ⟨_, hd1, rfl⟩, hc3, rfl⟩ ⟨_, _, hd3, ⟨_, hc2, rfl⟩, rfl⟩
+        specialize hu ⟨_, ⟨_, hd1, rfl⟩, _, hc3, rfl⟩ ⟨_, hd3, _, ⟨_, hc2, rfl⟩, rfl⟩
         rw [mul_left_cancel_iff, mul_right_cancel_iff,
             mul_assoc, ← mul_assoc c3, he, mul_assoc, mul_assoc] at hu; exact hu rfl
       push_neg at h12; obtain ⟨rfl, rfl⟩ := h12
       by_cases h21 : c2 ≠ 1 ∨ d1 ≠ 1
       · refine ⟨c2, hc2, d1, hd1, h21, fun c4 d4 hc4 hd4 he => ?_⟩
-        specialize hu ⟨_, _, ⟨_, hd4, rfl⟩, hC, rfl⟩ ⟨_, _, hD, ⟨_, hc4, rfl⟩, rfl⟩
+        specialize hu ⟨_, ⟨_, hd4, rfl⟩, _, hC, rfl⟩ ⟨_, hD, _, ⟨_, hc4, rfl⟩, rfl⟩
         simpa only [mul_one, one_mul, ← mul_inv_rev, he, true_imp_iff, inv_inj, and_comm] using hu
       push_neg at h21; obtain ⟨rfl, rfl⟩ := h21
       rcases hcard with hC | hD
       · obtain ⟨c, hc, hc1⟩ := exists_ne_of_one_lt_card hC 1
         refine (hc1 ?_).elim
-        simpa using hu ⟨_, _, ⟨_, hD, rfl⟩, hc, rfl⟩ ⟨_, _, hD, ⟨_, hc, rfl⟩, rfl⟩
+        simpa using hu ⟨_, ⟨_, hD, rfl⟩, _, hc, rfl⟩ ⟨_, hD, _, ⟨_, hc, rfl⟩, rfl⟩
       · obtain ⟨d, hd, hd1⟩ := exists_ne_of_one_lt_card hD 1
         refine (hd1 ?_).elim
-        simpa using hu ⟨_, _, ⟨_, hd, rfl⟩, hC, rfl⟩ ⟨_, _, hd, ⟨_, hC, rfl⟩, rfl⟩
+        simpa using hu ⟨_, ⟨_, hd, rfl⟩, _, hC, rfl⟩ ⟨_, hd, _, ⟨_, hC, rfl⟩, rfl⟩
     all_goals apply_rules [Nonempty.mul, Nonempty.image, Finset.Nonempty.map, hc.1, hc.2.1]
 
 open UniqueMul in
@@ -571,8 +571,8 @@ instance (priority := 100) of_covariant_right [IsRightCancelMul G]
     obtain ⟨hA, hB, -⟩ := Nat.one_lt_mul_iff.mp hc
     rw [card_pos] at hA hB
     rw [← card_product] at hc
-    obtain ⟨a0, b0, ha0, hb0, he0⟩ := mem_mul.mp (max'_mem _ <| hA.mul hB)
-    obtain ⟨a1, b1, ha1, hb1, he1⟩ := mem_mul.mp (min'_mem _ <| hA.mul hB)
+    obtain ⟨a0, ha0, b0, hb0, he0⟩ := mem_mul.mp (max'_mem _ <| hA.mul hB)
+    obtain ⟨a1, ha1, b1, hb1, he1⟩ := mem_mul.mp (min'_mem _ <| hA.mul hB)
     have : UniqueMul A B a0 b0
     · intro a b ha hb he
       obtain hl | rfl | hl := lt_trichotomy b b0

Mathlib/Algebra/Module/Injective.lean

@@ -260,7 +260,7 @@ private theorem extensionOfMax_adjoin.aux1 {y : N} (x : supExtensionOfMaxSinglet
     ∃ (a : (extensionOfMax i f).domain) (b : R), x.1 = a.1 + b • y := by
   have mem1 : x.1 ∈ (_ : Set _) := x.2
   rw [Submodule.coe_sup] at mem1
-  rcases mem1 with ⟨a, b, a_mem, b_mem : b ∈ (Submodule.span R _ : Submodule R N), eq1⟩
+  rcases mem1 with ⟨a, a_mem, b, b_mem : b ∈ (Submodule.span R _ : Submodule R N), eq1⟩
   rw [Submodule.mem_span_singleton] at b_mem
   rcases b_mem with ⟨z, eq2⟩
   exact ⟨⟨a, a_mem⟩, z, by rw [← eq1, ← eq2]⟩

Mathlib/Algebra/Module/Submodule/Bilinear.lean

@@ -68,12 +68,12 @@ theorem map₂_span_span (f : M →ₗ[R] N →ₗ[R] P) (s : Set M) (t : Set N)
     intro a ha
     apply @span_induction' R N _ _ _ t
     intro b hb
-    exact subset_span ⟨_, _, ‹_›, ‹_›, rfl⟩
+    exact subset_span ⟨_, ‹_›, _, ‹_›, rfl⟩
     all_goals intros; simp only [*, add_mem, smul_mem, zero_mem, _root_.map_zero, map_add,
                                  LinearMap.zero_apply, LinearMap.add_apply, LinearMap.smul_apply,
                                  map_smul]
-  · rw [span_le]
-    rintro _ ⟨a, b, ha, hb, rfl⟩
+  · rw [span_le, image2_subset_iff]
+    intro a ha b hb
     exact apply_mem_map₂ _ (subset_span ha) (subset_span hb)
 #align submodule.map₂_span_span Submodule.map₂_span_span
 variable {R}
@@ -132,7 +132,7 @@ theorem map₂_sup_left (f : M →ₗ[R] N →ₗ[R] P) (p₁ p₂ : Submodule R
 
 theorem image2_subset_map₂ (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
     Set.image2 (fun m n => f m n) (↑p : Set M) (↑q : Set N) ⊆ (↑(map₂ f p q) : Set P) := by
-  rintro _ ⟨i, j, hi, hj, rfl⟩
+  rintro _ ⟨i, hi, j, hj, rfl⟩
   exact apply_mem_map₂ _ hi hj
 #align submodule.image2_subset_map₂ Submodule.image2_subset_map₂
 

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -508,14 +508,13 @@ protected def pointwiseSetMulAction [SMulCommClass R R M] :
       fun h => ⟨m, h, (one_smul _ _).symm⟩⟩
   mul_smul s t x := le_antisymm
     (set_smul_le _ _ _ <| by rintro _ _ ⟨_, _, _, _, rfl⟩ _; rw [mul_smul]; aesop)
-    (set_smul_le _ _ _ <| by
-      rintro r m hr hm
+    (set_smul_le _ _ _ <| fun r m hr hm ↦ by
       have : SMulCommClass R R x := ⟨fun r s m => Subtype.ext <| smul_comm _ _ _⟩
       obtain ⟨c, hc1, rfl⟩ := mem_set_smul _ _ _ |>.mp hm
       simp only [Finsupp.sum, AddSubmonoid.coe_finset_sum, coe_toAddSubmonoid, SetLike.val_smul,
-        Finset.smul_sum]
-      exact Submodule.sum_mem _ fun r' hr' ↦ mul_smul r r' (c r' : M) ▸
-        mem_set_smul_of_mem_mem (mem1 := ⟨r, r', hr, hc1 hr', rfl⟩) (mem2 := (c _).2))
+        Finset.smul_sum, smul_smul]
+      exact Submodule.sum_mem _ fun r' hr' ↦
+        mem_set_smul_of_mem_mem (Set.mul_mem_mul hr (hc1 hr')) (c _).2)
 
 scoped[Pointwise] attribute [instance] Submodule.pointwiseSetMulAction
 

Mathlib/Algebra/Order/CompleteField.lean

@@ -150,11 +150,11 @@ theorem cutMap_add (a b : α) : cutMap β (a + b) = cutMap β a + cutMap β b :=
   refine (image_subset_iff.2 fun q hq => ?_).antisymm ?_
   · rw [mem_setOf_eq, ← sub_lt_iff_lt_add] at hq
     obtain ⟨q₁, hq₁q, hq₁ab⟩ := exists_rat_btwn hq
-    refine ⟨q₁, q - q₁, by rwa [coe_mem_cutMap_iff], ?_, add_sub_cancel'_right _ _⟩
+    refine ⟨q₁, by rwa [coe_mem_cutMap_iff], q - q₁, ?_, add_sub_cancel'_right _ _⟩
     · norm_cast
       rw [coe_mem_cutMap_iff]
       exact mod_cast sub_lt_comm.mp hq₁q
-  · rintro _ ⟨_, _, ⟨qa, ha, rfl⟩, ⟨qb, hb, rfl⟩, rfl⟩
+  · rintro _ ⟨_, ⟨qa, ha, rfl⟩, _, ⟨qb, hb, rfl⟩, rfl⟩
     -- After leanprover/lean4#2734, `norm_cast` needs help with beta reduction.
     refine' ⟨qa + qb, _, by beta_reduce; norm_cast⟩
     rw [mem_setOf_eq, cast_add]

Mathlib/Algebra/Pointwise/Stabilizer.lean

@@ -47,8 +47,8 @@ lemma map_stabilizer_le (f : G →* H) (s : Set G) :
 @[to_additive (attr := simp)]
 lemma stabilizer_mul_self (s : Set G) : (stabilizer G s : Set G) * s = s := by
   ext
-  refine ⟨?_, fun h ↦ ⟨_, _, (stabilizer G s).one_mem, h, one_mul _⟩⟩
-  rintro ⟨a, b, ha, hb, rfl⟩
+  refine ⟨?_, fun h ↦ ⟨_, (stabilizer G s).one_mem, _, h, one_mul _⟩⟩
+  rintro ⟨a, ha, b, hb, rfl⟩
   rw [← mem_stabilizer_iff.1 ha]
   exact smul_mem_smul_set hb
 

Mathlib/Analysis/Convex/Basic.lean

@@ -77,7 +77,7 @@ theorem convex_iff_pointwise_add_subset :
     Convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s :=
   Iff.intro
     (by
-      rintro hA a b ha hb hab w ⟨au, bv, ⟨u, hu, rfl⟩, ⟨v, hv, rfl⟩, rfl⟩
+      rintro hA a b ha hb hab w ⟨au, ⟨u, hu, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩
       exact hA hu hv ha hb hab)
     fun h x hx y hy a b ha hb hab => (h ha hb hab) (Set.add_mem_add ⟨_, hx, rfl⟩ ⟨_, hy, rfl⟩)
 #align convex_iff_pointwise_add_subset convex_iff_pointwise_add_subset
@@ -599,7 +599,7 @@ theorem Convex.exists_mem_add_smul_eq (h : Convex 𝕜 s) {x y : E} {p q : 𝕜}
 
 theorem Convex.add_smul (h_conv : Convex 𝕜 s) {p q : 𝕜} (hp : 0 ≤ p) (hq : 0 ≤ q) :
     (p + q) • s = p • s + q • s := (add_smul_subset _ _ _).antisymm <| by
-  rintro _ ⟨_, _, ⟨v₁, h₁, rfl⟩, ⟨v₂, h₂, rfl⟩, rfl⟩
+  rintro _ ⟨_, ⟨v₁, h₁, rfl⟩, _, ⟨v₂, h₂, rfl⟩, rfl⟩
   exact h_conv.exists_mem_add_smul_eq h₁ h₂ hp hq
 #align convex.add_smul Convex.add_smul
 

Mathlib/Analysis/Convex/Cone/Basic.lean

@@ -443,19 +443,19 @@ theorem pointed_zero : (0 : ConvexCone 𝕜 E).Pointed := by rw [Pointed, mem_ze
 
 instance instAdd : Add (ConvexCone 𝕜 E) :=
   ⟨fun K₁ K₂ =>
-    { carrier := { z | ∃ x y : E, x ∈ K₁ ∧ y ∈ K₂ ∧ x + y = z }
+    { carrier := { z | ∃ x ∈ K₁, ∃ y ∈ K₂, x + y = z }
       smul_mem' := by
-        rintro c hc _ ⟨x, y, hx, hy, rfl⟩
+        rintro c hc _ ⟨x, hx, y, hy, rfl⟩
         rw [smul_add]
-        use c • x, c • y, K₁.smul_mem hc hx, K₂.smul_mem hc hy
+        use c • x, K₁.smul_mem hc hx, c • y, K₂.smul_mem hc hy
       add_mem' := by
-        rintro _ ⟨x₁, x₂, hx₁, hx₂, rfl⟩ y ⟨y₁, y₂, hy₁, hy₂, rfl⟩
-        use x₁ + y₁, x₂ + y₂, K₁.add_mem hx₁ hy₁, K₂.add_mem hx₂ hy₂
+        rintro _ ⟨x₁, hx₁, x₂, hx₂, rfl⟩ y ⟨y₁, hy₁, y₂, hy₂, rfl⟩
+        use x₁ + y₁, K₁.add_mem hx₁ hy₁, x₂ + y₂, K₂.add_mem hx₂ hy₂
         abel }⟩
 
 @[simp]
 theorem mem_add {K₁ K₂ : ConvexCone 𝕜 E} {a : E} :
-    a ∈ K₁ + K₂ ↔ ∃ x y : E, x ∈ K₁ ∧ y ∈ K₂ ∧ x + y = a :=
+    a ∈ K₁ + K₂ ↔ ∃ x ∈ K₁, ∃ y ∈ K₂, x + y = a :=
   Iff.rfl
 #align convex_cone.mem_add ConvexCone.mem_add
 
@@ -465,8 +465,8 @@ instance instAddZeroClass : AddZeroClass (ConvexCone 𝕜 E) where
 
 instance instAddCommSemigroup : AddCommSemigroup (ConvexCone 𝕜 E) where
   add := Add.add
-  add_assoc _ _ _ := SetLike.coe_injective <| Set.addCommSemigroup.add_assoc _ _ _
-  add_comm _ _ := SetLike.coe_injective <| Set.addCommSemigroup.add_comm _ _
+  add_assoc _ _ _ := SetLike.coe_injective <| add_assoc _ _ _
+  add_comm _ _ := SetLike.coe_injective <| add_comm _ _
 
 end Module
 

Mathlib/Analysis/Convex/Side.lean

@@ -775,12 +775,12 @@ theorem setOf_wSameSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉
     · rw [vsub_eq_zero_iff_eq] at h
       exact False.elim (hx (h.symm ▸ hp))
     · rw [vsub_eq_zero_iff_eq] at h
-      refine' ⟨0, p₂, le_refl _, hp₂, _⟩
+      refine' ⟨0, le_rfl, p₂, hp₂, _⟩
       simp [h]
-    · refine' ⟨r₁ / r₂, p₂, (div_pos hr₁ hr₂).le, hp₂, _⟩
+    · refine' ⟨r₁ / r₂, (div_pos hr₁ hr₂).le, p₂, hp₂, _⟩
       rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel hr₂.ne.symm, one_smul,
         vsub_vadd]
-  · rintro ⟨t, p', ht, hp', rfl⟩
+  · rintro ⟨t, ht, p', hp', rfl⟩
     exact wSameSide_smul_vsub_vadd_right x hp hp' ht
 #align affine_subspace.set_of_w_same_side_eq_image2 AffineSubspace.setOf_wSameSide_eq_image2
 
@@ -795,10 +795,10 @@ theorem setOf_sSameSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉
       exact False.elim (hx (h.symm ▸ hp))
     · rw [vsub_eq_zero_iff_eq] at h
       exact False.elim (hy (h.symm ▸ hp₂))
-    · refine' ⟨r₁ / r₂, p₂, div_pos hr₁ hr₂, hp₂, _⟩
+    · refine' ⟨r₁ / r₂, div_pos hr₁ hr₂, p₂, hp₂, _⟩
       rw [div_eq_inv_mul, ← smul_smul, h, smul_smul, inv_mul_cancel hr₂.ne.symm, one_smul,
         vsub_vadd]
-  · rintro ⟨t, p', ht, hp', rfl⟩
+  · rintro ⟨t, ht, p', hp', rfl⟩
     exact sSameSide_smul_vsub_vadd_right hx hp hp' ht
 #align affine_subspace.set_of_s_same_side_eq_image2 AffineSubspace.setOf_sSameSide_eq_image2
 
@@ -812,12 +812,12 @@ theorem setOf_wOppSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉
     · rw [vsub_eq_zero_iff_eq] at h
       exact False.elim (hx (h.symm ▸ hp))
     · rw [vsub_eq_zero_iff_eq] at h
-      refine' ⟨0, p₂, le_refl _, hp₂, _⟩
+      refine' ⟨0, le_rfl, p₂, hp₂, _⟩
       simp [h]
-    · refine' ⟨-r₁ / r₂, p₂, (div_neg_of_neg_of_pos (Left.neg_neg_iff.2 hr₁) hr₂).le, hp₂, _⟩
+    · refine' ⟨-r₁ / r₂, (div_neg_of_neg_of_pos (Left.neg_neg_iff.2 hr₁) hr₂).le, p₂, hp₂, _⟩
       rw [div_eq_inv_mul, ← smul_smul, neg_smul, h, smul_neg, smul_smul, inv_mul_cancel hr₂.ne.symm,
         one_smul, neg_vsub_eq_vsub_rev, vsub_vadd]
-  · rintro ⟨t, p', ht, hp', rfl⟩
+  · rintro ⟨t, ht, p', hp', rfl⟩
     exact wOppSide_smul_vsub_vadd_right x hp hp' ht
 #align affine_subspace.set_of_w_opp_side_eq_image2 AffineSubspace.setOf_wOppSide_eq_image2
 
@@ -832,10 +832,10 @@ theorem setOf_sOppSide_eq_image2 {s : AffineSubspace R P} {x p : P} (hx : x ∉
       exact False.elim (hx (h.symm ▸ hp))
     · rw [vsub_eq_zero_iff_eq] at h
       exact False.elim (hy (h ▸ hp₂))
-    · refine' ⟨-r₁ / r₂, p₂, div_neg_of_neg_of_pos (Left.neg_neg_iff.2 hr₁) hr₂, hp₂, _⟩
+    · refine' ⟨-r₁ / r₂, div_neg_of_neg_of_pos (Left.neg_neg_iff.2 hr₁) hr₂, p₂, hp₂, _⟩
       rw [div_eq_inv_mul, ← smul_smul, neg_smul, h, smul_neg, smul_smul, inv_mul_cancel hr₂.ne.symm,
         one_smul, neg_vsub_eq_vsub_rev, vsub_vadd]
-  · rintro ⟨t, p', ht, hp', rfl⟩
+  · rintro ⟨t, ht, p', hp', rfl⟩
     exact sOppSide_smul_vsub_vadd_right hx hp hp' ht
 #align affine_subspace.set_of_s_opp_side_eq_image2 AffineSubspace.setOf_sOppSide_eq_image2
 

Mathlib/Analysis/Convex/Star.lean

@@ -94,7 +94,7 @@ theorem starConvex_iff_pointwise_add_subset :
   refine'
     ⟨_, fun h y hy a b ha hb hab =>
       h ha hb hab (add_mem_add (smul_mem_smul_set <| mem_singleton _) ⟨_, hy, rfl⟩)⟩
-  rintro hA a b ha hb hab w ⟨au, bv, ⟨u, rfl : u = x, rfl⟩, ⟨v, hv, rfl⟩, rfl⟩
+  rintro hA a b ha hb hab w ⟨au, ⟨u, rfl : u = x, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩
   exact hA hv ha hb hab
 #align star_convex_iff_pointwise_add_subset starConvex_iff_pointwise_add_subset
 

Mathlib/Analysis/Convex/Strict.lean

@@ -244,7 +244,7 @@ variable [ContinuousAdd E] {s t : Set E}
 
 theorem StrictConvex.add (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) :
     StrictConvex 𝕜 (s + t) := by
-  rintro _ ⟨v, w, hv, hw, rfl⟩ _ ⟨x, y, hx, hy, rfl⟩ h a b ha hb hab
+  rintro _ ⟨v, hv, w, hw, rfl⟩ _ ⟨x, hx, y, hy, rfl⟩ h a b ha hb hab
   rw [smul_add, smul_add, add_add_add_comm]
   obtain rfl | hvx := eq_or_ne v x
   · refine' interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) _

Mathlib/Analysis/Convolution.lean

@@ -124,7 +124,7 @@ theorem convolution_integrand_bound_right_of_le_of_subset {C : ℝ} (hC : ∀ i,
   · apply_rules [L.le_of_op_norm₂_le_of_le, le_rfl]
   · have : x - t ∉ support g := by
       refine mt (fun hxt => hu ?_) ht
-      refine' ⟨_, _, Set.neg_mem_neg.mpr (subset_closure hxt), hx, _⟩
+      refine' ⟨_, Set.neg_mem_neg.mpr (subset_closure hxt), _, hx, _⟩
       simp only [neg_sub, sub_add_cancel]
     simp only [nmem_support.mp this, (L _).map_zero, norm_zero, le_rfl]
 #align convolution_integrand_bound_right_of_le_of_subset convolution_integrand_bound_right_of_le_of_subset
@@ -560,7 +560,7 @@ theorem support_convolution_subset_swap : support (f ⋆[L, μ] g) ⊆ support g
   intro x h2x
   by_contra hx
   apply h2x
-  simp_rw [Set.mem_add, not_exists, not_and_or, nmem_support] at hx
+  simp_rw [Set.mem_add, ← exists_and_left, not_exists, not_and_or, nmem_support] at hx
   rw [convolution_def]
   convert integral_zero G F using 2
   ext t
@@ -641,7 +641,7 @@ theorem continuousOn_convolution_right_with_param {g : P → G → E'} {s : Set
     rintro ⟨p, x⟩ y ⟨hp, hx⟩ hy
     apply hgs p _ hp
     contrapose! hy
-    exact ⟨y - x, x, by simpa using hy, hx, by simp⟩
+    exact ⟨y - x, by simpa using hy, x, hx, by simp⟩
   apply ContinuousWithinAt.mono_of_mem (B (q₀, x₀) ⟨hq₀, mem_of_mem_nhds ht⟩)
   exact mem_nhdsWithin_prod_iff.2 ⟨s, self_mem_nhdsWithin, t, nhdsWithin_le_nhds ht, Subset.rfl⟩
 #align continuous_on_convolution_right_with_param' continuousOn_convolution_right_with_param

Mathlib/Analysis/Normed/Group/AddTorsor.lean

@@ -326,10 +326,10 @@ theorem IsClosed.vadd_right_of_isCompact {s : Set V} {t : Set P} (hs : IsClosed
   -- This result is still true for any `AddTorsor` where `-ᵥ` is continuous,
   -- but we don't yet have a nice way to state it.
   refine IsSeqClosed.isClosed (fun u p husv hup ↦ ?_)
-  choose! a v ha hv hav using husv
+  choose! a ha v hv hav using husv
   rcases ht.isSeqCompact hv with ⟨q, hqt, φ, φ_mono, hφq⟩
-  refine ⟨p -ᵥ q, q, hs.mem_of_tendsto ((hup.comp φ_mono.tendsto_atTop).vsub hφq)
-    (eventually_of_forall fun n ↦ ?_), hqt, vsub_vadd _ _⟩
+  refine ⟨p -ᵥ q, hs.mem_of_tendsto ((hup.comp φ_mono.tendsto_atTop).vsub hφq)
+    (eventually_of_forall fun n ↦ ?_), q, hqt, vsub_vadd _ _⟩
   convert ha (φ n) using 1
   exact (eq_vadd_iff_vsub_eq _ _ _).mp (hav (φ n)).symm
 

Mathlib/Analysis/Normed/Group/Pointwise.lean

@@ -31,7 +31,7 @@ theorem Bornology.IsBounded.mul (hs : IsBounded s) (ht : IsBounded t) : IsBounde
   obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le'
   obtain ⟨Rt, hRt⟩ : ∃ R, ∀ x ∈ t, ‖x‖ ≤ R := ht.exists_norm_le'
   refine' isBounded_iff_forall_norm_le'.2 ⟨Rs + Rt, _⟩
-  rintro z ⟨x, y, hx, hy, rfl⟩
+  rintro z ⟨x, hx, y, hy, rfl⟩
   exact norm_mul_le_of_le (hRs x hx) (hRt y hy)
 #align metric.bounded.mul Bornology.IsBounded.mul
 #align metric.bounded.add Bornology.IsBounded.add

Mathlib/Analysis/NormedSpace/lpSpace.lean

@@ -509,7 +509,7 @@ instance normedAddCommGroup [hp : Fact (1 ≤ p)] : NormedAddCommGroup (lp E p)
           refine' (lp.isLUB_norm (f + g)).2 _
           rintro x ⟨i, rfl⟩
           refine' le_trans _ (add_mem_upperBounds_add
-            (lp.isLUB_norm f).1 (lp.isLUB_norm g).1 ⟨_, _, ⟨i, rfl⟩, ⟨i, rfl⟩, rfl⟩)
+            (lp.isLUB_norm f).1 (lp.isLUB_norm g).1 ⟨_, ⟨i, rfl⟩, _, ⟨i, rfl⟩, rfl⟩)
           exact norm_add_le (f i) (g i)
         · have hp'' : 0 < p.toReal := zero_lt_one.trans_le hp'
           have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => norm_nonneg _

Mathlib/Analysis/Seminorm.lean

@@ -792,14 +792,14 @@ theorem closedBall_antitone {p q : Seminorm 𝕜 E} (h : q ≤ p) :
 
 theorem ball_add_ball_subset (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) (x₁ x₂ : E) :
     p.ball (x₁ : E) r₁ + p.ball (x₂ : E) r₂ ⊆ p.ball (x₁ + x₂) (r₁ + r₂) := by
-  rintro x ⟨y₁, y₂, hy₁, hy₂, rfl⟩
+  rintro x ⟨y₁, hy₁, y₂, hy₂, rfl⟩
   rw [mem_ball, add_sub_add_comm]
   exact (map_add_le_add p _ _).trans_lt (add_lt_add hy₁ hy₂)
 #align seminorm.ball_add_ball_subset Seminorm.ball_add_ball_subset
 
 theorem closedBall_add_closedBall_subset (p : Seminorm 𝕜 E) (r₁ r₂ : ℝ) (x₁ x₂ : E) :
     p.closedBall (x₁ : E) r₁ + p.closedBall (x₂ : E) r₂ ⊆ p.closedBall (x₁ + x₂) (r₁ + r₂) := by
-  rintro x ⟨y₁, y₂, hy₁, hy₂, rfl⟩
+  rintro x ⟨y₁, hy₁, y₂, hy₂, rfl⟩
   rw [mem_closedBall, add_sub_add_comm]
   exact (map_add_le_add p _ _).trans (add_le_add hy₁ hy₂)
 #align seminorm.closed_ball_add_closed_ball_subset Seminorm.closedBall_add_closedBall_subset