refactor(*): Extend ×ˢ notation (#15717)

Delete `has_set_prod` in favor of a direct notation declaration. Overload that notation with the `list`, `finset`, `multiset` versions. Use the new notation and remove type ascriptions to the existing uses where possible (because Lean gets more information from the notation now).

archive/100-theorems-list/73_ascending_descending_sequences.lean

@@ -132,7 +132,7 @@ begin
   by_contra q,
   push_neg at q,
   -- Then the labels `(a_i, b_i)` all fit in the following set: `{ (x,y) | 1 ≤ x ≤ r, 1 ≤ y ≤ s }`
-  let ran : finset (ℕ × ℕ) := ((range r).image nat.succ).product ((range s).image nat.succ),
+  let ran : finset (ℕ × ℕ) := (range r).image nat.succ ×ˢ (range s).image nat.succ,
   -- which we prove here.
   have : image ab univ ⊆ ran,
   -- First some logical shuffling

archive/100-theorems-list/81_sum_of_prime_reciprocals_diverges.lean

@@ -171,7 +171,7 @@ lemma card_le_two_pow_mul_sqrt {x k : ℕ} : card (M x k) ≤ 2 ^ k * nat.sqrt x
 begin
   let M₁ := {e ∈ M x k | squarefree (e + 1)},
   let M₂ := M (nat.sqrt x) k,
-  let K := finset.product M₁ M₂,
+  let K := M₁ ×ˢ M₂,
   let f : ℕ × ℕ → ℕ := λ mn, (mn.2 + 1) ^ 2 * (mn.1 + 1) - 1,
 
   -- Every element of `M x k` is one less than the product `(m + 1)² * (r + 1)` with `r + 1`

src/algebra/algebra/subalgebra/basic.lean

@@ -810,12 +810,11 @@ variables (S₁ : subalgebra R B)
 
 /-- The product of two subalgebras is a subalgebra. -/
 def prod : subalgebra R (A × B) :=
-{ carrier := (S : set A) ×ˢ (S₁ : set B),
+{ carrier := S ×ˢ S₁,
   algebra_map_mem' := λ r, ⟨algebra_map_mem _ _, algebra_map_mem _ _⟩,
   .. S.to_subsemiring.prod S₁.to_subsemiring }
 
-@[simp] lemma coe_prod :
-  (prod S S₁ : set (A × B)) = (S : set A) ×ˢ (S₁ : set B):= rfl
+@[simp] lemma coe_prod : (prod S S₁ : set (A × B)) = S ×ˢ S₁ := rfl
 
 lemma prod_to_submodule :
   (S.prod S₁).to_submodule = S.to_submodule.prod S₁.to_submodule := rfl

src/algebra/big_operators/basic.lean

@@ -512,24 +512,24 @@ eq.trans (by rw one_mul; refl) fold_op_distrib
 
 @[to_additive]
 lemma prod_product {s : finset γ} {t : finset α} {f : γ×α → β} :
-  (∏ x in s.product t, f x) = ∏ x in s, ∏ y in t, f (x, y) :=
-prod_finset_product (s.product t) s (λ a, t) (λ p, mem_product)
+  (∏ x in s ×ˢ t, f x) = ∏ x in s, ∏ y in t, f (x, y) :=
+prod_finset_product (s ×ˢ t) s (λ a, t) (λ p, mem_product)
 
 /-- An uncurried version of `finset.prod_product`. -/
 @[to_additive "An uncurried version of `finset.sum_product`"]
 lemma prod_product' {s : finset γ} {t : finset α} {f : γ → α → β} :
-  (∏ x in s.product t, f x.1 x.2) = ∏ x in s, ∏ y in t, f x y :=
+  (∏ x in s ×ˢ t, f x.1 x.2) = ∏ x in s, ∏ y in t, f x y :=
 prod_product
 
 @[to_additive]
 lemma prod_product_right {s : finset γ} {t : finset α} {f : γ×α → β} :
-  (∏ x in s.product t, f x) = ∏ y in t, ∏ x in s, f (x, y) :=
-prod_finset_product_right (s.product t) t (λ a, s) (λ p, mem_product.trans and.comm)
+  (∏ x in s ×ˢ t, f x) = ∏ y in t, ∏ x in s, f (x, y) :=
+prod_finset_product_right (s ×ˢ t) t (λ a, s) (λ p, mem_product.trans and.comm)
 
 /-- An uncurried version of `finset.prod_product_right`. -/
 @[to_additive "An uncurried version of `finset.prod_product_right`"]
 lemma prod_product_right' {s : finset γ} {t : finset α} {f : γ → α → β} :
-  (∏ x in s.product t, f x.1 x.2) = ∏ y in t, ∏ x in s, f x y :=
+  (∏ x in s ×ˢ t, f x.1 x.2) = ∏ y in t, ∏ x in s, f x y :=
 prod_product_right
 
 /-- Generalization of `finset.prod_comm` to the case when the inner `finset`s depend on the outer

src/algebra/big_operators/ring.lean

@@ -52,7 +52,7 @@ add_monoid_hom.map_sum (add_monoid_hom.mul_left b) _ s
 
 lemma sum_mul_sum {ι₁ : Type*} {ι₂ : Type*} (s₁ : finset ι₁) (s₂ : finset ι₂)
   (f₁ : ι₁ → β) (f₂ : ι₂ → β) :
-  (∑ x₁ in s₁, f₁ x₁) * (∑ x₂ in s₂, f₂ x₂) = ∑ p in s₁.product s₂, f₁ p.1 * f₂ p.2 :=
+  (∑ x₁ in s₁, f₁ x₁) * (∑ x₂ in s₂, f₂ x₂) = ∑ p in s₁ ×ˢ s₂, f₁ p.1 * f₂ p.2 :=
 by { rw [sum_product, sum_mul, sum_congr rfl], intros, rw mul_sum }
 
 end semiring

src/algebra/direct_sum/internal.lean

@@ -152,8 +152,7 @@ lemma direct_sum.coe_mul_apply [add_monoid ι] [semiring R] [set_like σ R]
   [add_submonoid_class σ R] (A : ι → σ) [set_like.graded_monoid A]
   [Π (i : ι) (x : A i), decidable (x ≠ 0)] (r r' : ⨁ i, A i) (i : ι) :
   ((r * r') i : R) =
-    ∑ ij in finset.filter (λ ij : ι × ι, ij.1 + ij.2 = i) (r.support.product r'.support),
-      r ij.1 * r' ij.2 :=
+    ∑ ij in (r.support ×ˢ r'.support).filter (λ ij : ι × ι, ij.1 + ij.2 = i), r ij.1 * r' ij.2 :=
 begin
   rw [direct_sum.mul_eq_sum_support_ghas_mul, dfinsupp.finset_sum_apply,
     add_submonoid_class.coe_finset_sum],

src/algebra/direct_sum/ring.lean

@@ -269,7 +269,7 @@ open_locale big_operators
 lemma mul_eq_sum_support_ghas_mul
   [Π (i : ι) (x : A i), decidable (x ≠ 0)] (a a' : ⨁ i, A i) :
   a * a' =
-    ∑ (ij : ι × ι) in (dfinsupp.support a).product (dfinsupp.support a'),
+    ∑ ij in dfinsupp.support a ×ˢ dfinsupp.support a',
       direct_sum.of _ _ (graded_monoid.ghas_mul.mul (a ij.fst) (a' ij.snd)) :=
 begin
   change direct_sum.mul_hom _ a a' = _,

src/algebra/indicator_function.lean

@@ -457,12 +457,8 @@ lemma inter_indicator_one {s t : set α} :
 funext (λ _, by simpa only [← inter_indicator_mul, pi.mul_apply, pi.one_apply, one_mul])
 
 lemma indicator_prod_one {s : set α} {t : set β} {x : α} {y : β} :
-  (s ×ˢ t : set _).indicator (1 : _ → M) (x, y) = s.indicator 1 x * t.indicator 1 y :=
-begin
-  letI := classical.dec_pred (∈ s),
-  letI := classical.dec_pred (∈ t),
-  simp [indicator_apply, ← ite_and],
-end
+  (s ×ˢ t).indicator (1 : _ → M) (x, y) = s.indicator 1 x * t.indicator 1 y :=
+by { classical, simp [indicator_apply, ←ite_and] }
 
 variables (M) [nontrivial M]
 

src/algebra/monoid_algebra/basic.lean

@@ -325,8 +325,8 @@ lemma mul_apply_antidiagonal [has_mul G] (f g : monoid_algebra k G) (x : G) (s :
 let F : G × G → k := λ p, by classical; exact if p.1 * p.2 = x then f p.1 * g p.2 else 0 in
 calc (f * g) x = (∑ a₁ in f.support, ∑ a₂ in g.support, F (a₁, a₂)) :
   mul_apply f g x
-... = ∑ p in f.support.product g.support, F p : finset.sum_product.symm
-... = ∑ p in (f.support.product g.support).filter (λ p : G × G, p.1 * p.2 = x), f p.1 * g p.2 :
+... = ∑ p in f.support ×ˢ g.support, F p : finset.sum_product.symm
+... = ∑ p in (f.support ×ˢ g.support).filter (λ p : G × G, p.1 * p.2 = x), f p.1 * g p.2 :
   (finset.sum_filter _ _).symm
 ... = ∑ p in s.filter (λ p : G × G, p.1 ∈ f.support ∧ p.2 ∈ g.support), f p.1 * g p.2 :
   sum_congr (by { ext, simp only [mem_filter, mem_product, hs, and_comm] }) (λ _ _, rfl)

src/algebraic_geometry/structure_sheaf.lean

@@ -688,7 +688,7 @@ begin
   have n_spec := λ (p : ι × ι), (exists_power p.fst p.snd).some_spec,
   -- We need one power `(h i * h j) ^ N` that works for *all* pairs `(i,j)`
   -- Since there are only finitely many indices involved, we can pick the supremum.
-  let N := (t.product t).sup n,
+  let N := (t ×ˢ t).sup n,
   have basic_opens_eq : ∀ i : ι, basic_open ((h i) ^ (N+1)) = basic_open (h i) :=
     λ i, basic_open_pow _ _ (by linarith),
   -- Expanding the fraction `a i / h i` by the power `(h i) ^ N` gives the desired normalization

src/analysis/calculus/cont_diff.lean

@@ -1160,10 +1160,10 @@ hf.fderiv_within' (by { rw [insert_eq_of_mem hxs], exact eventually_of_mem self_
 continuous. -/
 lemma cont_diff_on.continuous_on_fderiv_within_apply
   (h : cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hn : 1 ≤ n) :
-  continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1 : E → F) p.2) (s ×ˢ (univ : set E)) :=
+  continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1 : E → F) p.2) (s ×ˢ univ) :=
 begin
   have A : continuous (λq : (E →L[𝕜] F) × E, q.1 q.2) := is_bounded_bilinear_map_apply.continuous,
-  have B : continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1, p.2)) (s ×ˢ (univ : set E)),
+  have B : continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1, p.2)) (s ×ˢ univ),
   { apply continuous_on.prod _ continuous_snd.continuous_on,
     exact continuous_on.comp (h.continuous_on_fderiv_within hs hn) continuous_fst.continuous_on
       (prod_subset_preimage_fst _ _) },
@@ -2263,8 +2263,7 @@ lemma cont_diff_prod_assoc_symm : cont_diff 𝕜 ⊤ $ (equiv.prod_assoc E F G).
 /-- The bundled derivative of a `C^{n+1}` function is `C^n`. -/
 lemma cont_diff_on_fderiv_within_apply {m n : with_top  ℕ} {s : set E}
   {f : E → F} (hf : cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hmn : m + 1 ≤ n) :
-  cont_diff_on 𝕜 m (λp : E × E, (fderiv_within 𝕜 f s p.1 : E →L[𝕜] F) p.2)
-  (s ×ˢ (univ : set E)) :=
+  cont_diff_on 𝕜 m (λp : E × E, (fderiv_within 𝕜 f s p.1 : E →L[𝕜] F) p.2) (s ×ˢ univ) :=
 begin
   have A : cont_diff 𝕜 m (λp : (E →L[𝕜] F) × E, p.1 p.2),
   { apply is_bounded_bilinear_map.cont_diff,

src/analysis/convex/combination.lean

@@ -352,15 +352,15 @@ begin
   rw convex_hull_eq at ⊢ hx hy,
   obtain ⟨ι, a, w, S, hw, hw', hS, hSp⟩ := hx,
   obtain ⟨κ, b, v, T, hv, hv', hT, hTp⟩ := hy,
-  have h_sum : ∑ (i : ι × κ) in a.product b, w i.fst * v i.snd = 1,
+  have h_sum : ∑ (i : ι × κ) in a ×ˢ b, w i.fst * v i.snd = 1,
   { rw [finset.sum_product, ← hw'],
     congr,
     ext i,
     have : ∑ (y : κ) in b, w i * v y = ∑ (y : κ) in b, v y * w i,
     { congr, ext, simp [mul_comm] },
     rw [this, ← finset.sum_mul, hv'],
     simp },
-  refine ⟨ι × κ, a.product b, λ p, (w p.1) * (v p.2), λ p, (S p.1, T p.2),
+  refine ⟨ι × κ, a ×ˢ b, λ p, (w p.1) * (v p.2), λ p, (S p.1, T p.2),
     λ p hp, _, h_sum, λ p hp, _, _⟩,
   { rw mem_product at hp,
     exact mul_nonneg (hw p.1 hp.1) (hv p.2 hp.2) },

src/analysis/normed/field/basic.lean

@@ -784,7 +784,7 @@ suffices this : ∀ u : finset (ι × ι'), ∑ x in u, f x.1 * g x.2 ≤ s*t,
   from summable_of_sum_le (λ x, mul_nonneg (hf' _) (hg' _)) this,
 assume u,
 calc  ∑ x in u, f x.1 * g x.2
-    ≤ ∑ x in (u.image prod.fst).product (u.image prod.snd), f x.1 * g x.2 :
+    ≤ ∑ x in u.image prod.fst ×ˢ u.image prod.snd, f x.1 * g x.2 :
       sum_mono_set_of_nonneg (λ x, mul_nonneg (hf' _) (hg' _)) subset_product
 ... = ∑ x in u.image prod.fst, ∑ y in u.image prod.snd, f x * g y : sum_product
 ... = ∑ x in u.image prod.fst, f x * ∑ y in u.image prod.snd, g y :

src/combinatorics/additive/salem_spencer.lean

@@ -345,7 +345,7 @@ calc
 
 @[to_additive]
 lemma le_mul_roth_number_product (s : finset α) (t : finset β) :
-  mul_roth_number s * mul_roth_number t ≤ mul_roth_number (s.product t) :=
+  mul_roth_number s * mul_roth_number t ≤ mul_roth_number (s ×ˢ t) :=
 begin
   obtain ⟨u, hus, hucard, hu⟩ := mul_roth_number_spec s,
   obtain ⟨v, hvt, hvcard, hv⟩ := mul_roth_number_spec t,

src/combinatorics/simple_graph/density.lean

@@ -33,8 +33,7 @@ variables (r : α → β → Prop) [Π a, decidable_pred (r a)] {s s₁ s₂ : f
   {a : α} {b : β} {δ : ℚ}
 
 /-- Finset of edges of a relation between two finsets of vertices. -/
-def interedges (s : finset α) (t : finset β) : finset (α × β) :=
-(s.product t).filter $ λ e, r e.1 e.2
+def interedges (s : finset α) (t : finset β) : finset (α × β) := (s ×ˢ t).filter $ λ e, r e.1 e.2
 
 /-- Edge density of a relation between two finsets of vertices. -/
 def edge_density (s : finset α) (t : finset β) : ℚ := (interedges r s t).card / (s.card * t.card)
@@ -93,7 +92,7 @@ ext $ λ a, by simp only [mem_interedges_iff, mem_bUnion, ←exists_and_distrib_
 
 lemma interedges_bUnion (s : finset ι) (t : finset κ) (f : ι → finset α) (g : κ → finset β) :
   interedges r (s.bUnion f) (t.bUnion g) =
-    (s.product t).bUnion (λ ab, interedges r (f ab.1) (g ab.2)) :=
+    (s ×ˢ t).bUnion (λ ab, interedges r (f ab.1) (g ab.2)) :=
 by simp_rw [product_bUnion, interedges_bUnion_left, interedges_bUnion_right]
 
 end decidable_eq
@@ -143,7 +142,7 @@ end
 
 lemma card_interedges_finpartition [decidable_eq α] [decidable_eq β] (P : finpartition s)
   (Q : finpartition t) :
-  (interedges r s t).card = ∑ ab in P.parts.product Q.parts, (interedges r ab.1 ab.2).card :=
+  (interedges r s t).card = ∑ ab in P.parts ×ˢ Q.parts, (interedges r ab.1 ab.2).card :=
 by simp_rw [card_interedges_finpartition_left _ P, card_interedges_finpartition_right _ _ Q,
   sum_product]
 
@@ -262,7 +261,7 @@ def interedges (s t : finset α) : finset (α × α) := interedges G.adj s t
 def edge_density : finset α → finset α → ℚ := edge_density G.adj
 
 lemma interedges_def (s t : finset α) :
-  G.interedges s t = (s.product t).filter (λ e, G.adj e.1 e.2) := rfl
+  G.interedges s t = (s ×ˢ t).filter (λ e, G.adj e.1 e.2) := rfl
 
 lemma edge_density_def (s t : finset α) :
   G.edge_density s t = (G.interedges s t).card / (s.card * t.card) := rfl
@@ -302,14 +301,14 @@ interedges_bUnion_right _ _ _ _
 
 lemma interedges_bUnion (s : finset ι) (t : finset κ) (f : ι → finset α) (g : κ → finset α) :
   G.interedges (s.bUnion f) (t.bUnion g) =
-    (s.product t).bUnion (λ ab, G.interedges (f ab.1) (g ab.2)) :=
+    (s ×ˢ t).bUnion (λ ab, G.interedges (f ab.1) (g ab.2)) :=
 interedges_bUnion _ _ _ _ _
 
 lemma card_interedges_add_card_interedges_compl (h : disjoint s t) :
   (G.interedges s t).card + (Gᶜ.interedges s t).card = s.card * t.card :=
 begin
   rw [←card_product, interedges_def, interedges_def],
-  have : (s.product t).filter (λ e , Gᶜ.adj e.1 e.2) = (s.product t).filter (λ e , ¬ G.adj e.1 e.2),
+  have : (s ×ˢ t).filter (λ e , Gᶜ.adj e.1 e.2) = (s ×ˢ t).filter (λ e , ¬ G.adj e.1 e.2),
   { refine filter_congr (λ x hx, _),
     rw mem_product at hx,
     rw [compl_adj, and_iff_right (h.forall_ne_finset hx.1 hx.2)] },

src/computability/turing_machine.lean

@@ -1284,8 +1284,7 @@ end
 variables [fintype σ]
 /-- Given a finite set of accessible `Λ` machine states, there is a finite set of accessible
 machine states in the target (even though the type `Λ'` is infinite). -/
-noncomputable def tr_stmts (S : finset Λ) : finset Λ' :=
-(TM1.stmts M S).product finset.univ
+noncomputable def tr_stmts (S : finset Λ) : finset Λ' := TM1.stmts M S ×ˢ finset.univ
 
 open_locale classical
 local attribute [simp] TM1.stmts₁_self

src/data/fin_enum.lean

@@ -86,7 +86,7 @@ instance punit : fin_enum punit :=
 of_list [punit.star] (λ x, by cases x; simp)
 
 instance prod {β} [fin_enum α] [fin_enum β] : fin_enum (α × β) :=
-of_list ( (to_list α).product (to_list β) ) (λ x, by cases x; simp)
+of_list (to_list α ×ˢ to_list β) (λ x, by cases x; simp)
 
 instance sum {β} [fin_enum α] [fin_enum β] : fin_enum (α ⊕ β) :=
 of_list ( (to_list α).map sum.inl ++ (to_list β).map sum.inr ) (λ x, by cases x; simp)

src/data/finset/functor.lean

@@ -110,7 +110,7 @@ instance : is_comm_applicative finset :=
 { commutative_prod := λ α β s t, begin
     simp_rw [seq_def, fmap_def, sup_image, sup_eq_bUnion],
     change s.bUnion (λ a, t.image $ λ b, (a, b)) = t.bUnion (λ b, s.image $ λ a, (a, b)),
-    transitivity s.product t;
+    transitivity s ×ˢ t;
       [rw product_eq_bUnion, rw product_eq_bUnion_right]; congr; ext; simp_rw mem_image,
   end,
   .. finset.is_lawful_applicative }

src/data/finset/lattice.lean

@@ -116,7 +116,7 @@ end
 
 /-- See also `finset.product_bUnion`. -/
 lemma sup_product_left (s : finset β) (t : finset γ) (f : β × γ → α) :
-  (s.product t).sup f = s.sup (λ i, t.sup $ λ i', f ⟨i, i'⟩) :=
+  (s ×ˢ t).sup f = s.sup (λ i, t.sup $ λ i', f ⟨i, i'⟩) :=
 begin
   refine le_antisymm _ (sup_le (λ i hi, sup_le $ λ i' hi', le_sup $ mem_product.2 ⟨hi, hi'⟩)),
   refine sup_le _,
@@ -127,7 +127,7 @@ begin
 end
 
 lemma sup_product_right (s : finset β) (t : finset γ) (f : β × γ → α) :
-  (s.product t).sup f = t.sup (λ i', s.sup $ λ i, f ⟨i, i'⟩) :=
+  (s ×ˢ t).sup f = t.sup (λ i', s.sup $ λ i, f ⟨i, i'⟩) :=
 by rw [sup_product_left, sup_comm]
 
 @[simp] lemma sup_erase_bot [decidable_eq α] (s : finset α) : (s.erase ⊥).sup id = s.sup id :=
@@ -322,11 +322,11 @@ lemma inf_comm (s : finset β) (t : finset γ) (f : β → γ → α) :
 @sup_comm αᵒᵈ _ _ _ _ _ _ _
 
 lemma inf_product_left (s : finset β) (t : finset γ) (f : β × γ → α) :
-  (s.product t).inf f = s.inf (λ i, t.inf $ λ i', f ⟨i, i'⟩) :=
+  (s ×ˢ t).inf f = s.inf (λ i, t.inf $ λ i', f ⟨i, i'⟩) :=
 @sup_product_left αᵒᵈ _ _ _ _ _ _ _
 
 lemma inf_product_right (s : finset β) (t : finset γ) (f : β × γ → α) :
-  (s.product t).inf f = t.inf (λ i', s.inf $ λ i, f ⟨i, i'⟩) :=
+  (s ×ˢ t).inf f = t.inf (λ i', s.inf $ λ i, f ⟨i, i'⟩) :=
 @sup_product_right αᵒᵈ _ _ _ _ _ _ _
 
 @[simp] lemma inf_erase_top [decidable_eq α] (s : finset α) : (s.erase ⊤).inf id = s.inf id :=

src/data/finset/n_ary.lean

@@ -33,7 +33,7 @@ variables {α α' β β' γ γ' δ δ' ε ε' : Type*}
 /-- The image of a binary function `f : α → β → γ` as a function `finset α → finset β → finset γ`.
 Mathematically this should be thought of as the image of the corresponding function `α × β → γ`. -/
 def image₂ (f : α → β → γ) (s : finset α) (t : finset β) : finset γ :=
-(s.product t).image $ uncurry f
+(s ×ˢ t).image $ uncurry f
 
 @[simp] lemma mem_image₂ : c ∈ image₂ f s t ↔ ∃ a b, a ∈ s ∧ b ∈ t ∧ f a b = c :=
 by simp [image₂, and_assoc]
@@ -47,8 +47,7 @@ lemma card_image₂_le (f : α → β → γ) (s : finset α) (t : finset β) :
 card_image_le.trans_eq $ card_product _ _
 
 lemma card_image₂_iff :
-  (image₂ f s t).card = s.card * t.card ↔
-    ((s : set α) ×ˢ (t : set β) : set (α × β)).inj_on (λ x, f x.1 x.2) :=
+  (image₂ f s t).card = s.card * t.card ↔ (s ×ˢ t : set (α × β)).inj_on (λ x, f x.1 x.2) :=
 by { rw [←card_product, ←coe_product], exact card_image_iff }
 
 lemma card_image₂ (hf : injective2 f) (s : finset α) (t : finset β) :