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