fix: Add simps tag to Trans instance for Equiv (#2456)

See zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simps.20.2B.20Trans/near/329103653
leanprover-community · Feb 23, 2023 · 0245850 · 0245850
1 parent 1231af3
commit 0245850
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Mathlib/Logic/Equiv/Defs.lean b/Mathlib/Logic/Equiv/Defs.lean
@@ -183,6 +183,7 @@ protected def trans (e₁ : α ≃ β) (e₂ : β ≃ γ) : α ≃ γ :=
   ⟨e₂ ∘ e₁, e₁.symm ∘ e₂.symm, e₂.left_inv.comp e₁.left_inv, e₂.right_inv.comp e₁.right_inv⟩
 #align equiv.trans Equiv.trans
 
+@[simps]
 instance : Trans Equiv Equiv Equiv where
   trans := Equiv.trans