case a
F : Type ?u.86101
α : Type ?u.86104
β : Type ?u.86107
R : Type u_1
S : Type u_2
S' : Type ?u.86116
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
e : R ≃+* S
x✝ : S
⊢ ↑(NonUnitalRingHom.comp (toNonUnitalRingHom e) (toNonUnitalRingHom (RingEquiv.symm e))) x✝ =
    ↑(NonUnitalRingHom.id S) x✝
F : Type ?u.86101
α : Type ?u.86104
β : Type ?u.86107
R : Type u_1
S : Type u_2
S' : Type ?u.86116
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
e : R ≃+* S
⊢ NonUnitalRingHom.comp (toNonUnitalRingHom e) (toNonUnitalRingHom (RingEquiv.symm e)) = NonUnitalRingHom.id S
ext
no goals
case a
F : Type ?u.86101
α : Type ?u.86104
β : Type ?u.86107
R : Type u_1
S : Type u_2
S' : Type ?u.86116
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : NonUnitalNonAssocSemiring S
inst✝ : NonUnitalNonAssocSemiring S'
e : R ≃+* S
x✝ : S
⊢ ↑(NonUnitalRingHom.comp (toNonUnitalRingHom e) (toNonUnitalRingHom (RingEquiv.symm e))) x✝ =
    ↑(NonUnitalRingHom.id S) x✝
simp