have h := hom.property σ cs₁
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
⊢ ∃ a, Hom.hom hom a = Algebra.θ alg₂ σ (Vector.lift cs₂)
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
σ : Δ✝.alphabet
cs₂ : { a // Set.image hom.hom a }⋆RankedAlphabet.rank Δ✝ σ
cs₁ : Fin (RankedAlphabet.rank Δ✝ σ) → alg₁.carrier := fun x => choose (_ : Set.image hom.hom (cs₂ x).val)
h : Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (hom.hom ∘ cs₁)
⊢ ∃ a, Hom.hom hom a = Algebra.θ alg₂ σ (Vector.lift cs₂)