simp [Closed, Set.mem_image_iff]
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
⊢ Algebra.θ alg₂ σ (Vector.lift cs₂) ∈ Set.image hom.hom
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
⊢ ∃ a, Hom.hom hom a = Algebra.θ alg₂ σ (Vector.lift cs₂)