Theorem: lemma_2_6_2 (WTA.lean)

State before:
Δ✝ : RankedAlphabet
alg₁ alg₂ : Algebra Δ✝
hom : Hom alg₁ alg₂
⊢ Closed alg₂ (Set.image hom.hom)
Tactic:
intro σ cs₂
State after:
Δ✝ : 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

State before:
Δ✝ : 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
Tactic:
simp [Closed, Set.mem_image_iff]
State after:
Δ✝ : 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₂)

State before:
Δ✝ : 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₂)
Tactic:
have h := hom.property σ cs₁
State after:
Δ✝ : 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₂)

State before:
Δ✝ : 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₂)
Tactic:
exists alg₁.θ σ cs₁
State after:
Δ✝ : 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₁)
⊢ Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (Vector.lift cs₂)

State before:
Δ✝ : 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₁)
⊢ Hom.hom hom (Algebra.θ alg₁ σ cs₁) = Algebra.θ alg₂ σ (Vector.lift cs₂)
Tactic:
rw [h]
State after:
Δ✝ : 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₁)
⊢ Algebra.θ alg₂ σ (hom.hom ∘ cs₁) = Algebra.θ alg₂ σ (Vector.lift cs₂)

State before:
Δ✝ : 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₁)
⊢ Algebra.θ alg₂ σ (hom.hom ∘ cs₁) = Algebra.θ alg₂ σ (Vector.lift cs₂)
Tactic:
congr
State after:
case e_a
Δ✝ : 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₁)
⊢ hom.hom ∘ cs₁ = Vector.lift cs₂

State before:
case e_a
Δ✝ : 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₁)
⊢ hom.hom ∘ cs₁ = Vector.lift cs₂
Tactic:
funext i
State after:
case e_a.h
Δ✝ : 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₁)
i : Fin (RankedAlphabet.rank Δ✝ σ)
⊢ Function.comp hom.hom cs₁ i = Vector.lift cs₂ i

State before:
case e_a.h
Δ✝ : 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₁)
i : Fin (RankedAlphabet.rank Δ✝ σ)
⊢ Function.comp hom.hom cs₁ i = Vector.lift cs₂ i
Tactic:
apply Set.image_choose
State after:
no goals