no goals
R' : Type u'
R✝ : Type u
A✝ : Type v
B : Type w
C : Type w'
inst✝⁹ : CommSemiring R✝
inst✝⁸ : Semiring A✝
inst✝⁷ : Algebra R✝ A✝
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R✝ B
inst✝⁴ : Semiring C
inst✝³ : Algebra R✝ C
S✝ : Subalgebra R✝ A✝
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : toSubring S = toSubring T
x : A
⊢ x ∈ S ↔ x ∈ T
rw [← mem_toSubring, ← mem_toSubring, h]