Update Mathlib/Data/Setoid/Basic.lean

Co-authored-by: Johan Commelin <[email protected]>
leanprover-community · Oct 9, 2024 · 300c2bf · 300c2bf
1 parent 6cac389
commit 300c2bf
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/Data/Setoid/Basic.lean b/Mathlib/Data/Setoid/Basic.lean
@@ -121,6 +121,7 @@ lemma piSetoid_apply {ι : Sort*} {α : ι → Sort*} {r : ∀ i, Setoid (α i)}
 
 /-- A bijection between the product of two quotients and the quotient by the product of the
 equivalence relations. -/
+@[simps]
 def prodQuotientEquiv (r : Setoid α) (s : Setoid β) :
     Quotient r × Quotient s ≃ Quotient (r.prod s) where
   toFun := fun (x, y) ↦ Quotient.map₂' Prod.mk (fun _ _ hx _ _ hy ↦ ⟨hx, hy⟩) x y