case h.e'_2.h.e'_4
R : Type u_1
A : Type u_2
B : Type ?u.20732
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
⊢ ↑S₁ = id '' {x | x ∈ S₁}

case convert_4
R : Type u_1
A : Type u_2
B : Type ?u.20732
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
⊢ ∀ (x : A), x ∈ S₁ → id x ∈ S₂
R : Type u_1
A : Type u_2
B : Type ?u.20732
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
⊢ Subtype.val ⁻¹' ↑S₁ = range ↑(inclusion h)
convert(Set.range_subtype_map id _).symm
case h.e'_2.h.e'_4
R : Type u_1
A : Type u_2
B : Type ?u.20732
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
⊢ ↑S₁ = {x | x ∈ S₁}
case h.e'_2.h.e'_4
R : Type u_1
A : Type u_2
B : Type ?u.20732
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
⊢ ↑S₁ = id '' {x | x ∈ S₁}
rw [Set.image_id]
no goals
case h.e'_2.h.e'_4
R : Type u_1
A : Type u_2
B : Type ?u.20732
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
⊢ ↑S₁ = {x | x ∈ S₁}
rfl
case convert_4
R : Type u_1
A : Type u_2
B : Type ?u.20732
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
x✝ : A
h' : x✝ ∈ S₁
⊢ id x✝ ∈ S₂
case convert_4
R : Type u_1
A : Type u_2
B : Type ?u.20732
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
⊢ ∀ (x : A), x ∈ S₁ → id x ∈ S₂
intro _ h'
no goals
case convert_4
R : Type u_1
A : Type u_2
B : Type ?u.20732
inst✝⁶ : CommSemiring R
inst✝⁵ : StarRing R
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S₁ S₂ : StarSubalgebra R A
h : S₁ ≤ S₂
hS₁ : IsClosed ↑S₁
src✝ : Embedding ↑(inclusion h) := embedding_inclusion h
x✝ : A
h' : x✝ ∈ S₁
⊢ id x✝ ∈ S₂
apply h h'