case h
F : Type ?u.670328
R : Type u_1
A : Type u_2
B : Type ?u.670337
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
S T : StarSubalgebra R A
x✝ : A
⊢ x✝ ∈ (S ⊓ T).toSubalgebra ↔ x✝ ∈ S.toSubalgebra ⊓ T.toSubalgebra
F : Type ?u.670328
R : Type u_1
A : Type u_2
B : Type ?u.670337
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
S T : StarSubalgebra R A
⊢ (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra
ext
no goals
case h
F : Type ?u.670328
R : Type u_1
A : Type u_2
B : Type ?u.670337
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
S T : StarSubalgebra R A
x✝ : A
⊢ x✝ ∈ (S ⊓ T).toSubalgebra ↔ x✝ ∈ S.toSubalgebra ⊓ T.toSubalgebra
simp