case h
F : Type ?u.651840
R : Type u_2
A : Type u_1
B : Type ?u.651849
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
x✝ : A
⊢ x✝ ∈ ⊤.toSubalgebra ↔ x✝ ∈ ⊤
F : Type ?u.651840
R : Type u_2
A : Type u_1
B : Type ?u.651849
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
⊢ ⊤.toSubalgebra = ⊤
ext
no goals
case h
F : Type ?u.651840
R : Type u_2
A : Type u_1
B : Type ?u.651849
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
x✝ : A
⊢ x✝ ∈ ⊤.toSubalgebra ↔ x✝ ∈ ⊤
simp