From 184e0fe488ef70d6f334259e0ce553f86698a0ec Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 19 Apr 2021 09:07:20 +0000 Subject: [PATCH] fix(equiv/ring): fix bad typeclasses on ring_equiv.trans_apply (#7258) `ring_equiv.trans` had weaker typeclasses than the lemma which unfolds it. --- src/data/equiv/ring.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/data/equiv/ring.lean b/src/data/equiv/ring.lean index 17f26c8b6196c..63f1a46e70dcd 100644 --- a/src/data/equiv/ring.lean +++ b/src/data/equiv/ring.lean @@ -158,9 +158,8 @@ symm_bijective.injective $ ext $ λ x, rfl @[trans] protected def trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') : R ≃+* S' := { .. (e₁.to_mul_equiv.trans e₂.to_mul_equiv), .. (e₁.to_add_equiv.trans e₂.to_add_equiv) } -@[simp] lemma trans_apply {A B C : Type*} - [semiring A] [semiring B] [semiring C] (e : A ≃+* B) (f : B ≃+* C) (a : A) : - e.trans f a = f (e a) := rfl +@[simp] lemma trans_apply (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : R) : + e₁.trans e₂ a = e₂ (e₁ a) := rfl protected lemma bijective (e : R ≃+* S) : function.bijective e := e.to_equiv.bijective protected lemma injective (e : R ≃+* S) : function.injective e := e.to_equiv.injective